measure_lt_top_of_memLp_indicator

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

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