English
If a piecewise indicator built from a nonzero constant is MemLp, then μ(s) < ∞.
Русский
Если функция-индикатор с ненулевым значением принадлежит MemLp, то μ(с) < ∞.
LaTeX
$$$hp_{pos}: p\\neq 0,\\ hp_{ne}: p\\neq \\infty,\\ hc: c\\neq 0,\\ hs: MeasurableSet s,\\ hcs: MemLp((const_α c).piecewise s hs (const_α 0))\\Rightarrow\\mu(s)<\\infty$$$
Lean4
theorem measure_lt_top_of_memLp_indicator (hp_pos : p ≠ 0) (hp_ne_top : p ≠ ∞) {c : E} (hc : c ≠ 0) {s : Set α}
(hs : MeasurableSet s) (hcs : MemLp ((const α c).piecewise s hs (const α 0)) p μ) : μ s < ⊤ :=
by
have : Function.support (const α c) = Set.univ := Function.support_const hc
simpa only [memLp_iff_finMeasSupp hp_pos hp_ne_top, finMeasSupp_iff_support, support_indicator, Set.inter_univ,
this] using hcs