Target box on the Gaussian cutoff plateau

At target times the compact cutoff equals the original field and its spatial weak gradient, uniformly for small initial cutoff parameters.

theorem ESS.uc_target_box_weighted_le_cutoff_energy {ρ ε a : ℝ} (hρ : 4 ≤ ρ) (hε : 0 < ε) (hεsmall : ε < 1 / 4) (center : CKN.Foundation.Parabolic.Vec3) (hbox : CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1) ⊆ ucInnerRegion ρ) {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 < ⊤) (ha : 0 ≤ a) : have Z := ucCutoffField (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v; have DZ := ucCutoffDw (ucSpatialCutoff ρ ⋯) ucFinalTimeCutoff (ucInitialTimeCutoff ε) v Dv; ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in CKN.spaceTimeSet (CKN.Foundation.Parabolic.vec3Ball center 1) (Set.Ioo (1 / 2) 1), ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (v z) ^ 2 + CKN.spatialGradientSq v Dv z) ≤ ∫ (z : CKN.Foundation.Parabolic.ParabolicPoint) in ucCylinder ρ, ucGaussianWeight a z * (CKN.Foundation.Parabolic.vec3EuclideanNorm (Z z) ^ 2 + CKN.spatialGradientSq Z DZ z)

The weighted energy on a target box is bounded by the full weighted cutoff energy for every sufficiently small initial cutoff.