MeasureTheory.BoundedCompactSupport.prod_mul

@[fun_prop]theorem prod_mul (hf : BoundedCompactSupport f μ) (hg : BoundedCompactSupport g ν) :    BoundedCompactSupport (uncurry fun x y ↦ f x * g y) (μ.prod ν) where  memLp_top := by    -- todo: maybe separate out as lemmas    have h2f : MemLp (fun z : X × Y ↦ f z.1) ∞ (μ.prod ν) :=      hf.memLp_top.comp_quasiMeasurePreserving Measure.quasiMeasurePreserving_fst    have h2g : MemLp (fun z : X × Y ↦ g z.2) ∞ (μ.prod ν) :=      hg.memLp_top.comp_quasiMeasurePreserving Measure.quasiMeasurePreserving_snd    -- todo: reorder arguments of `mul`    exact h2g.mul (r := ∞) h2f  hasCompactSupport := by    -- todo: separate out as lemmas    apply HasCompactSupport.intro <| hf.hasCompactSupport.prod hg.hasCompactSupport    intro ⟨x, y⟩ hxy    simp only [uncurry_apply_pair, mul_eq_zero]    simp only [mem_prod, not_and] at hxy    by_cases hx : x ∈ tsupport f    · exact Or.inr (image_eq_zero_of_notMem_tsupport (hxy hx))    · exact Or.inl (image_eq_zero_of_notMem_tsupport hx)