mgf_id_gaussianReal

Mathlib.Probability.Distributions.Gaussian.Real

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

English

mgf_id_gaussianReal is an alias for mgf_fun_id_gaussianReal: mgf_id_gaussianReal = mgf_fun_id_gaussianReal.

Русский

mgf_id_gaussianReal является синонимом mgf_fun_id_gaussianReal: mgf_id_gaussianReal = mgf_fun_id_gaussianReal.

LaTeX

$$$\mathrm{mgf\_id\_gaussianReal} = \mathrm{mgf\_fun\_id\_gaussianReal}$$$

Lean4

theorem mgf_id_gaussianReal : mgf id (gaussianReal μ v) = fun t ↦ rexp (μ * t + v * t ^ 2 / 2) :=
  mgf_fun_id_gaussianReal

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

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

Разделы

Аффилиация

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