awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ mgf (fun (x : ℝ) ↦ x) (gaussianReal μ v) t = rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : Measure.map (fun (x : ℝ) ↦ x) (gaussianReal μ v) = gaussianReal μ v
Tactic: rw [mgf_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
t : ℝ
⊢ cgf X p t = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have rw : Real.log (mgf X p t) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [cgf, mgf_gaussianReal hX t, Real.log_exp]
-- 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 : ℝ
rw : Real.log (mgf X p t) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ cgf X p t = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have rw₁ : Real.log (rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [cgf, mgf_gaussianReal hX t, Real.log_exp]
-- 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 : ℝ
rw : Real.log (mgf X p t) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
rw₁ : Real.log (rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
⊢ cgf X p t = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
have rw₂ : μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2 = μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2
Tactic: rw [cgf, mgf_gaussianReal hX t, Real.log_exp]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ Integrable (ε := ℝ) (fun (x : ℝ) ↦ rexp (t * x)) (gaussianReal μ v)
have rw : 0 < rexp (μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [← mgf_pos_iff, mgf_gaussianReal (μ := μ) (v := v) (by simp)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ integrableExpSet id (gaussianReal μ v) = Set.univ
have h : ∀ (x : ℝ), x ∈ integrableExpSet id (gaussianReal μ v) ↔ Membership.mem (γ := Set ℝ) Set.univ x
Tactic: ext
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ ∫ (x : ℝ), x ∂gaussianReal μ v = μ
have rw : rexp (μ * 0 + (↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) *
    deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
  μ
Tactic: rw [← deriv_mgf_zero (by simp), mgf_fun_id_gaussianReal, _root_.deriv_exp (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ rexp (μ * 0 + (↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) *
      deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
    μ
have simp : deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 = μ
Tactic: simp only [mul_zero, ne_eq, OfNat.ofNat_ne_zero, not_false_eq_true, zero_pow, zero_div,
    add_zero, Real.exp_zero, one_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ deriv (fun (t : ℝ) ↦ μ * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 = μ
have rw : HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ μ) 0) 0 + μ * deriv (fun (y : ℝ) ↦ y) 0 +
    deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) 0 =
  μ
Tactic: rw [deriv_fun_add (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ Var[fun (x : ℝ) ↦ x; gaussianReal μ v] = (↑v : ℝ)
have rw : ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - ∫ (x : ℝ), x ∂gaussianReal μ v) 2 ∂gaussianReal μ v = (↑v : ℝ)
Tactic: rw [variance_eq_integral measurable_id'.aemeasurable]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - ∫ (x : ℝ), x ∂gaussianReal μ v) 2 ∂gaussianReal μ v = (↑v : ℝ)
have simp : ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
Tactic: simp only [integral_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
have rw : Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
  (∫ (x : ℝ), HPow.hPow (β := ℕ) (x - μ) 2 ∂gaussianReal μ v)
Tactic: rw [integral_map (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0
have rw : Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
  (∫ (x : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℕ) (fun (x : ℝ) ↦ x) 2 x ∂gaussianReal 0 v)
Tactic: rw [iteratedDeriv_mgf_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
rw :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
    (∫ (x : ℝ), HPow.hPow (α := ℝ → ℝ) (β := ℕ) (fun (x : ℝ) ↦ x) 2 x ∂gaussianReal 0 v)
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0
have h : 0 ∈ interior (integrableExpSet (fun (x : ℝ) ↦ x) (gaussianReal 0 v))
Tactic: rw [iteratedDeriv_mgf_zero]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0 = (↑v : ℝ)
have rw : deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp (0 * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
Tactic: rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp (0 * t + (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
have simp : deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
Tactic: simp only [zero_mul, zero_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : ∀ (t : ℝ),
  deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: ext t
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) t =
  (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: rw [_root_.deriv_exp (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
t : ℝ
⊢ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * deriv (fun (t : ℝ) ↦ (↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) t =
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
have h : rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2) * ((↑v : ℝ) * (2 * t) / 2) =
  (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
⊢ deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
have this : Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
  (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
Tactic: have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
this :
  Eq (α := (x : ℝ) → ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) fun (t : ℝ) ↦
    (↑v : ℝ) * t * rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)
⊢ deriv (𝕜 := ℝ) (deriv fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 = (↑v : ℝ)
have rw : (HMul.hMul (α := ℝ) (deriv (fun (y : ℝ) ↦ (↑v : ℝ)) 0) 0 + (↑v : ℝ) * deriv (fun (y : ℝ) ↦ y) 0) *
      rexp ((↑v : ℝ) * HPow.hPow (α := ℝ) (β := ℕ) 0 2 / 2) +
    (↑v : ℝ) * 0 * deriv (fun (t : ℝ) ↦ rexp ((↑v : ℝ) * HPow.hPow (β := ℕ) t 2 / 2)) 0 =
  (↑v : ℝ)
Tactic: rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
have calc : Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
    HPow.hPow (β := ℕ) ω 2)
Tactic: calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
calc :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
have calc₁ : Eq (α := ℝ)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
    HPow.hPow (β := ℕ) ω 2)
  (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
Tactic: calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
calc :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
calc₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
    (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
have calc₂ : ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0
Tactic: calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
calc :
  Eq (α := ℝ) (∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
calc₁ :
  Eq (α := ℝ)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (fun (x : ℝ) ↦ x - μ) (gaussianReal μ v)) fun (ω : ℝ) ↦
      HPow.hPow (β := ℕ) ω 2)
    (∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v)
calc₂ :
  ∫ (ω : ℝ), HPow.hPow (β := ℕ) ω 2 ∂gaussianReal 0 v = iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0
⊢ ∫ (ω : ℝ), HPow.hPow (β := ℕ) (ω - μ) 2 ∂gaussianReal μ v = (↑v : ℝ)
have calc₃ : iteratedDeriv 2 (mgf (fun (x : ℝ) ↦ x) (gaussianReal 0 v)) 0 = (↑v : ℝ)
Tactic: calc ∫ ω, (ω - μ) ^ 2 ∂gaussianReal μ v
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal μ v).map (fun x ↦ x - μ) := by
    rw [integral_map (by fun_prop) (by fun_prop)]
  _ = ∫ ω, ω ^ 2 ∂(gaussianReal 0 v) := by simp [gaussianReal_map_sub_const]
  _ = iteratedDeriv 2 (mgf (fun x ↦ x) (gaussianReal 0 v)) 0 := by
    rw [iteratedDeriv_mgf_zero] <;> simp
  _ = v := by
    rw [mgf_fun_id_gaussianReal, iteratedDeriv_succ, iteratedDeriv_one]
    simp only [zero_mul, zero_add]
    have : deriv (fun t ↦ rexp (v * t ^ 2 / 2)) = fun t ↦ v * t * rexp (v * t ^ 2 / 2) := by
      ext t
      rw [_root_.deriv_exp (by fun_prop)]
      simp only [deriv_div_const, differentiableAt_const, differentiableAt_fun_id, Nat.cast_ofNat,
        DifferentiableAt.fun_pow, deriv_fun_mul, deriv_const', zero_mul, deriv_fun_pow,
        Nat.add_one_sub_one, pow_one, deriv_id'', mul_one, zero_add]
      ring
    rw [this, deriv_fun_mul (by fun_prop) (by fun_prop), deriv_fun_mul (by fun_prop) (by fun_prop)]
    simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
p : ℝ≥0∞
hp : p ≠ ∞
⊢ MemLp id p (gaussianReal μ v)
have lift : ∀ (p : ℝ≥0), MemLp id (↑p : ℝ≥0∞) (gaussianReal μ v)
Tactic: lift p to ℝ≥0 using hp
Cleared hypotheses: p, hp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂ ↔ μ₁ = μ₂ ∧ v₁ = v₂
have refine : ∀ (h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂), μ₁ = μ₂ ∧ v₁ = v₂
Tactic: refine ⟨fun h ↦ ?_, by rintro ⟨rfl, rfl⟩; rfl⟩
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ μ₁ = μ₂ ∧ v₁ = v₂
have rw : Eq (α := ℝ) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) ∧ v₁ = v₂
Tactic: rw [← integral_id_gaussianReal (μ := μ₁) (v := v₁),
    ← integral_id_gaussianReal (μ := μ₂) (v := v₂), h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ Eq (α := ℝ) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) (∫ (x : ℝ), x ∂gaussianReal μ₂ v₂) ∧ v₁ = v₂
have simp : v₁ = v₂
Tactic: simp only [integral_id_gaussianReal, true_and]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ v₁ = v₂
have suffices : (↑v₁ : ℝ) = (↑v₂ : ℝ)
Tactic: suffices (v₁ : ℝ) = v₂ by simpa
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
⊢ (↑v₁ : ℝ) = (↑v₂ : ℝ)
have rw : Var[id; gaussianReal μ₁ v₁] = (↑v₂ : ℝ)
Tactic: rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
rw : Var[id; gaussianReal μ₁ v₁] = (↑v₂ : ℝ)
⊢ (↑v₁ : ℝ) = (↑v₂ : ℝ)
have rw₁ : Var[id; gaussianReal μ₁ v₁] = Var[id; gaussianReal μ₂ v₂]
Tactic: rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ₁ μ₂ : ℝ
v₁ v₂ : ℝ≥0
h : gaussianReal μ₁ v₁ = gaussianReal μ₂ v₂
rw : Var[id; gaussianReal μ₁ v₁] = (↑v₂ : ℝ)
rw₁ : Var[id; gaussianReal μ₁ v₁] = Var[id; gaussianReal μ₂ v₂]
⊢ (↑v₁ : ℝ) = (↑v₂ : ℝ)
have rw₂ : Var[id; gaussianReal μ₂ v₂] = Var[id; gaussianReal μ₂ v₂]
Tactic: rw [← variance_id_gaussianReal (μ := μ₁) (v := v₁),
    ← variance_id_gaussianReal (μ := μ₂) (v := v₂), h]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal ((L : (a : ℝ) → ℝ) μ) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v)
have this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
Tactic: have : (L : ℝ → ℝ) = fun x ↦ L 1 * x := by simp
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
⊢ Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v) =
    gaussianReal ((L : (a : ℝ) → ℝ) μ) ((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v)
have rw : gaussianReal (HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) μ)
    (NNReal.mk (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) sorry * v) =
  gaussianReal ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) μ)
    ((HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2).toNNReal * v)
Tactic: rw [this, gaussianReal_map_const_mul]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
⊢ gaussianReal (HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) μ)
      (NNReal.mk (HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2) ⋯ * v) =
    gaussianReal ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) μ)
      ((HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2).toNNReal * v)
have e_v : HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
  max (HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2) 0
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
this : Eq (α := (a : ℝ) → ℝ) (⇑L : (a : ℝ) → ℝ) fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x
⊢ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2 =
    max (HPow.hPow (α := ℝ) (β := ℕ) ((fun (x : ℝ) ↦ HMul.hMul (α := ℝ) ((L : (a : ℝ) → ℝ) 1 : ℝ) x) 1) 2) 0
have e_v : 0 ≤ HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2
Tactic: simp only [mul_one, left_eq_sup]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
    (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)) fun (x : ℝ) ↦ x)
have rw : Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
Tactic: rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (hypothesis)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v : ℝ) ((L : (a : ℝ) → ℝ) μ : ℝ)
have this : Eq (α := ℝ) (∫ (x : ℝ), (L : (a : ℝ) → ℝ) x ∂gaussianReal μ v)
  (@integral _ _ _ _ Real.measurableSpace (Measure.map (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)) fun (x : ℝ) ↦ x)
Tactic: have : ∫ x, L x ∂(gaussianReal μ v) = ∫ x, x ∂((gaussianReal μ v).map L) := by
    rw [integral_map (φ := L) (by fun_prop) (by fun_prop)]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
⊢ Var[(⇑L : (a : ℝ) → ℝ); gaussianReal μ v] =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)
have rw : (↑((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) : ℝ) =
  (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)
Tactic: rw [← variance_id_map, gaussianReal_map_linearMap, variance_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
μ : ℝ
v : ℝ≥0
L : ℝ →ₗ[ℝ] ℝ
rw :
  (↑((HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal * v) : ℝ) =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)
⊢ Var[(⇑L : (a : ℝ) → ℝ); gaussianReal μ v] =
    (↑(HPow.hPow (α := ℝ) (β := ℕ) ((L : (a : ℝ) → ℝ) 1 : ℝ) 2).toNNReal : ℝ) * (↑v : ℝ)
have rw₁ : AEMeasurable (β := ℝ) (⇑L : (a : ℝ) → ℝ) (gaussianReal μ v)
Tactic: rw [← variance_id_map, gaussianReal_map_linearMap, variance_id_gaussianReal]
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂ = gaussianReal (m₁ + m₂) (v₁ + v₂)
have refine : charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂))
Tactic: refine Measure.ext_of_charFun ?_
-- Lean 4 proof step from Mathlib.Probability.Distributions.Gaussian.Real (goal)
Goal:
m₁ m₂ : ℝ
v₁ v₂ : ℝ≥0
⊢ charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂))
have h : ∀ (t : ℝ), charFun (gaussianReal m₁ v₁ ∗ gaussianReal m₂ v₂) t = charFun (gaussianReal (m₁ + m₂) (v₁ + v₂)) t
Tactic: ext t