memLp_of_measure_ne_top — Mathlib

English

If f is monotone on a measurable set s with a least and a greatest element, and μ(s) is finite, then f belongs to Lp(μ|_s) for every p (i.e., MemLp f p (μ|_s) for all p).

Русский

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

LaTeX

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

Lean4

theorem memLp_of_measure_ne_top (hmono : MonotoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b)
    (hs : μ s ≠ ∞) (h's : MeasurableSet s) : MemLp f p (μ.restrict s) :=
  (hmono.memLp_top ha hb h's).mono_exponent_of_measure_support_ne_top (s := univ) (by simp) (by simpa using hs) le_top

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