cgf_undef

Mathlib.Probability.Moments.Basic

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

English

If exp(t X) is not integrable with respect to μ, then cgf(X; μ; t) = 0.

Русский

Если экспонента не интегрируема, то cgf(X; μ; t) = 0.

LaTeX

$$$\operatorname{cgf}(X; μ; t) = 0$ if $\int e^{t X} dμ$ is undefined$$

Lean4

theorem cgf_undef (hX : ¬Integrable (fun ω => exp (t * X ω)) μ) : cgf X μ t = 0 := by
  simp only [cgf, mgf_undef hX, log_zero]

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

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

Разделы

Аффилиация

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