eLpNormEssSup_trim — Mathlib

English

The essSup of eLpNorm' (or equivalently the eLpNorm) is invariant under trimming: eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ.

Русский

essSup eLpNorm' (а также eLpNorm) не изменяется при обрезке: eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ.

LaTeX

$$eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ$$

Lean4

theorem eLpNormEssSup_trim (hm : m ≤ m0) {f : α → ε} (hf : StronglyMeasurable[m] f) :
    eLpNormEssSup f (μ.trim hm) = eLpNormEssSup f μ :=
  essSup_trim _ (@StronglyMeasurable.enorm _ m _ _ _ _ hf)

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