Compact Multiplier

Part of the Caffarelli–Kohn–Nirenberg partial regularity proof.

theorem CKN.integrableOn_mul_continuous_of_tsupport_subset {d : ℕ} {U : Set (Vec d)} (hU : IsOpen U) {f q : Vec d → ℝ} (hf : MeasureTheory.LocallyIntegrableOn f U MeasureTheory.volume) (hq : Continuous q) (hqCompact : HasCompactSupport q) (hqU : tsupport q ⊆ U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => f x * q x) U MeasureTheory.volume

If f is locally integrable on an open set U and q is continuous with compact support whose topological support is contained in U, then the product f * q is integrable on U.