hasFPowerSeriesAt_mgf — Mathlib

English

The mgf has an analytic power series expansion around v with coefficients given by the integrals μ[X^n e^{v X}]/n!.

Русский

MGF имеет аналитическое разложение в ряд вокруг v с коэффициентами μ[X^n e^{v X}]/n!.

LaTeX

$$$\text{HasFPowerSeriesAt}(\mathrm{mgf}(X, \mu), \mathrm{FormalMultilinearSeries.ofScalars}(\mathbb{R}, n \mapsto (\mu[X^n e^{v X}])/n!))\, v.$$$

Lean4

theorem hasFPowerSeriesAt_mgf (hv : v ∈ interior (integrableExpSet X μ)) :
    HasFPowerSeriesAt (mgf X μ)
      (FormalMultilinearSeries.ofScalars ℝ (fun n ↦ (μ[fun ω ↦ X ω ^ n * exp (v * X ω)] : ℝ) / n !)) v :=
  by
  convert (analyticAt_mgf hv).hasFPowerSeriesAt
  rw [iteratedDeriv_mgf hv]

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