Quadratic integrability of cutoff errors

For fixed cutoff parameters the error in the weak heat equation is quadratically integrable on the compact support of the scalar cutoff.

theorem ESS.bu_short_cutoff_error_sq_integrable (scale R ε c₁ : ℝ) (hR : 0 < R) (K : Set CKN.Foundation.Parabolic.ParabolicPoint) (hK : IsCompact K) (v : CKN.Foundation.Parabolic.ParabolicPoint → CKN.Foundation.Parabolic.Vec3) (Dv : CKN.Foundation.Parabolic.ParabolicPoint → Fin 3 → CKN.Foundation.Parabolic.Vec3) (hv : MeasureTheory.MemLp v 2 (MeasureTheory.volume.restrict K)) (hDv : MeasureTheory.MemLp Dv 2 (MeasureTheory.volume.restrict K)) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => buShortCutoffHeatErrorSize scale R hR ε c₁ v Dv z ^ 2) K MeasureTheory.volume

The squared heat error of a fixed smooth cutoff is integrable on any compact set carrying L² field and weak-gradient data.