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

Proof state:
case e_a.hf
Ω : 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 ω)) μ
⊢ Integrable (fun ω => X ω ^ 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

Tactic:
exact (integrable_pow_mul_exp_of_mem_interior_integrableExpSet h 2).sub h_int

Result:
no goals

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

Tactic:
rw [integral_mul_left, mgf]

Result:
no goals

Proof state:
Ω : 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:
simp_rw [← mul_assoc]

Result:
Ω : 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) μ

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

Tactic:
congr with ω

Result:
case e_a.e_f.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
ω : Ω
⊢ (X ω ^ 2 - 2 * X ω * deriv (cgf X μ) v + deriv (cgf X μ) v ^ 2) * rexp (v * X ω) =
    (X ω - deriv (cgf X μ) v) ^ 2 * rexp (v * X ω)

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

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

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

Tactic:
rw [mul_div_cancel_right₀, deriv_cgf h]

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

case e_a.hb
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
⊢ mgf X μ v ≠ 0

Proof state:
case e_a.hg
Ω : 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 ω)) μ
⊢ Integrable (fun ω => deriv (cgf X μ) v ^ 2 * rexp (v * X ω)) μ

Tactic:
exact (interior_subset (s := integrableExpSet X μ) h).const_mul _

Result:
no goals

Proof state:
case e_a.e_a.e_a
Ω : 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 ω)) μ
⊢ (2 * ∫ (ω : Ω), X ω * rexp (v * X ω) ∂μ) * deriv (cgf X μ) v =
    ∫ (a : Ω), 2 * X a * deriv (cgf X μ) v * rexp (v * X a) ∂μ

Tactic:
rw [← integral_mul_left, ← integral_mul_right]

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

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

Tactic:
rw [integral_add]

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

case e_a.hf
Ω : 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 ω)) μ
⊢ Integrable (fun ω => X ω ^ 2 * rexp (v * X ω) - 2 * X ω * deriv (cgf X μ) v * rexp (v * X ω)) μ

case e_a.hg
Ω : 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 ω)) μ
⊢ Integrable (fun ω => deriv (cgf X μ) v ^ 2 * rexp (v * X ω)) μ

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

Tactic:
congr 1

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