norm_integral_le_integral_norm_uIoc

English

For any f: ℝ → E, the norm of the integral over a..b is bounded by the integral of the norm of f over I a b: ∥∫_{a}^{b} f x dμ∥ ≤ ∫_{Ι a b} ∥f x∥ dμ.

Русский

Для любой функции f: ℝ → E справедливо: ∥∫_{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_uIoc : ‖∫ x in a..b, f x ∂μ‖ ≤ ∫ x in Ι a b, ‖f x‖ ∂μ :=
  calc
    ‖∫ x in a..b, f x ∂μ‖ = ‖∫ x in Ι a b, f x ∂μ‖ := norm_integral_eq_norm_integral_uIoc f
    _ ≤ ∫ x in Ι a b, ‖f x‖ ∂μ := norm_integral_le_integral_norm f

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