eLpNorm_mono_ae' — Mathlib

English

If a measurable function is almost everywhere bounded by a real number C, then eLpNormEssSup ≤ ENNReal.ofReal C.

Русский

Если функция ограничена почти всюду разумным числом C, то eLpNormEssSup ≤ ENNReal.ofReal C.

LaTeX

$$$\\forall^{ae} x, \\|f(x)\\| ≤ C \\Rightarrow eLpNormEssSup(f,μ) ≤ ENNReal.ofReal C$.$$

Lean4

theorem eLpNorm_mono_ae' {ε' : Type*} [ENorm ε'] {f : α → ε} {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)

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