norm_integral_le_integral_norm — Mathlib

English

If a ≤ b, then the norm of the integral is bounded by the integral of the norm over [a,b]: ∥∫_{a}^{b} f x dμ∥ ≤ ∫_{a}^{b} ∥f x∥ dμ.

Русский

Если a ≤ b, то норма интеграла по [a,b] не превышает интеграл нормы: ∥∫_{a}^{b} f(x) dx∥ ≤ ∫_{a}^{b} ∥f(x)∥ dx.

LaTeX

$$$\|\int_{a}^{b} f(x) \, d\mu\| \leq \int_{a}^{b} \|f(x)\| \, d\mu$$$

Lean4

theorem norm_integral_le_integral_norm (h : a ≤ b) : ‖∫ x in a..b, f x ∂μ‖ ≤ ∫ x in a..b, ‖f x‖ ∂μ :=
  norm_integral_le_integral_norm_uIoc.trans_eq <| by rw [uIoc_of_le h, integral_of_le h]

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