integrable_condExpL2_of_isFiniteMeasure

English

The L2-norm of condExpL2 applied to f is bounded by the L2-norm of f: ||condExpL2 E 𝕜 hm f|| ≤ ||f||.

Русский

Нормa L2 от condExpL2 f не больше нормы f: ||condExpL2 E 𝕜 hm f|| ≤ ||f||.

LaTeX

$$$\|condExpL2 E 𝕜 hm f\| \leq \|f\|$$$

Lean4

theorem integrable_condExpL2_of_isFiniteMeasure (hm : m ≤ m0) [IsFiniteMeasure μ] {f : α →₂[μ] E} :
    Integrable (ε := E) (condExpL2 E 𝕜 hm f) μ :=
  integrableOn_univ.mp <| integrableOn_condExpL2_of_measure_ne_top hm (measure_ne_top _ _) f

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