I3

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

theorem CKN.caccioppoli_I3_holder {α : Type u_1} [MeasurableSpace α] {μ : MeasureTheory.Measure α} {P U : α → ENNReal} {C : ENNReal} (hP : AEMeasurable P μ) (hU : AEMeasurable U μ) (hC : C ≠ ⊤) : ∫⁻ (x : α), C * P x * U x ∂μ ≤ C * (∫⁻ (x : α), P x ^ (3 / 2) ∂μ) ^ (2 / 3) * (∫⁻ (x : α), U x ^ 3 ∂μ) ^ (1 / 3)

theorem CKN.caccioppoli_I3_pressure_integral_identity {Ω : 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) : ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder z.1 z.2 ρ, ENNReal.ofReal |p w| ^ (3 / 2) = ENNReal.ofReal (ρ ^ 2 * delta p z ρ ^ 3)

theorem CKN.caccioppoli_I3_normalization {κ δ γ K C₂₅ I₃ : ℝ} (hκ : 0 < κ) : 0 ≤ δ → ∀ (hγ : 0 ≤ γ) (hKbound : K ≤ C₂₅ ^ 2) (hraw : I₃ ≤ K * κ⁻¹ ^ 2 * δ ^ 2 * γ), I₃ ≤ (C₂₅ * κ⁻¹ * δ * γ ^ (1 / 2)) ^ 2