chore: deprecate Measure.Dirac

Archive/Wiedijk100Theorems/BuffonsNeedle.lean

@@ -198,7 +198,7 @@ lemma buffon_integral :
   rw [
     ← MeasureTheory.integral_map hBₘ.aemeasurable
       (stronglyMeasurable_needleCrossesIndicator l).aestronglyMeasurable,
-    hB, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, volume_needleSpace d hd,
+    hB.map_eq, ProbabilityTheory.cond, MeasureTheory.integral_smul_measure, volume_needleSpace d hd,
     ← ENNReal.ofReal_inv_of_pos (mul_pos hd Real.pi_pos),
     ENNReal.toReal_ofReal (inv_nonneg.mpr (mul_nonneg hd.le Real.pi_pos.le)), smul_eq_mul,
   ]

Mathlib.lean

@@ -5622,6 +5622,8 @@ public import Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
 public import Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
 public import Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
 public import Mathlib.MeasureTheory.Measure.Dirac
+public import Mathlib.MeasureTheory.Measure.Dirac.Basic
+public import Mathlib.MeasureTheory.Measure.Dirac.Def
 public import Mathlib.MeasureTheory.Measure.DiracProba
 public import Mathlib.MeasureTheory.Measure.Doubling
 public import Mathlib.MeasureTheory.Measure.EverywherePos

Mathlib/Analysis/Convolution.lean

@@ -174,7 +174,7 @@ section Group
 
 variable [AddGroup G]
 
-theorem AEStronglyMeasurable.convolution_integrand' [MeasurableAdd₂ G]
+theorem AEStronglyMeasurable.convolution_integrand' [SFinite ν] [MeasurableAdd₂ G]
     [MeasurableNeg G] (hf : AEStronglyMeasurable f ν)
     (hg : AEStronglyMeasurable g <| map (fun p : G × G => p.1 - p.2) (μ.prod ν)) :
     AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=

Mathlib/Dynamics/Ergodic/MeasurePreserving.lean

@@ -185,7 +185,7 @@ theorem add_measure {f μa' μb'} (hf : MeasurePreserving f μa μb)
 theorem smul_measure {R : Type*} [SMul R ℝ≥0∞] [IsScalarTower R ℝ≥0∞ ℝ≥0∞] {f : α → β}
     (hf : MeasurePreserving f μa μb) (c : R) : MeasurePreserving f (c • μa) (c • μb) where
   measurable := hf.measurable
-  map_eq := by rw [Measure.map_smul, hf.map_eq]
+  map_eq := by rw [Measure.map_smul _ hf.aemeasurable, hf.map_eq]
 
 variable {μ : Measure α} {f : α → α} {s : Set α}
 

Mathlib/Geometry/Euclidean/Volume/Measure.lean

@@ -138,7 +138,8 @@ theorem Isometry.euclideanHausdorffMeasure_preimage {f : X → Y} {d : ℕ} (hf
 theorem Isometry.map_euclideanHausdorffMeasure {f : X → Y} {d : ℕ} (hf : Isometry f) :
     μHE[d].map f = μHE[d].restrict (Set.range f) := by
   simp_rw [euclideanHausdorffMeasure_def]
-  rw [Measure.map_smul, map_hausdorffMeasure hf (by simp), Measure.restrict_smul]
+  rw [Measure.map_smul _ hf.continuous.aemeasurable, map_hausdorffMeasure hf (by simp),
+    Measure.restrict_smul]
 
 /-!
 ### Applying scalers to `μHE[d]`
@@ -335,7 +336,7 @@ theorem EuclideanGeometry.euclideanHausdorffMeasure_eq_lintegral (p : P) {v : V}
       ‖v‖ₑ • (volume : Measure ℝ).map g := by
     unfold g
     rw [euclideanHausdorffMeasure_eq p', ← map_map hadd.measurable hf.measurable,
-      ← Measure.map_smul]
+      ← Measure.map_smul _ (by fun_prop)]
     congr
     let v' : (AffineSubspace.mk' p (ℝ ∙ v)).direction := ⟨v, by simp⟩
     suffices volume = ‖v'‖ₑ • volume.map f by simpa [v']

Mathlib/MeasureTheory/Function/ConvergenceInDistribution.lean

