feat(MeasureTheory): Add MeasurableSingletonClass version of Measure.map_dirac (#35784)

Gives the new theorem the name `Measure.map_dirac` and rename the current `Measure.map_dirac` to `Measure.map_dirac'`. This follows a convention used elsewhere that for each Measure.dirac lemma with a MeasurableSingleton instance version and a version requiring some sort of measurability, the MeasurableSingleton version has the unprimed name, and the version requiring measurability has the primed name.

Co-authored-by: David Ledvinka <dledvinka.ledvinka@mail.utoronto.ca>

Author: DavidLedvinka

Mathlib/MeasureTheory/Category/MeasCat.lean

@@ -94,7 +94,7 @@ def Giry : CategoryTheory.Monad MeasCat where
   η :=
     { app := fun X => ⟨@Measure.dirac X.1 X.2, Measure.measurable_dirac⟩
       naturality :=
-        fun _ _ ⟨_, hf⟩ => Subtype.ext <| funext fun a => (Measure.map_dirac hf a).symm }
+        fun _ _ ⟨_, hf⟩ => Subtype.ext <| funext fun a => (Measure.map_dirac' hf a).symm }
   μ :=
     { app := fun X => ⟨@Measure.join X.1 X.2, Measure.measurable_join⟩
       naturality := fun _ _ ⟨_, hf⟩ => Subtype.ext <| funext fun μ => Measure.join_map_map hf μ }

Mathlib/MeasureTheory/Constructions/Pi.lean

@@ -884,7 +884,7 @@ theorem measurePreserving_pi_empty {ι : Type u} {α : ι → Type v} [Fintype 
       (Measure.dirac ()) := by
   set e := MeasurableEquiv.ofUniqueOfUnique (∀ i, α i) Unit
   refine ⟨e.measurable, ?_⟩
-  rw [Measure.pi_of_empty, Measure.map_dirac e.measurable]
+  rw [Measure.pi_of_empty, Measure.map_dirac' e.measurable]
 
 theorem volume_preserving_pi_empty {ι : Type u} (α : ι → Type v) [Fintype ι] [IsEmpty ι]
     [∀ i, MeasureSpace (α i)] :

Mathlib/MeasureTheory/Group/Convolution.lean

@@ -70,7 +70,7 @@ lemma mconv_dirac [MeasurableMul₂ M] (μ : Measure M) [SFinite μ] (x : M) :
 @[to_additive (attr := simp)]
 lemma dirac_mconv_dirac [MeasurableMul₂ M] (x y : M) :
     (dirac x) ∗ₘ (dirac y) = dirac (x * y) := by
-  rw [mconv_dirac, map_dirac (by fun_prop)]
+  rw [mconv_dirac, map_dirac' (by fun_prop)]
 
 /-- Convolution of the dirac measure at 1 with a measure μ returns μ. -/
 @[to_additive (attr := simp)

Mathlib/MeasureTheory/Measure/Dirac.lean

@@ -83,7 +83,7 @@ theorem dirac_apply [MeasurableSingletonClass α] (a : α) (s : Set α) :
   fun h ↦ by simpa [h] using dirac_apply_of_mem (mem_univ a)
 
 @[simp]
-theorem map_dirac {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by
+theorem map_dirac' {f : α → β} (hf : Measurable f) (a : α) : (dirac a).map f = dirac (f a) := by
   classical
   exact ext fun s hs => by simp [hs, map_apply hf hs, hf hs, indicator_apply]
 
@@ -215,6 +215,14 @@ lemma aemeasurable_dirac [MeasurableSingletonClass α] {a : α} {f : α → β}
     AEMeasurable f (Measure.dirac a) :=
   ⟨fun _ ↦ f a, measurable_const, ae_eq_dirac f⟩
 
+@[simp]
+theorem Measure.map_dirac [MeasurableSingletonClass α] [MeasurableSingletonClass β]
+    {f : α → β} (a : α) : (dirac a).map f = dirac (f a) := by
+  classical
+  ext s hs
+  rw [map_apply_of_aemeasurable (by fun_prop) hs]
+  simp [indicator_apply]
+
 instance Measure.dirac.isProbabilityMeasure {x : α} : IsProbabilityMeasure (dirac x) :=
   ⟨dirac_apply_of_mem <| mem_univ x⟩
 

Mathlib/MeasureTheory/Measure/GiryMonad.lean

@@ -300,7 +300,7 @@ theorem bind_bind {γ} [MeasurableSpace γ] {m : Measure α} {f : α → Measure
 
 @[simp]
 theorem dirac_bind {f : α → Measure β} (hf : Measurable f) (a : α) : bind (dirac a) f = f a := by
-  simp [bind, map_dirac hf]
+  simp [bind, map_dirac' hf]
 
 @[simp]
 theorem bind_dirac {m : Measure α} : bind m dirac = m := by

Mathlib/MeasureTheory/Measure/Haar/InnerProductSpace.lean

@@ -162,8 +162,7 @@ theorem PiLp.volume_preserving_toLp : MeasurePreserving (@toLp 2 (ι → ℝ)) :
 set_option backward.isDefEq.respectTransparency false in
 lemma volume_euclideanSpace_eq_dirac [IsEmpty ι] :
     (volume : Measure (EuclideanSpace ℝ ι)) = Measure.dirac 0 := by
-  rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0,
-    map_dirac (measurable_toLp 2 _), toLp_zero]
+  rw [← (PiLp.volume_preserving_toLp ι).map_eq, volume_pi_eq_dirac 0, map_dirac, toLp_zero]
 
 end PiLp
 

Mathlib/MeasureTheory/Measure/Prod.lean

@@ -800,7 +800,7 @@ theorem dirac_prod (x : α) : (dirac x).prod ν = map (Prod.mk x) ν := by
     dirac_apply' _ hs, ← indicator_mul_left _ _ fun _ => sfiniteSeq ν i t, Pi.one_apply, one_mul]
 
 theorem dirac_prod_dirac {x : α} {y : β} : (dirac x).prod (dirac y) = dirac (x, y) := by
-  rw [prod_dirac, map_dirac measurable_prodMk_right]
+  rw [prod_dirac, map_dirac' measurable_prodMk_right]
 
 theorem prod_add (ν' : Measure β) [SFinite ν'] : μ.prod (ν + ν') = μ.prod ν + μ.prod ν' := by
   simp_rw [← sum_sfiniteSeq ν, ← sum_sfiniteSeq ν', sum_add_sum, ← sum_sfiniteSeq μ, prod_sum,

Mathlib/Probability/Distributions/Gaussian/Basic.lean

@@ -108,7 +108,7 @@ variable {E F : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpa
 
 /-- Dirac measures are Gaussian. -/
 instance {x : E} : IsGaussian (Measure.dirac x) where
-  map_eq_gaussianReal L := by rw [Measure.map_dirac (by fun_prop)]; simp
+  map_eq_gaussianReal L := by simp
 
 lemma IsGaussian.memLp_dual (μ : Measure E) [IsGaussian μ] (L : StrongDual ℝ E)
     (p : ℝ≥0∞) (hp : p ≠ ∞) :

Mathlib/Probability/Distributions/Gaussian/Real.lean

@@ -278,8 +278,7 @@ lemma _root_.MeasurableEquiv.gaussianReal_map_symm_apply (hv : v ≠ 0) (f : ℝ
 lemma gaussianReal_map_add_const (y : ℝ) :
     (gaussianReal μ v).map (· + y) = gaussianReal (μ + y) v := by
   by_cases hv : v = 0
-  · simp only [hv, gaussianReal_zero_var]
-    exact Measure.map_dirac (measurable_id'.add_const _) _
+  · simp [hv, gaussianReal_zero_var]
   let e : ℝ ≃ᵐ ℝ := (Homeomorph.addRight y).symm.toMeasurableEquiv
   have he' : ∀ x, HasDerivAt e ((fun _ ↦ 1) x) x := fun _ ↦ (hasDerivAt_id _).sub_const y
   change (gaussianReal μ v).map e.symm = gaussianReal (μ + y) v
@@ -300,8 +299,7 @@ set_option backward.isDefEq.respectTransparency false in
 lemma gaussianReal_map_const_mul (c : ℝ) :
     (gaussianReal μ v).map (c * ·) = gaussianReal (c * μ) (⟨c ^ 2, sq_nonneg _⟩ * v) := by
   by_cases hv : v = 0
-  · simp only [hv, mul_zero, gaussianReal_zero_var]
-    exact Measure.map_dirac (measurable_id'.const_mul c) μ
+  · simp [hv, mul_zero, gaussianReal_zero_var]
   by_cases hc : c = 0
   · simp only [hc, zero_mul]
     rw [Measure.map_const]

Mathlib/Probability/Kernel/Composition/MapComap.lean

@@ -218,7 +218,7 @@ end MapComap
 @[simp]
 lemma id_map {f : α → β} (hf : Measurable f) : Kernel.id.map f = deterministic f hf := by
   ext
-  rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac hf]
+  rw [Kernel.map_apply _ hf, Kernel.deterministic_apply, Kernel.id_apply, Measure.map_dirac' hf]
 
 @[simp]
 lemma id_comap {f : α → β} (hf : Measurable f) : Kernel.id.comap f hf = deterministic f hf := by