[Merged by Bors] - feat(MeasurePreserving): use NullMeasurableSet

Mathlib/Dynamics/Ergodic/Conservative.lean

@@ -61,7 +61,7 @@ structure Conservative (f : α → α) (μ : Measure α) extends QuasiMeasurePre
 /-- A self-map preserving a finite measure is conservative. -/
 protected theorem MeasurePreserving.conservative [IsFiniteMeasure μ] (h : MeasurePreserving f μ μ) :
     Conservative f μ :=
-  ⟨h.quasiMeasurePreserving, fun _ hsm h0 => h.exists_mem_iterate_mem hsm h0⟩
+  ⟨h.quasiMeasurePreserving, fun _ hsm h0 => h.exists_mem_iterate_mem hsm.nullMeasurableSet h0⟩
 
 namespace Conservative
 

Mathlib/Dynamics/Ergodic/Ergodic.lean

@@ -84,8 +84,9 @@ theorem preErgodic_of_preErgodic_conjugate (hg : MeasurePreserving g μ μ') (hf
     intro s hs₀ hs₁
     replace hs₁ : f ⁻¹' (g ⁻¹' s) = g ⁻¹' s := by rw [← preimage_comp, h_comm, preimage_comp, hs₁]
     cases' hf.ae_empty_or_univ (hg.measurable hs₀) hs₁ with hs₂ hs₂ <;> [left; right]
