Theorems · Theorem · probability

ProbabilityTheory.integral_tilted_mul_self

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    (∫ (x : Ω), X x ∂μ.tilted fun x => t * X x) = deriv (ProbabilityTheory.cgf X μ) t

The integral of X against the tilted measure μ.tilted (t * X ·) is the first derivative of the cumulant-generating function of X at t.

Defined in

Mathlib.Probability.Moments.Tilted

Cited by

1 results in Mathlib

Foundations

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