feat: Integrability of g • f for g continuous with compact support an…

…d f locally integrable (#6100)

Mathlib/MeasureTheory/Function/LocallyIntegrable.lean

@@ -302,6 +302,44 @@ protected theorem LocallyIntegrable.sub (hf : LocallyIntegrable f μ) (hg : Loca
 protected theorem LocallyIntegrable.neg (hf : LocallyIntegrable f μ) :
     LocallyIntegrable (-f) μ := fun x ↦ (hf x).neg
 
+/-- If `f` is locally integrable and `g` is continuous with compact support,
+then `g • f` is integrable. -/
+theorem LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
+    [NormedSpace ℝ E] [OpensMeasurableSpace X] [T2Space X]
+    (hf : LocallyIntegrable f μ) {g : X → ℝ} (hg : Continuous g) (h'g : HasCompactSupport g) :
+    Integrable (fun x ↦ g x • f x) μ := by
+  let K := tsupport g
+  have hK : IsCompact K := h'g
+  have : K.indicator (fun x ↦ g x • f x) = (fun x ↦ g x • f x) := by
+    apply indicator_eq_self.2
+    apply support_subset_iff'.2
+    intros x hx
+    simp [image_eq_zero_of_nmem_tsupport hx]
+  rw [← this, indicator_smul]
+  apply Integrable.smul_of_top_right
+  · rw [integrable_indicator_iff hK.measurableSet]
+    exact hf.integrableOn_isCompact hK
+  · exact hg.memℒp_top_of_hasCompactSupport h'g μ
+
+/-- If `f` is locally integrable and `g` is continuous with compact support,
+then `f • g` is integrable. -/
+theorem LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
+    [NormedSpace ℝ E] [OpensMeasurableSpace X] [T2Space X] {f : X → ℝ} (hf : LocallyIntegrable f μ)
+    {g : X → E} (hg : Continuous g) (h'g : HasCompactSupport g) :
+    Integrable (fun x ↦ f x • g x) μ := by
+  let K := tsupport g
+  have hK : IsCompact K := h'g
+  have : K.indicator (fun x ↦ f x • g x) = (fun x ↦ f x • g x) := by
+    apply indicator_eq_self.2
+    apply support_subset_iff'.2
+    intros x hx
+    simp [image_eq_zero_of_nmem_tsupport hx]
+  rw [← this, indicator_smul_left]
+  apply Integrable.smul_of_top_left
+  · rw [integrable_indicator_iff hK.measurableSet]
+    exact hf.integrableOn_isCompact hK
+  · exact hg.memℒp_top_of_hasCompactSupport h'g μ
+
 end MeasureTheory
 
 open MeasureTheory

Mathlib/MeasureTheory/Function/LpSeminorm.lean

@@ -1690,6 +1690,15 @@ theorem ae_bdd_liminf_atTop_of_snorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0) {f : 
 
 end Liminf
 
+/-- A continuous function with compact support belongs to `L^∞`. -/
+theorem _root_.Continuous.memℒp_top_of_hasCompactSupport
+    {X : Type _} [TopologicalSpace X] [MeasurableSpace X] [OpensMeasurableSpace X]
+    {f : X → E} (hf : Continuous f) (h'f : HasCompactSupport f) (μ : Measure X) : Memℒp f ⊤ μ := by
+  borelize E
+  rcases hf.bounded_above_of_compact_support h'f with ⟨C, hC⟩
+  apply memℒp_top_of_bound ?_ C (Filter.eventually_of_forall hC)
+  exact (hf.stronglyMeasurable_of_hasCompactSupport h'f).aestronglyMeasurable
+
 end ℒp
 
 end MeasureTheory

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -681,7 +681,7 @@ theorem _root_.stronglyMeasurable_iff_measurable_separable {m : MeasurableSpace
 /-- A continuous function is strongly measurable when either the source space or the target space
 is second-countable. -/
 theorem _root_.Continuous.stronglyMeasurable [MeasurableSpace α] [TopologicalSpace α]
-    [OpensMeasurableSpace α] {β : Type _} [TopologicalSpace β] [PseudoMetrizableSpace β]
+    [OpensMeasurableSpace α] [TopologicalSpace β] [PseudoMetrizableSpace β]
     [h : SecondCountableTopologyEither α β] {f : α → β} (hf : Continuous f) :
     StronglyMeasurable f := by
   borelize β
@@ -693,6 +693,15 @@ theorem _root_.Continuous.stronglyMeasurable [MeasurableSpace α] [TopologicalSp
   · exact hf.measurable.stronglyMeasurable
 #align continuous.strongly_measurable Continuous.stronglyMeasurable
 
+/-- A continuous function with compact support is strongly measurable. -/
+theorem _root_.Continuous.stronglyMeasurable_of_hasCompactSupport
+    [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
+    [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [Zero β] {f : α → β}
+    (hf : Continuous f) (h'f : HasCompactSupport f) : StronglyMeasurable f := by
+  letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
+  rw [stronglyMeasurable_iff_measurable_separable]
+  refine ⟨hf.measurable, IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)⟩
+
 /-- If `g` is a topological embedding, then `f` is strongly measurable iff `g ∘ f` is. -/
 theorem _root_.Embedding.comp_stronglyMeasurable_iff {m : MeasurableSpace α} [TopologicalSpace β]
     [PseudoMetrizableSpace β] [TopologicalSpace γ] [PseudoMetrizableSpace γ] {g : β → γ} {f : α → β}

Mathlib/Topology/Support.lean

@@ -156,6 +156,11 @@ theorem HasCompactMulSupport.intro [T2Space α] {K : Set α} (hK : IsCompact K)
 #align has_compact_mul_support.intro HasCompactMulSupport.intro
 #align has_compact_support.intro HasCompactSupport.intro
 
+@[to_additive]
+theorem HasCompactMulSupport.of_mulSupport_subset_isCompact [T2Space α] {K : Set α}
+    (hK : IsCompact K) (h : mulSupport f ⊆ K) : HasCompactMulSupport f :=
+  isCompact_closure_of_subset_compact hK h
+
 @[to_additive]
 theorem HasCompactMulSupport.isCompact (hf : HasCompactMulSupport f) : IsCompact (mulTSupport f) :=
   hf