feat: |∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ (#20540)

From LeanAPAP
leanprover-community · Jan 8, 2025 · a5183c3 · a5183c3
1 parent 7cfa4bd
commit a5183c3
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/Mathlib/MeasureTheory/Integral/Bochner.lean b/Mathlib/MeasureTheory/Integral/Bochner.lean
@@ -1367,6 +1367,9 @@ theorem norm_integral_le_integral_norm (f : α → G) : ‖∫ a, f a ∂μ‖
   · rw [integral_non_aestronglyMeasurable h, norm_zero]
     exact integral_nonneg_of_ae le_ae
 
+lemma abs_integral_le_integral_abs {f : α → ℝ} : |∫ a, f a ∂μ| ≤ ∫ a, |f a| ∂μ :=
+  norm_integral_le_integral_norm f
+
 theorem norm_integral_le_of_norm_le {f : α → G} {g : α → ℝ} (hg : Integrable g μ)
     (h : ∀ᵐ x ∂μ, ‖f x‖ ≤ g x) : ‖∫ x, f x ∂μ‖ ≤ ∫ x, g x ∂μ :=
   calc