Approximate-identity estimates for the R-322 collapse

The Taylor region in paper (4.10) leaves two radial kernels in the outer variable. The first is the normalized indicator of a ball of radius O(ε). This file proves directly that convolution with this kernel preserves the inverse-square Green majorant. The critical annular kernel is treated below by the same near/far decomposition.

def Anderson4D.r322ScaleBall (supportConstant ε : ℝ) : Set T4

The closed torus ball at the primitive support scale.

Equations

• Anderson4D.r322ScaleBall supportConstant ε = {z : Anderson4D.T4 | Anderson4D.torusDistSq z ≤ (supportConstant * ε) ^ 2}

theorem Anderson4D.measurableSet_r322ScaleBall (supportConstant ε : ℝ) : MeasurableSet (r322ScaleBall supportConstant ε)

theorem Anderson4D.r322ScaleBall_subset_metricBall {supportConstant ε : ℝ} (hsupport : 0 < supportConstant) (hε : 0 < ε) : r322ScaleBall supportConstant ε ⊆ Metric.ball 0 (2 * (supportConstant * ε))

theorem Anderson4D.exists_r322ScaleBall_convolution_le {supportConstant : ℝ} (hsupport : 0 < supportConstant) : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (x : T4), 0 < ε → x ≠ 0 → ε⁻¹ ^ 4 * ∫ (z : T4) in r322ScaleBall supportConstant ε, invSqKer (x - z) ∂paperMeasure ≤ K * invSqKer x

The normalized ε-ball is an approximate identity for the inverse-square kernel. The constant is chosen before ε and the external point; dependence on the fixed primitive support radius is explicit in the choice of K.

def Anderson4D.r322CriticalAnnulus (ε : ℝ) : Set T4

The critical annulus outside the cutoff scale.

Equations

• Anderson4D.r322CriticalAnnulus ε = {z : Anderson4D.T4 | ε ^ 2 ≤ Anderson4D.torusDistSq z}

theorem Anderson4D.measurableSet_r322CriticalAnnulus (ε : ℝ) : MeasurableSet (r322CriticalAnnulus ε)

theorem Anderson4D.invSqKer_le_sixteen_mul_of_half_norm {x w : T4} (hx : x ≠ 0) (hfar : ‖x‖ / 2 ≤ ‖w‖) : invSqKer w ≤ 16 * invSqKer x

If w is at least half as far from zero as x, its inverse-square kernel is controlled by the kernel at x.

theorem Anderson4D.integrableOn_invSqKer_sq_r322CriticalAnnulus {ε : ℝ} (hε : 0 < ε) : MeasureTheory.IntegrableOn (fun (z : T4) => invSqKer z ^ 2) (r322CriticalAnnulus ε) paperMeasure

theorem Anderson4D.integrableOn_r322Critical_product {ε : ℝ} (hε : 0 < ε) (x : T4) : MeasureTheory.IntegrableOn (fun (z : T4) => invSqKer (x - z) * invSqKer z ^ 2) (r322CriticalAnnulus ε) paperMeasure

On the critical annulus the squared kernel is bounded, which supplies the joint integrability needed before splitting at the second singularity.

theorem Anderson4D.exists_r322CriticalAnnulus_convolution_le : ∃ (K : ℝ), 0 < K ∧ ∀ (ε : ℝ) (x : T4), 0 < ε → ε ≤ 1 → 1 ≤ |Real.log ε| → x ≠ 0 → 1 / |Real.log ε| * ∫ (z : T4) in r322CriticalAnnulus ε, invSqKer (x - z) * invSqKer z ^ 2 ∂paperMeasure ≤ K * invSqKer x

The logarithmically normalized critical annulus is also an approximate identity for the inverse-square kernel. The proof splits at a ball around the moving singularity x; this avoids any hidden use of a non-integrable product.