From 62567a59696e6a6f61f2779cfd45f9fb57f874fb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?R=C3=A9my=20Degenne?= Date: Wed, 8 Nov 2023 17:06:44 +0000 Subject: [PATCH] feat: SigmaFinite instances for Measure.withDensity (#8271) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit If a measure `μ` is sigma-finite, then `μ.withDensity f` is sigma-finite for any a.e.-measurable and a.e. finite function `f`. --- .../Constructions/BorelSpace/Basic.lean | 38 ++++++++++++++++++ .../Function/StronglyMeasurable/Basic.lean | 28 +++---------- .../MeasureTheory/Measure/WithDensity.lean | 39 +++++++++++++++++++ 3 files changed, 82 insertions(+), 23 deletions(-) diff --git a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean b/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean index d57db10f1d738e..cef61988ed7dce 100644 --- a/Mathlib/MeasureTheory/Constructions/BorelSpace/Basic.lean +++ b/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 β] diff --git a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean b/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean index 30d9a407e4af08..a1fe13eca72e38 100644 --- a/Mathlib/MeasureTheory/Function/StronglyMeasurable/Basic.lean +++ b/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 diff --git a/Mathlib/MeasureTheory/Measure/WithDensity.lean b/Mathlib/MeasureTheory/Measure/WithDensity.lean index fb140a8f2c598d..6e543d4d74a106 100644 --- a/Mathlib/MeasureTheory/Measure/WithDensity.lean +++ b/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) :