integrableOn_of_measure_ne_top — Mathlib

English

If h is antitone on s, then for finite μ(s) and measurable s, MemLp holds for all p.

Русский

Если h антитононна на s и μ(s) конечно, то для любого p выполняется MemLp.

LaTeX

$$$f \in L^{p}(\mu\restriction s)\quad(\forall p)$$

Lean4

theorem integrableOn_of_measure_ne_top (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b)
    (hs : μ s ≠ ∞) (h's : MeasurableSet s) : IntegrableOn f s μ :=
  memLp_one_iff_integrable.1 (hanti.memLp_of_measure_ne_top ha hb hs h's)

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