From 138491387e9fcf94356591de374108a116d2054d Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Sun, 8 Dec 2024 00:26:03 -0800
Subject: [PATCH 01/22] Add `mgf_smul_left`.

---
 Mathlib/Probability/Moments.lean | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 5cd7261ecfd42d..3b1412e923f78b 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -184,6 +184,9 @@ theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply
 
 theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 
+theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (t * α) := by
+    simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_assoc]
+
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
     IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by

From 2e46ac1b16897ff0b7aae270590005eb9a698e52 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Sun, 8 Dec 2024 20:21:43 -0800
Subject: [PATCH 02/22] Reorder the variables.

---
 Mathlib/Probability/Moments.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 3b1412e923f78b..1178661e1715f0 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -184,8 +184,8 @@ theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply
 
 theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 
-theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (t * α) := by
-    simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_assoc]
+theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t) := by
+  simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
 
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :

From a076818e61b706fb5a262b95d16be28fd8f2cef5 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 00:13:54 -0800
Subject: [PATCH 03/22] Add three lemmas about mgf.

---
 Mathlib/Probability/Moments.lean | 55 ++++++++++++++++++++++++++++++++
 1 file changed, 55 insertions(+)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 1178661e1715f0..043c56dbd0f19a 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -4,6 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import Mathlib.Probability.Variance
+import Mathlib.Probability.IdentDistrib
+import Mathlib.Probability.Distributions.Gaussian
 
 /-!
 # Moments and moment generating function
@@ -285,6 +287,26 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
   · rw [h_indep.mgf_sum h_meas]
   · exact (mgf_pos (h_int j hj)).ne'
 
+lemma mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) : mgf X μ t = mgf Y μ t := by
+    rw [mgf, mgf]
+    apply IdentDistrib.integral_eq
+    let u := fun x => Real.exp (t * x)
+    have compX : (fun ω ↦ Real.exp (t * X ω)) = u ∘ X := rfl
+    have compY : (fun ω ↦ Real.exp (t * Y ω)) = u ∘ Y := rfl
+    rw [compX, compY]
+    exact IdentDistrib.comp hident (Measurable.exp (measurable_const_mul t))
+
+theorem mgf_sum_iid
+{X : ι → Ω → ℝ}
+(h_meas : ∀ (i : ι), Measurable (X i))
+(h_indep : ProbabilityTheory.iIndepFun (fun _ => inferInstance) X μ)
+(hident : ∀ (i j : ι), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ)
+(s : Finset ι) (j : ι)
+: ∀ t : ℝ, mgf (∑ i ∈ s, X i) μ t = (mgf (X j) μ (t)) ^ s.card := by
+    intro t
+    rw [iIndepFun.mgf_sum h_indep h_meas]
+    exact Finset.prod_eq_pow_card (fun i si => mgf_ident_distrib (X i) (X j) (hident i j))
+
 /-- **Chernoff bound** on the upper tail of a real random variable. -/
 theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
     (h_int : Integrable (fun ω => exp (t * X ω)) μ) :
@@ -334,6 +356,39 @@ theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
   rw [exp_add]
   exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le
 
+open Measurable
+
+theorem mgf_of_gaussian
+(X: Ω → ℝ) (hXm: Measurable X) (hX: (Measure.map X μ) = (gaussianReal 0 1)) (t : ℝ) :
+  mgf X μ t = exp (t ^ 2 / 2) :=
+    calc
+      mgf X μ t = (Measure.map X μ)[fun x => exp (t * x)] := by
+        have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (Measure.map X μ) :=
+          AEMeasurable.aestronglyMeasurable (aemeasurable
+          (measurable_exp.comp (Continuous.measurable (continuous_const.mul continuous_id))))
+        rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
+      _ = ∫ (x : ℝ), exp (t * x) * (gaussianPDFReal 0 1 x) := by
+        rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
+        simp only [ENNReal.ofReal]
+        rw [integral_withDensity_eq_integral_smul
+        (real_toNNReal (measurable_gaussianPDFReal 0 1))]
+        apply congrArg (integral ℙ)
+        ext x
+        rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
+      _ = exp (t ^ 2 / 2) * ∫ x, (√(2 * π))⁻¹ * exp (-(x - t) ^ 2 / 2) := by
+        simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
+          mul_inv_rev, sub_zero]
+        rw [← integral_mul_left]
+        apply congrArg (integral ℙ)
+        ext x
+        field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
+          ← exp_sub, ← exp_add]
+        ring_nf
+      _ = exp (t ^ 2 / 2) * ∫ (x : ℝ), (gaussianPDFReal t 1 x) := by
+        field_simp [gaussianPDFReal_def]
+      _ = exp (t ^ 2 / 2) := by
+        rw [integral_gaussianPDFReal_eq_one t one_ne_zero, mul_one]
+
 end MomentGeneratingFunction
 
 end ProbabilityTheory

From cf4f4fac308c5050f5140dd5d8acd2a81857edb4 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 00:18:11 -0800
Subject: [PATCH 04/22] Rename lemma.

---
 Mathlib/Probability/Moments.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 043c56dbd0f19a..4f4f5a4d3f5a08 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -287,7 +287,7 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
   · rw [h_indep.mgf_sum h_meas]
   · exact (mgf_pos (h_int j hj)).ne'
 
-lemma mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) : mgf X μ t = mgf Y μ t := by
+theorem mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) : mgf X μ t = mgf Y μ t := by
     rw [mgf, mgf]
     apply IdentDistrib.integral_eq
     let u := fun x => Real.exp (t * x)
@@ -358,7 +358,7 @@ theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
 
 open Measurable
 
-theorem mgf_of_gaussian
+theorem mgf_gaussian
 (X: Ω → ℝ) (hXm: Measurable X) (hX: (Measure.map X μ) = (gaussianReal 0 1)) (t : ℝ) :
   mgf X μ t = exp (t ^ 2 / 2) :=
     calc

From c5eac6664c0af4189ad8072c468129adb5ec7b16 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 00:18:50 -0800
Subject: [PATCH 05/22] Fix indentation.

---
 Mathlib/Probability/Moments.lean | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 4f4f5a4d3f5a08..f3eaef3a69d71a 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -287,7 +287,8 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
   · rw [h_indep.mgf_sum h_meas]
   · exact (mgf_pos (h_int j hj)).ne'
 
-theorem mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) : mgf X μ t = mgf Y μ t := by
+theorem mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) :
+  mgf X μ t = mgf Y μ t := by
     rw [mgf, mgf]
     apply IdentDistrib.integral_eq
     let u := fun x => Real.exp (t * x)

From eafe8b9dae8ac46bfd70610cf451937abbb01919 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 09:09:41 -0800
Subject: [PATCH 06/22] Fix indentation and remove `mgf_gaussian`.

