indicator — Mathlib

English

Bounds for eLpNorm with indicator of a constant function.

Русский

Границы eLpNorm для индикатора константы.

LaTeX

$$$eLpNorm_indicator_const_le (hs) (p) (μ) : eLpNorm (s.indicator (fun x => c)) p μ \le \|c\| * μ(s)^{1/p}$$$

Lean4

theorem indicator {f : α → ε} (hs : MeasurableSet s) (hf : MemLp f p μ) : MemLp (s.indicator f) p μ :=
  ⟨hf.aestronglyMeasurable.indicator hs, lt_of_le_of_lt (eLpNorm_indicator_le f) hf.eLpNorm_lt_top⟩

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