The truncated Taylor profile in the R-322 collapse

After the class-E cancellation in region (4.10), the primitive block is weighted by the squared increment and integrated only over 2‖u‖ ≤ ‖q‖. This file proves the two pointwise profiles used by the outer integral:

• on torusDistSq q ≤ ε², a flat ε⁻⁴ / |log ε| bound;
• on ε² ≤ torusDistSq q, a critical invSqKer q ^ 2 / |log ε| bound.

Both are consequences of the explicit Proposition 4.1 majorant, not additional reduction hypotheses.

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

The radial moment remaining after Taylor cancellation in (4.10).

Equations

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

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

The outer density after inserting the Hessian singularity.

Equations

• Anderson4D.r322TaylorDensity C lam ε supportConstant n q = Anderson4D.invSqKer q ^ 2 * Anderson4D.r322TaylorMoment C lam ε supportConstant n q

theorem Anderson4D.measurable_primitiveKernelMajorant (C lam ε supportConstant : ℝ) (n : ℕ) : Measurable (primitiveKernelMajorant C lam ε supportConstant n)

theorem Anderson4D.measurable_r322TaylorMoment (C lam ε supportConstant : ℝ) (n : ℕ) : Measurable (r322TaylorMoment C lam ε supportConstant n)

theorem Anderson4D.measurable_r322TaylorDensity (C lam ε supportConstant : ℝ) (n : ℕ) : Measurable (r322TaylorDensity C lam ε supportConstant n)

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

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

theorem Anderson4D.torusDistSq_mul_invSqKer_le_one (z : T4) : torusDistSq z * invSqKer z ≤ 1

@[simp]

theorem Anderson4D.invSqKer_zero_r322 : invSqKer 0 = 0

theorem Anderson4D.invSqKer_sq_mul_norm_four_le_one (z : T4) : invSqKer z ^ 2 * ‖z‖ ^ 4 ≤ 1

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

theorem Anderson4D.primitiveKernelMajorant_nonneg_even (C lam ε supportConstant : ℝ) (n : ℕ) (z : T4) : 0 ≤ primitiveKernelMajorant C lam ε supportConstant n z

theorem Anderson4D.integrable_weighted_primitiveKernelMajorant {C lam ε supportConstant : ℝ} {n : ℕ} (hsupport : 0 < supportConstant) (hε : 0 < ε) : MeasureTheory.Integrable (fun (u : T4) => primitiveKernelMajorant C lam ε supportConstant n u * torusDistSq u) paperMeasure

theorem Anderson4D.integrable_r322TaylorMoment_integrand {C lam ε supportConstant : ℝ} {n : ℕ} {q : T4} (hsupport : 0 < supportConstant) (hε : 0 < ε) : MeasureTheory.Integrable (fun (u : T4) => reductionRegionOneKernel q (primitiveKernelMajorant C lam ε supportConstant n) u * torusDistSq u) paperMeasure

theorem Anderson4D.r322TaylorRegion_subset_ball {q : T4} (hq : q ≠ 0) : {u : T4 | 2 * ‖u‖ ≤ ‖q‖} ⊆ Metric.ball 0 ‖q‖

theorem Anderson4D.exists_r322TaylorDensity_inner_le : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε supportConstant : ℝ) (n : ℕ) (q : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → 0 < supportConstant → 1 ≤ |Real.log ε| → q ≠ 0 → torusDistSq q ≤ ε ^ 2 → r322TaylorDensity C lam ε supportConstant n q ≤ (C * lam) ^ (2 * n) * K * (ε⁻¹ ^ 4 / |Real.log ε|)

Inner-scale part of the Taylor density.

theorem Anderson4D.exists_r322TaylorDensity_outer_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (C lam ε : ℝ) (n : ℕ) (q : T4), 0 ≤ C → 0 ≤ lam → 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → r322TaylorDensity C lam ε supportConstant n q ≤ (C * lam) ^ (2 * n) * K * (1 / |Real.log ε| * invSqKer q ^ 2)

Outer-scale part of the Taylor density, retaining the critical inverse logarithm.

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

The complete Taylor-region outer integral preserves the inverse-square majorant. This is the analytic content of paper (4.10) after class-E cancellation: neither a cutoff power nor an extra logarithm is lost.