meas_eLpNormEssSup_lt

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

Same as above: finiteness of eLpNormEssSup corresponds to a boundedness under ae.

Русский

То же самое: конечность eLpNormEssSup эквивалентна ограниченности почти всюду.

LaTeX

$$eLpNormEssSup f μ < ⊤ ↔ IsBoundedUnder (· ≤ ·) (ae μ) (fun x => ‖f x‖₊)$$

Lean4

theorem meas_eLpNormEssSup_lt {f : α → ε} : μ {y | eLpNormEssSup f μ < ‖f y‖ₑ} = 0 :=
  meas_essSup_lt

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

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

Разделы

Аффилиация

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