integrable_id

Mathlib.Probability.Distributions.Gaussian.Fernique

URI: https://scilib.ai/kg/mathlib#ProbabilityTheory.IsGaussian.integrable_id

English

The identity function is integrable with respect to a Gaussian measure μ on a complete space.

Русский

Идентичная функция интегрируема по гауссовой μ на полном пространстве.

LaTeX

$$$\\int \\|x\\| dμ(x) < \\infty$ or equivalently Integrable(id, μ)$$$

Lean4

theorem integrable_id : Integrable id μ :=
  memLp_one_iff_integrable.1 <| memLp_id μ 1 (by norm_num)

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

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

Разделы

Аффилиация

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