eLpNorm_mono — Mathlib

English

If ∀ᵐ x, ‖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 eLpNorm_mono {f : α → F} {g : α → G} (h : ∀ x, ‖f x‖ ≤ ‖g x‖) : eLpNorm f p μ ≤ eLpNorm g p μ :=
  eLpNorm_mono_ae (Eventually.of_forall h)

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