Theorems · Theorem · probability

ProbabilityTheory.complexMGF_congr_identDistrib

∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {Ω' : Type u_3}
  {mΩ' : MeasurableSpace Ω'} {μ' : MeasureTheory.Measure Ω'} {Y : Ω' → ℝ},
  ProbabilityTheory.IdentDistrib X Y μ μ' → ProbabilityTheory.complexMGF X μ = ProbabilityTheory.complexMGF Y μ'

Defined in

Mathlib.Probability.Moments.ComplexMGF

Cited by

0 results in Mathlib

Foundations

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