eLpNormEssSup_mono_nnnorm_ae — Mathlib

English

If almost everywhere ‖f(x)‖₊ ≤ ‖g(x)‖₊, then eLpNormEssSup(f,μ) ≤ eLpNormEssSup(g,μ).

Русский

Если почти всюду ‖f(x)‖₊ ≤ ‖g(x)‖₊, essSup не больше.

LaTeX

$$$\\ae x, ‖f(x)‖₊ ≤ ‖g(x)‖₊ \\Rightarrow eLpNormEssSup(f,μ) ≤ eLpNormEssSup(g,μ)$.$$

Lean4

theorem eLpNormEssSup_mono_nnnorm_ae {f g : α → F} (hfg : ∀ᵐ x ∂μ, ‖f x‖₊ ≤ ‖g x‖₊) :
    eLpNormEssSup f μ ≤ eLpNormEssSup g μ :=
  essSup_mono_ae <| hfg.mono fun _x hx => ENNReal.coe_le_coe.mpr hx

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