eLpNorm_indicator_const' — Mathlib

English

A variant mirroring the previous result for indicator of constant c.

Русский

Вариант предыдущего результата для индикатора константы c.

LaTeX

$$$eLpNorm_indicator_const' (hs) (hμs) : eLpNorm (s.indicator (fun x => c)) p μ = \|c\|_ε * μ(s)^{1/p}$$$

Lean4

theorem eLpNorm_indicator_const' (hs : MeasurableSet s) (hμs : μ s ≠ 0) (hp : p ≠ 0) :
    eLpNorm (s.indicator fun _ => c) p μ = ‖c‖ₑ * μ s ^ (1 / p.toReal) :=
  by
  by_cases hp_top : p = ∞
  · simp [hp_top, eLpNormEssSup_indicator_const_eq s c hμs]
  · exact eLpNorm_indicator_const hs hp hp_top

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