norm_integral_le_abs_of_norm_le — Mathlib

English

Suppose f: ℝ → ℝ and ae-conditions ensure ‖f(t)‖ ≤ g(t) on Ι a b with g integrable; then ∥∫ f∥ ≤ |∫ g|.

Русский

Пусть f: ℝ → ℝ и выполняются условия AE, что ‖f(t)‖ ≤ g(t) на Ι a b и g интегрируем; тогда ∥∫ f∥ ≤ |∫ g|.

LaTeX

$$$\|\int_{a}^{b} f(t) \, dμ\| \leq |\int_{a}^{b} g(t) \, dμ|$$

Lean4

theorem norm_integral_le_abs_of_norm_le {g : ℝ → ℝ} (h : ∀ᵐ t ∂μ.restrict <| Ι a b, ‖f t‖ ≤ g t)
    (hbound : IntervalIntegrable g μ a b) : ‖∫ t in a..b, f t ∂μ‖ ≤ |∫ t in a..b, g t ∂μ| :=
  by
  rw [norm_intervalIntegral_eq, abs_intervalIntegral_eq]
  exact (norm_integral_le_of_norm_le hbound.def' h).trans (le_abs_self _)

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