From d9e40b4411a27d38e68a7f0ef0f7a217971e5e2f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 23 Nov 2021 13:11:55 +0000 Subject: [PATCH] chore(measure_theory/integral): generalize `interval_integral.norm_integral_le_integral_norm` (#10412) MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit It was formulated only for functions `f : α → ℝ`; generalize to `f : α → E`. --- src/measure_theory/integral/interval_integral.lean | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/src/measure_theory/integral/interval_integral.lean b/src/measure_theory/integral/interval_integral.lean index 2967281355783..24eff7771da40 100644 --- a/src/measure_theory/integral/interval_integral.lean +++ b/src/measure_theory/integral/interval_integral.lean @@ -521,6 +521,10 @@ begin exact le_trans (norm_integral_le_integral_norm _) (le_abs_self _) end +lemma 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_Ioc.trans_eq $ by rw [interval_oc_of_le h, integral_of_le h] + lemma norm_integral_le_of_norm_le_const_ae {a b C : ℝ} {f : ℝ → E} (h : ∀ᵐ x, x ∈ Ι a b → ∥f x∥ ≤ C) : ∥∫ x in a..b, f x∥ ≤ C * |b - a| := @@ -1176,14 +1180,9 @@ lemma integral_nonneg [topological_space α] [opens_measurable_space α] [order_ 0 ≤ (∫ u in a..b, f u ∂μ) := integral_nonneg_of_ae_restrict hab $ (ae_restrict_iff' measurable_set_Icc).mpr $ ae_of_all μ hf -lemma norm_integral_le_integral_norm : - ∥∫ x in a..b, f x ∂μ∥ ≤ ∫ x in a..b, ∥f x∥ ∂μ := -norm_integral_le_abs_integral_norm.trans_eq $ - abs_of_nonneg $ integral_nonneg_of_forall hab $ λ x, norm_nonneg _ - lemma abs_integral_le_integral_abs : |∫ x in a..b, f x ∂μ| ≤ ∫ x in a..b, |f x| ∂μ := -norm_integral_le_integral_norm hab +by simpa only [← real.norm_eq_abs] using norm_integral_le_integral_norm hab section mono