feat: SigmaFinite instances for Measure.withDensity (#8271)

If a measure `μ` is sigma-finite, then `μ.withDensity f` is sigma-finite for any a.e.-measurable and a.e. finite function `f`.

Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean

@@ -2004,6 +2004,11 @@ theorem Measurable.ennreal_ofReal {f : α → ℝ} (hf : Measurable f) :
   ENNReal.continuous_ofReal.measurable.comp hf
 #align measurable.ennreal_of_real Measurable.ennreal_ofReal
 
+@[measurability]
+lemma AEMeasurable.ennreal_ofReal {f : α → ℝ} {μ : Measure α} (hf : AEMeasurable f μ) :
+    AEMeasurable (fun x ↦ ENNReal.ofReal (f x)) μ :=
+  ENNReal.continuous_ofReal.measurable.comp_aemeasurable hf
+
 @[simp, norm_cast]
 theorem measurable_coe_nnreal_real_iff {f : α → ℝ≥0} :
     Measurable (fun x => f x : α → ℝ) ↔ Measurable f :=
@@ -2237,6 +2242,39 @@ theorem AEMeasurable.coe_ereal_ennreal {f : α → ℝ≥0∞} {μ : Measure α}
   measurable_coe_ennreal_ereal.comp_aemeasurable hf
 #align ae_measurable.coe_ereal_ennreal AEMeasurable.coe_ereal_ennreal
 
+/-- If a function `f : α → ℝ≥0` is measurable and the measure is σ-finite, then there exists
+spanning measurable sets with finite measure on which `f` is bounded.
+See also `StronglyMeasurable.exists_spanning_measurableSet_norm_le` for functions into normed
+groups. -/
+theorem exists_spanning_measurableSet_le {m : MeasurableSpace α} {f : α → ℝ≥0}
+    (hf : Measurable f) (μ : Measure α) [SigmaFinite μ] :
+    ∃ s : ℕ → Set α,
+      (∀ n, MeasurableSet (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, f x ≤ n) ∧
+      ⋃ i, s i = Set.univ := by
+  let sigma_finite_sets := spanningSets μ
+  let norm_sets := fun n : ℕ => { x | f x ≤ n }
+  have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ := by
+    ext1 x
+    simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true_iff]
+    exact exists_nat_ge (f x)
+  let sets n := sigma_finite_sets n ∩ norm_sets n
+  have h_meas : ∀ n, MeasurableSet (sets n) := by
+    refine' fun n => MeasurableSet.inter _ _
+    · exact measurable_spanningSets μ n
+    · exact hf measurableSet_Iic
+  have h_finite : ∀ n, μ (sets n) < ∞ := by
+    refine' fun n => (measure_mono (Set.inter_subset_left _ _)).trans_lt _
+    exact measure_spanningSets_lt_top μ n
+  refine' ⟨sets, fun n => ⟨h_meas n, h_finite n, _⟩, _⟩
+  · exact fun x hx => hx.2
+  · have :
+      ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i := by
+      refine' Set.iUnion_inter_of_monotone (monotone_spanningSets μ) fun i j hij x => _
+      simp only [Set.mem_setOf_eq]
+      refine' fun hif => hif.trans _
+      exact_mod_cast hij
+    rw [this, norm_sets_spanning, iUnion_spanningSets μ, Set.inter_univ]
+
 section NormedAddCommGroup
 
 variable [NormedAddCommGroup α] [OpensMeasurableSpace α] [MeasurableSpace β]

Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean

@@ -971,29 +971,11 @@ theorem exists_spanning_measurableSet_norm_le [SeminormedAddCommGroup β] {m m0
     ∃ s : ℕ → Set α,
       (∀ n, MeasurableSet[m] (s n) ∧ μ (s n) < ∞ ∧ ∀ x ∈ s n, ‖f x‖ ≤ n) ∧
       ⋃ i, s i = Set.univ := by
-  let sigma_finite_sets := spanningSets (μ.trim hm)
-  let norm_sets := fun n : ℕ => { x | ‖f x‖ ≤ n }
-  have norm_sets_spanning : ⋃ n, norm_sets n = Set.univ := by
-    ext1 x
-    simp only [Set.mem_iUnion, Set.mem_setOf_eq, Set.mem_univ, iff_true_iff]
-    exact ⟨⌈‖f x‖⌉₊, Nat.le_ceil ‖f x‖⟩
-  let sets n := sigma_finite_sets n ∩ norm_sets n
-  have h_meas : ∀ n, MeasurableSet[m] (sets n) := by
-    refine' fun n => MeasurableSet.inter _ _
-    · exact measurable_spanningSets (μ.trim hm) n
-    · exact hf.norm.measurableSet_le stronglyMeasurable_const
-  have h_finite : ∀ n, μ (sets n) < ∞ := by
-    refine' fun n => (measure_mono (Set.inter_subset_left _ _)).trans_lt _
-    exact (le_trim hm).trans_lt (measure_spanningSets_lt_top (μ.trim hm) n)
-  refine' ⟨sets, fun n => ⟨h_meas n, h_finite n, _⟩, _⟩
-  · exact fun x hx => hx.2
-  · have :
-      ⋃ i, sigma_finite_sets i ∩ norm_sets i = (⋃ i, sigma_finite_sets i) ∩ ⋃ i, norm_sets i := by
-      refine' Set.iUnion_inter_of_monotone (monotone_spanningSets (μ.trim hm)) fun i j hij x => _
-      simp only [Set.mem_setOf_eq]
-      refine' fun hif => hif.trans _
-      exact_mod_cast hij
-    rw [this, norm_sets_spanning, iUnion_spanningSets (μ.trim hm), Set.inter_univ]
+  obtain ⟨s, hs, hs_univ⟩ := exists_spanning_measurableSet_le hf.nnnorm.measurable (μ.trim hm)
+  refine ⟨s, fun n ↦ ⟨(hs n).1, (le_trim hm).trans_lt (hs n).2.1, fun x hx ↦ ?_⟩, hs_univ⟩
+  have hx_nnnorm : ‖f x‖₊ ≤ n := (hs n).2.2 x hx
+  rw [← coe_nnnorm]
+  norm_cast
 #align measure_theory.strongly_measurable.exists_spanning_measurable_set_norm_le MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le
 
 end StronglyMeasurable

Mathlib/MeasureTheory/Measure/WithDensity.lean

@@ -474,6 +474,45 @@ theorem exists_absolutelyContinuous_isFiniteMeasure {m : MeasurableSpace α} (μ
   exact withDensity_absolutelyContinuous _ _
 #align measure_theory.exists_absolutely_continuous_is_finite_measure MeasureTheory.exists_absolutelyContinuous_isFiniteMeasure
 
+lemma SigmaFinite.withDensity [SigmaFinite μ] {f : α → ℝ≥0} (hf : AEMeasurable f μ) :
+    SigmaFinite (μ.withDensity (fun x ↦ f x)) := by
+  have h : (fun x ↦ (f x : ℝ≥0∞)) =ᵐ[μ] fun x ↦ ((hf.mk f x : ℝ≥0) : ℝ≥0∞) := by
+    filter_upwards [hf.ae_eq_mk] with x hx using by rw [hx]
+  rw [withDensity_congr_ae h]
+  obtain ⟨s, hs, h⟩ := exists_spanning_measurableSet_le
+    hf.measurable_mk μ
+  constructor
+  refine ⟨s, by simp, fun i ↦ ?_, h⟩
+  rw [withDensity_apply _ (hs i).1]
+  calc ∫⁻ a in s i, ((hf.mk f a : ℝ≥0) : ℝ≥0∞) ∂μ
+    ≤ ∫⁻ _ in s i, i ∂μ := by
+        refine set_lintegral_mono hf.measurable_mk.coe_nnreal_ennreal
+          measurable_const (fun x hxs ↦ ?_)
+        norm_cast
+        exact (hs i).2.2 x hxs
+  _ = i * μ (s i) := by rw [set_lintegral_const]
+  _ < ⊤ := ENNReal.mul_lt_top (by simp) (hs i).2.1.ne
+
+lemma SigmaFinite.withDensity_of_ne_top' [SigmaFinite μ] {f : α → ℝ≥0∞}
+    (hf : AEMeasurable f μ) (hf_ne_top : ∀ x, f x ≠ ∞) :
+    SigmaFinite (μ.withDensity f) := by
+  lift f to (α → ℝ≥0) using hf_ne_top
+  rw [aemeasurable_coe_nnreal_ennreal_iff] at hf
+  exact SigmaFinite.withDensity hf
+
+lemma SigmaFinite.withDensity_of_ne_top [SigmaFinite μ] {f : α → ℝ≥0∞}
+    (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
+    SigmaFinite (μ.withDensity f) := by
+  let f' := fun x ↦ if f x = ∞ then 0 else f x
+  have hff' : f =ᵐ[μ] f' := by filter_upwards [hf_ne_top] with x hx using by simp [hx]
+  have hf'_ne_top : ∀ x, f' x ≠ ∞ := fun x ↦ by by_cases hfx : f x = ∞ <;> simp [hfx]
+  rw [withDensity_congr_ae hff']
+  exact SigmaFinite.withDensity_of_ne_top' (hf.congr hff') hf'_ne_top
+
+lemma SigmaFinite.withDensity_ofReal [SigmaFinite μ] {f : α → ℝ} (hf : AEMeasurable f μ) :
+    SigmaFinite (μ.withDensity (fun x ↦ ENNReal.ofReal (f x))) := by
+  refine SigmaFinite.withDensity_of_ne_top hf.ennreal_ofReal (ae_of_all _ (by simp))
+
 variable [TopologicalSpace α] [OpensMeasurableSpace α] [IsLocallyFiniteMeasure μ]
 
 lemma IsLocallyFiniteMeasure.withDensity_coe {f : α → ℝ≥0} (hf : Continuous f) :