eLpNorm_indicator_const — Mathlib

English

Alternative presentation of essSup indicator equality for constant c.

Русский

Альтернативная формулировка равенства essSup индикатора константы.

LaTeX

$$$eLpNormEssSup (s.indicator (fun _ => c) ) μ = \|c\|_ε$$$

Lean4

theorem eLpNorm_indicator_const (hs : MeasurableSet s) (hp : p ≠ 0) (hp_top : p ≠ ∞) :
    eLpNorm (s.indicator fun _ => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
  eLpNorm_indicator_const₀ hs.nullMeasurableSet hp hp_top

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