awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
e_a :
  HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2 =
    HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) *
          ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) /
        mgf X μ v -
      HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2
⊢ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v / mgf X μ v
have e_a₁ : mgf X μ v ≠ 0
Tactic: rw [mul_div_cancel_right₀, deriv_cgf h]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v =
    (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v
have e_a : ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
      HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  ∫ (ω : Ω),
    (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
      rexp (v * X ω) ∂μ
Tactic: congr 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
        rexp (v * X ω) ∂μ
have e_a : ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
      HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  ∫ (ω : Ω),
    HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ
Tactic: simp_rw [add_mul, sub_mul]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
have simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * (X ω * (rexp (v * X ω) * deriv (cgf X μ) v))) μ
Tactic: simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * (X ω * (rexp (v * X ω) * deriv (cgf X μ) v))) μ
have refine : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * (rexp (v * X ω) * deriv (cgf X μ) v)) μ
Tactic: refine Integrable.const_mul ?_ _
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * (rexp (v * X ω) * deriv (cgf X μ) v)) μ
have simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω) * deriv (cgf X μ) v) μ
Tactic: simp_rw [← mul_assoc]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω) * deriv (cgf X μ) v) μ
have refine : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) μ
Tactic: refine Integrable.mul_const ?_ _
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) μ
have h₁ : ∀ (x : Ω), X x = HPow.hPow (β := ℕ) (X x) 1
Tactic: convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (hypothesis)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ
have h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
Tactic: have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ := by
      simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc]
      refine Integrable.mul_const ?_ _
      convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
      simp
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ
have e_a : ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
      HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  HAdd.hAdd (α := ℝ)
    (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
    (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HAdd.hAdd (α := ℝ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ
have e_a₁ : Integrable (ε := ℝ)
  (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HAdd.hAdd (α := ℝ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)
e_a₁ :
  Integrable (ε := ℝ)
    (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (ω : Ω),
      HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω) +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ
have e_a₂ : Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X ω)) μ
Tactic: rw [integral_add]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HAdd.hAdd (α := ℝ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) - 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
      (∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ)
have e_a : ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
      HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  HSub.hSub (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) ∂μ)
      (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ) +
    ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
Tactic: rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HSub.hSub (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) ∂μ)
        (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ) +
      ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
have e_a : HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
  ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ
⊢ ∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HSub.hSub (α := ℝ) (∫ (a : Ω), HPow.hPow (β := ℕ) (X a) 2 * rexp (v * X a) ∂μ)
        (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ) +
      ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
