eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict

English

For f, and MeasSet s, the essSup of (s.indicator f) is bounded by essSup of f.

Русский

Предел по мере essSup для индикатора множества ограничивает essSup самой функции.

LaTeX

$$$eLpNormEssSup (s.indicator f) \le eLpNormEssSup f$$$

Lean4

theorem eLpNormEssSup_indicator_eq_eLpNormEssSup_restrict (hs : MeasurableSet s) :
    eLpNormEssSup (s.indicator f) μ = eLpNormEssSup f (μ.restrict s) := by
  simp_rw [← eLpNorm_exponent_top, eLpNorm_indicator_eq_eLpNorm_restrict hs]

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