chore(MeasureTheory): move Measure.comap to a new file (#19178)

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

Mathlib/MeasureTheory/Measure/Comap.lean

@@ -0,0 +1,159 @@
+/-
+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
+
+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
+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

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

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