---
 Mathlib/Probability/Moments.lean | 71 +++++++++-----------------------
 1 file changed, 19 insertions(+), 52 deletions(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index f3eaef3a69d71a..23adab4a90ad52 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -5,7 +5,6 @@ Authors: Rémy Degenne
 -/
 import Mathlib.Probability.Variance
 import Mathlib.Probability.IdentDistrib
-import Mathlib.Probability.Distributions.Gaussian
 
 /-!
 # Moments and moment generating function
@@ -287,26 +286,27 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
   · rw [h_indep.mgf_sum h_meas]
   · exact (mgf_pos (h_int j hj)).ne'
 
-theorem mgf_ident_distrib (X Y : Ω → ℝ) (hident : IdentDistrib X Y μ μ) :
-  mgf X μ t = mgf Y μ t := by
-    rw [mgf, mgf]
-    apply IdentDistrib.integral_eq
-    let u := fun x => Real.exp (t * x)
-    have compX : (fun ω ↦ Real.exp (t * X ω)) = u ∘ X := rfl
-    have compY : (fun ω ↦ Real.exp (t * Y ω)) = u ∘ Y := rfl
-    rw [compX, compY]
-    exact IdentDistrib.comp hident (Measurable.exp (measurable_const_mul t))
+theorem mgf_ident_distrib
+    (X : Ω → ℝ) {Ω' : Type u_1} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} (X' : Ω' → ℝ)
+    (hident : IdentDistrib X X' μ μ') (t : ℝ) :
+    mgf X μ t = mgf X' μ' t := by
+  rw [mgf, mgf]
+  apply IdentDistrib.integral_eq
+  let u := fun x => Real.exp (t * x)
+  have compX : (fun ω ↦ Real.exp (t * X ω)) = u ∘ X := rfl
+  have compX' : (fun ω ↦ Real.exp (t * X' ω)) = u ∘ X' := rfl
+  rw [compX, compX']
+  exact IdentDistrib.comp hident (Measurable.exp (measurable_const_mul t))
 
 theorem mgf_sum_iid
-{X : ι → Ω → ℝ}
-(h_meas : ∀ (i : ι), Measurable (X i))
-(h_indep : ProbabilityTheory.iIndepFun (fun _ => inferInstance) X μ)
-(hident : ∀ (i j : ι), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ)
-(s : Finset ι) (j : ι)
-: ∀ t : ℝ, mgf (∑ i ∈ s, X i) μ t = (mgf (X j) μ (t)) ^ s.card := by
-    intro t
-    rw [iIndepFun.mgf_sum h_indep h_meas]
-    exact Finset.prod_eq_pow_card (fun i si => mgf_ident_distrib (X i) (X j) (hident i j))
+    {X : ι → Ω → ℝ}
+    (h_meas : ∀ (i : ι), Measurable (X i))
+    (h_indep : ProbabilityTheory.iIndepFun (fun _ => inferInstance) X μ)
+    (hident : ∀ (i j : ι), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ)
+    (s : Finset ι) (j : ι) : ∀ t : ℝ, mgf (∑ i ∈ s, X i) μ t = (mgf (X j) μ (t)) ^ s.card := by
+  intro t
+  rw [iIndepFun.mgf_sum h_indep h_meas]
+  exact Finset.prod_eq_pow_card (fun i si => mgf_ident_distrib (X i) (X j) (hident i j) t)
 
 /-- **Chernoff bound** on the upper tail of a real random variable. -/
 theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
@@ -357,39 +357,6 @@ theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
   rw [exp_add]
   exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le
 
-open Measurable
-
-theorem mgf_gaussian
-(X: Ω → ℝ) (hXm: Measurable X) (hX: (Measure.map X μ) = (gaussianReal 0 1)) (t : ℝ) :
-  mgf X μ t = exp (t ^ 2 / 2) :=
-    calc
-      mgf X μ t = (Measure.map X μ)[fun x => exp (t * x)] := by
-        have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (Measure.map X μ) :=
-          AEMeasurable.aestronglyMeasurable (aemeasurable
-          (measurable_exp.comp (Continuous.measurable (continuous_const.mul continuous_id))))
-        rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
-      _ = ∫ (x : ℝ), exp (t * x) * (gaussianPDFReal 0 1 x) := by
-        rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
-        simp only [ENNReal.ofReal]
-        rw [integral_withDensity_eq_integral_smul
-        (real_toNNReal (measurable_gaussianPDFReal 0 1))]
-        apply congrArg (integral ℙ)
-        ext x
-        rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
-      _ = exp (t ^ 2 / 2) * ∫ x, (√(2 * π))⁻¹ * exp (-(x - t) ^ 2 / 2) := by
-        simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
-          mul_inv_rev, sub_zero]
-        rw [← integral_mul_left]
-        apply congrArg (integral ℙ)
-        ext x
-        field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
-          ← exp_sub, ← exp_add]
-        ring_nf
-      _ = exp (t ^ 2 / 2) * ∫ (x : ℝ), (gaussianPDFReal t 1 x) := by
-        field_simp [gaussianPDFReal_def]
-      _ = exp (t ^ 2 / 2) := by
-        rw [integral_gaussianPDFReal_eq_one t one_ne_zero, mul_one]
-
 end MomentGeneratingFunction
 
 end ProbabilityTheory

From 574507a596fcf3bdfc05ebc4cc00001687bf8920 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 09:21:09 -0800
Subject: [PATCH 07/22] Add `mgf_gaussian`.

---
 .../Probability/Distributions/Gaussian.lean   | 33 +++++++++++++++++++
 1 file changed, 33 insertions(+)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 10a5c010266d0a..474bdbb6dc9bf8 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -6,6 +6,7 @@ Authors: Lorenzo Luccioli, Rémy Degenne, Alexander Bentkamp
 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
 import Mathlib.Probability.Notation
 import Mathlib.MeasureTheory.Decomposition.Lebesgue
+import Mathlib.Probability.Moments
 
 /-!
 # Gaussian distributions over ℝ
@@ -347,6 +348,38 @@ lemma gaussianReal_mul_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussian
 
 end Transformations
 
+open Measurable Real
+
+theorem mgf_gaussian {Ω : Type} {m : MeasurableSpace Ω} {μ : Measure Ω}
+    (X: Ω → ℝ) (hXm: Measurable X) (hX: (Measure.map X μ) = (gaussianReal 0 1)) (t : ℝ) :
+    mgf X μ t = exp (t ^ 2 / 2) := calc
+  mgf X μ t = (Measure.map X μ)[fun x => exp (t * x)] := by
+    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (Measure.map X μ) :=
+      AEMeasurable.aestronglyMeasurable (aemeasurable
+      (measurable_exp.comp (Continuous.measurable (continuous_const.mul continuous_id))))
+    rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
+  _ = ∫ (x : ℝ), exp (t * x) * (gaussianPDFReal 0 1 x) := by
+    rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
+    simp only [ENNReal.ofReal]
+    rw [integral_withDensity_eq_integral_smul
+    (real_toNNReal (measurable_gaussianPDFReal 0 1))]
+    apply congrArg (integral ℙ)
+    ext x
+    rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
+  _ = exp (t ^ 2 / 2) * ∫ x, (√(2 * π))⁻¹ * exp (-(x - t) ^ 2 / 2) := by
+    simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
+      mul_inv_rev, sub_zero]
+    rw [← integral_mul_left]
+    apply congrArg (integral ℙ)
+    ext x
+    field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
+      ← exp_sub, ← exp_add]
+    ring_nf
+  _ = exp (t ^ 2 / 2) * ∫ (x : ℝ), (gaussianPDFReal t 1 x) := by
+    field_simp [gaussianPDFReal_def]
+  _ = exp (t ^ 2 / 2) := by
+    rw [integral_gaussianPDFReal_eq_one t one_ne_zero, mul_one]
+
 end GaussianReal
 
 end ProbabilityTheory

