Continuous weights on compact short-time supports

A continuous scalar weight preserves integrability of data restricted to the compact support of the short-time cutoff.

theorem ESS.bu_integrableOn_mul_continuous_compact {K : Set CKN.Foundation.Parabolic.ParabolicPoint} (hK : IsCompact K) (f g : CKN.Foundation.Parabolic.ParabolicPoint → ℝ) (hf : MeasureTheory.IntegrableOn f K MeasureTheory.volume) (hg : ContinuousOn g K) : MeasureTheory.IntegrableOn (fun (z : CKN.Foundation.Parabolic.ParabolicPoint) => g z * f z) K MeasureTheory.volume

Multiplication by a continuous real weight preserves integrability on a compact measurable set.