Lin34 Centred Potential Growth

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

Summation of the centred potentials p₂--p₆

The five sources of prop:pressure-decomposition produced in Lin34CentredPotentialSource.lean are fed to the single-potential growth engines and the resulting nine-entry groups are summed.

Step D: summation of the nine-entry groups

theorem CKN.lin34_double_sum_memLp_and_lpNorm_growth {G : Fin 3 → Fin 3 → Foundation.Parabolic.Vec3 → ℝ} {C : Fin 3 → Fin 3 → ℝ} (hmem : ∀ (i j : Fin 3) (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (G i j) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) (hb : ∀ (i j : Fin 3) (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (G i j) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ C i j * (1 + ρ)) : (∀ (ρ : ℝ), 0 < ρ → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, G i j x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ))) ∧ ∀ (ρ : ℝ), 0 < ρ → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, G i j x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 ρ)) ≤ (∑ i : Fin 3, ∑ j : Fin 3, C i j) * (1 + ρ)

A double sum of L^{3/2} functions, each obeying a local linear growth bound, obeys the local membership and the linear growth bound with the sum of the constants. This packages the Fin 3 × Fin 3 index range over which the potentials p₂, p₃, p₄ of prop:pressure-decomposition are summed.

Steps C and D: the group p₂ + p₃ + p₄ + p₅ + p₆

theorem CKN.lin34_centred_potentials_memLp_and_growth {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {x₀ : Foundation.Parabolic.Vec3} {ρ : ℝ} (hρ : 0 < ρ) {s : ℝ} (hu : MeasureTheory.AEStronglyMeasurable (fun (y : Foundation.Parabolic.Vec3) => u (y, s)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) (hv : MeasureTheory.IntegrableOn (fun (y : Foundation.Parabolic.Vec3) => Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) (euclideanBall x₀ ρ) MeasureTheory.volume) (hp : MeasureTheory.MemLp (fun (y : Foundation.Parabolic.Vec3) => p (y, s)) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (Foundation.Parabolic.vec3Ball x₀ ρ))) : ∃ (C : ℝ), 0 ≤ C ∧ (∀ (R : ℝ), 0 < R → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => pressureP2 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP3 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP4 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP5 (mollifiedBallCutoff x₀ hρ) p s x + pressureP6 (mollifiedBallCutoff x₀ hρ) p s x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R))) ∧ ∀ (R : ℝ), 0 < R → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => pressureP2 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP3 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP4 (mollifiedBallCutoff x₀ hρ) (lin34CentredVelocity u x₀ ρ) 0 s x + pressureP5 (mollifiedBallCutoff x₀ hρ) p s x + pressureP6 (mollifiedBallCutoff x₀ hρ) p s x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R)) ≤ C * (1 + R)

Local L^{3/2} membership on every round ball about the origin, with linear growth of the norm, for the five Newtonian-potential parts p₂, p₃, p₄, p₅, p₆ of the pressure decomposition prop:pressure-decomposition, run with the mollified cut-off of B_ρ(x₀) and the doubly centred velocity eq:Uhat. This is the decay input of the Liouville identification step of prop:lin34.