feat: Fubini for functions with compact support and non-sigma-finite …

…measures (#8125)

Mathlib/MeasureTheory/Constructions/Prod/Integral.lean

@@ -24,6 +24,9 @@ In this file we prove Fubini's theorem.
   Tonelli's theorem (see `MeasureTheory.lintegral_prod`). The lemma
   `MeasureTheory.Integrable.integral_prod_right` states that the inner integral of the right-hand
   side is integrable.
+* `MeasureTheory.integral_integral_swap_of_hasCompactSupport`: a version of Fubini theorem for
+  continuous functions with compact support, which does not assume that the measures are σ-finite
+  contrary to all the usual versions of Fubini.
 
 ## Tags
 
@@ -540,4 +543,59 @@ theorem integral_fun_fst (f : α → E) : ∫ z, f z.1 ∂μ.prod ν = (ν univ)
   rw [← integral_prod_swap]
   apply integral_fun_snd
 
+section
+
+variable {X Y : Type*}
+    [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
+    [OpensMeasurableSpace X] [OpensMeasurableSpace Y]
+
+/-- A version of *Fubini theorem* for continuous functions with compact support: one may swap
+the order of integration with respect to locally finite measures. One does not assume that the
+measures are σ-finite, contrary to the usual Fubini theorem. -/
+lemma integral_integral_swap_of_hasCompactSupport
+    {f : X → Y → E} (hf : Continuous f.uncurry) (h'f : HasCompactSupport f.uncurry)
+    {μ : Measure X} {ν : Measure Y} [IsFiniteMeasureOnCompacts μ] [IsFiniteMeasureOnCompacts ν] :
+    ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
+  let U := Prod.fst '' (tsupport f.uncurry)
+  have : Fact (μ U < ∞) := ⟨(IsCompact.image h'f continuous_fst).measure_lt_top⟩
+  let V := Prod.snd '' (tsupport f.uncurry)
+  have : Fact (ν V < ∞) := ⟨(IsCompact.image h'f continuous_snd).measure_lt_top⟩
+  calc
+  ∫ x, (∫ y, f x y ∂ν) ∂μ = ∫ x, (∫ y in V, f x y ∂ν) ∂μ := by
+    congr 1 with x
+    apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)).symm
+    contrapose! hy
+    have : (x, y) ∈ Function.support f.uncurry := hy
+    exact mem_image_of_mem _ (subset_tsupport _ this)
+  _ = ∫ x in U, (∫ y in V, f x y ∂ν) ∂μ := by
+    apply (set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)).symm
+    have : ∀ y, f x y = 0 := by
+      intro y
+      contrapose! hx
+      have : (x, y) ∈ Function.support f.uncurry := hx
+      exact mem_image_of_mem _ (subset_tsupport _ this)
+    simp [this]
+  _ = ∫ y in V, (∫ x in U, f x y ∂μ) ∂ν := by
+    apply integral_integral_swap
+    apply (integrableOn_iff_integrable_of_support_subset (subset_tsupport f.uncurry)).mp
+    refine ⟨(h'f.stronglyMeasurable_of_prod hf).aestronglyMeasurable, ?_⟩
+    obtain ⟨C, hC⟩ : ∃ C, ∀ p, ‖f.uncurry p‖ ≤ C := hf.bounded_above_of_compact_support h'f
+    exact hasFiniteIntegral_of_bounded (C := C) (eventually_of_forall hC)
+  _ = ∫ y, (∫ x in U, f x y ∂μ) ∂ν := by
+    apply set_integral_eq_integral_of_forall_compl_eq_zero (fun y hy ↦ ?_)
+    have : ∀ x, f x y = 0 := by
+      intro x
+      contrapose! hy
+      have : (x, y) ∈ Function.support f.uncurry := hy
+      exact mem_image_of_mem _ (subset_tsupport _ this)
+    simp [this]
+  _ = ∫ y, (∫ x, f x y ∂μ) ∂ν := by
+    congr 1 with y
+    apply set_integral_eq_integral_of_forall_compl_eq_zero (fun x hx ↦ ?_)
+    contrapose! hx
+    have : (x, y) ∈ Function.support f.uncurry := hx
+    exact mem_image_of_mem _ (subset_tsupport _ this)
+
+end
+
 end MeasureTheory

Mathlib/MeasureTheory/Function/SimpleFuncDense.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Zhouhang Zhou, Yury Kudryashov, Heather Macbeth
 -/
 import Mathlib.MeasureTheory.Function.SimpleFunc
+import Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
 
 #align_import measure_theory.function.simple_func_dense from "leanprover-community/mathlib"@"7317149f12f55affbc900fc873d0d422485122b9"
 
@@ -190,3 +191,77 @@ theorem edist_approxOn_y0_le {f : β → α} (hf : Measurable f) {s : Set α} {y
 end SimpleFunc
 
 end MeasureTheory
+
+section CompactSupport
+
+variable {X Y α : Type*} [Zero α]
+    [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
+    [OpensMeasurableSpace X] [OpensMeasurableSpace Y]
+
+/-- A continuous function with compact support on a product space can be uniformly approximated by
+simple functions. The subtlety is that we do not assume that the spaces are separable, so the
+product of the Borel sigma algebras might not contain all open sets, but still it contains enough
+of them to approximate compactly supported continuous functions. -/
+lemma HasCompactSupport.exists_simpleFunc_approx_of_prod [PseudoMetricSpace α]
+    {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f)
+    {ε : ℝ} (hε : 0 < ε) :
+    ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < ε := by
+  have M : ∀ (K : Set (X × Y)), IsCompact K →
+      ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ K ⊆ s ∧
+      ∀ x ∈ s, dist (f x) (g x) < ε := by
+    intro K hK
+    apply IsCompact.induction_on
+      (p := fun t ↦ ∃ (g : SimpleFunc (X × Y) α), ∃ (s : Set (X × Y)), MeasurableSet s ∧ t ⊆ s ∧
+        ∀ x ∈ s, dist (f x) (g x) < ε) hK
+    · exact ⟨0, ∅, by simp⟩
+    · intro t t' htt' ⟨g, s, s_meas, ts, hg⟩
+      exact ⟨g, s, s_meas, htt'.trans ts, hg⟩
+    · intro t t' ⟨g, s, s_meas, ts, hg⟩ ⟨g', s', s'_meas, t's', hg'⟩
+      refine ⟨g.piecewise s s_meas g', s ∪ s', s_meas.union s'_meas,
+        union_subset_union ts t's', fun p hp ↦ ?_⟩
+      by_cases H : p ∈ s
+      · simpa [H, SimpleFunc.piecewise_apply] using hg p H
+      · simp only [SimpleFunc.piecewise_apply, H, ite_false]
+        apply hg'
+        simpa [H] using (mem_union _ _ _).1 hp
+    · rintro ⟨x, y⟩ -
+      obtain ⟨u, v, hu, xu, hv, yv, huv⟩ : ∃ u v, IsOpen u ∧ x ∈ u ∧ IsOpen v ∧ y ∈ v ∧
+        u ×ˢ v ⊆ {z | dist (f z) (f (x, y)) < ε} :=
+          mem_nhds_prod_iff'.1 <| Metric.continuousAt_iff'.1 hf.continuousAt ε hε
+      refine ⟨u ×ˢ v, nhdsWithin_le_nhds <| (hu.prod hv).mem_nhds (mk_mem_prod xu yv), ?_⟩
+      exact ⟨SimpleFunc.const _ (f (x, y)), u ×ˢ v, hu.measurableSet.prod hv.measurableSet,
+        Subset.rfl, fun z hz ↦ huv hz⟩
+  obtain ⟨g, s, s_meas, fs, hg⟩ : ∃ g s, MeasurableSet s ∧ tsupport f ⊆ s ∧
+    ∀ (x : X × Y), x ∈ s → dist (f x) (g x) < ε := M _ h'f
+  refine ⟨g.piecewise s s_meas 0, fun p ↦ ?_⟩
+  by_cases H : p ∈ s
+  · simpa [H, SimpleFunc.piecewise_apply] using hg p H
+  · have : f p = 0 := by
+      contrapose! H
+      rw [← Function.mem_support] at H
+      exact fs (subset_tsupport _ H)
+    simp [SimpleFunc.piecewise_apply, H, ite_false, this, hε]
+
+/-- A continuous function with compact support on a product space is measurable for the product
+sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
+product of the Borel sigma algebras might not contain all open sets, but still it contains enough
+of them to approximate compactly supported continuous functions. -/
+lemma HasCompactSupport.measurable_of_prod
+    [TopologicalSpace α] [PseudoMetrizableSpace α] [MeasurableSpace α] [BorelSpace α]
+    {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) :
+    Measurable f := by
+  letI : PseudoMetricSpace α := TopologicalSpace.pseudoMetrizableSpacePseudoMetric α
+  obtain ⟨u, -, u_pos, u_lim⟩ : ∃ u, StrictAnti u ∧ (∀ (n : ℕ), 0 < u n) ∧ Tendsto u atTop (𝓝 0) :=
+    exists_seq_strictAnti_tendsto (0 : ℝ)
+  have : ∀ n, ∃ (g : SimpleFunc (X × Y) α), ∀ x, dist (f x) (g x) < u n :=
+    fun n ↦ h'f.exists_simpleFunc_approx_of_prod hf (u_pos n)
+  choose g hg using this
+  have A : ∀ x, Tendsto (fun n ↦ g n x) atTop (𝓝 (f x)) := by
+    intro x
+    rw [tendsto_iff_dist_tendsto_zero]
+    apply squeeze_zero (fun n ↦ dist_nonneg) (fun n ↦ ?_) u_lim
+    rw [dist_comm]
+    exact (hg n x).le
+  apply measurable_of_tendsto_metrizable (fun n ↦ (g n).measurable) (tendsto_pi_nhds.2 A)
+
+end CompactSupport

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -5,7 +5,6 @@ Authors: Rémy Degenne, Sébastien Gouëzel
 -/
 import Mathlib.Analysis.NormedSpace.FiniteDimension
 import Mathlib.Analysis.NormedSpace.BoundedLinearMaps
-import Mathlib.MeasureTheory.Constructions.BorelSpace.Metrizable
 import Mathlib.MeasureTheory.Measure.WithDensity
 import Mathlib.MeasureTheory.Function.SimpleFuncDense
 
@@ -699,14 +698,38 @@ 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
+/-- A continuous function whose support is contained in a compact set is strongly measurable. -/
+@[to_additive]
+theorem _root_.Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact
     [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
-    [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [Zero β] {f : α → β}
-    (hf : Continuous f) (h'f : HasCompactSupport f) : StronglyMeasurable f := by
+    [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [One β] {f : α → β}
+    (hf : Continuous f) {k : Set α} (hk : IsCompact k)
+    (h'f : mulSupport f ⊆ k) : StronglyMeasurable f := by
   letI : PseudoMetricSpace β := pseudoMetrizableSpacePseudoMetric β
   rw [stronglyMeasurable_iff_measurable_separable]
-  exact ⟨hf.measurable, IsCompact.isSeparable (s := range f) (h'f.isCompact_range hf)⟩
+  exact ⟨hf.measurable, (isCompact_range_of_mulSupport_subset_isCompact hf hk h'f).isSeparable⟩
+
+/-- A continuous function with compact support is strongly measurable. -/
+@[to_additive]
+theorem _root_.Continuous.stronglyMeasurable_of_hasCompactMulSupport
+    [MeasurableSpace α] [TopologicalSpace α] [OpensMeasurableSpace α] [MeasurableSpace β]
+    [TopologicalSpace β] [PseudoMetrizableSpace β] [BorelSpace β] [One β] {f : α → β}
+    (hf : Continuous f) (h'f : HasCompactMulSupport f) : StronglyMeasurable f :=
+  hf.stronglyMeasurable_of_mulSupport_subset_isCompact h'f (subset_mulTSupport f)
+
+/-- A continuous function with compact support on a product space is strongly measurable for the
+product sigma-algebra. The subtlety is that we do not assume that the spaces are separable, so the
+product of the Borel sigma algebras might not contain all open sets, but still it contains enough
+of them to approximate compactly supported continuous functions. -/
+lemma _root_.HasCompactSupport.stronglyMeasurable_of_prod {X Y : Type*} [Zero α]
+    [TopologicalSpace X] [TopologicalSpace Y] [MeasurableSpace X] [MeasurableSpace Y]
+    [OpensMeasurableSpace X] [OpensMeasurableSpace Y] [TopologicalSpace α] [PseudoMetrizableSpace α]
+    {f : X × Y → α} (hf : Continuous f) (h'f : HasCompactSupport f) :
+    StronglyMeasurable f := by
+  borelize α
+  apply stronglyMeasurable_iff_measurable_separable.2 ⟨h'f.measurable_of_prod hf, ?_⟩
+  letI : PseudoMetricSpace α := pseudoMetrizableSpacePseudoMetric α
+  exact 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 β]