Caccioppoli Energy

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

theorem CKN.caccioppoli_heat_cutoff_lower {x₀ : Foundation.Parabolic.Vec3} {t₀ ρ ε r : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (hr : 0 < r) (hscale : r ≤ ρ / 2) {z : Foundation.Parabolic.ParabolicPoint} (hz : z ∈ Foundation.Parabolic.parabolicCylinder x₀ t₀ r) : 1 / (2000 * r) ≤ backwardHeatCutoff (caccioppoliHeatCutoff x₀ t₀ ρ ε hρ hε) x₀ t₀ r z

theorem CKN.caccioppoli_cutoff_norm_measurable {Ω : 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) : AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u z))) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)) ∧ AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal |p z|) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ)) ∧ AEMeasurable (fun (z : Foundation.Parabolic.ParabolicPoint) => ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (f z))) (MeasureTheory.volume.restrict (Foundation.Parabolic.parabolicCylinder x₀ t₀ ρ))

theorem CKN.caccioppoli_nested_integral_eq {Ω : Set Foundation.Parabolic.Vec3} {T : Set ℝ} {g : Foundation.Parabolic.ParabolicPoint → ℝ} (hg : MeasureTheory.IntegrableOn g (Ω ×ˢ T) (MeasureTheory.volume.prod MeasureTheory.volume)) : ∫ (s : ℝ) in T, ∫ (x : Foundation.Parabolic.Vec3) in Ω, g (x, s) = ∫ (z : Foundation.Parabolic.Vec3 × ℝ) in Ω ×ˢ T, g z ∂MeasureTheory.volume.prod MeasureTheory.volume

theorem CKN.caccioppoli_lower_from_slice_bounds {u : Foundation.Parabolic.ParabolicPoint → Foundation.Parabolic.Vec3} {Du : Foundation.Parabolic.ParabolicPoint → Fin 3 → Foundation.Parabolic.Vec3} {x₀ : Foundation.Parabolic.Vec3} {t₀ r S : ℝ} (hr : 0 < r) (hS : 0 ≤ S) (hE : ∀ᵐ (t : ℝ) ∂MeasureTheory.volume.restrict (Set.Ioc (t₀ - r ^ 2) t₀), ∫⁻ (x : Foundation.Parabolic.Vec3) in Foundation.Parabolic.vec3Ball x₀ r, ENNReal.ofReal (Foundation.Parabolic.vec3EuclideanNorm (u (x, t)) ^ 2) ≤ ENNReal.ofReal (2000 * r * S)) (hG : ∫⁻ (z : Foundation.Parabolic.ParabolicPoint) in Foundation.Parabolic.parabolicCylinder x₀ t₀ r, ENNReal.ofReal (spatialGradientSq u Du z) ≤ ENNReal.ofReal (1000 * r * S)) : (alpha u (x₀, t₀) r + beta u Du (x₀, t₀) r) ^ 2 ≤ 6000 * S