-- Mathlib/Probability/Moments/MGFAnalytic.lean
lemma iteratedDeriv_two_cgf (h : v ∈ interior (integrableExpSet X μ)) :
    iteratedDeriv 2 (cgf X μ) v
      = μ[fun ω ↦ (X ω)^2 * exp (v * X ω)] / mgf X μ v - deriv (cgf X μ) v ^ 2

Proof state:
case hc
Ω : 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

Result:
no goals

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv 0 = 0

Tactic:
ext

Result:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
x✝ : ℝ
⊢ deriv 0 x✝ = 0 x✝

Proof state:
case h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
x✝ : ℝ
⊢ deriv 0 x✝ = 0 x✝

Tactic:
exact deriv_const _ 0

Result:
no goals

Proof state:
case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
have h_d_cgf : deriv (cgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] / mgf X μ u := by
  filter_upwards [h_mem] with u hu using deriv_cgf hu

Result:
case neg
Ω : 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
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Proof state:
case e_a
Ω : 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 ∂μ
⊢ deriv (fun u => ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v * mgf X μ v / 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]

Result:
case e_a
Ω : 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

Proof state:
case h.e'_2
Ω : 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 ∂μ
⊢ deriv (fun u => ∫ (ω : Ω), X ω * rexp (u * X ω) ∂μ) v =
    deriv (fun t => ∫ (x : Ω), (fun ω => X ω ^ 1 * rexp (t * X ω)) x ∂μ) v

Tactic:
simp

Result:
no goals

Proof state:
case neg
Ω : 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
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
have h_d_mgf : deriv (mgf X μ) =ᶠ[𝓝 v] fun u ↦ μ[fun ω ↦ X ω * exp (u * X ω)] := by
  filter_upwards [h_mem] with u hu using deriv_mgf hu

Result:
case neg
Ω : 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 ∂μ
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
h_mem : ∀ᶠ (y : ℝ) in 𝓝 v, y ∈ interior (integrableExpSet X μ)
⊢ deriv (cgf X μ) =ᶠ[𝓝 v] fun u => (∫ (x : Ω), (fun ω => X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u

Tactic:
filter_upwards [h_mem] with u hu using deriv_cgf hu

Result:
no goals

Proof state:
case neg
Ω : 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 ∂μ
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
rw [h_d_cgf.deriv_eq]

Result:
case neg
Ω : 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 ∂μ
⊢ deriv (fun u => (∫ (x : Ω), (fun ω => X ω * rexp (u * X ω)) x ∂μ) / mgf X μ u) v =
    (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Proof state:
case e_a
Ω : 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'

Result:
no goals