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

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

Tactic:
have hv : Integrable (fun ω ↦ exp (v * X ω)) μ := interior_subset (s := integrableExpSet X μ) h

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

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

Tactic:
exact deriv_const v 0

Result:
no goals

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

Tactic:
rw [deriv_mgf h]

Result:
no goals

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

Tactic:
simp only [hμ, cgf_zero_measure, integral_zero_measure, mgf_zero_measure, div_zero,
  Pi.zero_apply]

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

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

Tactic:
by_cases hμ : μ = 0

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

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

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
v : ℝ
h : v ∈ interior (integrableExpSet X μ)
hμ : ¬μ = 0
hv : Integrable (fun ω => rexp (v * X ω)) μ
⊢ deriv (fun x => log (mgf X μ x)) v = deriv (mgf X μ) v / mgf X μ v

Tactic:
rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]

Result:
no goals

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

Tactic:
calc deriv (fun x ↦ log (mgf X μ x)) v
_ = deriv (mgf X μ) v / mgf X μ v := by
  rw [deriv.log (differentiableAt_mgf h) ((mgf_pos' hμ hv).ne')]
_ = μ[fun ω ↦ X ω * exp (v * X ω)] / mgf X μ v := by rw [deriv_mgf h]

Result:
no goals