Theorems · Theorem · probability

ProbabilityTheory.hasDerivAt_integral_pow_mul_exp

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

For z : ℂ with z.re ∈ interior (integrableExpSet X μ), the derivative of the function z' ↦ μ[X ^ n * cexp (z' * X)] at z is μ[X ^ (n + 1) * cexp (z * X)].

Defined in

Mathlib.Probability.Moments.ComplexMGF

Cited by

3 results in Mathlib

Foundations

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