The crude Green profile in region (4.12)

In the last region put q = z-y, u = z-w, so q-u = w-y. The condition 2‖q-u‖ ≤ ‖u‖ makes u comparable with q. Consequently the inner inverse-square mass supplies a factor O(torusDistSq q). Applied to the two Proposition 4.1 summands this gives a flat ε⁻⁴ / |log ε| profile at primitive scale and the same critical invSqKer² / |log ε| profile as in region (4.11).

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

Restriction and inner Green factor for the last crude region.

Equations

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

theorem Anderson4D.measurableSet_reductionRegionThree (q : T4) : MeasurableSet {u : T4 | 2 * ‖q - u‖ ≤ ‖u‖}

theorem Anderson4D.reductionRegionThreeKernel_eq_indicator (q : T4) (J : T4 → ℝ) : reductionRegionThreeKernel q J = {u : T4 | 2 * ‖q - u‖ ≤ ‖u‖}.indicator fun (u : T4) => invSqKer (q - u) * J u

theorem Anderson4D.measurable_reductionRegionThreeKernel_joint {J : T4 → ℝ} (hJ : Measurable J) : Measurable fun (p : T4 × T4) => reductionRegionThreeKernel p.1 J p.2

theorem Anderson4D.measurable_reductionRegionThreeKernel (q : T4) {J : T4 → ℝ} (hJ : Measurable J) : Measurable (reductionRegionThreeKernel q J)

noncomputable def Anderson4D.r322RegionThreeLocalMoment (supportConstant ε : ℝ) (q : T4) : ℝ

The local-support part of the (4.12) inner integral.

Equations

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

noncomputable def Anderson4D.r322RegionThreeRegularMoment (ε : ℝ) (q : T4) : ℝ

The regularized part of the (4.12) inner integral.

Equations

• Anderson4D.r322RegionThreeRegularMoment ε q = ∫ (u : Anderson4D.T4), Anderson4D.reductionRegionThreeKernel q (Anderson4D.regularizedInvCube ε) u ∂Anderson4D.paperMeasure

theorem Anderson4D.measurable_r322RegionThreeLocalMoment (supportConstant ε : ℝ) : Measurable (r322RegionThreeLocalMoment supportConstant ε)

theorem Anderson4D.measurable_r322RegionThreeRegularMoment (ε : ℝ) : Measurable (r322RegionThreeRegularMoment ε)

theorem Anderson4D.r322RegionThreeKernel_nonneg {q : T4} {J : T4 → ℝ} (hJ : ∀ (u : T4), 0 ≤ J u) (u : T4) : 0 ≤ reductionRegionThreeKernel q J u

theorem Anderson4D.r322RegionThreeLocalMoment_nonneg (supportConstant ε : ℝ) (q : T4) : 0 ≤ r322RegionThreeLocalMoment supportConstant ε q

theorem Anderson4D.r322RegionThreeRegularMoment_nonneg (ε : ℝ) (q : T4) : 0 ≤ r322RegionThreeRegularMoment ε q

@[simp]

theorem Anderson4D.reductionRegionThreeKernel_zero (J : T4 → ℝ) : reductionRegionThreeKernel 0 J = 0

@[simp]

theorem Anderson4D.r322RegionThreeLocalMoment_zero (supportConstant ε : ℝ) : r322RegionThreeLocalMoment supportConstant ε 0 = 0

@[simp]

theorem Anderson4D.r322RegionThreeRegularMoment_zero (ε : ℝ) : r322RegionThreeRegularMoment ε 0 = 0

theorem Anderson4D.r322RegionThree_geometry {q u : T4} (hq : q ≠ 0) (hregion : 2 * ‖q - u‖ ≤ ‖u‖) : u ∈ Metric.ball q (2 * ‖q‖) ∧ torusDistSq q ≤ 9 * torusDistSq u

In region (4.12), the inner Green singularity lies in a ball about q, and the primitive displacement is comparable to q.

theorem Anderson4D.invSqKer_le_nine_mul_regionThree {q u : T4} (hq : q ≠ 0) (hregion : 2 * ‖q - u‖ ≤ ‖u‖) : invSqKer u ≤ 9 * invSqKer q

theorem Anderson4D.regularizedInvCube_le_regionThree {ε : ℝ} (hε : 0 < ε) {q u : T4} (hq : q ≠ 0) (hregion : 2 * ‖q - u‖ ≤ ‖u‖) : regularizedInvCube ε u ≤ 729 * (torusDistSq q + ε ^ 2)⁻¹ ^ 3

