mgf_zero' — Mathlib

English

If X is a real-valued function on Ω and μ is a measure, then the moment generating function at t = 0 equals the total mass μ(Ω): M_X(μ; 0) = ∫Ω e^{0·X(ω)} dμ = μ(Ω).

Русский

Пусть X: Ω→ℝ и μ — мера. Тогда M_X(μ; 0) = ∫_Ω e^{0·X(ω)} dμ = μ(Ω).

LaTeX

$$$\mathrm{mgf}_X(\mu)(0) = \mu(\Omega)$$$

Lean4

@[simp]
theorem mgf_zero' : mgf X μ 0 = μ.real Set.univ := by
  simp only [mgf, zero_mul, exp_zero, integral_const, smul_eq_mul, mul_one]

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