enorm_ae_le_eLpNormEssSup

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

← MathLib Explorer

English

For f: α → ε, almost everywhere, the ENorm of f(x) is ≤ eLpNormEssSup f μ.

Русский

Пусть f: α → ε. Почти всюду ENorm(f(x)) ≤ eLpNormEssSup f μ.

LaTeX

$$∀ᵐ x ∂μ, ∥f(x)∥ₑ ≤ eLpNormEssSup f μ$$

Lean4

theorem enorm_ae_le_eLpNormEssSup {_ : MeasurableSpace α} (f : α → ε) (μ : Measure α) :
    ∀ᵐ x ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ :=
  ENNReal.ae_le_essSup fun x => ‖f x‖ₑ

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

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

Разделы

MathLib Explorer
Graph RAG
Лаборатория
Блог
О проекте
Команда

Аффилиация

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