integralCLM' — Mathlib

English

The Bochner integral over simple functions in L1 forms a continuous linear map (CLM) from the L1-simple function space to E, with respect to the real scalar field, i.e., a continuous linear operator.

Русский

Пусть существуют непрерывно линейные отображения для интеграла Бо́хнера на простых функций в L1, образующие непрерывно-линейное отображение из пространства L1 в E.

LaTeX

$$$\text{integralCLM}' : (\alpha \to \!₁[μ] E) \to_L[\mathbb{R}] E$$$

Lean4

/-- The Bochner integral over simple functions in L1 space as a continuous linear map. -/
def integralCLM' : (α →₁ₛ[μ] E) →L[𝕜] E :=
  LinearMap.mkContinuous ⟨⟨integral, integral_add⟩, integral_smul⟩ 1 fun f =>
    le_trans (norm_integral_le_norm _) <| by rw [one_mul]

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