Theorems · Theorem · probability

ProbabilityTheory.hasDerivAt_integral_pow_mul_exp_real

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

For t : ℝ with t ∈ interior (integrableExpSet X μ), the derivative of the function x ↦ μ[X ^ n * exp (x * X)] at t is μ[X ^ (n + 1) * exp (t * X)].

Defined in

Mathlib.Probability.Moments.MGFAnalytic

Cited by

3 results in Mathlib

Foundations

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