complexMGF_congr_identDistrib — Mathlib

English

If two random variables X and Y on possibly different measure spaces μ and μ' have identical distribution (IdentDistrib X Y μ μ'), then their complex MGFs coincide: complexMGF X μ = complexMGF Y μ'.

Русский

Если случайные величины X и Y на возможно различных пространствах меры μ и μ' имеют одинаковое распределение (IdentDistrib X Y μ μ'), то их комплексные MGF совпадают: complexMGF X μ = complexMGF Y μ'.

LaTeX

$$$\text{IdentDistrib } X Y\ μ\ μ' \;\Longrightarrow\; complexMGF X μ = complexMGF Y μ'$$$

Lean4

theorem complexMGF_congr_identDistrib {Ω' : Type*} {mΩ' : MeasurableSpace Ω'} {μ' : Measure Ω'} {Y : Ω' → ℝ}
    (h : IdentDistrib X Y μ μ') : complexMGF X μ = complexMGF Y μ' := by
  rw [← complexMGF_id_map h.aemeasurable_fst, ← complexMGF_id_map h.aemeasurable_snd, h.map_eq]

Похожие утверждения