eLpNorm_mono_ae — Mathlib

English

If f is almost everywhere bounded by a constant C, then the essential supremum of f is bounded by C.

Русский

Если функция ограничена почти всюду константой C, то ее essSup не превосходит C.

LaTeX

$$$\\forall^* x, \\|f(x)\\| ≤ C \\Rightarrow eLpNormEssSup(f,μ) ≤ C$ (иногда приводится через ENNReal).$$

Lean4

theorem eLpNorm_mono_ae {f : α → F} {g : α → G} (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ ‖g x‖) : eLpNorm f p μ ≤ eLpNorm g p μ :=
  eLpNorm_mono_enorm_ae (by simpa only [enorm_le_iff_norm_le] using h)

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