Lin34 Slice Integrated

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

eq:lin34-pointwise for a suitable weak solution, and its time integral

This file discharges, for a suitable weak solution, every hypothesis of the integrated estimate eq:lin35-force of prop:lin34(ii-b) in paper/ckn.tex except the Calderón--Zygmund bound ext:CZ for the centred first potential, which stays named as hCZ_p1.

theorem CKN.lin34_slice_pointwise_bound_ae_of_sws (C₁₁ : ℝ) (hC₁₁ : 0 ≤ C₁₁) {Ω : 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} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (hCZ_p1 : ∀ᵐ (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 ≤ C₁₁ * lin34VelocitySlice u z ρ s ^ (2 / 3)) : ∀ᵐ (s : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), r⁻¹ ^ 2 * lin34PressureSlice p z r s ≤ lin34PointwiseConstant C₁₁ * ((ρ / r) ^ 2 * lin34G u z ρ s + r / ρ * lin34H p z ρ s + r⁻¹ ^ 2 * lin34ForceSliceIntegral f z ρ r hρ s)

eq:lin34-pointwise at solution level. For a suitable weak solution and a.e.\ time in J_ρ, the normalised inner pressure mass is controlled by the velocity oscillation, the outer pressure mass, and the force group. The only named analytic input is hCZ_p1.

noncomputable def CKN.lin34ForceExponent (C₁₁ : ℝ) : ℝ

The exponent constant C₁₃ that makes the constant of eq:lin35-force dominate the pointwise constant of eq:lin34-pointwise.

Equations

• CKN.lin34ForceExponent C₁₁ = CKN.lin34PointwiseConstant C₁₁ ^ (2 / 3)

theorem CKN.lin34ForceExponent_nonneg {C₁₁ : ℝ} (hC₁₁ : 0 ≤ C₁₁) : 0 ≤ lin34ForceExponent C₁₁

theorem CKN.lin34_pointwiseConstant_le_forceConstant {C₁₁ : ℝ} (hC₁₁ : 0 ≤ C₁₁) : lin34PointwiseConstant C₁₁ ≤ lin34ForceConstant (lin34ForceExponent C₁₁)

theorem CKN.lin34_pointwise_bound_ae_of_sws (C₁₁ : ℝ) (hC₁₁ : 0 ≤ C₁₁) {Ω : 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} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (hCZ_p1 : ∀ᵐ (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 ≤ C₁₁ * lin34VelocitySlice u z ρ s ^ (2 / 3)) : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (z.2 - ρ ^ 2) z.2), lin34F p z r t ≤ lin34ForceConstant (lin34ForceExponent C₁₁) * ((ρ / r) ^ 2 * lin34G u z ρ t + r / ρ * lin34H p z ρ t + lin34J f z ρ r hρ t)

The pointwise hypothesis of eq:lin35-force. The four time functions F, G, H, J satisfy the pointwise inequality that the integrated estimate consumes, for a.e. time in J_ρ.

theorem CKN.lin34J_integral_bound {Ω : 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} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) : ∫ (t : ℝ) in Set.Ioc (z.2 - ρ ^ 2) z.2, lin34J f z ρ r hρ t ≤ (r / ρ) ^ (3 / 2) * (lin34ForceCylinderConstant q * lambda q f z ρ) ^ (3 / 2)

The force hypothesis of eq:lin35-force. The time integral of the force quantity carries the factor (r/ρ)^{3/2} of prop:lin34(ii-b).

theorem CKN.pressure_lin34_force_of_sws (C₁₁ : ℝ) (hC₁₁ : 0 ≤ C₁₁) {Ω : 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} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (hCZ_p1 : ∀ᵐ (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 ≤ C₁₁ * lin34VelocitySlice u z ρ s ^ (2 / 3)) : pressureD p z r ≤ lin34ForceConstant (lin34ForceExponent C₁₁) * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * (lin34ForceCylinderConstant q * lambda q f z ρ) ^ (3 / 2))

eq:lin35-force of prop:lin34(ii-b) for a suitable weak solution.

The pressure quantity D(z₀,r) is bounded by the velocity oscillation C_hat(z₀,ρ) with the factor (ρ/r)², the pressure quantity D(z₀,ρ) with the factor r/ρ, and the force quantity λ(z₀,ρ)^{3/2} with the factor (r/ρ)^{3/2}. The only named analytic input is the Calderón--Zygmund bound ext:CZ for the centred first potential.

noncomputable def CKN.lin34SolutionForceExponent (C₁₁ q : ℝ) : ℝ

The constant C₃₂(q) of eq:lin35-force in paper/ckn.tex, expressed through the exponent that lin34ForceConstant consumes.

Equations

• CKN.lin34SolutionForceExponent C₁₁ q = (CKN.lin34ForceConstant (CKN.lin34ForceExponent C₁₁) * (1 + CKN.lin34ForceCylinderConstant q ^ (3 / 2))) ^ (2 / 3)

theorem CKN.pressure_lin34_force_lambda_of_sws (C₁₁ : ℝ) (hC₁₁ : 0 ≤ C₁₁) {Ω : 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} {ρ r : ℝ} (hρ : 0 < ρ) (hr : 0 < r) (hhalf : r ≤ ρ / 2) (hsub : closure (Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ) ⊆ spaceTimeSet Ω I) (hCZ_p1 : ∀ᵐ (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 ≤ C₁₁ * lin34VelocitySlice u z ρ s ^ (2 / 3)) : pressureD p z r ≤ lin34ForceConstant (lin34SolutionForceExponent C₁₁ q) * ((ρ / r) ^ 2 * pressureChat u z ρ + r / ρ * pressureD p z ρ + (r / ρ) ^ (3 / 2) * lambda q f z ρ ^ (3 / 2))

eq:lin35-force in the shape consumed by the scale iteration. The force enters through λ(z₀,ρ)^{3/2} alone, the constant C₁₃(q) of lem:pk-bounds(d)--(e) having been absorbed into C₃₂.