eLpNorm_mono_enorm_ae — Mathlib

English

If f =ᵐ[μ] g, then eLpNormEssSup(f,μ) = eLpNormEssSup(g,μ).

Русский

Если функции равны почти всюду, их essSup равны.

LaTeX

$$$f =^{ae}_{μ} g \\Rightarrow eLpNormEssSup(f,μ) = eLpNormEssSup(g,μ)$.$$

Lean4

theorem eLpNorm_mono_enorm_ae {f : α → ε} {g : α → ε'} (h : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ ‖g x‖ₑ) : eLpNorm f p μ ≤ eLpNorm g p μ :=
  by
  simp only [eLpNorm]
  split_ifs
  · exact le_rfl
  · exact essSup_mono_ae h
  · exact eLpNorm'_mono_enorm_ae ENNReal.toReal_nonneg h

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