awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (iteratedDeriv 1 (mgf X μ)) v

Tactic:
exact differentiableAt_iteratedDeriv_mgf h 1

Premises used: ProbabilityTheory.differentiableAt_iteratedDeriv_mgf, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (mgf X μ) v

Tactic:
differentiableAt_mgf h

Premises used: ProbabilityTheory.differentiableAt_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ DifferentiableAt ℝ (mgf X μ) v

Tactic:
exact differentiableAt_mgf h

Premises used: ProbabilityTheory.differentiableAt_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ mgf X μ v ≠ 0

Tactic:
(mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

Premises used: interior_subset, ProbabilityTheory.mgf_pos', LT.lt.ne'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ mgf X μ v ≠ 0

Tactic:
exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

Premises used: interior_subset, ProbabilityTheory.mgf_pos', LT.lt.ne'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
rw rw₁ :
  (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)
          (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2
⊢ (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (mgf X μ) v) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2

Tactic:
rw [deriv_mgf h]

Premises used: ProbabilityTheory.deriv_mgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
rw :
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
        HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
⊢ (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v -
        HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ)) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2

Tactic:
rw [sub_div]

Premises used: sub_div
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
e_a :
  deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v
e_a₁ :
  HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 -
      HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
        HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2

Tactic:
congr 1
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
e_a : mgf X μ v ≠ 0
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v

Tactic:
rw [pow_two, div_mul_eq_div_div, mul_div_assoc, div_self, mul_one]

Premises used: pow_two, mul_div_assoc, mul_one, div_mul_eq_div_div, div_self
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
e_a :
  HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2
⊢ HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2

Tactic:
rw [deriv_cgf h]

Premises used: ProbabilityTheory.deriv_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ HMul.hMul (α := ℝ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) (∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) /
      HPow.hPow (β := ℕ) (mgf X μ v) 2 =
    HPow.hPow (β := ℕ) ((∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) x ∂μ) / mgf X μ v) 2

Tactic:
ring
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
e_a :
  Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ)
⊢ deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2

Tactic:
congr
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ Eq (α := ℝ) (deriv (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 1 * rexp (t * X ω)) x ∂μ) v)
    (∫ (x : Ω), (fun (ω : Ω) ↦ X ω ^ HAdd.hAdd (α := ℕ) 1 1 * rexp (v * X ω)) x ∂μ)

Tactic:
(hasDerivAt_integral_pow_mul_exp_real h 1).deriv

Premises used: HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
h₁ :
  Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
    (deriv (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 1 * rexp (t * X ω)) x ∂μ) v)
⊢ Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ)

Tactic:
convert! (hasDerivAt_integral_pow_mul_exp_real h 1).deriv using 1

Premises used: HasDerivAt.deriv, ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ (∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u
h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun (u : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ X ω * rexp (u * X ω)) x ∂μ
⊢ Eq (α := ℝ) (deriv (fun (u : ℝ) ↦ ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v)
    (deriv (fun (t : ℝ) ↦ ∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 1 * rexp (t * X ω)) x ∂μ) v)

Tactic:
simp
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
pos :
  ∀ (hμ : μ = 0),
    iteratedDeriv 2 (cgf X μ) v =
      (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
neg :
  ∀ (hμ : ¬μ = 0),
    iteratedDeriv 2 (cgf X μ) v =
      (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
by_cases hμ : μ = 0
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
simp [hμ]
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
neg :
  (∫ (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
⊢ iteratedDeriv 2 (cgf X μ) v =
    (∫ (x : Ω), (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω - deriv (cgf X μ) v) 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v

Tactic:
rw [iteratedDeriv_two_cgf h]

Premises used: ProbabilityTheory.iteratedDeriv_two_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
rw :
  (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
      (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)
⊢ (∫ (ω : Ω), 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:
rw [add_div, sub_div, sub_add]

Premises used: sub_add, sub_div, add_div
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
e_a :
  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
⊢ (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v - HPow.hPow (β := ℕ) (deriv (cgf X μ) v) 2 =
    (∫ (ω : Ω), HPow.hPow (β := ℕ) (X ω) 2 * rexp (v * X ω) ∂μ) / mgf X μ v -
      (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)

Tactic:
congr 1
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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
e_a₁ : mgf X μ v ≠ 0
⊢ 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

Tactic:
rw [mul_div_cancel_right₀, deriv_cgf h]

Premises used: mul_div_cancel_right₀, ProbabilityTheory.deriv_cgf
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ 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

Tactic:
ring
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ mgf X μ v ≠ 0

Tactic:
(mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

Premises used: interior_subset, ProbabilityTheory.mgf_pos', LT.lt.ne'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ mgf X μ v ≠ 0

Tactic:
exact (mgf_pos' hμ (interior_subset (s := integrableExpSet X μ) h)).ne'

Premises used: interior_subset, ProbabilityTheory.mgf_pos', LT.lt.ne'
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
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 ω) ∂μ
⊢ (∫ (ω : Ω), 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:
congr 1
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
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 ω) ∂μ
⊢ ∫ (ω : Ω), 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:
simp_rw [add_mul, sub_mul]

Premises used: add_mul, sub_mul
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * (X ω * (rexp (v * X ω) * deriv (cgf X μ) v))) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

Tactic:
simp_rw [mul_assoc, mul_comm (deriv (cgf X μ) v)]

Premises used: ProbabilityTheory.cgf, deriv, mul_assoc, mul_comm
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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))) μ

Tactic:
Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
refine : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * (rexp (v * X ω) * deriv (cgf X μ) v)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ 2 * (X ω * (rexp (v * X ω) * deriv (cgf X μ) v))) μ

Tactic:
refine Integrable.const_mul ?_ _

Premises used: MeasureTheory.Integrable.const_mul
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
simp_rw : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω) * deriv (cgf X μ) v) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * (rexp (v * X ω) * deriv (cgf X μ) v)) μ

Tactic:
simp_rw [← mul_assoc]

Premises used: mul_assoc
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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) μ

Tactic:
Integrable.mul_const ?_ _

Premises used: MeasureTheory.Integrable.mul_const
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
refine : Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) μ
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω) * deriv (cgf X μ) v) μ

Tactic:
refine Integrable.mul_const ?_ _

Premises used: MeasureTheory.Integrable.mul_const
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ HPow.hPow (β := ℕ) (X ω) 1 * rexp (v * X ω)) μ

Tactic:
integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1

Premises used: ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h₁ : ∀ (x : Ω), X x = HPow.hPow (β := ℕ) (X x) 1
⊢ Integrable (ε := ℝ) (fun (ω : Ω) ↦ X ω * rexp (v * X ω)) μ

Tactic:
convert! integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 1

Premises used: ProbabilityTheory.integrable_pow_mul_exp_of_mem_interior_integrableExpSet, OfNat.ofNat
-- Module: Mathlib.Probability.Moments.MGFAnalytic
Goal:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
x : Ω
⊢ X x = HPow.hPow (β := ℕ) (X x) 1

Tactic:
simp
-- Module: Mathlib.Probability.Moments.MGFAnalytic
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 ω)) μ

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