awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
x : ℝ
⊢ cexp (-HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ)) =
    cexp
      (-(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
        -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
have e_a : -HPow.hPow (β := ℕ) ((↑x : ℂ) - (↑μ : ℂ)) 2 / (2 * (↑(↑v : ℝ) : ℂ)) + z * (↑x : ℂ) =
  -(2 * (↑(↑v : ℝ) : ℂ))⁻¹ * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
    -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ))
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
have rw : (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
    (((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))) =
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
Tactic: rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
rw :
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      (((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
        cexp
          (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
            HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
⊢ ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
have rw₁ : (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
Tactic: rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
have e_a : (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) = 1
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) = 1
have e_a : HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(HPow.hPow (β := ℝ) (2 * π * (↑v : ℝ)) 2⁻¹) : ℂ)
Tactic: simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(HPow.hPow (β := ℝ) (2 * π * (↑v : ℝ)) 2⁻¹) : ℂ)
have e_a : HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(2 * π * (↑v : ℝ)) : ℂ) ^ (↑2⁻¹ : ℂ)
Tactic: rw [Complex.ofReal_cpow (by positivity)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = (↑(2 * π * (↑v : ℝ)) : ℂ) ^ (↑2⁻¹ : ℂ)
have e_a : HPow.hPow (β := ℂ) ((↑π : ℂ) * (2 * (↑(↑v : ℝ) : ℂ))) 2⁻¹ = HPow.hPow (β := ℂ) (2 * (↑π : ℂ) * (↑(↑v : ℝ) : ℂ)) 2⁻¹
Tactic: push_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ 1 *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have rw : cexp
    (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
      HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
  cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: rw [one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have e_z : -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
    HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) =
  z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
      HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) =
    z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2
have this : (↑(↑v : ℝ) : ℂ) ≠ 0
Tactic: have : (v : ℂ) ≠ 0 := by simpa
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
this : (↑(↑v : ℝ) : ℂ) ≠ 0
⊢ -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
      HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) =
    z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2
have e_z : -(HPow.hPow (β := ℕ) (↑μ : ℂ) 2 * 4) +
    HPow.hPow (α := ℂ) (β := ℕ) 2 2 * HPow.hPow (β := ℕ) ((↑(↑v : ℝ) : ℂ) * z + (↑μ : ℂ)) 2 =
  4 * (↑(↑v : ℝ) : ℂ) * z * ((↑μ : ℂ) * 2 + (↑(↑v : ℝ) : ℂ) * z)
Tactic: simp [field]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have calc : Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
    (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
Tactic: calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
calc :
  Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have calc₁ : (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
    (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ))) =
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      cexp
        (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
          -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
Tactic: calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
calc :
  Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
calc₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have calc₂ : ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      cexp
        (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
          -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
  (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
Tactic: calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
z : ℂ
hv : ¬v = 0
calc :
  Eq (α := ℂ) (∫ (x : ℝ), cexp (z * (↑x : ℂ)) ∂gaussianReal μ v)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ)))
calc₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
      (↑(gaussianPDFReal μ v x) : ℂ) * cexp (z * (↑x : ℂ))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))
calc₂ :
  ((↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) *
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace ℙ fun (x : ℝ) ↦
        cexp
          (-(↑(↑(2 * v)⁻¹ : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑x : ℂ) 2 + (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) * (↑x : ℂ) +
            -HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)))) =
    (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
      cexp
        (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
          HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
⊢ complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have calc₃ : (↑(√(2 * π * (↑v : ℝ)))⁻¹ : ℂ) * ((↑π : ℂ) / - -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)) ^ (1 / 2) *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ))) =
  1 *
    cexp
      (-HPow.hPow (β := ℕ) (↑μ : ℂ) 2 / (2 * (↑(↑v : ℝ) : ℂ)) -
        HPow.hPow (β := ℕ) (z + (↑μ : ℂ) / (↑(↑v : ℝ) : ℂ)) 2 / (4 * -(↑(↑(2 * v)⁻¹ : ℝ) : ℂ)))
