memLp_indicator_iff_restrict — Mathlib

English

Equivalence between MemLp of indicator and MemLp on restricted measure.

Русский

Эквивалентность MemLp индикатора и MemLp на ограниченной мере.

LaTeX

$$$\text{MemLp} (s.indicator f) p μ \quad\leftrightarrow\quad \text{MemLp} f p (μ.restrict s)$$$

Lean4

theorem memLp_indicator_iff_restrict {f : α → ε} (hs : MeasurableSet s) :
    MemLp (s.indicator f) p μ ↔ MemLp f p (μ.restrict s) := by
  simp [MemLp, aestronglyMeasurable_indicator_iff hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]

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