Lin34 Slice Force Cylinder

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

The two cylinder bounds for the force terms p₇ and p₈ are added into a single L^{3/2} bound on the parabolic cylinder. This is the estimate r^{-2} ∫∫_{Q_r} |p₇ + p₈|^{3/2} ≤ (C₁₃(q) κ λ(z₀,ρ))^{3/2} appearing in the proof of prop:lin34(ii-b) of paper/ckn.tex.

noncomputable def CKN.lin34ForceCylinderConstant (q : ℝ) : ℝ

The constant C₁₃(q) of lem:pk-bounds(d)--(e) in paper/ckn.tex.

Equations

• CKN.lin34ForceCylinderConstant q = (CKN.pressureP7SolutionConstant q).toReal + CKN.pressureP13Constant q

theorem CKN.lin34ForceCylinderConstant_nonneg (q : ℝ) (hq : 5 / 2 < q) : 0 ≤ lin34ForceCylinderConstant q

The constant C₁₃(q) of lem:pk-bounds(d)--(e) in paper/ckn.tex is nonnegative for q > 5/2.

theorem CKN.lin34_force_cylinder_lintegral_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) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, ENNReal.ofReal (|pressureP7 (mollifiedBallCutoff z.1 hρ) f w.2 w.1 + pressureP8 (mollifiedBallCutoff z.1 hρ) f w.2 w.1| ^ (3 / 2)) ≤ ENNReal.ofReal (r ^ 2 * (lin34ForceCylinderConstant q * (r / ρ * lambda q f z ρ)) ^ (3 / 2))

The real-valued cylinder bound for the summed force terms in the proof of prop:lin34(ii-b) of paper/ckn.tex: integrating |p₇ + p₈|^{3/2} over Q_r is bounded by r^2 (C₁₃(q) κ λ(z₀,ρ))^{3/2}, the L^{3/2} form of lem:pk-bounds(d)--(e).

theorem CKN.lin34_force_integrableOn_cylinder {Ω : 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) : MeasureTheory.IntegrableOn (fun (w : Foundation.Parabolic.ParabolicPoint) => |pressureP7 (mollifiedBallCutoff z.1 hρ) f w.2 w.1 + pressureP8 (mollifiedBallCutoff z.1 hρ) f w.2 w.1| ^ (3 / 2)) (Foundation.Parabolic.parabolicCylinder z.1 z.2 r) MeasureTheory.volume

The force group p₇ + p₈ is L^{3/2} on the parabolic cylinder Q_r.

theorem CKN.lin34_force_cylinder_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) : ∫ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 r, |pressureP7 (mollifiedBallCutoff z.1 hρ) f w.2 w.1 + pressureP8 (mollifiedBallCutoff z.1 hρ) f w.2 w.1| ^ (3 / 2) ≤ r ^ 2 * (lin34ForceCylinderConstant q * (r / ρ * lambda q f z ρ)) ^ (3 / 2)

The real-valued form of the force cylinder bound in the proof of prop:lin34(ii-b) of paper/ckn.tex.