From 6af0e2300e6b7e8889978ca44c3c83c678d3bc1b Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 09:21:54 -0800
Subject: [PATCH 08/22] Remove lemmas in Moments.

---
 Mathlib/Probability/Moments.lean | 23 -----------------------
 1 file changed, 23 deletions(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 23adab4a90ad52..1178661e1715f0 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Rémy Degenne
 -/
 import Mathlib.Probability.Variance
-import Mathlib.Probability.IdentDistrib
 
 /-!
 # Moments and moment generating function
@@ -286,28 +285,6 @@ theorem iIndepFun.cgf_sum {X : ι → Ω → ℝ}
   · rw [h_indep.mgf_sum h_meas]
   · exact (mgf_pos (h_int j hj)).ne'
 
-theorem mgf_ident_distrib
-    (X : Ω → ℝ) {Ω' : Type u_1} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} (X' : Ω' → ℝ)
-    (hident : IdentDistrib X X' μ μ') (t : ℝ) :
-    mgf X μ t = mgf X' μ' t := by
-  rw [mgf, mgf]
-  apply IdentDistrib.integral_eq
-  let u := fun x => Real.exp (t * x)
-  have compX : (fun ω ↦ Real.exp (t * X ω)) = u ∘ X := rfl
-  have compX' : (fun ω ↦ Real.exp (t * X' ω)) = u ∘ X' := rfl
-  rw [compX, compX']
-  exact IdentDistrib.comp hident (Measurable.exp (measurable_const_mul t))
-
-theorem mgf_sum_iid
-    {X : ι → Ω → ℝ}
-    (h_meas : ∀ (i : ι), Measurable (X i))
-    (h_indep : ProbabilityTheory.iIndepFun (fun _ => inferInstance) X μ)
-    (hident : ∀ (i j : ι), ProbabilityTheory.IdentDistrib (X i) (X j) μ μ)
-    (s : Finset ι) (j : ι) : ∀ t : ℝ, mgf (∑ i ∈ s, X i) μ t = (mgf (X j) μ (t)) ^ s.card := by
-  intro t
-  rw [iIndepFun.mgf_sum h_indep h_meas]
-  exact Finset.prod_eq_pow_card (fun i si => mgf_ident_distrib (X i) (X j) (hident i j) t)
-
 /-- **Chernoff bound** on the upper tail of a real random variable. -/
 theorem measure_ge_le_exp_mul_mgf [IsFiniteMeasure μ] (ε : ℝ) (ht : 0 ≤ t)
     (h_int : Integrable (fun ω => exp (t * X ω)) μ) :

From c360bfa796d4804d7e162ac3802dfeed53281e3e Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Wed, 11 Dec 2024 09:26:18 -0800
Subject: [PATCH 09/22] Remove an extra lemma.

---
 Mathlib/Probability/Moments.lean | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 1178661e1715f0..5cd7261ecfd42d 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -184,9 +184,6 @@ theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply
 
 theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 
-theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t) := by
-  simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
-
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
     IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by

From 6f58ec7f4805dd5a3f98831f3438a27f5f87492d Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 06:44:22 -0800
Subject: [PATCH 10/22] Simplify notation.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 474bdbb6dc9bf8..d6618f26838b8d 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,19 +350,19 @@ end Transformations
 
 open Measurable Real
 
-theorem mgf_gaussian {Ω : Type} {m : MeasurableSpace Ω} {μ : Measure Ω}
-    (X: Ω → ℝ) (hXm: Measurable X) (hX: (Measure.map X μ) = (gaussianReal 0 1)) (t : ℝ) :
+theorem mgf_gaussian {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
+    (X : Ω → ℝ) (hXm : Measurable X) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
     mgf X μ t = exp (t ^ 2 / 2) := calc
-  mgf X μ t = (Measure.map X μ)[fun x => exp (t * x)] := by
-    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (Measure.map X μ) :=
+  mgf X μ t = μ.map X[fun x => exp (t * x)] := by
+    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) μ.map X :=
       AEMeasurable.aestronglyMeasurable (aemeasurable
-      (measurable_exp.comp (Continuous.measurable (continuous_const.mul continuous_id))))
+      (measurable_exp.comp (continuous_const.mul continuous_id).measurable))
     rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
   _ = ∫ (x : ℝ), exp (t * x) * (gaussianPDFReal 0 1 x) := by
     rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
     simp only [ENNReal.ofReal]
     rw [integral_withDensity_eq_integral_smul
-    (real_toNNReal (measurable_gaussianPDFReal 0 1))]
+      (measurable_gaussianPDFReal 0 1).real_toNNReal]
     apply congrArg (integral ℙ)
     ext x
     rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]

From 88e3588267bfed59c569c37213d03ba44797cdbd Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 07:03:58 -0800
Subject: [PATCH 11/22] Clean up `mgf_gaussian`.

---
 .../Probability/Distributions/Gaussian.lean   | 19 +++++++++----------
 1 file changed, 9 insertions(+), 10 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index d6618f26838b8d..51c2c180fe56a4 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -351,20 +351,19 @@ end Transformations
 open Measurable Real
 
 theorem mgf_gaussian {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
-    (X : Ω → ℝ) (hXm : Measurable X) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
-    mgf X μ t = exp (t ^ 2 / 2) := calc
-  mgf X μ t = μ.map X[fun x => exp (t * x)] := by
-    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) μ.map X :=
-      AEMeasurable.aestronglyMeasurable (aemeasurable
-      (measurable_exp.comp (continuous_const.mul continuous_id).measurable))
+  (X : Ω → ℝ) (hXm : Measurable X) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
+  mgf X μ t = exp (t ^ 2 / 2) := calc
+  mgf X μ t = (μ.map X)[fun x => exp (t * x)] := by
+    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (μ.map X) :=
+      (aemeasurable (measurable_exp.comp (continuous_const.mul
+      continuous_id).measurable)).aestronglyMeasurable
     rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
-  _ = ∫ (x : ℝ), exp (t * x) * (gaussianPDFReal 0 1 x) := by
+  _ = ∫ x, exp (t * x) * gaussianPDFReal 0 1 x := by
     rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
     simp only [ENNReal.ofReal]
     rw [integral_withDensity_eq_integral_smul
       (measurable_gaussianPDFReal 0 1).real_toNNReal]
