Integrability of the weighted cutoff energy

The lower time cutoff removes the Gaussian weight singularity at time zero.

theorem ESS.uc_cutoff_energy_zero_below {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (z : CKN.Foundation.Parabolic.ParabolicPoint) (hz : z.2 ≤ ε) : ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v z = 0 ∧ ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv z = 0

The cut off field and its first spatial derivative vanish through the initial cutoff time.

theorem ESS.uc_weighted_cutoff_energy_integrable {ρ ε a : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) (ha : 0 ≤ a) {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 0 2) v Dv D2v Dtv) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dv z‖ₑ ^ 2 + ‖D2v z‖ₑ ^ 2 + ‖Dtv z‖ₑ ^ 2 < ⊤) : have Z := ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v; have DZ := ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv; MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2 + CKN.spatialGradientSq Z DZ z)) (ucCylinder ρ) MeasureTheory.volume

The Gaussian weight times the cutoff field energy is integrable on the normalized cylinder for each positive initial cutoff time.