Theorems · Theorem · probability

ProbabilityTheory.iteratedDeriv_two_cgf_eq_integral

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

Defined in

Mathlib.Probability.Moments.MGFAnalytic

Cited by

1 results in Mathlib

Foundations

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