Lin34 Centred CZResidual

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

ext:CZ for the centred potential from the residual growth alone

Feeding the centred identification data of Lin34CentredPairingSWS.lean into the unconditional singular-integral estimate leaves a single named input: the local L^{3/2} membership, with linear growth, of the difference between the centred potential p₁ of prop:pressure-decomposition and the indexed second-order Riesz extension of its source. That is the decay hypothesis of the Liouville step of ext:newtonian.

theorem CKN.lin34_hCZ_p1_of_residual_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) (hresidual : ∀ᵐ (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)) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), MeasureTheory.MemLp (lin34CentredP1 u p f z.1 ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (lin34CentredP1 u p f z.1 ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ lin34CZConstant * lin34VelocitySlice u z ρ s ^ (2 / 3)

ext:CZ at solution level, from the residual decay alone. For a suitable weak solution and almost every time of the cylinder Q_ρ(z₀), the centred first potential is globally L^{3/2} with norm at most lin34CZConstant times the velocity oscillation eq:Chat to the power 2/3. This is the hypothesis hCZ_p1 of pressure_lin34_force_lambda_of_sws.