Lin34 Centred CZ

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

The Calderón--Zygmund bound for the centred first pressure potential

The oscillation estimate prop:lin34 of paper/ckn.tex consumes the external input ext:CZ in the shape

‖p₁(·, s)‖_{L^{3/2}(ℝ³)} ≤ C₁₁ · (∫_{B_ρ} |u - ⨍u|³)^{2/3},

where p₁ is the leading potential of prop:pressure-decomposition run with the doubly centred nonlinearity eq:Uhat. This file derives that display from the unconditional singular-integral estimate for the indexed second-order Riesz extension, the source estimate for the cut-off centred tensor, and the distributional identification data for the centred potential.

noncomputable def CKN.lin34CZConstant : ℝ

The Calderón--Zygmund constant C₁₁ of ext:CZ produced here: nine times the component constant of the indexed second-order extension, the factor nine coming from summing the nine entries of the tensor source.

Equations

• CKN.lin34CZConstant = 9 * CKN.Foundation.Euclidean.czP1OperatorConstant

theorem CKN.lin34CZConstant_nonneg : 0 ≤ lin34CZConstant

theorem CKN.lin34_hCZ_p1_slice_of_identification {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {p : Foundation.Parabolic.ParabolicPoint → ℝ} {f : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {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) (hP1 : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f x₀ ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), lin34CentredP1 u p f x₀ ρ hρ s x * spatialLaplacian ψ x = pressureSecondPairing (lin34CentredSource u x₀ hρ s) ψ) (hP1Int : ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f x₀ ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume) (hresidual : ∃ (C : ℝ), 0 ≤ C ∧ (∀ (R : ℝ), 0 < R → MeasureTheory.MemLp (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f x₀ ρ hρ s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (lin34CentredSource u x₀ 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 x₀ ρ hρ s x - pressureSecondExtensionOperator Foundation.Euclidean.rieszSecondL2Input Foundation.Euclidean.rieszSecondL2_weak_type (lin34CentredSource u x₀ hρ s) x) (ENNReal.ofReal (3 / 2)) (MeasureTheory.volume.restrict (euclideanBall 0 R)) ≤ C * (1 + R)) : MeasureTheory.MemLp (lin34CentredP1 u p f x₀ ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ∧ MeasureTheory.lpNorm (lin34CentredP1 u p f x₀ ρ hρ s) (ENNReal.ofReal (3 / 2)) MeasureTheory.volume ≤ lin34CZConstant * (∫ (y : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ ρ, Foundation.Parabolic.vec3EuclideanNorm (meanFreeVec u x₀ ρ s y) ^ 3) ^ (2 / 3)

ext:CZ for the centred potential on one time slice. Given the distributional identification data for the centred first potential and the linear-growth control of its residual against the indexed extension, the L^{3/2} norm of p₁ is controlled by the L³ oscillation of the velocity on B_ρ, with the explicit constant lin34CZConstant.

theorem CKN.lin34_hCZ_p1_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) (hP1 : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume → ∫ (x : Foundation.Parabolic.Vec3), lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x = pressureSecondPairing (lin34CentredSource u z.1 hρ s) ψ) (hP1Int : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), ∀ (ψ : Foundation.Parabolic.Vec3 → ℝ), ContDiff ℝ (↑⊤) ψ → HasCompactSupport ψ → MeasureTheory.Integrable (fun (x : Foundation.Parabolic.Vec3) => lin34CentredP1 u p f z.1 ρ hρ s x * spatialLaplacian ψ x) MeasureTheory.volume) (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. For a suitable weak solution and almost every time of the cylinder Q_ρ(z₀), the centred first potential of prop:pressure-decomposition is globally L^{3/2} with norm controlled by the velocity oscillation eq:Chat. This is exactly the hypothesis hCZ_p1 that pressure_lin34_force_lambda_of_sws consumes, with C₁₁ = lin34CZConstant. The named inputs are the distributional identification data for the centred potential and the linear growth of its residual.