-    apply congrArg (integral ℙ)
-    ext x
+    congr with x
     rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
   _ = exp (t ^ 2 / 2) * ∫ x, (√(2 * π))⁻¹ * exp (-(x - t) ^ 2 / 2) := by
     simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
@@ -375,7 +374,7 @@ theorem mgf_gaussian {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
     field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
       ← exp_sub, ← exp_add]
     ring_nf
-  _ = exp (t ^ 2 / 2) * ∫ (x : ℝ), (gaussianPDFReal t 1 x) := by
+  _ = exp (t ^ 2 / 2) * ∫ x, gaussianPDFReal t 1 x := by
     field_simp [gaussianPDFReal_def]
   _ = exp (t ^ 2 / 2) := by
     rw [integral_gaussianPDFReal_eq_one t one_ne_zero, mul_one]

From 13c9010e99845715b0ae98bbeb6673ef104bbbad Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 09:50:38 -0800
Subject: [PATCH 12/22] Make two supporting lemmas.

---
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean |  7 +++++++
 Mathlib/Probability/Distributions/Gaussian.lean | 13 ++++++-------
 Mathlib/Probability/Moments.lean                |  7 +++++++
 3 files changed, 20 insertions(+), 7 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index 92a5dcb5aa47ba..c64196a12902f2 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1194,6 +1194,13 @@ theorem map_zero (f : α → β) : (0 : Measure α).map f = 0 := by
 theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) :
     μ.map f = 0 := by simp [map, hf]
 
+theorem aemeasurable_of_map_ne_zero {μ : Measure α} {μ' : Measure β} {f : α → β}
+  (hf : μ.map f = μ') (nezero : μ' ≠ 0) : AEMeasurable f μ := by
+    by_contra h
+    simp only [h, not_false_eq_true, Measure.map_of_not_aemeasurable] at hf
+    apply nezero
+    rw [hf]
+
 theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ := by
   by_cases hf : AEMeasurable f μ
   · have hg : AEMeasurable g μ := hf.congr h
diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 51c2c180fe56a4..55042a16118ba4 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,14 +350,13 @@ end Transformations
 
 open Measurable Real
 
-theorem mgf_gaussian {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
-  (X : Ω → ℝ) (hXm : Measurable X) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
-  mgf X μ t = exp (t ^ 2 / 2) := calc
+theorem mgf_gaussianReal {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
+    (X : Ω → ℝ) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
+    mgf X μ t = exp (t ^ 2 / 2) := calc
   mgf X μ t = (μ.map X)[fun x => exp (t * x)] := by
-    have : AEStronglyMeasurable (fun x ↦ exp (t * x)) (μ.map X) :=
-      (aemeasurable (measurable_exp.comp (continuous_const.mul
-      continuous_id).measurable)).aestronglyMeasurable
-    rw [mgf, MeasureTheory.integral_map (aemeasurable hXm) this]
+    rw [← mgf_id_map, mgf]
+    · rfl
+    · exact aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal 0 1))
   _ = ∫ x, exp (t * x) * gaussianPDFReal 0 1 x := by
     rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
     simp only [ENNReal.ofReal]
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 1178661e1715f0..431b0dc453d614 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -180,6 +180,13 @@ theorem mgf_pos [IsProbabilityMeasure μ] (h_int_X : Integrable (fun ω => exp (
     0 < mgf X μ t :=
   mgf_pos' (IsProbabilityMeasure.ne_zero μ) h_int_X
 
+lemma mgf_id_map {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
+  (X : Ω → ℝ) (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ := by
+  ext t
+  rw [mgf, integral_map hX]
+  · rfl
+  · exact (measurable_exp.comp (measurable_const_mul _)).aestronglyMeasurable
+
 theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]
 
 theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]

From 024aad75215306adac7c64e055e7d3f074a79903 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 10:39:57 -0800
Subject: [PATCH 13/22] Fix.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 15 ++++++++-------
 Mathlib/Probability/Moments.lean                |  6 ++++++
 2 files changed, 14 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 55042a16118ba4..1d0ea4d063be3a 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,13 +350,15 @@ end Transformations
 
 open Measurable Real
 
-theorem mgf_gaussianReal {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
-    (X : Ω → ℝ) (hX : μ.map X = gaussianReal 0 1) (t : ℝ) :
-    mgf X μ t = exp (t ^ 2 / 2) := calc
-  mgf X μ t = (μ.map X)[fun x => exp (t * x)] := by
+variable {Ω : Type} [MeasureSpace Ω]
+
+theorem mgf_standard_gaussianReal
+    {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal 0 1) (t : ℝ) :
+    mgf X ℙ t = exp (t ^ 2 / 2) := calc
+  mgf X ℙ t = (Measure.map X ℙ)[fun x => exp (t * x)] := by
     rw [← mgf_id_map, mgf]
     · rfl
-    · exact aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal 0 1))
+    · exact Measure.aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal 0 1))
   _ = ∫ x, exp (t * x) * gaussianPDFReal 0 1 x := by
     rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
     simp only [ENNReal.ofReal]
@@ -368,8 +370,7 @@ theorem mgf_gaussianReal {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
     simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
       mul_inv_rev, sub_zero]
     rw [← integral_mul_left]
-    apply congrArg (integral ℙ)
-    ext x
+    congr with x
     field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
       ← exp_sub, ← exp_add]
     ring_nf
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 431b0dc453d614..c45babc06a6580 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -194,6 +194,12 @@ theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t) := by
   simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
 
+theorem mgf_const_add_left (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α) * mgf X μ t := by
+  rw [mgf, mgf, ← integral_mul_left]
+  congr with x
+  dsimp
+  rw [mul_add, exp_add]
+
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
     IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by

From a5f1ab4c7c7dc25eaa3a06cebd99804d34972d72 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 11:19:08 -0800
Subject: [PATCH 14/22] Prove `mgf_gaussianReal` for a general gaussian.

---
 .../Probability/Distributions/Gaussian.lean   | 34 ++++++++-----------
 1 file changed, 15 insertions(+), 19 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 1d0ea4d063be3a..a9a67631748ca3 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,34 +350,30 @@ end Transformations
 
 open Measurable Real
 
