Caccioppoli estimates on Gaussian collar cells

The local energy inequality applies to each enlarged cell of the rescaled Gaussian collar.

theorem ESS.buGaussian_local_energy_integrable {Ω : Set CKN.Foundation.Parabolic.Vec3} {I : Set ℝ} {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs Ω I v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet Ω I, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) : MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I)) ∧ MeasureTheory.Integrable (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => CKN.spatialGradientSq v Dv z) (MeasureTheory.volume.restrict (CKN.spaceTimeSet Ω I))

Finite quadratic data imply integrability of the scalar velocity and gradient energies on the cylinder (lem:bu-gaussian#caccioppoli).

theorem ESS.buGaussian_cell_caccioppoli (ρ : ℝ) (x : CKN.Foundation.Parabolic.Vec3) (σ t r c : ℝ) (hr : 0 < r) (hc : 0 ≤ c) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hcont : ContinuousOn v (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ico σ 2)) (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2), ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo σ 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) (hspace : CKN.Foundation.Parabolic.vec3Ball x (2 * r) ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (htime : Set.Ioo t (t + 4 * r ^ 2) ⊆ Set.Ioo σ 2) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo t (t + r ^ 2)), CKN.spatialGradientSq v Dv 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 (v z) ^ 2

Apply lem:caccioppoli to one space-time cell inside the rescaled Gaussian cylinder.

theorem ESS.buGaussian_weighted_caccioppoli_cell {ρ a r c t : ℝ} {x : CKN.Foundation.Parabolic.Vec3} (hρ : 0 < ρ) (ha : 0 < a) (hr : 0 < r) (hcenter : CKN.Foundation.Parabolic.vec3EuclideanNorm x ≤ ρ - 1 / 2) (hspace : CKN.Foundation.Parabolic.vec3Ball x r ⊆ CKN.Foundation.Parabolic.vec3Ball 0 ρ) (htime : Set.Ioo t (t + r ^ 2) ⊆ Set.Ioo (1 / 6) 2) {v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} {Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3} {D2v : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → Fin 3 → CKN.Foundation.Parabolic.Vec3} {Dtv : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2) v Dv D2v Dtv) (hcont : ContinuousOn v (CKN.Foundation.Parabolic.vec3Ball 0 ρ ×ˢ Set.Ico (1 / 6) 2)) (hc : 0 ≤ c) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2), ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) (hineq : ∀ᵐ (z : CKN.Foundation.Parabolic.ParabolicPoint) ∂MeasureTheory.volume.restrict (CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo (1 / 6) 2)), CKN.Foundation.Parabolic.vec3EuclideanNorm (ucWeakHeatVector D2v Dtv z) ≤ c * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) + √(CKN.spatialGradientSq v Dv z))) : ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x (r / 2)) (Set.Ioo t (t + (r / 2) ^ 2)), ucGaussianWeight a z * CKN.spatialGradientSq v Dv z ≤ Real.exp (2 * (56 * a * r ^ 2 + 12 * ρ * r + 36 * ρ ^ 2 * r ^ 2)) * (256 * (1 + c ^ 2 + 1 / (r / 2) ^ 2)) * ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball x r) (Set.Ioo t (t + r ^ 2)), ucGaussianWeight a z * CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2

The Gaussian weight lets the Caccioppoli estimate be compared on one enlarged collar cell.