Theorems · Theorem · probability

ProbabilityTheory.iteratedDeriv_mgf

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), iteratedDeriv n (ProbabilityTheory.mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (t * X ω)) x ∂μ

For t ∈ interior (integrableExpSet X μ), the n-th derivative of mgf X μ at t is μ[X ^ n * exp (t * X)].

Defined in

Mathlib.Probability.Moments.MGFAnalytic

Cited by

2 results in Mathlib

Foundations

Depth 269 from the axioms · uses propext, Classical.choice, Quot.sound