memLp_isCompact — Mathlib

English

If s is compact and f is monotone on s, then f lies in Lp(μ|_s) for any p, provided μ is finite on compact subsets (e.g., IsFiniteMeasureOnCompacts).

Русский

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

LaTeX

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

Lean4

theorem memLp_isCompact [IsFiniteMeasureOnCompacts μ] (hs : IsCompact s) (hmono : MonotoneOn f s) :
    MemLp f p (μ.restrict s) := by
  obtain rfl | h := s.eq_empty_or_nonempty
  · simp
  · exact hmono.memLp_of_measure_ne_top (hs.isLeast_sInf h) (hs.isGreatest_sSup h) hs.measure_lt_top.ne hs.measurableSet

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