Pk Bounds Unconditional P56

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

theorem CKN.pressure_integral_mul_le_volume_rpow {μ : MeasureTheory.Measure Foundation.Parabolic.Vec3} [MeasureTheory.IsFiniteMeasure μ] {f g : Foundation.Parabolic.Vec3 → ℝ} (hf : AEMeasurable f μ) (hg : AEMeasurable g μ) (hf0 : ∀ (y : Foundation.Parabolic.Vec3), 0 ≤ f y) (hg0 : ∀ (y : Foundation.Parabolic.Vec3), 0 ≤ g y) (hXfin : ∫⁻ (y : Foundation.Parabolic.Vec3), ENNReal.ofReal ((f y * g y) ^ (3 / 2)) ∂μ < ⊤) : ∫ (y : Foundation.Parabolic.Vec3), f y * g y ∂μ ≤ (μ Set.univ).toReal ^ (1 / 3) * (∫ (y : Foundation.Parabolic.Vec3), (f y * g y) ^ (3 / 2) ∂μ) ^ (2 / 3)

theorem CKN.pressureP56_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) => pressureP5 (mollifiedBallCutoff z.1 hρ) p w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r)) + MeasureTheory.eLpNorm' (fun (w : Foundation.Parabolic.ParabolicPoint) => pressureP6 (mollifiedBallCutoff z.1 hρ) p w.2 w.1) (3 / 2) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder z.1 z.2 r))) ≤ ENNReal.ofReal (pressureP12Constant * (r / ρ) ^ (2 / 3) * delta p z ρ ^ 2)