-    · simpa only [ae_eq_empty, hg.measure_preimage hs₀] using hs₂
-    · simpa only [ae_eq_univ, ← preimage_compl, hg.measure_preimage hs₀.compl] using hs₂⟩
+    · simpa only [ae_eq_empty, hg.measure_preimage hs₀.nullMeasurableSet] using hs₂
+    · simpa only [ae_eq_univ, ← preimage_compl,
+        hg.measure_preimage hs₀.compl.nullMeasurableSet] using hs₂⟩
 
 theorem preErgodic_conjugate_iff {e : α ≃ᵐ β} (h : MeasurePreserving e μ μ') :
     PreErgodic (e ∘ f ∘ e.symm) μ' ↔ PreErgodic f μ := by
@@ -142,15 +143,17 @@ theorem quasiErgodic (hf : Ergodic f μ) : QuasiErgodic f μ :=
 theorem ae_empty_or_univ_of_preimage_ae_le' (hf : Ergodic f μ) (hs : MeasurableSet s)
     (hs' : f ⁻¹' s ≤ᵐ[μ] s) (h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ := by
   refine hf.quasiErgodic.ae_empty_or_univ' hs ?_
-  refine ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).symm.le ?_ h_fin
+  refine ae_eq_of_ae_subset_of_measure_ge hs'
+    (hf.measure_preimage hs.nullMeasurableSet).symm.le ?_ h_fin
   exact measurableSet_preimage hf.measurable hs
 
 /-- See also `Ergodic.ae_empty_or_univ_of_ae_le_preimage`. -/
 theorem ae_empty_or_univ_of_ae_le_preimage' (hf : Ergodic f μ) (hs : MeasurableSet s)
     (hs' : s ≤ᵐ[μ] f ⁻¹' s) (h_fin : μ s ≠ ∞) : s =ᵐ[μ] (∅ : Set α) ∨ s =ᵐ[μ] univ := by
-  replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs]
+  replace h_fin : μ (f ⁻¹' s) ≠ ∞ := by rwa [hf.measure_preimage hs.nullMeasurableSet]
   refine hf.quasiErgodic.ae_empty_or_univ' hs ?_
-  exact (ae_eq_of_ae_subset_of_measure_ge hs' (hf.measure_preimage hs).le hs h_fin).symm
+  exact (ae_eq_of_ae_subset_of_measure_ge hs'
+    (hf.measure_preimage hs.nullMeasurableSet).le hs h_fin).symm
 
 /-- See also `Ergodic.ae_empty_or_univ_of_image_ae_le`. -/
 theorem ae_empty_or_univ_of_image_ae_le' (hf : Ergodic f μ) (hs : MeasurableSet s)

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -114,7 +114,9 @@ protected theorem sigmaFinite {f : α → β} (hf : MeasurePreserving f μa μb)
   SigmaFinite.of_map μa hf.aemeasurable (by rwa [hf.map_eq])
 
 theorem measure_preimage {f : α → β} (hf : MeasurePreserving f μa μb) {s : Set β}
-    (hs : MeasurableSet s) : μa (f ⁻¹' s) = μb s := by rw [← hf.map_eq, map_apply hf.1 hs]
+    (hs : NullMeasurableSet s μb) : μa (f ⁻¹' s) = μb s := by
+  rw [← hf.map_eq] at hs ⊢
+  rw [map_apply₀ hf.1.aemeasurable hs]
 
 theorem measure_preimage_emb {f : α → β} (hf : MeasurePreserving f μa μb)
     (hfe : MeasurableEmbedding f) (s : Set β) : μa (f ⁻¹' s) = μb s := by
@@ -133,26 +135,27 @@ variable {μ : Measure α} {f : α → α} {s : Set α}
 
 open scoped symmDiff in
 lemma measure_symmDiff_preimage_iterate_le
-    (hf : MeasurePreserving f μ μ) (hs : MeasurableSet s) (n : ℕ) :
+    (hf : MeasurePreserving f μ μ) (hs : NullMeasurableSet s μ) (n : ℕ) :
     μ (s ∆ (f^[n] ⁻¹' s)) ≤ n • μ (s ∆ (f ⁻¹' s)) := by
   induction' n with n ih; · simp
   simp only [add_smul, one_smul, ← n.add_one]
   refine le_trans (measure_symmDiff_le s (f^[n] ⁻¹' s) (f^[n+1] ⁻¹' s)) (add_le_add ih ?_)
-  replace hs : MeasurableSet (s ∆ (f ⁻¹' s)) := hs.symmDiff <| hf.measurable hs
+  replace hs : NullMeasurableSet (s ∆ (f ⁻¹' s)) μ :=
+    hs.symmDiff <| hs.preimage hf.quasiMeasurePreserving
   rw [iterate_succ', preimage_comp, ← preimage_symmDiff, (hf.iterate n).measure_preimage hs]
 
 /-- If `μ univ < n * μ s` and `f` is a map preserving measure `μ`,
 then for some `x ∈ s` and `0 < m < n`, `f^[m] x ∈ s`. -/
 theorem exists_mem_iterate_mem_of_volume_lt_mul_volume (hf : MeasurePreserving f μ μ)
-    (hs : MeasurableSet s) {n : ℕ} (hvol : μ (Set.univ : Set α) < n * μ s) :
+    (hs : NullMeasurableSet s μ) {n : ℕ} (hvol : μ (Set.univ : Set α) < n * μ s) :
     ∃ x ∈ s, ∃ m ∈ Set.Ioo 0 n, f^[m] x ∈ s := by
-  have A : ∀ m, MeasurableSet (f^[m] ⁻¹' s) := fun m ↦ (hf.iterate m).measurable hs
+  have A : ∀ m, NullMeasurableSet (f^[m] ⁻¹' s) μ := fun m ↦
+    hs.preimage (hf.iterate m).quasiMeasurePreserving
   have B : ∀ m, μ (f^[m] ⁻¹' s) = μ s := fun m ↦ (hf.iterate m).measure_preimage hs
   have : μ (univ : Set α) < ∑ m ∈ Finset.range n, μ (f^[m] ⁻¹' s) := by simpa [B]
   obtain ⟨i, hi, j, hj, hij, x, hxi : f^[i] x ∈ s, hxj : f^[j] x ∈ s⟩ :
       ∃ i < n, ∃ j < n, i ≠ j ∧ (f^[i] ⁻¹' s ∩ f^[j] ⁻¹' s).Nonempty := by
-    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ
-      (fun m _ ↦ (A m).nullMeasurableSet) this
+    simpa using exists_nonempty_inter_of_measure_univ_lt_sum_measure μ (fun m _ ↦ A m) this
   wlog hlt : i < j generalizing i j
   · exact this j hj i hi hij.symm hxj hxi (hij.lt_or_lt.resolve_left hlt)
   refine ⟨f^[i] x, hxi, j - i, ⟨tsub_pos_of_lt hlt, lt_of_le_of_lt (j.sub_le i) hj⟩, ?_⟩
@@ -163,7 +166,7 @@ theorem exists_mem_iterate_mem_of_volume_lt_mul_volume (hf : MeasurePreserving f
 infinitely many times, see `MeasureTheory.MeasurePreserving.conservative` and theorems about
 `MeasureTheory.Conservative`. -/
 theorem exists_mem_iterate_mem [IsFiniteMeasure μ] (hf : MeasurePreserving f μ μ)
-    (hs : MeasurableSet s) (hs' : μ s ≠ 0) : ∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s := by
+    (hs : NullMeasurableSet s μ) (hs' : μ s ≠ 0) : ∃ x ∈ s, ∃ m ≠ 0, f^[m] x ∈ s := by
   rcases ENNReal.exists_nat_mul_gt hs' (measure_ne_top μ (Set.univ : Set α)) with ⟨N, hN⟩
   rcases hf.exists_mem_iterate_mem_of_volume_lt_mul_volume hs hN with ⟨x, hx, m, hm, hmx⟩
   exact ⟨x, hx, m, hm.1.ne', hmx⟩

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -891,7 +891,7 @@ theorem measurePreserving_pi {β : ι → Type*} [∀ i, MeasurableSpace (β i)]
     haveI : ∀ i, SigmaFinite (μ i) := fun i ↦ (hf i).sigmaFinite
     refine (Measure.pi_eq fun s hs ↦ ?_).symm
     rw [Measure.map_apply, Set.preimage_pi, Measure.pi_pi]
-    · simp_rw [← MeasurePreserving.measure_preimage (hf _) (hs _)]
+    · simp_rw [← MeasurePreserving.measure_preimage (hf _) (hs _).nullMeasurableSet]
     · exact measurable_pi_iff.mpr <| fun i ↦ (hf i).measurable.comp (measurable_pi_apply i)
     · exact MeasurableSet.univ_pi hs
 

Mathlib/MeasureTheory/Function/LpSpace.lean

@@ -960,7 +960,8 @@ theorem toLp_compMeasurePreserving {g : β → E} (hg : Memℒp g p μb) (hf : M
 theorem indicatorConstLp_compMeasurePreserving {s : Set β} (hs : MeasurableSet s)
     (hμs : μb s ≠ ∞) (c : E) (hf : MeasurePreserving f μ μb) :
     Lp.compMeasurePreserving f hf (indicatorConstLp p hs hμs c) =
-      indicatorConstLp p (hs.preimage hf.measurable) (by rwa [hf.measure_preimage hs]) c :=
+      indicatorConstLp p (hs.preimage hf.measurable)
+        (by rwa [hf.measure_preimage hs.nullMeasurableSet]) c :=
   rfl
 
 variable (𝕜 : Type*) [NormedRing 𝕜] [Module 𝕜 E] [BoundedSMul 𝕜 E]

Mathlib/MeasureTheory/Function/LpSpace/ContinuousCompMeasurePreserving.lean

@@ -70,12 +70,13 @@ theorem tendsto_measure_symmDiff_preimage_nhds_zero
         apply measure_symmDiff_le
       _ ≤ ε / 3 + ε / 3 + ε / 3 := by
         gcongr
-        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU), symmDiff_comm]
-        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs)]
+        · rwa [← preimage_symmDiff, hfa.measure_preimage (hs.symmDiff hmU).nullMeasurableSet,
+            symmDiff_comm]
+        · rwa [← preimage_symmDiff, hg.measure_preimage (hmU.symmDiff hs).nullMeasurableSet]
       _ = ε := by simp
   -- Take a compact closed subset `K ⊆ g ⁻¹' s` of almost full measure,
   -- `μ (g ⁻¹' s \ K) < ε / 2`.
-  have hνs' : μ (g ⁻¹' s) ≠ ∞ := by rwa [hg.measure_preimage hs]
+  have hνs' : μ (g ⁻¹' s) ≠ ∞ := by rwa [hg.measure_preimage hs.nullMeasurableSet]
   obtain ⟨K, hKg, hKco, hKcl, hKμ⟩ :
       ∃ K, MapsTo g K s ∧ IsCompact K ∧ IsClosed K ∧ μ (g ⁻¹' s \ K) < ε / 2 :=
     (hs.preimage hg.measurable).exists_isCompact_isClosed_diff_lt hνs' <| by simp [hε.ne']
@@ -90,8 +91,9 @@ theorem tendsto_measure_symmDiff_preimage_nhds_zero
   rw [symmDiff_of_ge ha.subset_preimage, symmDiff_of_le hKg.subset_preimage]
   gcongr
   have hK' : μ K ≠ ∞ := ne_top_of_le_ne_top hνs' <| measure_mono hKg.subset_preimage
-  rw [measure_diff_le_iff_le_add hKm ha.subset_preimage hK', hfa.measure_preimage hs,
-    ← hg.measure_preimage hs, ← measure_diff_le_iff_le_add hKm hKg.subset_preimage hK']
+  rw [measure_diff_le_iff_le_add hKm ha.subset_preimage hK',
+    hfa.measure_preimage hs.nullMeasurableSet, ← hg.measure_preimage hs.nullMeasurableSet,
+    ← measure_diff_le_iff_le_add hKm hKg.subset_preimage hK']
   exact hKμ.le
 
 namespace Lp

Mathlib/MeasureTheory/Measure/Lebesgue/VolumeOfBalls.lean

@@ -328,7 +328,7 @@ theorem EuclideanSpace.volume_ball (x : EuclideanSpace ℝ ι) (r : ℝ) :
         .ofReal (Real.sqrt π ^ card ι / Gamma (card ι / 2 + 1)) by
       rw [Measure.addHaar_ball _ _ hr, this, ofReal_pow hr, finrank_euclideanSpace]
     rw [← ((EuclideanSpace.volume_preserving_measurableEquiv _).symm).measure_preimage
-      measurableSet_ball]
+      measurableSet_ball.nullMeasurableSet]
     convert (volume_sum_rpow_lt_one ι one_le_two) using 4
     · simp_rw [EuclideanSpace.ball_zero_eq _ zero_le_one, one_pow, Real.rpow_two, sq_abs,
         Set.setOf_app_iff]
@@ -358,7 +358,7 @@ theorem InnerProductSpace.volume_ball (x : E) (r : ℝ) :
     volume (Metric.ball x r) = (.ofReal r) ^ finrank ℝ E *
       .ofReal (sqrt π ^ finrank ℝ E / Gamma (finrank ℝ E / 2 + 1)) := by
   rw [← ((stdOrthonormalBasis ℝ E).measurePreserving_repr_symm).measure_preimage
-      measurableSet_ball]
+      measurableSet_ball.nullMeasurableSet]
   have : Nonempty (Fin (finrank ℝ E)) := Fin.pos_iff_nonempty.mp finrank_pos
   have := EuclideanSpace.volume_ball (Fin (finrank ℝ E)) ((stdOrthonormalBasis ℝ E).repr x) r
   simp_rw [Fintype.card_fin] at this

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean

@@ -445,7 +445,7 @@ theorem volume_fundamentalDomain_stdBasis :
   rw [fundamentalDomain_stdBasis, volume_eq_prod, prod_prod, volume_pi, volume_pi, pi_pi, pi_pi,
     Complex.volume_preserving_equiv_pi.measure_preimage ?_, volume_pi, pi_pi, Real.volume_Ico,
     sub_zero, ENNReal.ofReal_one, prod_const_one, prod_const_one, prod_const_one, one_mul]
-  exact MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)
+  exact (MeasurableSet.pi Set.countable_univ (fun _ _ => measurableSet_Ico)).nullMeasurableSet
 
 /-- The `Equiv` between `index K` and `K →+* ℂ` defined by sending a real infinite place `w` to
 the unique corresponding embedding `w.embedding`, and the pair `⟨w, 0⟩` (resp. `⟨w, 1⟩`) for a

Mathlib/NumberTheory/NumberField/CanonicalEmbedding/ConvexBody.lean

@@ -228,7 +228,7 @@ theorem convexBodyLT'_volume :
       simp_rw [volume_eq_prod, prod_prod, Real.volume_Ioo, sub_neg_eq_add, one_add_one_eq_two,
         ← two_mul, ofReal_mul zero_le_two, ofReal_pow (coe_nonneg B), ofReal_ofNat,
         ofReal_coe_nnreal, ← mul_assoc, show (2 : ℝ≥0∞) * 2 = 4 by norm_num]
-    · refine MeasurableSet.inter ?_ ?_
+    · refine (MeasurableSet.inter ?_ ?_).nullMeasurableSet
       · exact measurableSet_lt (measurable_norm.comp Complex.measurable_re) measurable_const
       · exact measurableSet_lt (measurable_norm.comp Complex.measurable_im) measurable_const
   calc