deriv_cgf_zero — Mathlib

English

If 0 is in the interior of integrableExpSet(X, μ), then the derivative of cgf at 0 equals the mean μ[X] divided by μ(Ω).

Русский

Если 0 лежит во внутренности integrableExpSet(X, μ), то производная cgf в 0 равна \\frac{E_{μ}[X]}{μ(Ω)}.

LaTeX

$$$0 \\in \\mathrm{int}(\\mathrm{integrableExpSet}(X,\\mu)) \\Rightarrow \\mathrm{deriv}(\\mathrm{cgf}(X,\\mu))(0) = \\dfrac{\\mu[X]}{\\mu(\\Omega)}.$$$

Lean4

theorem deriv_cgf_zero (h : 0 ∈ interior (integrableExpSet X μ)) : deriv (cgf X μ) 0 = μ[X] / μ.real Set.univ := by
  simp [deriv_cgf h]

Похожие утверждения