integrable_fun_id

Mathlib.Probability.Distributions.Gaussian.Fernique

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

English

The function x ↦ x is integrable with respect to μ for a Gaussian μ.

Русский

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

LaTeX

$$$\\text{Integrable}(\\mathrm{id}, μ)$$$

Lean4

theorem integrable_fun_id : Integrable (fun x ↦ x) μ :=
  integrable_id

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

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

Разделы

Аффилиация

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