mgf_congr_identDistrib — Mathlib

English

If X and Y have IdentDistrib with respect to μ and μ', then mgf X μ = mgf Y μ'.

Русский

Если X и Y имеют идентичное распределение относительно μ и μ', то mgf X μ = mgf Y μ'.

LaTeX

$$$\mathrm{mgf}(X; μ) = \mathrm{mgf}(Y; μ')$$$

Lean4

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

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