Theorems · Theorem · probability

ProbabilityTheory.hasDerivAt_iteratedDeriv_mgf

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

Defined in

Mathlib.Probability.Moments.MGFAnalytic

Cited by

1 results in Mathlib

Foundations

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