The analytic one-block estimate in R-322

This file connects the three explicit profile estimates (4.10)--(4.12) to the Green difference which occurs in one proper-block collapse. The Taylor region uses class-E cancellation. On its complement the free Green function is split into the two crude regions of the paper.

noncomputable def Anderson4D.r322GreenDifferenceSection (J : T4 → ℝ) (q : T4) : ℝ

The Green difference after the inner change of variables u = z - w.

Equations

• Anderson4D.r322GreenDifferenceSection J q = ∫ (u : Anderson4D.T4), J u * (Anderson4D.greenFn (q - u) - Anderson4D.greenFn q) ∂Anderson4D.paperMeasure

noncomputable def Anderson4D.r322CrudeSectionIntegrand (J : T4 → ℝ) (q u : T4) : ℝ

The complement of the Taylor region in the inner Green difference.

Equations

• Anderson4D.r322CrudeSectionIntegrand J q u = if 2 * ‖u‖ ≤ ‖q‖ then 0 else J u * (Anderson4D.greenFn (q - u) - Anderson4D.greenFn q)

noncomputable def Anderson4D.r322CrudeSectionMajorant (greenConstant : ℝ) (P : T4 → ℝ) (q u : T4) : ℝ

The positive majorant supplied by the two crude regions (4.11)--(4.12).

Equations

• One or more equations did not get rendered due to their size.

theorem Anderson4D.measurable_r322CrudeSectionIntegrand {J : T4 → ℝ} (hJ : Measurable J) (q : T4) : Measurable (r322CrudeSectionIntegrand J q)

theorem Anderson4D.measurable_r322CrudeSectionMajorant {P : T4 → ℝ} (hP : Measurable P) (greenConstant : ℝ) (q : T4) : Measurable (r322CrudeSectionMajorant greenConstant P q)

theorem Anderson4D.measurable_reductionRegionOneKernel (q : T4) {J : T4 → ℝ} (hJ : Measurable J) : Measurable (reductionRegionOneKernel q J)

theorem Anderson4D.measurable_r322GreenRemainder (q : T4) : Measurable (r322GreenRemainder q)

theorem Anderson4D.torusLinearTerm_eq_sum_r322OneBlock (D : R4 →L[ℝ] ℝ) (u : T4) : torusLinearTerm D u = ∑ i : Fin dim, torusLift u i * D (Pi.single i 1)

theorem Anderson4D.reductionRegionTwo_of_not_regionOne {q u : T4} (hregion : ¬2 * ‖u‖ ≤ ‖q‖) : ‖q‖ ≤ 2 * ‖u‖

Outside the Taylor region, q lies in the first crude region.

theorem Anderson4D.torusDistSq_le_thirtySix_mul_of_crude_regions {q u : T4} (hregionThree : ¬2 * ‖q - u‖ ≤ ‖u‖) : torusDistSq q ≤ 36 * torusDistSq (q - u)

In the overlap complement of the last crude region, the singular point q-u controls q with the numerical constant used in (4.11).

theorem Anderson4D.invSqKer_sub_le_thirtySix_mul {q u : T4} (hq : q ≠ 0) (huq : u ≠ q) (hregionThree : ¬2 * ‖q - u‖ ≤ ‖u‖) : invSqKer (q - u) ≤ 36 * invSqKer q

theorem Anderson4D.abs_r322CrudeSectionIntegrand_le {J P : T4 → ℝ} {greenConstant : ℝ} {q u : T4} (hgreenConstant : 0 ≤ greenConstant) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ greenConstant / torusDistSq z) (hq : q ≠ 0) (huq : u ≠ q) (hP : 0 ≤ P u) (hJ : |J u| ≤ P u) : |r322CrudeSectionIntegrand J q u| ≤ r322CrudeSectionMajorant greenConstant P q u

Pointwise domination of the non-Taylor part of a Green difference. The only excluded point is the null set u = q, where the off-diagonal Green estimate is not stated.

theorem Anderson4D.integrable_reductionRegionThreeKernel_primitiveKernelMajorant (C lam ε supportConstant : ℝ) (n : ℕ) (q : T4) (hε : 0 < ε) : MeasureTheory.Integrable (reductionRegionThreeKernel q (primitiveKernelMajorant C lam ε supportConstant n)) paperMeasure

The region-(4.12) restriction of the full Proposition 4.1 majorant is integrable. This is the integrability fact implicit in the exact density identity.

theorem Anderson4D.integrable_r322CrudeSectionMajorant (greenConstant C lam ε supportConstant : ℝ) (n : ℕ) (q : T4) (hε : 0 < ε) : MeasureTheory.Integrable (r322CrudeSectionMajorant greenConstant (primitiveKernelMajorant C lam ε supportConstant n) q) paperMeasure

theorem Anderson4D.r322CrudeSectionMajorant_nonneg {greenConstant C lam : ℝ} (hgreenConstant : 0 ≤ greenConstant) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (ε supportConstant : ℝ) (n : ℕ) (q u : T4) : 0 ≤ r322CrudeSectionMajorant greenConstant (primitiveKernelMajorant C lam ε supportConstant n) q u

