eLpNormEssSup_count

Mathlib.MeasureTheory.Function.LpSeminorm.Basic

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

English

If μ assigns nonzero mass to every singleton, the ess sup of f with respect to μ equals the iSup over a∈α of ‖f(a)‖ₑ.

Русский

Если μ(\{a\}) ≠ 0 для всех a, ess sup f(μ) = ⨆ a, ‖f(a)‖ₑ.

LaTeX

$$eLpNormEssSup f μ = ⨆ a, ‖f a‖ₑ.$$

Lean4

@[simp]
theorem eLpNormEssSup_count [MeasurableSingletonClass α] (f : α → ε) : eLpNormEssSup f .count = ⨆ a, ‖f a‖ₑ :=
  essSup_count _

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

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

Разделы

Аффилиация

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