@@ -67,8 +67,7 @@ structure TendstoInDistribution [OpensMeasurableSpace E] (X : (i : ι) → Ω i
   forall_aemeasurable : ∀ i, AEMeasurable (X i) (μ i)
   aemeasurable_limit : AEMeasurable Z μ' := by fun_prop
   tendsto : Tendsto (β := ProbabilityMeasure E)
-      (fun n ↦ ⟨(μ n).map (X n), Measure.isProbabilityMeasure_map (forall_aemeasurable n)⟩) l
-      (𝓝 ⟨μ'.map Z, Measure.isProbabilityMeasure_map aemeasurable_limit⟩)
+      (fun n ↦ ⟨(μ n).map (X n), inferInstance⟩) l (𝓝 ⟨μ'.map Z, inferInstance⟩)
 
 lemma tendstoInDistribution_const [OpensMeasurableSpace E] (hZ : AEMeasurable Z μ') :
     TendstoInDistribution (fun _ ↦ Z) l Z (fun _ ↦ μ') μ' where
@@ -198,8 +197,6 @@ lemma tendstoInDistribution_of_tendstoInMeasure_sub {X : ι → Ω'' → E}
   · simp only [LipschitzWith.zero_iff] at hF_lip
     specialize hF_lip x₀
     simp only [← hF_lip, integral_const, smul_eq_mul]
-    have h_prob n : IsProbabilityMeasure (μ''.map (Y n)) := Measure.isProbabilityMeasure_map (hY n)
-    have : IsProbabilityMeasure (μ'.map Z) := Measure.isProbabilityMeasure_map hZ
     simpa using! tendsto_const_nhds
   -- now `F` is `L`-Lipschitz with `L > 0`
   simp_rw [Metric.tendsto_nhds, Real.dist_eq]

Mathlib/MeasureTheory/Group/Convolution.lean

@@ -103,10 +103,10 @@ theorem mconv_zero (μ : Measure M) : μ ∗ₘ (0 : Measure M) = (0 : Measure M
 -- `mconv_smul_right` needs an instance to get `SFinite (c • ν)` from `SFinite ν`,
 -- hence it is placed in the `WithDensity` file, where the instance is defined.
 @[to_additive conv_smul_left]
-theorem mconv_smul_left (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) :
+theorem mconv_smul_left [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) [SFinite ν] (s : ℝ≥0∞) :
     (s • μ) ∗ₘ ν = s • (μ ∗ₘ ν) := by
   unfold mconv
-  rw [← Measure.map_smul, Measure.prod_smul_left]
+  rw [← Measure.map_smul _ (by fun_prop), Measure.prod_smul_left]
 
 @[to_additive]
 theorem mconv_add [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ]
@@ -158,9 +158,10 @@ theorem mconv_assoc [MeasurableMul₂ M] (μ ν ρ : Measure M)
 
 @[to_additive]
 instance probabilitymeasure_of_probabilitymeasures_mconv (μ : Measure M) (ν : Measure M)
-    [MeasurableMul₂ M] [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
-    IsProbabilityMeasure (μ ∗ₘ ν) :=
-  isProbabilityMeasure_map (by fun_prop)
+    [IsProbabilityMeasure μ] [IsProbabilityMeasure ν] :
+    IsProbabilityMeasure (μ ∗ₘ ν) := by
+  rw [mconv]
+  infer_instance
 
 @[to_additive]
 theorem mconv_absolutelyContinuous [MeasurableMul₂ M] {μ ν ρ : Measure M}

Mathlib/MeasureTheory/Group/Defs.lean

@@ -5,6 +5,7 @@ Authors: Floris van Doorn, Yury Kudryashov
 -/
 module
 
+public import Mathlib.MeasureTheory.Group.Arithmetic
 public import Mathlib.MeasureTheory.Measure.Map
 
 /-!
@@ -91,19 +92,23 @@ class IsMulRightInvariant [Mul G] (μ : Measure G) : Prop where
 variable {μ : Measure G}
 
 @[to_additive]
-instance IsMulLeftInvariant.smulInvariantMeasure [Mul G] [IsMulLeftInvariant μ] :
+instance IsMulLeftInvariant.smulInvariantMeasure [Mul G] [IsMulLeftInvariant μ]
+    [MeasurableConstSMul G G] :
     SMulInvariantMeasure G G μ :=
-  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _) hs.nullMeasurableSet⟩
+  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_left_eq_self _)
+    (measurable_const_smul (_x)).aemeasurable hs.nullMeasurableSet⟩
 
 @[to_additive]
-instance [Monoid G] (s : Submonoid G) [IsMulLeftInvariant μ] :
+instance [Monoid G] [MeasurableConstSMul G G] (s : Submonoid G) [IsMulLeftInvariant μ] :
     SMulInvariantMeasure {x // x ∈ s} G μ :=
   ⟨fun ⟨x, _⟩ _ h ↦ IsMulLeftInvariant.smulInvariantMeasure.1 x h⟩
 
 @[to_additive]
-instance IsMulRightInvariant.toSMulInvariantMeasure_op [Mul G] [μ.IsMulRightInvariant] :
+instance IsMulRightInvariant.toSMulInvariantMeasure_op [Mul G] [MeasurableConstSMul Gᵐᵒᵖ G]
+    [μ.IsMulRightInvariant] :
     SMulInvariantMeasure Gᵐᵒᵖ G μ :=
-  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _) hs.nullMeasurableSet⟩
+  ⟨fun _x _s hs => measure_preimage_of_map_eq_self (map_mul_right_eq_self _)
+    (measurable_const_smul _x).aemeasurable hs.nullMeasurableSet⟩
 
 end Measure
 

Mathlib/MeasureTheory/Group/MeasurableEquiv.lean

@@ -237,7 +237,7 @@ lemma domSMul_apply (μ : Measure A) (g : Gᵈᵐᵃ) (s : Set A) :
   exact Set.preimage_smul_inv (DomMulAct.mk.symm g) s
 
 instance : SMulCommClass ℝ≥0 Gᵈᵐᵃ (Measure A) where
-  smul_comm r g μ := show r • μ.map _ = (r • μ).map _ by simp
+  smul_comm r g μ := show r • μ.map _ = (r • μ).map _ by rw [Measure.map_smul _ (by fun_prop)]
 
 instance : SMulCommClass Gᵈᵐᵃ ℝ≥0 (Measure A) := .symm ..
 

Mathlib/MeasureTheory/Group/Measure.lean

@@ -54,21 +54,27 @@ theorem map_mul_right_eq_self (μ : Measure G) [IsMulRightInvariant μ] (g : G)
   IsMulRightInvariant.map_mul_right_eq_self g
 
 @[to_additive MeasureTheory.isAddLeftInvariant_smul]
-instance isMulLeftInvariant_smul [IsMulLeftInvariant μ] (c : ℝ≥0∞) : IsMulLeftInvariant (c • μ) :=
-  ⟨fun g => by rw [Measure.map_smul, map_mul_left_eq_self]⟩
+instance isMulLeftInvariant_smul [MeasurableConstSMul G G] [IsMulLeftInvariant μ] (c : ℝ≥0∞) :
+    IsMulLeftInvariant (c • μ) :=
+  ⟨fun g => by
+    rw [Measure.map_smul, map_mul_left_eq_self]
+    exact (measurable_const_smul g).aemeasurable⟩
 
 @[to_additive MeasureTheory.isAddRightInvariant_smul]
-instance isMulRightInvariant_smul [IsMulRightInvariant μ] (c : ℝ≥0∞) :
+instance isMulRightInvariant_smul [MeasurableConstSMul Gᵐᵒᵖ G] [IsMulRightInvariant μ] (c : ℝ≥0∞) :
     IsMulRightInvariant (c • μ) :=
-  ⟨fun g => by rw [Measure.map_smul, map_mul_right_eq_self]⟩
+  ⟨fun g => by
+    rw [Measure.map_smul, map_mul_right_eq_self]
+    exact (measurable_const_smul (MulOpposite.op g)).aemeasurable⟩
 
 @[to_additive MeasureTheory.isAddLeftInvariant_smul_nnreal]
-instance isMulLeftInvariant_smul_nnreal [IsMulLeftInvariant μ] (c : ℝ≥0) :
+instance isMulLeftInvariant_smul_nnreal [MeasurableConstSMul G G] [IsMulLeftInvariant μ] (c : ℝ≥0) :
     IsMulLeftInvariant (c • μ) :=
   MeasureTheory.isMulLeftInvariant_smul (c : ℝ≥0∞)
 
 @[to_additive MeasureTheory.isAddRightInvariant_smul_nnreal]
-instance isMulRightInvariant_smul_nnreal [IsMulRightInvariant μ] (c : ℝ≥0) :
+instance isMulRightInvariant_smul_nnreal [MeasurableConstSMul Gᵐᵒᵖ G] [IsMulRightInvariant μ]
+    (c : ℝ≥0) :
     IsMulRightInvariant (c • μ) :=
   MeasureTheory.isMulRightInvariant_smul (c : ℝ≥0∞)
 
@@ -788,12 +794,14 @@ theorem haar_singleton [ContinuousMul G] [BorelSpace G] (g : G) : μ {g} = μ {(
   simp only [mul_one, preimage_mul_left_singleton, inv_inv]
 
 @[to_additive IsAddHaarMeasure.smul]
-theorem IsHaarMeasure.smul {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) : IsHaarMeasure (c • μ) :=
+theorem IsHaarMeasure.smul [MeasurableConstSMul G G] {c : ℝ≥0∞} (cpos : c ≠ 0) (ctop : c ≠ ∞) :
+    IsHaarMeasure (c • μ) :=
   { lt_top_of_isCompact := fun _K hK => ENNReal.mul_lt_top ctop.lt_top hK.measure_lt_top
     toIsOpenPosMeasure := isOpenPosMeasure_smul μ cpos }
 
 @[to_additive IsAddHaarMeasure.nnreal_smul]
-lemma IsHaarMeasure.nnreal_smul {c : ℝ≥0} (hc : c ≠ 0) : IsHaarMeasure (c • μ) :=
+lemma IsHaarMeasure.nnreal_smul [MeasurableConstSMul G G] {c : ℝ≥0} (hc : c ≠ 0) :
+    IsHaarMeasure (c • μ) :=
   .smul _ (by simp [hc]) (Option.some_ne_none _)
 
 /-- If a left-invariant measure gives positive mass to some compact set with nonempty interior, then

Mathlib/MeasureTheory/Integral/Lebesgue/Basic.lean

@@ -28,7 +28,7 @@ We introduce the following notation for the lower Lebesgue integral of a functio
 
 @[expose] public section
 
-assert_not_exists Module.Basis Norm MeasureTheory.MeasurePreserving MeasureTheory.Measure.dirac
+assert_not_exists Module.Basis Norm MeasureTheory.MeasurePreserving
 
 open Set hiding restrict restrict_apply
 

Mathlib/MeasureTheory/Integral/Lebesgue/Map.lean

@@ -46,14 +46,12 @@ theorem lintegral_map' {f : β → ℝ≥0∞} {g : α → β}
     _ = ∫⁻ a, hf.mk f (g a) ∂μ := lintegral_congr_ae <| hg.ae_eq_mk.symm.fun_comp _
     _ = ∫⁻ a, f (g a) ∂μ := lintegral_congr_ae (ae_eq_comp hg hf.ae_eq_mk.symm)
 
-theorem lintegral_map_le (f : β → ℝ≥0∞) (g : α → β) :
+theorem lintegral_map_le (f : β → ℝ≥0∞) {g : α → β} (hg : AEMeasurable g μ) :
     ∫⁻ a, f a ∂Measure.map g μ ≤ ∫⁻ a, f (g a) ∂μ := by
-  by_cases hg : AEMeasurable g μ
-  · rw [← iSup_lintegral_measurable_le_eq_lintegral]
-    refine iSup₂_le fun i hi => iSup_le fun h'i => ?_
-    rw [lintegral_map' hi.aemeasurable hg]
-    exact lintegral_mono fun _ ↦ h'i _
-  · simp [map_of_not_aemeasurable hg]
+  rw [← iSup_lintegral_measurable_le_eq_lintegral]
+  refine iSup₂_le fun i hi => iSup_le fun h'i => ?_
+  rw [lintegral_map' hi.aemeasurable hg]
+  exact lintegral_mono fun _ ↦ h'i _
 
 theorem lintegral_comp {f : β → ℝ≥0∞} {g : α → β} (hf : Measurable f)
     (hg : Measurable g) : lintegral μ (f ∘ g) = ∫⁻ a, f a ∂map g μ :=

Mathlib/MeasureTheory/Integral/Prod.lean

@@ -128,11 +128,11 @@ protected theorem MeasureTheory.AEStronglyMeasurable.prod_swap [SFinite μ] [SFi
   rw [← prod_swap] at hf
   exact hf.comp_measurable measurable_swap
 
-theorem MeasureTheory.AEStronglyMeasurable.comp_fst {γ} [TopologicalSpace γ] {f : α → γ}
+theorem MeasureTheory.AEStronglyMeasurable.comp_fst [SFinite ν] {γ} [TopologicalSpace γ] {f : α → γ}
     (hf : AEStronglyMeasurable f μ) : AEStronglyMeasurable (fun z : α × β => f z.1) (μ.prod ν) :=
   hf.comp_quasiMeasurePreserving quasiMeasurePreserving_fst
 
-theorem MeasureTheory.AEStronglyMeasurable.comp_snd {γ} [TopologicalSpace γ] {f : β → γ}
+theorem MeasureTheory.AEStronglyMeasurable.comp_snd [SFinite ν] {γ} [TopologicalSpace γ] {f : β → γ}
     (hf : AEStronglyMeasurable f ν) : AEStronglyMeasurable (fun z : α × β => f z.2) (μ.prod ν) :=
   hf.comp_quasiMeasurePreserving quasiMeasurePreserving_snd
 
@@ -258,7 +258,6 @@ theorem Integrable.integral_norm_prod_right [SFinite μ] ⦃f : α × β → E
     (hf : Integrable f (μ.prod ν)) : Integrable (fun y => ∫ x, ‖f (x, y)‖ ∂μ) ν :=
   hf.swap.integral_norm_prod_left
 
-omit [SFinite ν] in
 theorem Integrable.op_fst_snd {F G : Type*} [NormedAddCommGroup F] [NormedAddCommGroup G]
     {op : E → F → G} (hop : Continuous op.uncurry) (hop_norm : ∃ C, ∀ x y, ‖op x y‖ ≤ C * ‖x‖ * ‖y‖)
     {f : α → E} {g : β → F} (hf : Integrable f μ) (hg : Integrable g ν) :
@@ -288,14 +287,12 @@ lemma Integrable.comp_snd {f : β → E} (hf : Integrable f ν) (μ : Measure α
   rw [← memLp_one_iff_integrable] at hf ⊢
   exact hf.comp_snd μ
 
-omit [SFinite ν] in
 @[fun_prop]
 theorem Integrable.smul_prod {R : Type*} [NormedRing R] [Module R E] [IsBoundedSMul R E]
     {f : α → R} {g : β → E} (hf : Integrable f μ) (hg : Integrable g ν) :
     Integrable (fun z : α × β => f z.1 • g z.2) (μ.prod ν) :=
   hf.op_fst_snd continuous_smul ⟨1, by simpa using norm_smul_le⟩ hg
 
-omit [SFinite ν] in
 @[fun_prop]
 theorem Integrable.mul_prod {L : Type*} [NormedRing L] {f : α → L} {g : β → L} (hf : Integrable f μ)
     (hg : Integrable g ν) : Integrable (fun z : α × β => f z.1 * g z.2) (μ.prod ν) :=

Mathlib/MeasureTheory/Measure/AEMeasurable.lean

@@ -42,12 +42,6 @@ theorem aemeasurable_id'' (μ : Measure α) {m : MeasurableSpace α} (hm : m ≤
     @AEMeasurable α α m m0 id μ :=
   @Measurable.aemeasurable α α m0 m id μ (measurable_id'' hm)
 
-lemma aemeasurable_of_map_neZero {μ : Measure α}
-    {f : α → β} (h : NeZero (μ.map f)) :
-    AEMeasurable f μ := by
-  by_contra h'
-  simp [h'] at h
-
 namespace AEMeasurable
 
 theorem mono_set {s t} (h : s ⊆ t) (ht : AEMeasurable f (μ.restrict t)) :
@@ -449,7 +443,13 @@ instance (μ : Measure α) (f : α → β) [SFinite μ] : SFinite (μ.map f) :=
   · rw [← sum_sfiniteSeq μ] at H ⊢
     rw [map_sum H]
     infer_instance
-  · rw [map_of_not_aemeasurable H]
+  · obtain rfl | hμ := eq_or_ne μ 0
+    · rw [Measure.map_zero]; infer_instance
+    rw [map_of_not_aemeasurable_of_ne_zero H hμ]
+    have : Nonempty β := by
+      contrapose! H
+      exact (measurable_of_empty_codomain f).aemeasurable
+    have : IsFiniteMeasure (dirac Classical.ofNonempty : Measure β) := isFiniteMeasure_dirac
     infer_instance
 
 end Measure

Mathlib/MeasureTheory/Measure/CharacteristicFunction/TaylorExpansion.lean

@@ -127,7 +127,6 @@ lemma taylorWithinEval_charFun_two_zero (hX : AEMeasurable X P)
     (hint : MemLp id 2 (P.map X)) (t : ℝ) :
     taylorWithinEval (charFun (P.map X)) 2 univ 0 t =
       1 + (P[X] : ℝ) * t * I - (P[X ^ 2] : ℝ) * t ^ 2 / 2 := by
-  have : IsProbabilityMeasure (P.map X) := Measure.isProbabilityMeasure_map hX
   convert! taylorWithinEval_charFun_zero hint t with x
   simp only [Pi.pow_apply, Nat.reduceAdd, Finset.sum_range_succ, Finset.range_one,
     Finset.sum_singleton, Nat.factorial_zero, Nat.cast_one, inv_one, pow_zero, mul_one,

Mathlib/MeasureTheory/Measure/Count.lean

@@ -5,7 +5,7 @@ Authors: Johannes Hölzl
 -/
 module
 
-public import Mathlib.MeasureTheory.Measure.Dirac
+public import Mathlib.MeasureTheory.Measure.Dirac.Basic
 
 import Mathlib.SetTheory.Cardinal.ENNReal