norm_integral_le — Mathlib

English

For any f in L1(μ;E), the norm of its Bochner integral is no larger than the L1-norm of f.

Русский

Для любого f из L1(μ;E) норма его Бо́хнерова интеграла не превосходит L1‑нормы f.

LaTeX

$$$\\|\\int f\\| \\le \\|f\\|_{L^1(μ;E)}$$$

Lean4

theorem norm_integral_le (f : α →₁[μ] E) : ‖integral f‖ ≤ ‖f‖ :=
  calc
    ‖integral f‖ = ‖integralCLM f‖ := by simp only [integral]
    _ ≤ ‖integralCLM (α := α) (μ := μ)‖ * ‖f‖ := (le_opNorm _ _)
    _ ≤ 1 * ‖f‖ := (mul_le_mul_of_nonneg_right norm_Integral_le_one <| norm_nonneg _)
    _ = ‖f‖ := one_mul _

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