eLpNorm_mono_real — Mathlib

English

If ∀ᵐ x, ‖f(x)‖₊ ≤ ‖g(x)‖₊, then eLpNormEssSup f μ ≤ eLpNormEssSup g μ.

Русский

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

LaTeX

$$$\\ae x, \\|f(x)\\|_{nn} ≤ \\|g(x)\\|_{nn} \\Rightarrow eLpNormEssSup(f,μ) ≤ eLpNormEssSup(g,μ)$.$$

Lean4

theorem eLpNorm_mono_real {f : α → F} {g : α → ℝ} (h : ∀ x, ‖f x‖ ≤ g x) : eLpNorm f p μ ≤ eLpNorm g p μ :=
  eLpNorm_mono_ae_real (Eventually.of_forall h)

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