theorem Anderson4D.integrable_r322CrudeSectionIntegrand {J : T4 → ℝ} {greenConstant C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmeas : Measurable J) (hgreenConstant : 0 ≤ greenConstant) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ greenConstant / torusDistSq z) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : MeasureTheory.Integrable (r322CrudeSectionIntegrand J q) paperMeasure

theorem Anderson4D.abs_integral_r322CrudeSectionIntegrand_le {J : T4 → ℝ} {greenConstant C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmeas : Measurable J) (hgreenConstant : 0 ≤ greenConstant) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ greenConstant / torusDistSq z) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : |∫ (u : T4), r322CrudeSectionIntegrand J q u ∂paperMeasure| ≤ 37 * greenConstant * r322RegionTwoDensity C lam ε supportConstant n q + greenConstant * r322RegionThreeDensity C lam ε supportConstant n q

The crude section is absolutely integrable and its integral is bounded by the exact sum of the densities from (4.11) and (4.12).

theorem Anderson4D.integrable_r322RegionOne_coordinateMoment {J : T4 → ℝ} {C lam ε supportConstant : ℝ} {n : ℕ} (q : T4) (i : Fin dim) (hJmeas : Measurable J) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hε : 0 < ε) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * torusLift u i) paperMeasure

theorem Anderson4D.integrable_r322TaylorMajorant_of_bound {J : T4 → ℝ} {C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmeas : Measurable J) (hsupport : 0 < supportConstant) (hε : 0 < ε) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : MeasureTheory.Integrable (fun (u : T4) => |reductionRegionOneKernel q J u| * (6144 * greenLocalHessSingularBound * invSqKer q ^ 2 * torusDistSq u)) paperMeasure

theorem Anderson4D.integrable_r322GreenRemainder_of_bound {J : T4 → ℝ} {C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmeas : Measurable J) (hsupport : 0 < supportConstant) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * r322GreenRemainder q u) paperMeasure

theorem Anderson4D.integrable_r322TaylorDifference_of_bound {J : T4 → ℝ} {C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmeas : Measurable J) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hsupport : 0 < supportConstant) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * (greenFn q - greenFn (q - u))) paperMeasure

theorem Anderson4D.r322GreenDifferenceSection_eq_taylor_add_crude (J : T4 → ℝ) (q : T4) (hintTaylor : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * (greenFn q - greenFn (q - u))) paperMeasure) (hintCrude : MeasureTheory.Integrable (r322CrudeSectionIntegrand J q) paperMeasure) : r322GreenDifferenceSection J q = -∫ (u : T4), reductionRegionOneKernel q J u * (greenFn q - greenFn (q - u)) ∂paperMeasure + ∫ (u : T4), r322CrudeSectionIntegrand J q u ∂paperMeasure

Algebraic splitting of the full Green difference into the Taylor region and its crude complement.

theorem Anderson4D.abs_r322GreenDifferenceSection_le {J : T4 → ℝ} {greenConstant C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmem : MemEClassT4 J) (hJmeas : Measurable J) (hgreenConstant : 0 ≤ greenConstant) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ greenConstant / torusDistSq z) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hsupport : 0 < supportConstant) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) (hmoment : ∀ (i : Fin dim), MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * torusLift u i) paperMeasure) (hintR : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * r322GreenRemainder q u) paperMeasure) (hintMajorant : MeasureTheory.Integrable (fun (u : T4) => |reductionRegionOneKernel q J u| * (6144 * greenLocalHessSingularBound * invSqKer q ^ 2 * torusDistSq u)) paperMeasure) (hintTaylor : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q J u * (greenFn q - greenFn (q - u))) paperMeasure) : |r322GreenDifferenceSection J q| ≤ 6144 * greenLocalHessSingularBound * r322TaylorDensity C lam ε supportConstant n q + 37 * greenConstant * r322RegionTwoDensity C lam ε supportConstant n q + greenConstant * r322RegionThreeDensity C lam ε supportConstant n q

The three-region inner estimate. This is the analytic content of (4.10)--(4.12) before the outer convolution.

theorem Anderson4D.abs_r322GreenDifferenceSection_le_of_majorant {J : T4 → ℝ} {greenConstant C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hJmem : MemEClassT4 J) (hJmeas : Measurable J) (hgreenConstant : 0 ≤ greenConstant) (hgreen : ∀ (z : T4), torusDistSq z ≠ 0 → greenFn z ≤ greenConstant / torusDistSq z) (hC : 0 ≤ C) (hlam : 0 ≤ lam) (hsupport : 0 < supportConstant) (hε : 0 < ε) (hq : q ≠ 0) (hJ : ∀ (u : T4), |J u| ≤ primitiveKernelMajorant C lam ε supportConstant n u) : |r322GreenDifferenceSection J q| ≤ 6144 * greenLocalHessSingularBound * r322TaylorDensity C lam ε supportConstant n q + 37 * greenConstant * r322RegionTwoDensity C lam ε supportConstant n q + greenConstant * r322RegionThreeDensity C lam ε supportConstant n q

Constructive one-block inner estimate with no technical integrability assumptions left to the caller.