English
If v lies in the interior of integrableExpSet(X, μ), then the derivative of cgf at v is equal to the μ-expectation of X e^{vX} divided by the mgf at v. More precisely
Русский
Пусть v лежит во внутренности integrableExpSet(X, μ). Тогда производная cgf в точке v равна отношению ∫ X e^{vX} dμ к mgf(X, μ)(v).
LaTeX
$$$\\forall v \\in \\mathrm{int}(\\mathrm{integrableExpSet}(X,\\mu)):\\quad \\mathrm{deriv}(\\mathrm{cgf}(X,\\mu))(v) = \\dfrac{\\int X(\\omega) e^{v X(\\omega)}\, d\\mu(\\omega)}{\\mathrm{mgf}(X,\\mu)(v)}.$$$
Lean4
theorem deriv_cgf (h : v ∈ interior (integrableExpSet X μ)) :
deriv (cgf X μ) v = μ[fun ω ↦ X ω * exp (v * X ω)] / mgf X μ v :=
by
by_cases hμ : μ = 0
· simp only [hμ, cgf_zero_measure, integral_zero_measure, mgf_zero_measure, div_zero, Pi.zero_apply]
exact deriv_const v 0
have hv : Integrable (fun ω ↦ exp (v * X ω)) μ := interior_subset (s := integrableExpSet X μ) h
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]
