norm_condExpL2_le_one

Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2

URI: https://scilib.ai/kg/mathlib#MeasureTheory.norm_condExpL2_le_one

← MathLib Explorer

English

If f is integrable, then condExpL2 E 𝕜 hm f is integrable.

Русский

Если f интегрируем, то condExpL2 E 𝕜 hm f интегрируем.

LaTeX

$$Integrable (condExpL2 E 𝕜 hm f)$$

Lean4

theorem norm_condExpL2_le_one (hm : m ≤ m0) : ‖@condExpL2 α E 𝕜 _ _ _ _ _ _ μ hm‖ ≤ 1 :=
  haveI : Fact (m ≤ m0) := ⟨hm⟩
  Submodule.orthogonalProjection_norm_le _

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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