theorem Anderson4D.integrable_reductionRegionThreeLocal {supportConstant ε : ℝ} {q : T4} (hq : q ≠ 0) : MeasureTheory.Integrable (reductionRegionThreeKernel q fun (u : T4) => invSqKer u * primitiveSupportIndicator supportConstant ε u) paperMeasure

theorem Anderson4D.integrable_reductionRegionThreeRegular {ε : ℝ} (hε : 0 < ε) (q : T4) : MeasureTheory.Integrable (reductionRegionThreeKernel q (regularizedInvCube ε)) paperMeasure

theorem Anderson4D.r322RegionThree_torusDistSq_le {q u : T4} (hregion : 2 * ‖q - u‖ ≤ ‖u‖) : torusDistSq q ≤ 9 * torusDistSq u

Comparability part of the last-region geometry, without the off-diagonal hypothesis needed only for the open-ball statement.

theorem Anderson4D.r322RegionThreeLocalMoment_eq_zero_of_not_scale {supportConstant ε : ℝ} (hsupport : 0 < supportConstant) (hε : 0 < ε) {q : T4} (hq : q ∉ r322ScaleBall (3 * supportConstant + 1) ε) : r322RegionThreeLocalMoment supportConstant ε q = 0

theorem Anderson4D.exists_r322RegionThreeLocalMoment_le : ∃ (K : ℝ), 0 < K ∧ ∀ (supportConstant ε : ℝ) (q : T4), r322RegionThreeLocalMoment supportConstant ε q ≤ K

The local-support inner Green integral in (4.12) is uniformly bounded; its outer support is handled separately above.

theorem Anderson4D.exists_r322RegionThreeRegularMoment_le : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (q : T4), 0 < ε → r322RegionThreeRegularMoment ε q ≤ K * torusDistSq q * (torusDistSq q + ε ^ 2)⁻¹ ^ 3

The regularized inner Green integral is controlled by the radial quadratic profile at the external variable.

noncomputable def Anderson4D.r322RegionThreeDensity (C lam ε supportConstant : ℝ) (n : ℕ) (q : T4) : ℝ

Full outer density of the last crude region.

Equations

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

theorem Anderson4D.measurable_r322RegionThreeDensity (C lam ε supportConstant : ℝ) (n : ℕ) : Measurable (r322RegionThreeDensity C lam ε supportConstant n)

theorem Anderson4D.r322RegionThreeDensity_nonneg {C lam : ℝ} (hC : 0 ≤ C) (hlam : 0 ≤ lam) (ε supportConstant : ℝ) (n : ℕ) (q : T4) : 0 ≤ r322RegionThreeDensity C lam ε supportConstant n q

theorem Anderson4D.r322RegionThreeDensity_eq_integral (C lam ε supportConstant : ℝ) (n : ℕ) (q : T4) (hε : 0 < ε) : r322RegionThreeDensity C lam ε supportConstant n q = ∫ (u : T4), reductionRegionThreeKernel q (primitiveKernelMajorant C lam ε supportConstant n) u ∂paperMeasure

The split expression is exactly the region-restricted primitive majorant with the inner Green factor.

theorem Anderson4D.exists_r322RegionThreeDensity_profile_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (Knear : ℝ) (Kouter : ℝ), 0 < Knear ∧ 0 < Kouter ∧ ∀ (C lam ε : ℝ) (n : ℕ) (q : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → r322RegionThreeDensity C lam ε supportConstant n q ≤ (r322ScaleBall (3 * supportConstant + 1) ε).indicator (fun (x : T4) => (C * lam) ^ (2 * n) * Knear * (ε⁻¹ ^ 4 / |Real.log ε|)) q + (r322CriticalAnnulus ε).indicator (fun (z : T4) => (C * lam) ^ (2 * n) * Kouter * (1 / |Real.log ε|) * invSqKer z ^ 2) q

Pointwise two-profile estimate for (4.12).

theorem Anderson4D.exists_r322RegionThreeDensity_convolution_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ) (x : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → x ≠ 0 → ∫ (q : T4), invSqKer (x - q) * r322RegionThreeDensity C lam ε supportConstant n q ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K * invSqKer x

The full (4.12) density preserves the inverse-square Green majorant after the outer integration.