-variable {Ω : Type} [MeasureSpace Ω]
-
-theorem mgf_standard_gaussianReal
-    {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal 0 1) (t : ℝ) :
-    mgf X ℙ t = exp (t ^ 2 / 2) := calc
+theorem mgf_gaussianReal {Ω : Type} [MeasureSpace Ω] (μ : ℝ) (v : ℝ≥0) (hv : v ≠ 0)
+    {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
+    mgf X ℙ t = exp (μ * t + v * t ^ 2 / 2) := calc
   mgf X ℙ t = (Measure.map X ℙ)[fun x => exp (t * x)] := by
     rw [← mgf_id_map, mgf]
     · rfl
-    · exact Measure.aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal 0 1))
-  _ = ∫ x, exp (t * x) * gaussianPDFReal 0 1 x := by
-    rw [hX, gaussianReal_of_var_ne_zero 0 one_ne_zero, gaussianPDF_def]
+    · exact Measure.aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal μ v))
+  _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
+    rw [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def]
     simp only [ENNReal.ofReal]
     rw [integral_withDensity_eq_integral_smul
-      (measurable_gaussianPDFReal 0 1).real_toNNReal]
+      (measurable_gaussianPDFReal μ v).real_toNNReal]
     congr with x
-    rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg 0 1 x), smul_eq_mul, mul_comm]
-  _ = exp (t ^ 2 / 2) * ∫ x, (√(2 * π))⁻¹ * exp (-(x - t) ^ 2 / 2) := by
-    simp only [gaussianPDFReal, NNReal.coe_one, mul_one, Nat.ofNat_nonneg, sqrt_mul,
-      mul_inv_rev, sub_zero]
-    rw [← integral_mul_left]
+    rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg μ v x), smul_eq_mul, mul_comm]
+  _ = exp (μ * t + v * t ^ 2 / 2)
+      * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
+    rw [gaussianPDFReal_def, ← integral_mul_left]
     congr with x
-    field_simp only [mul_sub, sub_eq_zero, mul_assoc, mul_comm, mul_left_comm,
-      ← exp_sub, ← exp_add]
+    field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
     ring_nf
-  _ = exp (t ^ 2 / 2) * ∫ x, gaussianPDFReal t 1 x := by
+  _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
     field_simp [gaussianPDFReal_def]
-  _ = exp (t ^ 2 / 2) := by
-    rw [integral_gaussianPDFReal_eq_one t one_ne_zero, mul_one]
+  _ = exp (μ * t + v * t ^ 2 / 2) := by
+    rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
 
 end GaussianReal
 

From 34a12dba980ce4d2545580fd23581c33e1b686e4 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Fri, 20 Dec 2024 11:33:59 -0800
Subject: [PATCH 15/22] Add `cgf_gaussianReal`.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 9 +++++++--
 1 file changed, 7 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index a9a67631748ca3..cf490ad947bfb5 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,8 +350,9 @@ end Transformations
 
 open Measurable Real
 
