integralCLM

Mathlib.MeasureTheory.Integral.Bochner.L1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.L1.SimpleFunc.integralCLM

← MathLib Explorer

English

The operator norm of the integral CLM is at most 1: the CLM has operator norm ≤ 1.

Русский

Нормa операторa интеграла CLM не превосходит 1: нормa оператора не более единицы.

LaTeX

$$$\|\text{integralCLM} \| \le 1$$$

Lean4

/-- The Bochner integral over simple functions in L1 space as a continuous linear map over ℝ. -/
def integralCLM : (α →₁ₛ[μ] E) →L[ℝ] E :=
  integralCLM' α E ℝ μ

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

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

Разделы

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

Аффилиация

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