hasDerivAt_mgf — Mathlib

English

The mgf is analytic at any point v with v in the interior of integrableExpSet(X, μ).

Русский

MGF аналитичен в любой точке v внутри interior integrableExpSet(X, μ).

LaTeX

$$$\text{AnalyticAt}_{\mathbb{R}} (\mathrm{mgf}(X, \mu), v).$$$

Lean4

/-- For `t ∈ interior (integrableExpSet X μ)`, the derivative of `mgf X μ` at `t` is
`μ[X * exp (t * X)]`. -/
theorem hasDerivAt_mgf (h : t ∈ interior (integrableExpSet X μ)) :
    HasDerivAt (mgf X μ) (μ[fun ω ↦ X ω * exp (t * X ω)]) t :=
  by
  convert hasDerivAt_integral_pow_mul_exp_real h 0
  · simp [mgf]
  · simp

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