Pk Bounds P7 Solution Bound

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

noncomputable def CKN.pressureP7SolutionConstant (q : ℝ) : ENNReal

Force coefficient in the P7 estimate after the Hardy–Littlewood–Sobolev bound.

Equations

• CKN.pressureP7SolutionConstant q = 3 * (ENNReal.ofReal (4 * Real.pi)⁻¹ * CKN.Foundation.Euclidean.hlsRieszConstant) * ENNReal.ofReal (4 * Real.pi / 3) ^ (1 - 1 / q)

theorem CKN.pressureP7SolutionConstant_ne_top {q : ℝ} (hq : 5 / 2 < q) : pressureP7SolutionConstant q ≠ ⊤

theorem CKN.pressureP7_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) : ENNReal.ofReal (r ^ (-4 / 3)) * MeasureTheory.eLpNorm' (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP7 (mollifiedBallCutoff z.1 hρ) f w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) ≤ pressureP7SolutionConstant q * ENNReal.ofReal (r / ρ * lambda q f z ρ)