have e_a₁ : HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
Tactic: congr
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ
have e_a : Eq (α := ℝ) (∫ (a : Ω), 2 * (X a * rexp (v * X a)) * deriv (cgf X μ) v ∂μ)
  (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
Tactic: rw [← integral_const_mul, ← integral_mul_const]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ Eq (α := ℝ) (∫ (a : Ω), 2 * (X a * rexp (v * X a)) * deriv (cgf X μ) v ∂μ)
    (∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ)
have e_a : ∀ (ω : Ω), 2 * (X ω * rexp (v * X ω)) * deriv (cgf X μ) v = 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
⊢ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
have e_a : HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
Tactic: rw [integral_const_mul, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_int : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ
e_a :
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
⊢ HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v =
    ∫ (a : Ω), HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * rexp (v * X a) ∂μ
have e_a₁ : HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (x : Ω), (fun (ω : Ω) ↦ rexp (v * X ω)) x ∂μ =
  HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * ∫ (a : Ω), rexp (v * X a) ∂μ
Tactic: rw [integral_const_mul, mgf]
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ) / mgf X μ v
have e_a : ∀ (ω : Ω),
  (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
      rexp (v * X ω) =
    HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)
Tactic: congr with ω
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have calc : (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
    mgf X μ v
Tactic: calc (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ - 2 * (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (cgf X μ) v
      + deriv (cgf X μ) v ^ 2 * mgf X μ v) / mgf X μ v := by
    rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (∫ ω, ((X ω) ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * exp (v * X ω) ∂μ)
      / mgf X μ v := by
    congr 1
    simp_rw [add_mul, sub_mul]
    have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ := by
      simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc]
      refine Integrable.mul_const ?_ _
      convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
      simp
    rw [integral_add]
    rotate_left
    · exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int
    · exact (interior_subset (s := integrableExpSet X μ) h).const_mul _
    rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
    congr
    · rw [← integral_const_mul, ← integral_mul_const]
      congr with ω
      ring
    · rw [integral_const_mul, mgf]
  _ = (∫ ω, (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v := by
    congr with ω
    ring
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
calc :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v
⊢ (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have calc₁ : (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
        HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
    mgf X μ v =
  (∫ (ω : Ω),
      (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
        rexp (v * X ω) ∂μ) /
    mgf X μ v
Tactic: calc (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ - 2 * (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (cgf X μ) v
      + deriv (cgf X μ) v ^ 2 * mgf X μ v) / mgf X μ v := by
    rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (∫ ω, ((X ω) ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * exp (v * X ω) ∂μ)
      / mgf X μ v := by
    congr 1
    simp_rw [add_mul, sub_mul]
    have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ := by
      simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc]
      refine Integrable.mul_const ?_ _
      convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
      simp
    rw [integral_add]
    rotate_left
    · exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int
    · exact (interior_subset (s := integrableExpSet X μ) h).const_mul _
    rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
    congr
    · rw [← integral_const_mul, ← integral_mul_const]
      congr with ω
      ring
    · rw [integral_const_mul, mgf]
  _ = (∫ ω, (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v := by
    congr with ω
    ring
-- Lean 4 proof step from Mathlib.Probability.Moments.MGFAnalytic (goal)
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
calc :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v
calc₁ :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ -
          HMul.hMul (α := ℝ) 2 (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v +
        HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 * mgf X μ v) /
      mgf X μ v =
    (∫ (ω : Ω),
        (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
          rexp (v * X ω) ∂μ) /
      mgf X μ v
⊢ (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v -
      HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
have calc₂ : (∫ (ω : Ω),
      (HPow.hPow (β := ℕ) (X ω) 2 - 2 * X ω * deriv (cgf X μ) v + HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2) *
        rexp (v * X ω) ∂μ) /
    mgf X μ v =
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω) ∂μ) / mgf X μ v
Tactic: calc (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2
  _ = (∫ ω, (X ω) ^ 2 * exp (v * X ω) ∂μ - 2 * (∫ ω, X ω * exp (v * X ω) ∂μ) * deriv (cgf X μ) v
      + deriv (cgf X μ) v ^ 2 * mgf X μ v) / mgf X μ v := by
    rw [add_div, sub_div, sub_add]
    congr 1
    rw [mul_div_cancel_right₀, deriv_cgf h]
    · ring
    · exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'
  _ = (∫ ω, ((X ω) ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * exp (v * X ω) ∂μ)
      / mgf X μ v := by
    congr 1
    simp_rw [add_mul, sub_mul]
    have h_int : Integrable (fun ω ↦ 2 * X ω * deriv (cgf X μ) v * exp (v * X ω)) μ := by
      simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]
      refine Integrable.const_mul ?_ _
      simp_rw [← mul_assoc]
      refine Integrable.mul_const ?_ _
      convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1
      simp
    rw [integral_add]
    rotate_left
    · exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int
    · exact (interior_subset (s := integrableExpSet X μ) h).const_mul _
    rw [integral_sub (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2) h_int]
    congr
    · rw [← integral_const_mul, ← integral_mul_const]
      congr with ω
      ring
    · rw [integral_const_mul, mgf]
  _ = (∫ ω, (X ω - deriv (cgf X μ) v) ^ 2 * exp (v * X ω) ∂μ) / mgf X μ v := by
    congr with ω
    ring