The scale-covariant local triple convolution

This file closes the one analytic predicate deliberately isolated in Continuum/CellSingular.lean. The proof uses the following four-dimensional scaling argument.

• the 3/2 power of the inverse-square kernel has local mass O(r);
• pointwise AM--GM bounds a product of three inverse-square kernels by the sum of the three products of two 3/2 powers;
• in the all-near cell configuration, every relevant cell is contained in a ball of radius 6r about the adjacent endpoint.

Thus each of the three separated products costs O(r) · O(r) = O(r²). The local 3/2-power estimate is proved by transporting to the fundamental cube and evaluating the radial integral ∫_{‖x‖<r} ‖x‖⁻³ dx = 4 vol(B₁) r in dimension four.

The subcritical 3/2 power

noncomputable def Anderson4D.invSqKerThreeHalf (z : T4) : ℝ

The 3/2 power of the inverse-square kernel, i.e. the model |z|⁻³ singularity.

Equations

• Anderson4D.invSqKerThreeHalf z = Anderson4D.invSqKer z ^ (3 / 2)

theorem Anderson4D.invSqKerThreeHalf_nonneg (z : T4) : 0 ≤ invSqKerThreeHalf z

theorem Anderson4D.measurable_invSqKerThreeHalf : Measurable invSqKerThreeHalf

theorem Anderson4D.invSqKerThreeHalf_neg (z : T4) : invSqKerThreeHalf (-z) = invSqKerThreeHalf z

theorem Anderson4D.invSqKerThreeHalf_sub_comm (x y : T4) : invSqKerThreeHalf (x - y) = invSqKerThreeHalf (y - x)

Cube transport for the local mass

theorem Anderson4D.integrable_invSqKerThreeHalf : MeasureTheory.Integrable invSqKerThreeHalf paperMeasure

The |z|⁻³ kernel is integrable on the torus.

theorem Anderson4D.integrable_invSqKerThreeHalf_sub_left (x : T4) : MeasureTheory.Integrable (fun (z : T4) => invSqKerThreeHalf (x - z)) paperMeasure

theorem Anderson4D.integrable_invSqKerThreeHalf_sub_right (x : T4) : MeasureTheory.Integrable (fun (z : T4) => invSqKerThreeHalf (z - x)) paperMeasure

theorem Anderson4D.integral_invSqKerThreeHalf_sub_left (x : T4) : ∫ (z : T4), invSqKerThreeHalf (x - z) ∂paperMeasure = ∫ (z : T4), invSqKerThreeHalf z ∂paperMeasure

Translation invariance of the total |z|⁻³ mass.

theorem Anderson4D.integral_invSqKerThreeHalf_sub_right (x : T4) : ∫ (z : T4), invSqKerThreeHalf (z - x) ∂paperMeasure = ∫ (z : T4), invSqKerThreeHalf z ∂paperMeasure

theorem Anderson4D.invSqKerThreeHalf_ball_sub_le : ∃ (C : ℝ), 0 < C ∧ ∀ (x : T4) (r : ℝ), 0 < r → ∫ (z : T4) in Metric.ball x r, invSqKerThreeHalf (x - z) ∂paperMeasure ≤ C * r

Uniform local |z|⁻³ mass. A radius-r torus ball about the singularity has mass O(r), uniformly in its centre.

Pointwise AM--GM and cell geometry

theorem Anderson4D.invSqKer_triple_le_threeHalf_pairs (u v w : T4) : invSqKer u * invSqKer v * invSqKer w ≤ invSqKerThreeHalf u * invSqKerThreeHalf v + invSqKerThreeHalf v * invSqKerThreeHalf w + invSqKerThreeHalf u * invSqKerThreeHalf w

Closure of the all-near predicate

theorem Anderson4D.localTripleCellIntegral_le_scale : ∃ (C : ℝ), 0 < C ∧ ∀ (r : ℝ), 0 < r → ∀ (c₀ c₁ c₂ c₃ x y : T4), x ∈ Metric.ball c₀ r → y ∈ Metric.ball c₃ r → dist c₀ c₁ ≤ 4 * r → dist c₁ c₂ ≤ 4 * r → dist c₂ c₃ ≤ 4 * r → localTripleCellIntegral r c₁ c₂ x y ≤ C * r ^ 2

The local three-edge cell convolution has the sharp O(r²) scale whenever its four consecutive cell centres are 4r-near.

theorem Anderson4D.localTripleCellScaleBound : LocalTripleCellScaleBound

The isolated analytic predicate from CellSingular.lean is true.