mgf_congr_of_identDistrib — Mathlib

English

If X and X' have the same distribution, then mgf(X; μ; t) = mgf(X'; μ'; t) for all t.

Русский

Если X и X' имеют одну и ту же распределение, то mgf(X; μ; t) = mgf(X'; μ'; t) для всех t.

LaTeX

$$$\mathrm{mgf}(X, \mu, t) = \mathrm{mgf}(X', \mu', t).$$$

Lean4

theorem mgf_congr_of_identDistrib (X : Ω → ℝ) {Ω' : Type*} {m' : MeasurableSpace Ω'} {μ' : Measure Ω'} (X' : Ω' → ℝ)
    (hident : IdentDistrib X X' μ μ') (t : ℝ) : mgf X μ t = mgf X' μ' t :=
  hident.comp (measurable_const_mul t).exp |>.integral_eq

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