norm_setToL1_le'

Mathlib.MeasureTheory.Integral.SetToL1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.norm_setToL1_le'

← MathLib Explorer

English

The operator norm of setToL1 is bounded by max{C,0}, i.e., ||setToL1 hT|| ≤ max(C,0).

Русский

Нормa оператора setToL1 не превосходит max(C,0).

LaTeX

$$$\|setToL1\, h_T\| \le \max\{C,0\}$$$

Lean4

theorem norm_setToL1_le' (hT : DominatedFinMeasAdditive μ T C) : ‖setToL1 hT‖ ≤ max C 0 :=
  ContinuousLinearMap.opNorm_le_bound _ (le_max_right _ _) (norm_setToL1_le_mul_norm' hT)

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

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

Разделы

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

Аффилиация

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