From 663ccf8917da0f580d30861a1c459a0d7926789a Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 17 Nov 2024 18:54:35 -0600 Subject: [PATCH 1/3] chore(MeasureTheory): move `Measure.comap` to a new file --- Mathlib/MeasureTheory/Measure/Comap.lean | 151 ++++++++++++++++++ .../MeasureTheory/Measure/MeasureSpace.lean | 124 +------------- Mathlib/MeasureTheory/Measure/Restrict.lean | 2 +- 3 files changed, 153 insertions(+), 124 deletions(-) create mode 100644 Mathlib/MeasureTheory/Measure/Comap.lean diff --git a/Mathlib/MeasureTheory/Measure/Comap.lean b/Mathlib/MeasureTheory/Measure/Comap.lean new file mode 100644 index 0000000000000..998728733d016 --- /dev/null +++ b/Mathlib/MeasureTheory/Measure/Comap.lean @@ -0,0 +1,151 @@ +/- +Copyright (c) 2020 Yury Kudryashov. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Yury Kudryashov, Rémy Degenne +-/ +import Mathlib.MeasureTheory.Measure.MeasureSpace + +/-! +# Pullback of a measure +-/ + +open Function Set Filter +open scoped ENNReal + +noncomputable section + +namespace MeasureTheory + +namespace Measure + +variable {α β : Type*} {s : Set α} + +open Classical in +/-- Pullback of a `Measure` as a linear map. If `f` sends each measurable set to a measurable +set, then for each measurable set `s` we have `comapₗ f μ s = μ (f '' s)`. + +Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. + +If the linearity is not needed, please use `comap` instead, which works for a larger class of +functions. `comapₗ` is an auxiliary definition and most lemmas deal with comap. -/ +def comapₗ [MeasurableSpace α] [MeasurableSpace β] (f : α → β) : Measure β →ₗ[ℝ≥0∞] Measure α := + if hf : Injective f ∧ ∀ s, MeasurableSet s → MeasurableSet (f '' s) then + liftLinear (OuterMeasure.comap f) fun μ s hs t => by + simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1] + apply le_toOuterMeasure_caratheodory + exact hf.2 s hs + else 0 + +theorem comapₗ_apply {_ : MeasurableSpace α} {_ : MeasurableSpace β} (f : α → β) + (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) + (hs : MeasurableSet s) : comapₗ f μ s = μ (f '' s) := by + rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] + exact ⟨hfi, hf⟩ + +open Classical in +/-- Pullback of a `Measure`. If `f` sends each measurable set to a null-measurable set, +then for each measurable set `s` we have `comap f μ s = μ (f '' s)`. + +Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. -/ +def comap [MeasurableSpace α] [MeasurableSpace β] (f : α → β) (μ : Measure β) : Measure α := + if hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ then + (OuterMeasure.comap f μ.toOuterMeasure).toMeasure fun s hs t => by + simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1] + exact (measure_inter_add_diff₀ _ (hf.2 s hs)).symm + else 0 + +variable {ma : MeasurableSpace α} {mb : MeasurableSpace β} + +theorem comap_apply₀ (f : α → β) (μ : Measure β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) + (hs : NullMeasurableSet s (comap f μ)) : comap f μ s = μ (f '' s) := by + rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢ + rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] + +theorem le_comap_apply (f : α → β) (μ : Measure β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) (s : Set α) : + μ (f '' s) ≤ comap f μ s := by + rw [comap, dif_pos (And.intro hfi hf)] + exact le_toMeasure_apply _ _ _ + +theorem comap_apply (f : α → β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) (hs : MeasurableSet s) : + comap f μ s = μ (f '' s) := + comap_apply₀ f μ hfi (fun s hs => (hf s hs).nullMeasurableSet) hs.nullMeasurableSet + +theorem comapₗ_eq_comap (f : α → β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) (hs : MeasurableSet s) : + comapₗ f μ s = comap f μ s := + (comapₗ_apply f hfi hf μ hs).trans (comap_apply f hfi hf μ hs).symm + +theorem measure_image_eq_zero_of_comap_eq_zero (f : α → β) (μ : Measure β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) {s : Set α} (hs : comap f μ s = 0) : + μ (f '' s) = 0 := + le_antisymm ((le_comap_apply f μ hfi hf s).trans hs.le) (zero_le _) + +theorem ae_eq_image_of_ae_eq_comap (f : α → β) (μ : Measure β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) + {s t : Set α} (hst : s =ᵐ[comap f μ] t) : f '' s =ᵐ[μ] f '' t := by + rw [EventuallyEq, ae_iff] at hst ⊢ + have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by + ext1 x + simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff] + tauto + have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by + ext1 x + simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff] + tauto + rw [← Set.image_diff hfi, ← Set.image_diff hfi, ← Set.image_union] at h_eq_β + rw [h_eq_β] + rw [h_eq_α] at hst + exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst + +theorem NullMeasurableSet.image (f : α → β) (μ : Measure β) (hfi : Injective f) + (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) + (hs : NullMeasurableSet s (μ.comap f)) : NullMeasurableSet (f '' s) μ := by + refine ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, ?_⟩ + refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm + swap + · exact hf _ (measurableSet_toMeasurable _ _) + have h : toMeasurable (comap f μ) s =ᵐ[comap f μ] s := + NullMeasurableSet.toMeasurable_ae_eq hs + exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm + +theorem comap_preimage (f : α → β) (μ : Measure β) (hf : Injective f) (hf' : Measurable f) + (h : ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ) {s : Set β} (hs : MeasurableSet s) : + μ.comap f (f ⁻¹' s) = μ (s ∩ range f) := by + rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range] + +@[simp] lemma comap_zero (f : α → β) : (0 : Measure β).comap f = 0 := by + by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β) + · simp [comap, hf] + · simp [comap, hf] + +end Measure + +end MeasureTheory + +open MeasureTheory Measure + +variable {α β : Type*} {ma : MeasurableSpace α} {mb : MeasurableSpace β} + +lemma MeasurableEmbedding.comap_add {f : α → β} (hf : MeasurableEmbedding f) (μ ν : Measure β) : + (μ + ν).comap f = μ.comap f + ν.comap f := by + ext s hs + simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs, + _root_.map_add, add_apply] + +namespace MeasurableEquiv + +lemma comap_symm {μ : Measure α} (e : α ≃ᵐ β) : μ.comap e.symm = μ.map e := by + ext s hs + rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm] + exact fun t ht ↦ e.symm.measurableSet_image.mpr ht + +lemma map_symm {μ : Measure α} (e : β ≃ᵐ α) : μ.map e.symm = μ.comap e := by + rw [← comap_symm, symm_symm] + +end MeasurableEquiv + +lemma comap_swap (μ : Measure (α × β)) : μ.comap Prod.swap = μ.map Prod.swap := + (MeasurableEquiv.prodComm ..).comap_symm diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean index e80720475f839..754db225acc6d 100644 --- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean +++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean @@ -1244,107 +1244,6 @@ theorem preimage_null_of_map_null {f : α → β} (hf : AEMeasurable f μ) {s : theorem tendsto_ae_map {f : α → β} (hf : AEMeasurable f μ) : Tendsto f (ae μ) (ae (μ.map f)) := fun _ hs => preimage_null_of_map_null hf hs -open Classical in -/-- Pullback of a `Measure` as a linear map. If `f` sends each measurable set to a measurable -set, then for each measurable set `s` we have `comapₗ f μ s = μ (f '' s)`. - -Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. - -If the linearity is not needed, please use `comap` instead, which works for a larger class of -functions. `comapₗ` is an auxiliary definition and most lemmas deal with comap. -/ -def comapₗ [MeasurableSpace α] (f : α → β) : Measure β →ₗ[ℝ≥0∞] Measure α := - if hf : Injective f ∧ ∀ s, MeasurableSet s → MeasurableSet (f '' s) then - liftLinear (OuterMeasure.comap f) fun μ s hs t => by - simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1] - apply le_toOuterMeasure_caratheodory - exact hf.2 s hs - else 0 - -theorem comapₗ_apply {β} {_ : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) - (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) - (hs : MeasurableSet s) : comapₗ f μ s = μ (f '' s) := by - rw [comapₗ, dif_pos, liftLinear_apply _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] - exact ⟨hfi, hf⟩ - -open Classical in -/-- Pullback of a `Measure`. If `f` sends each measurable set to a null-measurable set, -then for each measurable set `s` we have `comap f μ s = μ (f '' s)`. - -Note that if `f` is not injective, this definition assigns `Set.univ` measure zero. -/ -def comap [MeasurableSpace α] (f : α → β) (μ : Measure β) : Measure α := - if hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ then - (OuterMeasure.comap f μ.toOuterMeasure).toMeasure fun s hs t => by - simp only [OuterMeasure.comap_apply, image_inter hf.1, image_diff hf.1] - exact (measure_inter_add_diff₀ _ (hf.2 s hs)).symm - else 0 - -theorem comap_apply₀ {_ : MeasurableSpace α} (f : α → β) (μ : Measure β) (hfi : Injective f) - (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) - (hs : NullMeasurableSet s (comap f μ)) : comap f μ s = μ (f '' s) := by - rw [comap, dif_pos (And.intro hfi hf)] at hs ⊢ - rw [toMeasure_apply₀ _ _ hs, OuterMeasure.comap_apply, coe_toOuterMeasure] - -theorem le_comap_apply {β} {_ : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) - (μ : Measure β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) - (s : Set α) : μ (f '' s) ≤ comap f μ s := by - rw [comap, dif_pos (And.intro hfi hf)] - exact le_toMeasure_apply _ _ _ - -theorem comap_apply {β} {_ : MeasurableSpace α} {_mβ : MeasurableSpace β} (f : α → β) - (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) - (hs : MeasurableSet s) : comap f μ s = μ (f '' s) := - comap_apply₀ f μ hfi (fun s hs => (hf s hs).nullMeasurableSet) hs.nullMeasurableSet - -theorem comapₗ_eq_comap {β} {_ : MeasurableSpace α} {_mβ : MeasurableSpace β} (f : α → β) - (hfi : Injective f) (hf : ∀ s, MeasurableSet s → MeasurableSet (f '' s)) (μ : Measure β) - (hs : MeasurableSet s) : comapₗ f μ s = comap f μ s := - (comapₗ_apply f hfi hf μ hs).trans (comap_apply f hfi hf μ hs).symm - -theorem measure_image_eq_zero_of_comap_eq_zero {β} {_ : MeasurableSpace α} {_mβ : MeasurableSpace β} - (f : α → β) (μ : Measure β) (hfi : Injective f) - (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) {s : Set α} (hs : comap f μ s = 0) : - μ (f '' s) = 0 := - le_antisymm ((le_comap_apply f μ hfi hf s).trans hs.le) (zero_le _) - -theorem ae_eq_image_of_ae_eq_comap {β} {_ : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) - (μ : Measure β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) - {s t : Set α} (hst : s =ᵐ[comap f μ] t) : f '' s =ᵐ[μ] f '' t := by - rw [EventuallyEq, ae_iff] at hst ⊢ - have h_eq_α : { a : α | ¬s a = t a } = s \ t ∪ t \ s := by - ext1 x - simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff] - tauto - have h_eq_β : { a : β | ¬(f '' s) a = (f '' t) a } = f '' s \ f '' t ∪ f '' t \ f '' s := by - ext1 x - simp only [eq_iff_iff, mem_setOf_eq, mem_union, mem_diff] - tauto - rw [← Set.image_diff hfi, ← Set.image_diff hfi, ← Set.image_union] at h_eq_β - rw [h_eq_β] - rw [h_eq_α] at hst - exact measure_image_eq_zero_of_comap_eq_zero f μ hfi hf hst - -theorem NullMeasurableSet.image {β} {_ : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) - (μ : Measure β) (hfi : Injective f) (hf : ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) μ) - {s : Set α} (hs : NullMeasurableSet s (μ.comap f)) : NullMeasurableSet (f '' s) μ := by - refine ⟨toMeasurable μ (f '' toMeasurable (μ.comap f) s), measurableSet_toMeasurable _ _, ?_⟩ - refine EventuallyEq.trans ?_ (NullMeasurableSet.toMeasurable_ae_eq ?_).symm - swap - · exact hf _ (measurableSet_toMeasurable _ _) - have h : toMeasurable (comap f μ) s =ᵐ[comap f μ] s := - NullMeasurableSet.toMeasurable_ae_eq hs - exact ae_eq_image_of_ae_eq_comap f μ hfi hf h.symm - -theorem comap_preimage {β} {_ : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) - (μ : Measure β) {s : Set β} (hf : Injective f) (hf' : Measurable f) - (h : ∀ t, MeasurableSet t → NullMeasurableSet (f '' t) μ) (hs : MeasurableSet s) : - μ.comap f (f ⁻¹' s) = μ (s ∩ range f) := by - rw [comap_apply₀ _ _ hf h (hf' hs).nullMeasurableSet, image_preimage_eq_inter_range] - -@[simp] lemma comap_zero : (0 : Measure β).comap f = 0 := by - by_cases hf : Injective f ∧ ∀ s, MeasurableSet s → NullMeasurableSet (f '' s) (0 : Measure β) - · simp [comap, hf] - · simp [comap, hf] - section Sum variable {f : ι → Measure α} @@ -1953,12 +1852,6 @@ nonrec theorem map_apply (hf : MeasurableEmbedding f) (μ : Measure α) (s : Set μ.map f s ≤ μ.map f t := by gcongr _ = μ (f ⁻¹' s) := by rw [map_apply hf.measurable htm, hft, measure_toMeasurable] -lemma comap_add (hf : MeasurableEmbedding f) (μ ν : Measure β) : - (μ + ν).comap f = μ.comap f + ν.comap f := by - ext s hs - simp only [← comapₗ_eq_comap _ hf.injective (fun _ ↦ hf.measurableSet_image.mpr) _ hs, - _root_.map_add, add_apply] - lemma absolutelyContinuous_map (hf : MeasurableEmbedding f) (hμν : μ ≪ ν) : μ.map f ≪ ν.map f := by intro t ht @@ -1980,14 +1873,6 @@ variable {_ : MeasurableSpace α} [MeasurableSpace β] {μ : Measure α} {ν : M protected theorem map_apply (f : α ≃ᵐ β) (s : Set β) : μ.map f s = μ (f ⁻¹' s) := f.measurableEmbedding.map_apply _ _ -lemma comap_symm (e : α ≃ᵐ β) : μ.comap e.symm = μ.map e := by - ext s hs - rw [e.map_apply, Measure.comap_apply _ e.symm.injective _ _ hs, image_symm] - exact fun t ht ↦ e.symm.measurableSet_image.mpr ht - -lemma map_symm (e : β ≃ᵐ α) : μ.map e.symm = μ.comap e := by - rw [← comap_symm, symm_symm] - @[simp] theorem map_symm_map (e : α ≃ᵐ β) : (μ.map e).map e.symm = μ := by simp [map_map e.symm.measurable e.measurable] @@ -2014,13 +1899,6 @@ theorem quasiMeasurePreserving_symm (μ : Measure α) (e : α ≃ᵐ β) : end MeasurableEquiv -namespace MeasureTheory.Measure -variable {mα : MeasurableSpace α} {mβ : MeasurableSpace β} - -lemma comap_swap (μ : Measure (α × β)) : μ.comap Prod.swap = μ.map Prod.swap := - (MeasurableEquiv.prodComm ..).comap_symm - -end MeasureTheory.Measure end -set_option linter.style.longFile 2200 +set_option linter.style.longFile 2100 diff --git a/Mathlib/MeasureTheory/Measure/Restrict.lean b/Mathlib/MeasureTheory/Measure/Restrict.lean index f9ddf8fd820c1..b3823303c8980 100644 --- a/Mathlib/MeasureTheory/Measure/Restrict.lean +++ b/Mathlib/MeasureTheory/Measure/Restrict.lean @@ -3,7 +3,7 @@ Copyright (c) 2017 Johannes Hölzl. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Johannes Hölzl, Mario Carneiro -/ -import Mathlib.MeasureTheory.Measure.MeasureSpace +import Mathlib.MeasureTheory.Measure.Comap /-! # Restricting a measure to a subset or a subtype From 2fdc6d7b2c54d648c46db4628821968cb9fe56a8 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 17 Nov 2024 19:02:43 -0600 Subject: [PATCH 2/3] Update --- Mathlib.lean | 1 + 1 file changed, 1 insertion(+) diff --git a/Mathlib.lean b/Mathlib.lean index 3b1c7dbea4b29..436046abaaf0f 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -3600,6 +3600,7 @@ import Mathlib.MeasureTheory.MeasurableSpace.Prod import Mathlib.MeasureTheory.Measure.AEDisjoint import Mathlib.MeasureTheory.Measure.AEMeasurable import Mathlib.MeasureTheory.Measure.AddContent +import Mathlib.MeasureTheory.Measure.Comap import Mathlib.MeasureTheory.Measure.Complex import Mathlib.MeasureTheory.Measure.Content import Mathlib.MeasureTheory.Measure.ContinuousPreimage From 5d06c5680779fca08740fe653415648858b01f64 Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sun, 17 Nov 2024 19:56:26 -0600 Subject: [PATCH 3/3] Docs --- Mathlib/MeasureTheory/Measure/Comap.lean | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/Mathlib/MeasureTheory/Measure/Comap.lean b/Mathlib/MeasureTheory/Measure/Comap.lean index 998728733d016..adefd18c588f4 100644 --- a/Mathlib/MeasureTheory/Measure/Comap.lean +++ b/Mathlib/MeasureTheory/Measure/Comap.lean @@ -7,6 +7,14 @@ import Mathlib.MeasureTheory.Measure.MeasureSpace /-! # Pullback of a measure + +In this file we define the pullback `MeasureTheory.Measure.comap f μ` +of a measure `μ` along an injective map `f` +such that the image of any measurable set under `f` is a null-measurable set. +If `f` does not have these properties, then we define `comap f μ` to be zero. + +In the future, we may decide to redefine `comap f μ` so that it gives meaningful results, e.g., +for covering maps like `(↑) : ℝ → AddCircle (1 : ℝ)`. -/ open Function Set Filter