memLp_top — Mathlib

English

If f is antitone on s (i.e., monotone in the opposite order) and s has a least and a greatest element, then f ∈ Lp(μ|_s) for all p (with appropriate measure restriction).

Русский

Если f антимонотонна на s и на s существуют наименьший и наибольший элементы, то f ∈ Lp(μ|_s) для всех p.

LaTeX

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

Lean4

theorem memLp_top (hanti : AntitoneOn f s) {a b : X} (ha : IsLeast s a) (hb : IsGreatest s b) (h's : MeasurableSet s) :
    MemLp f ∞ (μ.restrict s) :=
  MonotoneOn.memLp_top (E := Eᵒᵈ) hanti ha hb h's

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