Caccioppoli Centered

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

theorem CKN.caccioppoli_centered_hcenter {Ω : 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) {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ : ℝ} (hρ : 0 < ρ) (hsub : closure (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ) ⊆ spaceTimeSet Ω I) : ∃ (c : Foundation.Parabolic.ParabolicPoint → ℝ), AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w|) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)) ∧ AEMeasurable (fun (w : Foundation.Parabolic.ParabolicPoint) => c w) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)) ∧ (∀ (w : Foundation.Parabolic.ParabolicPoint), c w = c (x₀, w.2)) ∧ (∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal |Foundation.Parabolic.vec3EuclideanNorm (u w) ^ 2 - c w| ^ (3 / 2)) ^ (2 / 3) ≤ ENNReal.ofReal (poincareSobolevL1VectorConstant * ρ ^ (4 / 3) * alpha u (x₀, t₀) ρ * beta u Du (x₀, t₀) ρ) ∧ (∀ (w : Foundation.Parabolic.ParabolicPoint), 0 ≤ c w) ∧ ∫⁻ (w : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ, ENNReal.ofReal (c w) ^ (3 / 2) ≤ ENNReal.ofReal (ρ ^ 2 * gamma u (x₀, t₀) ρ ^ 3)