norm_integral_le_lintegral_norm — Mathlib

English

The norm of the integral is bounded above by the Lintegral of the norm: ||∫ f|| ≤ ∫ ‖f‖.

Русский

Норма интеграла не превосходит линтеграл нормы: ||∫ f|| ≤ ∫ ‖f‖.

LaTeX

$$$\|\int a, f(a) \partial μ\| \leq \int a, \|f(a)\| \partial μ$$$

Lean4

theorem norm_integral_le_lintegral_norm (f : α → G) : ‖∫ a, f a ∂μ‖ ≤ ENNReal.toReal (∫⁻ a, ENNReal.ofReal ‖f a‖ ∂μ) :=
  by
  by_cases hG : CompleteSpace G
  · by_cases hf : Integrable f μ
    · rw [integral_eq f hf, ← Integrable.norm_toL1_eq_lintegral_norm f hf]
      exact L1.norm_integral_le _
    · rw [integral_undef hf, norm_zero]; exact toReal_nonneg
  · simp [integral, hG]

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