memLp_two_fun_id

Mathlib.Probability.Distributions.Gaussian.Fernique

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

English

Similarly, the function x ↦ x is in L^2(μ) for Gaussian μ.

Русский

Функция x ↦ x ∈ L^2(μ) для гауссовой μ.

LaTeX

$$$\\text{MemLp}(\\mathrm{id}, 2, μ)$$$

Lean4

theorem memLp_two_fun_id : MemLp (fun x ↦ x) 2 μ :=
  memLp_two_id

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

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

Разделы

Аффилиация

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