Theorems · Theorem · probability

ProbabilityTheory.mgf_map

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {Ω' : Type u_3} {mΩ' : MeasurableSpace Ω'} {μ : MeasureTheory.Measure Ω'}
  {Y : Ω' → Ω} {X : Ω → ℝ},
  AEMeasurable Y μ →
    ∀ {t : ℝ},
      MeasureTheory.AEStronglyMeasurable (fun ω => Real.exp (t * X ω)) (MeasureTheory.Measure.map Y μ) →
        ProbabilityTheory.mgf X (MeasureTheory.Measure.map Y μ) t = ProbabilityTheory.mgf (X ∘ Y) μ t

Defined in

Mathlib.Probability.Moments.Basic

Cited by

3 results in Mathlib

Foundations

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