mgf_congr — Mathlib

English

If X and Y have identically distributed laws under μ and μ', then mgf X μ = mgf Y μ'.

Русский

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

LaTeX

$$$\mathrm{mgf}(X; μ) = \mathrm{mgf}(Y; μ')$ при $\mathrm{IdentDistrib}(X,Y; μ, μ')$$$

Lean4

theorem mgf_congr {Y : Ω → ℝ} (h : X =ᵐ[μ] Y) : mgf X μ t = mgf Y μ t :=
  integral_congr_ae <| by filter_upwards [h] with ω hω using by rw [hω]

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