English
For v in interior of integrableExpSet, iteratedDeriv_2 of cgf at v equals the integral of (X−deriv(cgf)(v))^2 e^{vX} divided by mgf, i.e. a variance-type identity.
Русский
Для v внутри interior integrableExpSet, iteratedDeriv_2 cgf в точке v равен интегралу по μ от (X−deriv(cgf)(v))^2 e^{v X} делённому на mgf(X, μ)(v) — тождество, напоминающее дисперсию.
LaTeX
$$$\\mathrm{iteratedDeriv}_2(\\mathrm{cgf}(X,\\mu), v) = \\dfrac{\\int (X(\\omega) - \\mathrm{deriv}(\\mathrm{cgf}(X,\\mu))(v))^2 e^{v X(\\omega)} d\\mu(\\omega)}{\\mathrm{mgf}(X,\\mu)(v)}$ for $v\\in\\mathrm{int}(\\mathrm{integrableExpSet}(X,\\mu)).$$$
Lean4
theorem ae_forall_integrable_exp_mul (h : HasSubgaussianMGF X c κ ν) :
∀ᵐ ω' ∂ν, ∀ t, Integrable (fun ω ↦ exp (t * X ω)) (κ ω') :=
by
have h_int (n : ℤ) : ∀ᵐ ω' ∂ν, Integrable (fun ω ↦ exp (n * X ω)) (κ ω') := h.ae_integrable_exp_mul _
rw [← ae_all_iff] at h_int
filter_upwards [h_int] with ω' h_int t
exact integrable_exp_mul_of_le_of_le (h_int _) (h_int _) (Int.floor_le t) (Int.le_ceil t)
