eLpNormEssSup_le_of_ae_enorm_bound

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

URI: https://scilib.ai/kg/mathlib#MeasureTheory.eLpNormEssSup_le_of_ae_enorm_bound

English

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

Русский

Если f и g равны почти всюду, essSup совпадает.

LaTeX

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

Lean4

theorem eLpNormEssSup_le_of_ae_enorm_bound {f : α → ε} {C : ℝ≥0∞} (hfC : ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ C) : eLpNormEssSup f μ ≤ C :=
  essSup_le_of_ae_le C hfC

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru