integrableOn_condExpL2_of_measure_ne_top

English

For f: α →₂[μ] E, Integrable (condExpL2 E 𝕜 hm f) holds.

Русский

Для f: α →₂[μ] E выполняется Integrable (condExpL2 E 𝕜 hm f).

LaTeX

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

Lean4

theorem integrableOn_condExpL2_of_measure_ne_top (hm : m ≤ m0) (hμs : μ s ≠ ∞) (f : α →₂[μ] E) :
    IntegrableOn (ε := E) (condExpL2 E 𝕜 hm f) s μ :=
  integrableOn_Lp_of_measure_ne_top (condExpL2 E 𝕜 hm f : α →₂[μ] E) fact_one_le_two_ennreal.elim hμs

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