Lin34 Centred Residual

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

Local growth of the centred first potential against its indexed extension

This file supplies the decay hypothesis of the Liouville step of ext:newtonian in paper/ckn.tex for the centred first potential of prop:pressure-decomposition: for a suitable weak solution and almost every time of the cylinder Q_ρ(z₀), the difference between the centred potential p₁ and the indexed second-order Riesz extension of its source lies in L^{3/2} on every round ball about the origin, with norm growing at most linearly in the radius.

The residual bookkeeping is the established comparison pressureSecondExtension_residual_growth_of_decomposition, fed with the p₂--p₆ group of prop:pressure-decomposition, the force group p₇ + p₈, the cut-off pressure, and the indexed extension of the cut-off centred tensor.

theorem CKN.lin34_centred_residual_local_growth_ae_of_sws {Ω : Set Foundation.Parabolic.Vec3} {I : Set ℝ} {q : ℝ} {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} (hsol : IsSuitableWeakSolutionIntegrable Ω I q u Du p f) {z : Foundation.Parabolic.ParabolicPoint} {ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∃ (C : ℝ), 0 ≤ C ∧ (∀ (R : ℝ), 0 < R → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (lin34CentredSource u z.1 hρ s) x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R))) ∧ ∀ (R : ℝ), 0 < R → MeasureTheory.lpNorm (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (lin34CentredSource u z.1 hρ s) x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R)) ≤ C * (1 + R)

Decay of the centred potential residual. For a suitable weak solution and almost every time s of the cylinder Q_ρ(z₀), the difference between the centred first potential p₁ of prop:pressure-decomposition and the indexed second-order Riesz extension of its source η·Û lies in L^{3/2} on every round ball about the origin, with local norm bounded by a constant times 1 + R.

The constant accumulates the four pieces of the decomposition: the cut-off pressure, the p₂--p₆ group, the force group p₇ + p₈, and the indexed extension itself. This is the Liouville decay input of ext:newtonian in paper/ckn.tex.