integral — Mathlib

English

The norm of the integral of a simple function is bounded by the integral of the norm of the function.

Русский

Норма интеграла простой функции ограничена интегралом нормы самой функции.

LaTeX

$$$$ \\|f_{integral}\\| \\le (f.map \\|\\cdot\\|)_{integral} $$$$

Lean4

/-- The Bochner integral over simple functions in L1 space. -/
def integral (f : α →₁ₛ[μ] E) : E :=
  (toSimpleFunc f).integral μ

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