-- 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 pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
this : deriv 0 = 0
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

Tactic:
simp [hμ, this]

Result:
no goals

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

Result:
no goals

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

Tactic:
congr

Result:
case e_a.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 = ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ

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

Tactic:
have h_mem : ∀ᶠ y in 𝓝 v, y ∈ interior (integrableExpSet X μ) :=
  isOpen_interior.eventually_mem h

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

Tactic:
by_cases hμ : μ = 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
⊢ deriv (deriv (cgf X μ)) v = (∫ (x : Ω), (fun ω => X ω ^ 2 * rexp (v * X ω)) x ∂μ) / mgf X μ v - deriv (cgf X μ) v ^ 2

case neg
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ 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 ∂μ
⊢ ((∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) / mgf X μ v ^ 2 = deriv (cgf X μ) v ^ 2

Tactic:
rw [deriv_cgf h]

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

Tactic:
rw [sub_div]

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

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

Tactic:
have : deriv (0 : ℝ → ℝ) = 0 := by ext; exact deriv_const _ 0

Result:
case pos
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : μ = 0
this : deriv 0 = 0
⊢ 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.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 = ∫ (ω : Ω), X ω ^ 2 * rexp (v * X ω) ∂μ

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

Result:
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