Tactic: calc ∫ x, cexp (z * x) ∂gaussianReal μ v
    _ = ∫ x, gaussianPDFReal μ v x * cexp (z * x) ∂ℙ := by
      simp_rw [integral_gaussianReal_eq_integral_smul hv, Complex.real_smul]
    _ = (√(2 * π * v))⁻¹
        * ∫ x : ℝ, cexp (-(2 * v)⁻¹ * x ^ 2 + (z + μ / v) * x + -μ ^ 2 / (2 * v)) ∂ℙ := by
      unfold gaussianPDFReal
      push_cast
      simp_rw [mul_assoc, integral_const_mul, ← Complex.exp_add]
      congr with x
      congr 1
      ring
    _ = (√(2 * π * v))⁻¹ * (π / - -(2 * v)⁻¹) ^ (1 / 2 : ℂ)
        * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      rw [integral_cexp_quadratic (by simpa using pos_iff_ne_zero.mpr hv), ← mul_assoc]
    _ = 1 * cexp (-μ ^ 2 / (2 * v) - (z + μ / v) ^ 2 / (4 * -(2 * v)⁻¹)) := by
      congr 1
      simp only [field, sqrt_eq_rpow, one_div, ofReal_inv, NNReal.coe_inv, NNReal.coe_mul,
        NNReal.coe_ofNat, ofReal_mul, ofReal_ofNat, neg_neg, div_inv_eq_mul,
        ne_eq, ofReal_eq_zero, rpow_eq_zero, not_false_eq_true]
      rw [Complex.ofReal_cpow (by positivity)]
      push_cast
      ring_nf
    _ = cexp (z * μ + v * z ^ 2 / 2) := by
      rw [one_mul]
      congr 1
      have : (v : ℂ) ≠ 0 := by simpa
      simp [field]
      ring
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ NeZero (R := Measure ℝ) (Measure.map X p)
have rw : NeZero (gaussianReal μ v)
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
⊢ complexMGF X p z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have hX_meas : AEMeasurable X p
Tactic: have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
⊢ complexMGF X p z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have rw : complexMGF (m := Real.measurableSpace) id (Measure.map X p) z =
  cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
rw :
  complexMGF (m := Real.measurableSpace) id (Measure.map X p) z =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF X p z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have rw₁ : complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
z : ℂ
hX_meas : AEMeasurable X p
rw :
  complexMGF (m := Real.measurableSpace) id (Measure.map X p) z =
    cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
rw₁ : complexMGF id (gaussianReal μ v) z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
⊢ complexMGF X p z = cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
have rw₂ : cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2) =
  cexp (z * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) z 2 / 2)
Tactic: rw [← complexMGF_id_map hX_meas, hX, complexMGF_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ charFun (gaussianReal μ v) t = cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
have rw : cexp ((↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2) =
  cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
Tactic: rw [← complexMGF_id_mul_I, complexMGF_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ cexp ((↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2) =
    cexp ((↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
have e_z : (↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2 =
  (↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ (↑t : ℂ) * I * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) ((↑t : ℂ) * I) 2 / 2 =
    (↑t : ℂ) * (↑μ : ℂ) * I - (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2
have e_z : (↑t : ℂ) * I * (↑μ : ℂ) + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2) / 2 =
  (↑t : ℂ) * (↑μ : ℂ) * I + -((↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2)
Tactic: simp only [mul_pow, I_sq, mul_neg, mul_one, sub_eq_add_neg]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : 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 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have suffices : (↑(mgf X p t) : ℂ) = (↑(rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
Tactic: suffices (mgf X p t : ℂ) = rexp (μ * t + ↑v * t ^ 2 / 2) from mod_cast this
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ NeZero (R := Measure ℝ) (Measure.map X p)
have rw : NeZero (gaussianReal μ v)
Tactic: rw [hX]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
Ω : 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 : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
have hX_meas : AEMeasurable X p
Tactic: have hX_meas : AEMeasurable X p := aemeasurable_of_map_neZero (by rw [hX]; infer_instance)
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
⊢ (↑(mgf X p t) : ℂ) = (↑(rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
have rw : cexp ((↑t : ℂ) * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
  (↑(rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
Tactic: rw [← mgf_id_map hX_meas, ← complexMGF_ofReal, hX, complexMGF_id_gaussianReal, mul_comm μ]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
hX_meas : AEMeasurable X p
⊢ cexp ((↑t : ℂ) * (↑μ : ℂ) + (↑(↑v : ℝ) : ℂ) * HPow.hPow (β := ℕ) (↑t : ℂ) 2 / 2) =
    (↑(rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) : ℂ)
have norm_cast : rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) = rexp (t * μ + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) = fun (t : ℝ) ↦ rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : ∀ (t : ℝ), mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) t = rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: ext t