memLp_of_measure_ne_top — Mathlib

English

If f is antitone on s and μ(s) ≠ ∞, then f ∈ Lp(μ|_s) for any p.

Русский

Если f антитононна на s и μ(s) конечна, то f принадлежит Lp(μ|_s) для любого p.

LaTeX

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

Lean4

theorem memLp_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) : MemLp f p (μ.restrict s) :=
  MonotoneOn.memLp_of_measure_ne_top (E := Eᵒᵈ) hanti ha hb hs h's

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