The crude Green profile in region (4.11)

Write q = z - y and u = z - w. The first non-Taylor region has ‖q‖ ≤ 2 ‖u‖; after taking the crude Green bound, its density is invSqKer q times the primitive-kernel mass on that region.

The local part of Proposition 4.1 is supported at q = O(ε) and has size ε⁻² / |log ε|. For the regularized part, the same bound holds at q = O(ε), while outside that ball one inverse-square factor is extracted and the remaining critical square contributes one logarithm.

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

Restriction to the crude z-y region in (4.11).

Equations

• Anderson4D.reductionRegionTwoKernel q J u = if ‖q‖ ≤ 2 * ‖u‖ then J u else 0

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

theorem Anderson4D.reductionRegionTwoKernel_eq_indicator (q : T4) (J : T4 → ℝ) : reductionRegionTwoKernel q J = {u : T4 | ‖q‖ ≤ 2 * ‖u‖}.indicator J

theorem Anderson4D.measurable_reductionRegionTwoKernel (q : T4) {J : T4 → ℝ} (hJ : Measurable J) : Measurable (reductionRegionTwoKernel q J)

theorem Anderson4D.integrable_reductionRegionTwoKernel (q : T4) {J : T4 → ℝ} (hJ : MeasureTheory.Integrable J paperMeasure) : MeasureTheory.Integrable (reductionRegionTwoKernel q J) paperMeasure

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

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

Local-support primitive mass left after integrating w.

Equations

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

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

Regularized primitive mass left after integrating w.

Equations

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

theorem Anderson4D.measurable_r322RegionTwoLocalMoment (supportConstant ε : ℝ) : Measurable (r322RegionTwoLocalMoment supportConstant ε)

theorem Anderson4D.measurable_r322RegionTwoRegularMoment (ε : ℝ) : Measurable (r322RegionTwoRegularMoment ε)

theorem Anderson4D.r322RegionTwoLocalMoment_nonneg (supportConstant ε : ℝ) (q : T4) : 0 ≤ r322RegionTwoLocalMoment supportConstant ε q

theorem Anderson4D.r322RegionTwoRegularMoment_nonneg (ε : ℝ) (q : T4) : 0 ≤ r322RegionTwoRegularMoment ε q

theorem Anderson4D.r322RegionTwoLocalMoment_le_total {supportConstant ε : ℝ} (q : T4) : r322RegionTwoLocalMoment supportConstant ε q ≤ ∫ (u : T4), invSqKer u * primitiveSupportIndicator supportConstant ε u ∂paperMeasure

theorem Anderson4D.r322RegionTwoRegularMoment_le_total {ε : ℝ} (hε : 0 < ε) (q : T4) : r322RegionTwoRegularMoment ε q ≤ ∫ (u : T4), regularizedInvCube ε u ∂paperMeasure

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

The local primitive contribution can occur only when the outer variable is itself at primitive scale.

theorem Anderson4D.r322RegionTwo_torusDistSq_le {q u : T4} (hregion : ‖q‖ ≤ 2 * ‖u‖) : torusDistSq q ≤ 16 * torusDistSq u

The region condition converts outer scale in q into an annular lower bound for the primitive variable.

theorem Anderson4D.regularizedInvCube_le_regionTwo_outer {ε : ℝ} (hε : 0 < ε) {q u : T4} (hq : ε ^ 2 ≤ torusDistSq q) (hregion : ‖q‖ ≤ 2 * ‖u‖) : regularizedInvCube ε u ≤ 16 * invSqKer q * invSqKer u ^ 2

theorem Anderson4D.exists_r322RegionTwoRegularMoment_outer_le : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (q : T4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → ε ^ 2 ≤ torusDistSq q → r322RegionTwoRegularMoment ε q ≤ K * |Real.log ε| * invSqKer q

Outside primitive scale, the regularized region-(4.11) mass gains one inverse-square factor and loses exactly one logarithm.

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

Full outer density of the (4.11) contribution, split according to the two explicit summands of Proposition 4.1.

Equations

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

theorem Anderson4D.measurable_r322RegionTwoDensity (C lam ε supportConstant : ℝ) (n : ℕ) : Measurable (r322RegionTwoDensity C lam ε supportConstant n)

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

theorem Anderson4D.r322RegionTwoDensity_eq_integral (C lam ε supportConstant : ℝ) (n : ℕ) (q : T4) (hε : 0 < ε) : r322RegionTwoDensity C lam ε supportConstant n q = invSqKer q * ∫ (u : T4), reductionRegionTwoKernel q (primitiveKernelMajorant C lam ε supportConstant n) u ∂paperMeasure

The split density is exactly invSqKer q times the restricted primitive majorant, rather than a new comparison kernel.

theorem Anderson4D.exists_r322RegionTwoDensity_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 ε| → r322RegionTwoDensity C lam ε supportConstant n q ≤ (r322ScaleBall (4 * supportConstant + 1) ε).indicator (fun (z : T4) => (C * lam) ^ (2 * n) * Knear * (ε⁻¹ ^ 2 / |Real.log ε|) * invSqKer z) q + (r322CriticalAnnulus ε).indicator (fun (z : T4) => (C * lam) ^ (2 * n) * Kouter * (1 / |Real.log ε|) * invSqKer z ^ 2) q

Pointwise two-profile estimate for (4.11): a scale-local inverse-square density plus the logarithmically normalized critical density.

theorem Anderson4D.exists_r322RegionTwoDensity_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) * r322RegionTwoDensity C lam ε supportConstant n q ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K * invSqKer x

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