integral_eq_setToL1 — Mathlib

English

The L1 Bochner integral operator in the real setting forms a continuous linear map, with respect to Real scalars, from simple L1 functions to E.

Русский

Оператор интеграла Бо́хнера в L1 над Real образует непрерывное линейное отображение из простых функций L1 в E по вещественным скалярам.

LaTeX

$$$\text{integralCLM} : (\alpha \to_1[\mu] E) \to_L[\mathbb{R}] E$$$

Lean4

theorem integral_eq_setToL1 (f : α →₁[μ] E) : integral f = setToL1 (dominatedFinMeasAdditive_weightedSMul μ) f := by
  simp only [integral]; rfl

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