cgf_zero_fun

Mathlib.Probability.Moments.Basic

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.cgf_zero_fun

English

For a constant function c, cgf and mgf satisfy cgf( X, μ, t ) and mgf( X, μ, t ) relate to e^{t c} and μ(Ω).

Русский

Для константной функции c существует связь cgf и mgf через e^{t c} и μ(Ω).

LaTeX

$$cgf( X, μ, t ) = log( mgf(X, μ, t) )$$

Lean4

@[simp]
theorem cgf_zero_fun : cgf 0 μ t = log (μ.real Set.univ) := by simp only [cgf, mgf_zero_fun]

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru