-- Mathlib/Probability/Distributions/Gaussian.lean
theorem mgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
    mgf X p t = exp (μ * t + v * t ^ 2 / 2)

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ mgf X p t = ∫ (x : ℝ), (fun x => rexp (t * x)) x ∂Measure.map X p

Tactic:
rw [← mgf_id_map, mgf]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (fun ω => rexp (t * id ω)) x ∂Measure.map X p = ∫ (x : ℝ), (fun x => rexp (t * x)) x ∂Measure.map X p

Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ AEMeasurable X p

Proof state:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
x : ℝ
⊢ 1 * rexp ((t * x * (2 * ↑v) + -(x - μ) ^ 2) / (2 * ↑v)) * √(π * (2 * ↑v)) =
    1 * rexp ((2 * ((μ * t * 2 + ↑v * t ^ 2) * ↑v) + -(x - (μ + ↑v * t)) ^ 2 * 2) / (2 * (2 * ↑v))) * √(π * (2 * ↑v))

Tactic:
ring_nf

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (√(2 * (π * ↑v)))⁻¹ * rexp (t * x + -(x - μ) ^ 2 / (2 * ↑v)) =
    ∫ (x : ℝ), (√(2 * (π * ↑v)))⁻¹ * rexp (μ * t + ↑v * t ^ 2 / 2 + -(x - (μ + ↑v * t)) ^ 2 / (2 * ↑v))

Tactic:
congr with x

Result:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
x : ℝ
⊢ (√(2 * (π * ↑v)))⁻¹ * rexp (t * x + -(x - μ) ^ 2 / (2 * ↑v)) =
    (√(2 * (π * ↑v)))⁻¹ * rexp (μ * t + ↑v * t ^ 2 / 2 + -(x - (μ + ↑v * t)) ^ 2 / (2 * ↑v))

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), rexp (t * x) * gaussianPDFReal μ v x =
    ∫ (x : ℝ), rexp (μ * t + ↑v * t ^ 2 / 2) * gaussianPDFReal (μ + ↑v * t) v x

Tactic:
simp only [gaussianPDFReal_def, mul_left_comm (exp _), mul_assoc, ← exp_add]

Result:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (√(2 * (π * ↑v)))⁻¹ * rexp (t * x + -(x - μ) ^ 2 / (2 * ↑v)) =
    ∫ (x : ℝ), (√(2 * (π * ↑v)))⁻¹ * rexp (μ * t + ↑v * t ^ 2 / 2 + -(x - (μ + ↑v * t)) ^ 2 / (2 * ↑v))

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ AEMeasurable X p

Tactic:
simp [AEMeasurable.of_map_ne_zero, hX, IsProbabilityMeasure.ne_zero]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
by_cases hv : v = 0

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : v = 0
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Proof state:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
x : ℝ
⊢ (√(2 * (π * ↑v)))⁻¹ * rexp (t * x + -(x - μ) ^ 2 / (2 * ↑v)) =
    (√(2 * (π * ↑v)))⁻¹ * rexp (μ * t + ↑v * t ^ 2 / 2 + -(x - (μ + ↑v * t)) ^ 2 / (2 * ↑v))

Tactic:
field_simp only [mul_left_comm, ← exp_sub, ← exp_add]

Result:
case e_f.h
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
x : ℝ
⊢ 1 * rexp ((t * x * (2 * ↑v) + -(x - μ) ^ 2) / (2 * ↑v)) * √(π * (2 * ↑v)) =
    1 * rexp ((2 * ((μ * t * 2 + ↑v * t ^ 2) * ↑v) + -(x - (μ + ↑v * t)) ^ 2 * 2) / (2 * (2 * ↑v))) * √(π * (2 * ↑v))

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (fun ω => rexp (t * id ω)) x ∂Measure.map X p = ∫ (x : ℝ), (fun x => rexp (t * x)) x ∂Measure.map X p

Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ AEMeasurable X p

Tactic:
all_goals simp [AEMeasurable.of_map_ne_zero, hX, IsProbabilityMeasure.ne_zero]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
t : ℝ
hv : v = 0
hX : Measure.map X p = Measure.dirac μ
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
simp [mgf_dirac hX, hv]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), (fun x => rexp (t * x)) x ∂Measure.map X p = ∫ (x : ℝ), rexp (t * x) * gaussianPDFReal μ v x

Tactic:
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]

Result:
no goals

Proof state:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : v = 0
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
simp only [gaussianReal, hv, ↓reduceIte] at hX

Result:
case pos
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
t : ℝ
hv : v = 0
hX : Measure.map X p = Measure.dirac μ
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Proof state:
case neg
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ mgf X p t = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
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]

Result:
no goals

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hv : ¬v = 0
⊢ ∫ (x : ℝ), rexp (μ * t + ↑v * t ^ 2 / 2) * gaussianPDFReal (μ + ↑v * t) v x = rexp (μ * t + ↑v * t ^ 2 / 2)

Tactic:
rw [integral_mul_left, integral_gaussianPDFReal_eq_one (μ + v * t) hv, mul_one]

Result:
no goals