Quadratic data for the Gaussian cutoff

Bounded smooth cutoff factors preserve the finite quadratic data used in lem:uc-gaussian.

theorem ESS.ucGaussianCutoff_memLp_data {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {v : 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} (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (ucCylinder ρ))) (hDw : MeasureTheory.MemLp Dw 2 (MeasureTheory.volume.restrict (ucCylinder ρ))) (hD2w : MeasureTheory.MemLp D2w 2 (MeasureTheory.volume.restrict (ucCylinder ρ))) (hDtw : MeasureTheory.MemLp Dtw 2 (MeasureTheory.volume.restrict (ucCylinder ρ))) : MeasureTheory.MemLp (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffD2 (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw D2w) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffDt (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dtw) 2 (MeasureTheory.volume.restrict (ucCylinder ρ))

The Gaussian cutoff preserves quadratic data for all three weak derivative fields on the normalized cylinder.

theorem ESS.ucGaussianCutoff_l2_data {ρ ε : ℝ} (hρ : 0 < ρ) (hε : 0 < ε) {v : 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} (hweak : CKN.HasSpaceTimeWeakDerivs (CKN.Foundation.Parabolic.vec3Ball 0 ρ) (Set.Ioo 0 2) v Dw D2w Dtw) (hL2 : ∫⁻ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ‖v z‖ₑ ^ 2 + ‖Dw z‖ₑ ^ 2 + ‖D2w z‖ₑ ^ 2 + ‖Dtw z‖ₑ ^ 2 < ⊤) : MeasureTheory.MemLp (ucCutoffField (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffDw (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffD2 (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dw D2w) 2 (MeasureTheory.volume.restrict (ucCylinder ρ)) ∧ MeasureTheory.MemLp (ucCutoffDt (ucSpatialCutoff ρ hρ) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dtw) 2 (MeasureTheory.volume.restrict (ucCylinder ρ))

Finite quadratic data on the normalized cylinder give finite quadratic data after the Gaussian cutoff.