Theorems · Theorem · probability

ProbabilityTheory.eqOn_complexMGF_of_mgf

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {Y : Ω' → ℝ} {μ' : MeasureTheory.Measure Ω'} [MeasureTheory.IsProbabilityMeasure μ],
  ProbabilityTheory.mgf X μ = ProbabilityTheory.mgf Y μ' →
    Set.EqOn (ProbabilityTheory.complexMGF X μ) (ProbabilityTheory.complexMGF Y μ')
      {z | z.re ∈ interior (ProbabilityTheory.integrableExpSet X μ)}

If two random variables have the same moment-generating function then they have the same complexMGF on the vertical strip {z | z.re ∈ interior (integrableExpSet X μ)}.

Defined in

Mathlib.Probability.Moments.ComplexMGF

Cited by

0 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsProbabilityMeasure