Local energy estimate for a parabolic differential inequality

This file proves the estimate in lem:caccioppoli.

theorem ESS.caccioppoli (x : CKN.Foundation.Parabolic.Vec3) (t r c₁ : ℝ) (hr : 0 < r) (hc₁ : 0 ≤ c₁) {w : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dw : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2w : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtw : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hderiv : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball x (2 * r)) (Set.Ioo t (t + 4 * r ^ 2)) w Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x (2 * r)) (Set.Ioo t (t + 4 * r ^ 2)), ‖w z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x (2 * r)) (Set.Ioo t (t + 4 * r ^ 2))), (CKN.Foundation.Parabolic.vec3EuclideanNorm fun (i : Fin 3) => Dtw z i + ∑ j : Fin 3, D2w z i j j) ≤ c₁ * (CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) + √(CKN.spatialGradientSq w Dw z))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo t (t + r ^ 2)), CKN.spatialGradientSq w Dw z ≤ 256 * (1 + c₁ ^ 2 + 1 / r ^ 2) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x (2 * r)) (Set.Ioo t (t + 4 * r ^ 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (w z) ^ 2

The local energy estimate for a vector field satisfying a backward parabolic differential inequality (lem:caccioppoli). The integrals are real Bochner integrals; the stated weak derivative and square-integrability hypotheses make their integrands integrable on the indicated cylinders.