-theorem mgf_gaussianReal {Ω : Type} [MeasureSpace Ω] (μ : ℝ) (v : ℝ≥0) (hv : v ≠ 0)
-    {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
+variable {Ω : Type} [MeasureSpace Ω] {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
+
+theorem mgf_gaussianReal (hv : v ≠ 0) (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
     mgf X ℙ t = exp (μ * t + v * t ^ 2 / 2) := calc
   mgf X ℙ t = (Measure.map X ℙ)[fun x => exp (t * x)] := by
     rw [← mgf_id_map, mgf]
@@ -375,6 +376,10 @@ theorem mgf_gaussianReal {Ω : Type} [MeasureSpace Ω] (μ : ℝ) (v : ℝ≥0)
   _ = exp (μ * t + v * t ^ 2 / 2) := by
     rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
 
+theorem cgf_gaussianReal (hv : v ≠ 0) (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
+    cgf X ℙ t = μ * t + v * t ^ 2 / 2 := by
+  rw [cgf, mgf_gaussianReal hv hX t, log_exp]
+
 end GaussianReal
 
 end ProbabilityTheory

From a4d345940af1af64ef9cf768fa6e4e5a0f61bb95 Mon Sep 17 00:00:00 2001
From: Vas <vasilin97@gmail.com>
Date: Sat, 21 Dec 2024 12:58:57 -0800
Subject: [PATCH 16/22] Remove assumption `hv : v \neq 0`.

---
 .../MeasureTheory/Measure/MeasureSpace.lean   |  7 +-
 .../Probability/Distributions/Gaussian.lean   | 72 +++++++++++--------
 Mathlib/Probability/Moments.lean              |  8 ++-
 3 files changed, 51 insertions(+), 36 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index c64196a12902f2..d5838a8bee0c53 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1194,12 +1194,11 @@ theorem map_zero (f : α → β) : (0 : Measure α).map f = 0 := by
 theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) :
     μ.map f = 0 := by simp [map, hf]
 
-theorem aemeasurable_of_map_ne_zero {μ : Measure α} {μ' : Measure β} {f : α → β}
-  (hf : μ.map f = μ') (nezero : μ' ≠ 0) : AEMeasurable f μ := by
+theorem aemeasurable_of_map_ne_zero {μ : Measure α} {f : α → β}
+  (hf : μ.map f ≠ 0) : AEMeasurable f μ := by
     by_contra h
     simp only [h, not_false_eq_true, Measure.map_of_not_aemeasurable] at hf
-    apply nezero
-    rw [hf]
+    apply hf rfl
 
 theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ := by
   by_cases hf : AEMeasurable f μ
diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index cf490ad947bfb5..97d56110c8aaff 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,35 +350,49 @@ end Transformations
 
 open Measurable Real
 
-variable {Ω : Type} [MeasureSpace Ω] {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
-
-theorem mgf_gaussianReal (hv : v ≠ 0) (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
-    mgf X ℙ t = exp (μ * t + v * t ^ 2 / 2) := calc
-  mgf X ℙ t = (Measure.map X ℙ)[fun x => exp (t * x)] := by
-    rw [← mgf_id_map, mgf]
-    · rfl
-    · exact Measure.aemeasurable_of_map_ne_zero hX (IsProbabilityMeasure.ne_zero (gaussianReal μ v))
-  _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
-    rw [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def]
-    simp only [ENNReal.ofReal]
-    rw [integral_withDensity_eq_integral_smul
-      (measurable_gaussianPDFReal μ v).real_toNNReal]
-    congr with x
-    rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg μ v x), smul_eq_mul, mul_comm]
-  _ = exp (μ * t + v * t ^ 2 / 2)
-      * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
-    rw [gaussianPDFReal_def, ← integral_mul_left]
-    congr with x
-    field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
-    ring_nf
-  _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
-    field_simp [gaussianPDFReal_def]
-  _ = exp (μ * t + v * t ^ 2 / 2) := by
-    rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
-
-theorem cgf_gaussianReal (hv : v ≠ 0) (hX : Measure.map X ℙ = gaussianReal μ v) (t : ℝ) :
-    cgf X ℙ t = μ * t + v * t ^ 2 / 2 := by
-  rw [cgf, mgf_gaussianReal hv hX t, log_exp]
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {p : Measure Ω} {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
+
+lemma mgf_dirac (hX : Measure.map X p = Measure.dirac μ) (t : ℝ) : mgf X p t = exp (μ * t) := by
+  rw [← mgf_id_map, mgf, hX, integral_dirac, mul_comm]
+  · rfl
+  · apply Measure.aemeasurable_of_map_ne_zero
+    rw [hX]
+    exact IsProbabilityMeasure.ne_zero (Measure.dirac μ)
+
+theorem mgf_gaussianReal (hX : Measure.map X p = gaussianReal μ v) (t : ℝ) :
+    mgf X p t = exp (μ * t + v * t ^ 2 / 2) := by
+  by_cases hv : v = 0
+  · simp only [gaussianReal, hv, ↓reduceIte] at hX
+    rw [mgf_dirac hX, hv]
+    simp only [NNReal.coe_zero, zero_mul, zero_div, add_zero]
+  · calc
+    mgf X p t = (Measure.map X p)[fun x => exp (t * x)] := by
+      rw [← mgf_id_map, mgf]
+      · rfl
+      · apply Measure.aemeasurable_of_map_ne_zero
+        rw [hX]
+        exact IsProbabilityMeasure.ne_zero (gaussianReal μ v)
+    _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
+      rw [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def]
+      simp only [ENNReal.ofReal]
+      rw [integral_withDensity_eq_integral_smul
+        (measurable_gaussianPDFReal μ v).real_toNNReal]
+      congr with x
+      rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg μ v x), smul_eq_mul, mul_comm]
+    _ = exp (μ * t + v * t ^ 2 / 2)
+        * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
+      rw [gaussianPDFReal_def, ← integral_mul_left]
+      congr with x
+      field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
+      ring_nf
+    _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
+      field_simp [gaussianPDFReal_def]
+    _ = exp (μ * t + v * t ^ 2 / 2) := by
+      rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
+
+theorem cgf_gaussianReal (hX : Measure.map X p = gaussianReal μ v) (t : ℝ) :
+    cgf X p t = μ * t + v * t ^ 2 / 2 := by
+  rw [cgf, mgf_gaussianReal hX t, log_exp]
 
 end GaussianReal
 
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index c45babc06a6580..f2f6099ad33653 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -180,8 +180,7 @@ theorem mgf_pos [IsProbabilityMeasure μ] (h_int_X : Integrable (fun ω => exp (
     0 < mgf X μ t :=
   mgf_pos' (IsProbabilityMeasure.ne_zero μ) h_int_X
 
-lemma mgf_id_map {Ω : Type*} {m : MeasurableSpace Ω} {μ : Measure Ω}
-  (X : Ω → ℝ) (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ := by
+lemma mgf_id_map (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ := by
   ext t
   rw [mgf, integral_map hX]
   · rfl
@@ -194,12 +193,15 @@ theorem cgf_neg : cgf (-X) μ t = cgf X μ (-t) := by simp_rw [cgf, mgf_neg]
 theorem mgf_smul_left (α : ℝ) : mgf (α • X) μ t = mgf X μ (α * t) := by
   simp_rw [mgf, Pi.smul_apply, smul_eq_mul, mul_comm α t, mul_assoc]
 
-theorem mgf_const_add_left (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α) * mgf X μ t := by
+theorem mgf_const_add (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α) * mgf X μ t := by
   rw [mgf, mgf, ← integral_mul_left]
   congr with x
   dsimp
   rw [mul_add, exp_add]
 
+theorem mgf_add_const (α : ℝ) : mgf (fun ω => X ω + α) μ t = exp (t * α) * mgf X μ t := by
+  simp only [add_comm, mgf_const_add]
+
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :
     IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by

From 8185027df39cec62491c013f8749d7ccda8ebc6a Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Mon, 30 Dec 2024 19:54:01 +0000
Subject: [PATCH 17/22] Change naming.

---
 Mathlib/MeasureTheory/Measure/MeasureSpace.lean |  7 ++-----
 Mathlib/Probability/Distributions/Gaussian.lean | 14 +++++++-------
 2 files changed, 9 insertions(+), 12 deletions(-)

diff --git a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
index d5838a8bee0c53..17535bf1a4ccc9 100644
--- a/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
+++ b/Mathlib/MeasureTheory/Measure/MeasureSpace.lean
@@ -1194,11 +1194,8 @@ theorem map_zero (f : α → β) : (0 : Measure α).map f = 0 := by
 theorem map_of_not_aemeasurable {f : α → β} {μ : Measure α} (hf : ¬AEMeasurable f μ) :
     μ.map f = 0 := by simp [map, hf]
 
-theorem aemeasurable_of_map_ne_zero {μ : Measure α} {f : α → β}
-  (hf : μ.map f ≠ 0) : AEMeasurable f μ := by
-    by_contra h
-    simp only [h, not_false_eq_true, Measure.map_of_not_aemeasurable] at hf
-    apply hf rfl
+theorem _root_.AEMeasurable.of_map_ne_zero {f : α → β} {μ : Measure α} (hf : μ.map f ≠ 0) :
+    AEMeasurable f μ := not_imp_comm.1 map_of_not_aemeasurable hf
 
 theorem map_congr {f g : α → β} (h : f =ᵐ[μ] g) : Measure.map f μ = Measure.map g μ := by
   by_cases hf : AEMeasurable f μ
diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 97d56110c8aaff..b32c649cb7c884 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -352,24 +352,24 @@ open Measurable Real
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {p : Measure Ω} {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
 
-lemma mgf_dirac (hX : Measure.map X p = Measure.dirac μ) (t : ℝ) : mgf X p t = exp (μ * t) := by
+lemma mgf_dirac (hX : p.map X = .dirac μ) (t : ℝ) : mgf X p t = exp (μ * t) := by
   rw [← mgf_id_map, mgf, hX, integral_dirac, mul_comm]
   · rfl
-  · apply Measure.aemeasurable_of_map_ne_zero
+  · apply AEMeasurable.of_map_ne_zero
     rw [hX]
-    exact IsProbabilityMeasure.ne_zero (Measure.dirac μ)
+    exact IsProbabilityMeasure.ne_zero (.dirac μ)
 
-theorem mgf_gaussianReal (hX : Measure.map X p = gaussianReal μ v) (t : ℝ) :
+theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     mgf X p t = exp (μ * t + v * t ^ 2 / 2) := by
   by_cases hv : v = 0
   · simp only [gaussianReal, hv, ↓reduceIte] at hX
     rw [mgf_dirac hX, hv]
     simp only [NNReal.coe_zero, zero_mul, zero_div, add_zero]
   · calc
-    mgf X p t = (Measure.map X p)[fun x => exp (t * x)] := by
+    mgf X p t = (p.map X)[fun x => exp (t * x)] := by
       rw [← mgf_id_map, mgf]
       · rfl
-      · apply Measure.aemeasurable_of_map_ne_zero
+      · apply AEMeasurable.of_map_ne_zero
         rw [hX]
         exact IsProbabilityMeasure.ne_zero (gaussianReal μ v)
     _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
@@ -390,7 +390,7 @@ theorem mgf_gaussianReal (hX : Measure.map X p = gaussianReal μ v) (t : ℝ) :
     _ = exp (μ * t + v * t ^ 2 / 2) := by
       rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
 
-theorem cgf_gaussianReal (hX : Measure.map X p = gaussianReal μ v) (t : ℝ) :
+theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     cgf X p t = μ * t + v * t ^ 2 / 2 := by
   rw [cgf, mgf_gaussianReal hX t, log_exp]
 

From e96ae6ebff628f00d9b7009577923f4bdc16b48f Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Mon, 30 Dec 2024 23:53:07 +0000
Subject: [PATCH 18/22] Apply suggestions.

---
 .../Probability/Distributions/Gaussian.lean   | 50 ++++++++-----------
 Mathlib/Probability/Moments.lean              |  4 +-
 2 files changed, 24 insertions(+), 30 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index b32c649cb7c884..acf062ad25411c 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -4,8 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Lorenzo Luccioli, Rémy Degenne, Alexander Bentkamp
 -/
 import Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
-import Mathlib.Probability.Notation
-import Mathlib.MeasureTheory.Decomposition.Lebesgue
 import Mathlib.Probability.Moments
 
 /-!
@@ -363,32 +361,28 @@ theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     mgf X p t = exp (μ * t + v * t ^ 2 / 2) := by
   by_cases hv : v = 0
   · simp only [gaussianReal, hv, ↓reduceIte] at hX
-    rw [mgf_dirac hX, hv]
-    simp only [NNReal.coe_zero, zero_mul, zero_div, add_zero]
-  · calc
-    mgf X p t = (p.map X)[fun x => exp (t * x)] := by
-      rw [← mgf_id_map, mgf]
-      · rfl
-      · apply AEMeasurable.of_map_ne_zero
-        rw [hX]
-        exact IsProbabilityMeasure.ne_zero (gaussianReal μ v)
-    _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
-      rw [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def]
-      simp only [ENNReal.ofReal]
-      rw [integral_withDensity_eq_integral_smul
-        (measurable_gaussianPDFReal μ v).real_toNNReal]
-      congr with x
-      rw [NNReal.smul_def, coe_toNNReal _ (gaussianPDFReal_nonneg μ v x), smul_eq_mul, mul_comm]
-    _ = exp (μ * t + v * t ^ 2 / 2)
-        * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
-      rw [gaussianPDFReal_def, ← integral_mul_left]
-      congr with x
-      field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
-      ring_nf
-    _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
-      field_simp [gaussianPDFReal_def]
-    _ = exp (μ * t + v * t ^ 2 / 2) := by
-      rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
+    simp [mgf_dirac hX, hv]
+  calc
+  mgf X p t = (p.map X)[fun x => exp (t * x)] := by
+    rw [← mgf_id_map, mgf]
+    · rfl
+    · apply AEMeasurable.of_map_ne_zero
+      rw [hX]
+      exact IsProbabilityMeasure.ne_zero (gaussianReal μ v)
+  _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
+    simp [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def, ENNReal.ofReal,
+      integral_withDensity_eq_integral_smul (measurable_gaussianPDFReal μ v).real_toNNReal,
+      NNReal.smul_def, coe_toNNReal', gaussianPDFReal_nonneg, sup_of_le_left, smul_eq_mul, mul_comm]
+  _ = exp (μ * t + v * t ^ 2 / 2)
+      * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
+    rw [gaussianPDFReal_def, ← integral_mul_left]
+    congr with x
+    field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
+    ring_nf
+  _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
+    field_simp [gaussianPDFReal_def]
+  _ = exp (μ * t + v * t ^ 2 / 2) := by
+    rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
 
 theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     cgf X p t = μ * t + v * t ^ 2 / 2 := by
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index f2f6099ad33653..0c84543fb70b76 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -199,8 +199,8 @@ theorem mgf_const_add (α : ℝ) : mgf (fun ω => α + X ω) μ t = exp (t * α)
   dsimp
   rw [mul_add, exp_add]
 
-theorem mgf_add_const (α : ℝ) : mgf (fun ω => X ω + α) μ t = exp (t * α) * mgf X μ t := by
-  simp only [add_comm, mgf_const_add]
+theorem mgf_add_const (α : ℝ) : mgf (fun ω => X ω + α) μ t = mgf X μ t *  exp (t * α) := by
+  simp only [add_comm, mgf_const_add, mul_comm]
 
 /-- This is a trivial application of `IndepFun.comp` but it will come up frequently. -/
 theorem IndepFun.exp_mul {X Y : Ω → ℝ} (h_indep : IndepFun X Y μ) (s t : ℝ) :

From 9b15b4ed97a815685c2aa209b1618dec5c36426b Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Tue, 31 Dec 2024 19:47:24 +0000
Subject: [PATCH 19/22] Apply suggestions.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 7 ++-----
 1 file changed, 2 insertions(+), 5 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index acf062ad25411c..b010370186d328 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -365,14 +365,11 @@ theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
   calc
   mgf X p t = (p.map X)[fun x => exp (t * x)] := by
     rw [← mgf_id_map, mgf]
-    · rfl
-    · apply AEMeasurable.of_map_ne_zero
-      rw [hX]
-      exact IsProbabilityMeasure.ne_zero (gaussianReal μ v)
+    all_goals {simp [AEMeasurable.of_map_ne_zero, hX, IsProbabilityMeasure.ne_zero]}
   _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
     simp [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def, ENNReal.ofReal,
       integral_withDensity_eq_integral_smul (measurable_gaussianPDFReal μ v).real_toNNReal,
-      NNReal.smul_def, coe_toNNReal', gaussianPDFReal_nonneg, sup_of_le_left, smul_eq_mul, mul_comm]
+      NNReal.smul_def, gaussianPDFReal_nonneg, mul_comm]
   _ = exp (μ * t + v * t ^ 2 / 2)
       * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
     rw [gaussianPDFReal_def, ← integral_mul_left]

From 74a1cad1db64640f04a0a436f2fdd2a90cae3f9d Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Wed, 1 Jan 2025 23:56:59 +0000
Subject: [PATCH 20/22] Apply suggestions.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 2 +-
 Mathlib/Probability/Moments.lean                | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index b010370186d328..91957996504232 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -365,7 +365,7 @@ theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
   calc
   mgf X p t = (p.map X)[fun x => exp (t * x)] := by
     rw [← mgf_id_map, mgf]
-    all_goals {simp [AEMeasurable.of_map_ne_zero, hX, IsProbabilityMeasure.ne_zero]}
+    all_goals simp [AEMeasurable.of_map_ne_zero, hX, IsProbabilityMeasure.ne_zero]
   _ = ∫ x, exp (t * x) * gaussianPDFReal μ v x := by
     simp [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def, ENNReal.ofReal,
       integral_withDensity_eq_integral_smul (measurable_gaussianPDFReal μ v).real_toNNReal,
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index 0c84543fb70b76..ca856f722de3b1 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -184,7 +184,7 @@ lemma mgf_id_map (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ := by
   ext t
   rw [mgf, integral_map hX]
   · rfl
-  · exact (measurable_exp.comp (measurable_const_mul _)).aestronglyMeasurable
+  · exact (measurable_const_mul _).exp.aestronglyMeasurable
 
 theorem mgf_neg : mgf (-X) μ t = mgf X μ (-t) := by simp_rw [mgf, Pi.neg_apply, mul_neg, neg_mul]
 

From bff656c55a1f853f31dd95cfc000479f4a022d3b Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= <yael.dillies@gmail.com>
Date: Thu, 2 Jan 2025 09:32:10 +0000
Subject: [PATCH 21/22] golf

---
 .../Function/SpecialFunctions/Basic.lean      | 19 +++++++------------
 .../Probability/Distributions/Gaussian.lean   |  9 +++------
 2 files changed, 10 insertions(+), 18 deletions(-)

diff --git a/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean b/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
index b866f1253eceb2..231fd905364ef0 100644
--- a/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
+++ b/Mathlib/MeasureTheory/Function/SpecialFunctions/Basic.lean
@@ -136,32 +136,27 @@ variable {α : Type*} {m : MeasurableSpace α} {f : α → ℝ} (hf : Measurable
 include hf
 
 @[measurability]
-theorem Measurable.exp : Measurable fun x => Real.exp (f x) :=
+protected theorem Measurable.exp : Measurable fun x => Real.exp (f x) :=
   Real.measurable_exp.comp hf
 
 @[measurability]
-theorem Measurable.log : Measurable fun x => log (f x) :=
+protected theorem Measurable.log : Measurable fun x => log (f x) :=
   measurable_log.comp hf
 
 @[measurability]
-theorem Measurable.cos : Measurable fun x => Real.cos (f x) :=
-  Real.measurable_cos.comp hf
+protected theorem Measurable.cos : Measurable fun x ↦ cos (f x) := measurable_cos.comp hf
 
 @[measurability]
-theorem Measurable.sin : Measurable fun x => Real.sin (f x) :=
-  Real.measurable_sin.comp hf
+protected theorem Measurable.sin : Measurable fun x ↦ sin (f x) := measurable_sin.comp hf
 
 @[measurability]
-theorem Measurable.cosh : Measurable fun x => Real.cosh (f x) :=
-  Real.measurable_cosh.comp hf
+protected theorem Measurable.cosh : Measurable fun x ↦ cosh (f x) := measurable_cosh.comp hf
 
 @[measurability]
-theorem Measurable.sinh : Measurable fun x => Real.sinh (f x) :=
-  Real.measurable_sinh.comp hf
+protected theorem Measurable.sinh : Measurable fun x ↦ sinh (f x) := measurable_sinh.comp hf
 
 @[measurability]
-theorem Measurable.sqrt : Measurable fun x => √(f x) :=
-  continuous_sqrt.measurable.comp hf
+protected theorem Measurable.sqrt : Measurable fun x => √(f x) := continuous_sqrt.measurable.comp hf
 
 end RealComposition
 
diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index 91957996504232..b21a2f5d2d74aa 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -370,16 +370,13 @@ theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     simp [hX, gaussianReal_of_var_ne_zero μ hv, gaussianPDF_def, ENNReal.ofReal,
       integral_withDensity_eq_integral_smul (measurable_gaussianPDFReal μ v).real_toNNReal,
       NNReal.smul_def, gaussianPDFReal_nonneg, mul_comm]
-  _ = exp (μ * t + v * t ^ 2 / 2)
-      * ∫ x, (√(2 * π * v))⁻¹ * exp (-(x - (μ + v * t)) ^ 2 / (2 * v)) := by
-    rw [gaussianPDFReal_def, ← integral_mul_left]
+  _ = ∫ x, exp (μ * t + v * t ^ 2 / 2) * gaussianPDFReal (μ + v * t) v x := by
+    simp only [gaussianPDFReal_def, mul_left_comm (exp _), mul_assoc, ← exp_add]
     congr with x
     field_simp only [mul_left_comm, ← exp_sub, ← exp_add]
     ring_nf
-  _ = exp (μ * t + v * t ^ 2 / 2) * ∫ x, gaussianPDFReal (μ + v * t) v x := by
-    field_simp [gaussianPDFReal_def]
   _ = exp (μ * t + v * t ^ 2 / 2) := by
-    rw [integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
+    rw [integral_mul_left, integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]
 
 theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     cgf X p t = μ * t + v * t ^ 2 / 2 := by

From 3d9fb9e50761ec122fc502368f7d523bcf3f471a Mon Sep 17 00:00:00 2001
From: Vasily Ilin <vasilin97@gmail.com>
Date: Thu, 2 Jan 2025 19:07:21 +0000
Subject: [PATCH 22/22] Move `mgf_dirac` from `Guassian` to `Moments`.

---
 Mathlib/Probability/Distributions/Gaussian.lean | 7 -------
 Mathlib/Probability/Moments.lean                | 5 +++++
 2 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/Mathlib/Probability/Distributions/Gaussian.lean b/Mathlib/Probability/Distributions/Gaussian.lean
index b21a2f5d2d74aa..41df4ffe5d082e 100644
--- a/Mathlib/Probability/Distributions/Gaussian.lean
+++ b/Mathlib/Probability/Distributions/Gaussian.lean
@@ -350,13 +350,6 @@ open Measurable Real
 
 variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {p : Measure Ω} {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
 
-lemma mgf_dirac (hX : p.map X = .dirac μ) (t : ℝ) : mgf X p t = exp (μ * t) := by
-  rw [← mgf_id_map, mgf, hX, integral_dirac, mul_comm]
-  · rfl
-  · apply AEMeasurable.of_map_ne_zero
-    rw [hX]
-    exact IsProbabilityMeasure.ne_zero (.dirac μ)
-
 theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
     mgf X p t = exp (μ * t + v * t ^ 2 / 2) := by
   by_cases hv : v = 0
diff --git a/Mathlib/Probability/Moments.lean b/Mathlib/Probability/Moments.lean
index ca856f722de3b1..41fb7a9465a194 100644
--- a/Mathlib/Probability/Moments.lean
+++ b/Mathlib/Probability/Moments.lean
@@ -349,6 +349,11 @@ theorem measure_le_le_exp_cgf [IsFiniteMeasure μ] (ε : ℝ) (ht : t ≤ 0)
   rw [exp_add]
   exact mul_le_mul le_rfl (le_exp_log _) mgf_nonneg (exp_pos _).le
 
+lemma mgf_dirac {x : ℝ} (hX : μ.map X = .dirac x) (t : ℝ) : mgf X μ t = exp (x * t) := by
+  have : IsProbabilityMeasure (μ.map X) := by rw [hX]; infer_instance
+  rw [← mgf_id_map (.of_map_ne_zero <| IsProbabilityMeasure.ne_zero _), mgf, hX, integral_dirac,
+    mul_comm, id_def]
+
 end MomentGeneratingFunction
 
 end ProbabilityTheory