Theorems · Theorem · probability

ProbabilityTheory.integral_tilted_mul_eq_cgf

∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {t : ℝ} {E : Type u_2}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : Ω → E),
  MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ →
    (∫ (ω : Ω), g ω ∂μ.tilted fun x => t * X x) = ∫ (ω : Ω), Real.exp (t * X ω - ProbabilityTheory.cgf X μ t) • g ω ∂μ

Defined in

Mathlib.Probability.Moments.Tilted

Cited by

0 results in Mathlib

Foundations

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

Assumes

NormedAddCommGroupNormedSpace