abs_integral_le_integral_abs — Mathlib

English

For any f on [a,b], the absolute value of its integral is bounded by the integral of the absolute value: |∫ f| ≤ ∫ |f|.

Русский

Для любого f на [a,b] модуль интеграла меньше либо равен интегралу модуля: |∫ f| ≤ ∫ |f|.

LaTeX

$$$|\\int_a^b f(x)\\,d\\mu| \\le \\int_a^b |f(x)|\\,d\\mu$.$$

Lean4

theorem abs_integral_le_integral_abs (hab : a ≤ b) : |∫ x in a..b, f x ∂μ| ≤ ∫ x in a..b, |f x| ∂μ := by
  simpa only [← Real.norm_eq_abs] using norm_integral_le_integral_norm hab

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