Quadratic data for smooth compact cutoffs

On the compact support of a smooth scalar cutoff, bounded multipliers preserve square integrability of the field and its specified derivatives.

def ESS.buCutSupportSet (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) : Set CKN.Foundation.Parabolic.ParabolicPoint

The parabolic preimage of a scalar cutoff's product-space support.

Equations

• ESS.buCutSupportSet κ = ⇑CKN.Foundation.Parabolic.parabolicHomeomorph ⁻¹' tsupport κ

theorem ESS.buCut_memLp_data (κ : CKN.Foundation.Parabolic.Vec3 × ℝ → ℝ) (hκsmooth : ContDiff ℝ (↑⊤) κ) (hκcompact : HasCompactSupport κ) (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) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict (buCutSupportSet κ))) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict (buCutSupportSet κ))) (hD2v : MeasureTheory.MemLp D2v 2 (MeasureTheory.volume.restrict (buCutSupportSet κ))) (hDtv : MeasureTheory.MemLp Dtv 2 (MeasureTheory.volume.restrict (buCutSupportSet κ))) : MeasureTheory.MemLp (buCutField κ v) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buCutDw κ v Dv) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buCutD2 κ v Dv D2v) 2 MeasureTheory.volume ∧ MeasureTheory.MemLp (buCutDt κ v Dtv) 2 MeasureTheory.volume

Smooth compact scalar factors preserve quadratic data in all specified weak derivative fields.