Radial moment ledger for the R-322 collapse

The Taylor region of paper (4.10) and the two crude regions (4.11)--(4.12) all reduce to the same scale-free fact: after multiplying the ordinary Proposition 4.1 majorant by torusDistSq, its integral is bounded uniformly in the cutoff scale. This file proves that fact from the public ball and critical-annulus estimates in SingularConv.

noncomputable def Anderson4D.r322LocalMoment (supportConstant ε : ℝ) (z : T4) : ℝ

The local-support contribution after multiplication by the quadratic Taylor factor.

Equations

• Anderson4D.r322LocalMoment supportConstant ε z = Anderson4D.torusDistSq z * Anderson4D.invSqKer z * Anderson4D.primitiveSupportIndicator supportConstant ε z

noncomputable def Anderson4D.r322RegularizedMoment (ε : ℝ) (z : T4) : ℝ

The regularized contribution after multiplication by the quadratic Taylor factor.

Equations

• Anderson4D.r322RegularizedMoment ε z = Anderson4D.torusDistSq z * (Anderson4D.torusDistSq z + ε ^ 2)⁻¹ ^ 3

theorem Anderson4D.r322LocalMoment_nonneg (supportConstant ε : ℝ) (z : T4) : 0 ≤ r322LocalMoment supportConstant ε z

theorem Anderson4D.r322RegularizedMoment_nonneg (ε : ℝ) (z : T4) : 0 ≤ r322RegularizedMoment ε z

theorem Anderson4D.measurable_r322LocalMoment (supportConstant ε : ℝ) : Measurable (r322LocalMoment supportConstant ε)

theorem Anderson4D.measurable_r322RegularizedMoment (ε : ℝ) : Measurable (r322RegularizedMoment ε)

theorem Anderson4D.integrable_r322LocalMoment {supportConstant ε : ℝ} (hsupport : 0 < supportConstant) (hε : 0 < ε) : MeasureTheory.Integrable (r322LocalMoment supportConstant ε) paperMeasure

theorem Anderson4D.integrable_r322RegularizedMoment {ε : ℝ} (hε : 0 < ε) : MeasureTheory.Integrable (r322RegularizedMoment ε) paperMeasure

theorem Anderson4D.integral_r322LocalMoment_le {Cball supportConstant ε : ℝ} (hball : ∀ (r : ℝ), 0 < r → ∫ (z : T4) in {z : T4 | torusDistSq z ≤ r ^ 2}, invSqKer z ∂paperMeasure ≤ Cball * r ^ 2) (hsupport : 0 < supportConstant) (hε : 0 < ε) : ∫ (z : T4), r322LocalMoment supportConstant ε z ∂paperMeasure ≤ Cball * (supportConstant * ε) ^ 4

The local-support moment is O((supportConstant * ε)^4).

theorem Anderson4D.integral_r322RegularizedMoment_le {Cball Cannulus ε : ℝ} (hball : ∀ (r : ℝ), 0 < r → ∫ (z : T4) in {z : T4 | torusDistSq z ≤ r ^ 2}, invSqKer z ∂paperMeasure ≤ Cball * r ^ 2) (hannulus : ∀ (r : ℝ), 0 < r → r ≤ 1 → ∫ (z : T4) in {z : T4 | r ^ 2 ≤ torusDistSq z}, invSqKer z ^ 2 ∂paperMeasure ≤ Cannulus * (1 + |Real.log r|)) (hε : 0 < ε) (hε1 : ε ≤ 1) : ∫ (z : T4), r322RegularizedMoment ε z ∂paperMeasure ≤ Cball + Cannulus * (1 + |Real.log ε|)

The regularized moment has only the critical logarithmic loss.

theorem Anderson4D.exists_primitiveKernelMajorant_moment_bound {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → MeasureTheory.Integrable (fun (z : T4) => torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z) paperMeasure ∧ ∫ (z : T4), torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z ∂paperMeasure ≤ (C * lam) ^ (2 * n) * K

Uniform quadratic-moment bound for the complete ordinary Proposition 4.1 majorant. The constant is chosen before the coupling, scale, and perturbative order.

theorem Anderson4D.exists_primitiveKernelMajorant_moment_bound_div_log {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → MeasureTheory.Integrable (fun (z : T4) => torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z) paperMeasure ∧ ∫ (z : T4), torusDistSq z * primitiveKernelMajorant C lam ε supportConstant n z ∂paperMeasure ≤ (C * lam) ^ (2 * n) * (K / |Real.log ε|)

Sharpened form of the preceding moment ledger, retaining the inverse logarithm which is needed before the outer approximate-identity convolution in paper (4.10).