indicatorConstLp — Mathlib

English

The Lp indicator of a sum equals the sum of Lp indicators with the same measure properties

Русский

Индикатор Lp суммы равен сумме индикаторов Lp с теми же свойствами меры

LaTeX

$$indicatorConstLp p hs hμs c + indicatorConstLp p hs hμs c' = indicatorConstLp p hs hμs (c + c')$$

Lean4

/-- Indicator of a set as an element of `Lp`. -/
def indicatorConstLp (p : ℝ≥0∞) (hs : MeasurableSet s) (hμs : μ s ≠ ∞) (c : E) : Lp E p μ :=
  MemLp.toLp (s.indicator fun _ => c) (memLp_indicator_const p hs c (Or.inr hμs))

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