[Merged by Bors] - feat(Probability/Distributions/Gaussian): the mgf of a gaussian

Mathlib/MeasureTheory/Measure/MeasureSpace.lean

@@ -1194,6 +1194,9 @@ 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 _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 μ
   · have hg : AEMeasurable g μ := hf.congr h

Mathlib/Probability/Distributions/Gaussian.lean

@@ -4,8 +4,7 @@ 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
 
 /-!
 # Gaussian distributions over ℝ
@@ -347,6 +346,35 @@ lemma gaussianReal_mul_const {X : Ω → ℝ} (hX : Measure.map X ℙ = gaussian
 
 end Transformations
 
+open Measurable Real
+
+variable {Ω : Type*} {mΩ : MeasurableSpace Ω} {p : Measure Ω} {μ : ℝ} {v : ℝ≥0} {X : Ω → ℝ}
+
+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
+    simp [mgf_dirac hX, hv]
+  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]
+  _ = ∫ 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, gaussianPDFReal_nonneg, mul_comm]
+  _ = ∫ 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) := by
+    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
+  rw [cgf, mgf_gaussianReal hX t, log_exp]
+
 end GaussianReal
 
 end ProbabilityTheory

Mathlib/Probability/Moments.lean

@@ -180,13 +180,28 @@ 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 (hX : AEMeasurable X μ) : mgf id (μ.map X) = mgf X μ := by
+  ext t
+  rw [mgf, integral_map hX]
+  · rfl
+  · 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]
 
 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 (α : ℝ) : 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 = 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 : ℝ) :
     IndepFun (fun ω => exp (s * X ω)) (fun ω => exp (t * Y ω)) μ := by
@@ -334,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