From e9f0a88e5333f1edc2843a9164fb035a96406f5e Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Sat, 19 Oct 2024 21:53:49 +0000 Subject: [PATCH] feat(Normed/Group): add `nndist_one_right` etc (#17954) Add - `nndist_one_right`, `nndist_zero_right`, `nndist_one_left`, `nndist_zero_left`; - `edist_one_right`, `edist_zero_right`, `edist_one_left`, `edist_zero_left`. --- Mathlib/Analysis/Normed/Group/Basic.lean | 14 ++++++++++++++ Mathlib/MeasureTheory/Function/L1Space.lean | 6 ++---- 2 files changed, 16 insertions(+), 4 deletions(-) diff --git a/Mathlib/Analysis/Normed/Group/Basic.lean b/Mathlib/Analysis/Normed/Group/Basic.lean index e379a64547598..b3742ef73f777 100644 --- a/Mathlib/Analysis/Normed/Group/Basic.lean +++ b/Mathlib/Analysis/Normed/Group/Basic.lean @@ -635,6 +635,13 @@ theorem nndist_eq_nnnorm_div (a b : E) : nndist a b = ‖a / b‖₊ := alias nndist_eq_nnnorm := nndist_eq_nnnorm_sub +@[to_additive (attr := simp)] +theorem nndist_one_right (a : E) : nndist a 1 = ‖a‖₊ := by simp [nndist_eq_nnnorm_div] + +@[to_additive (attr := simp)] +theorem edist_one_right (a : E) : edist a 1 = ‖a‖₊ := by + rw [edist_nndist, nndist_one_right] + @[to_additive (attr := simp) nnnorm_zero] theorem nnnorm_one' : ‖(1 : E)‖₊ = 0 := NNReal.eq norm_one' @@ -653,6 +660,13 @@ theorem nnnorm_mul_le' (a b : E) : ‖a * b‖₊ ≤ ‖a‖₊ + ‖b‖₊ := theorem nnnorm_inv' (a : E) : ‖a⁻¹‖₊ = ‖a‖₊ := NNReal.eq <| norm_inv' a +@[to_additive (attr := simp)] +theorem nndist_one_left (a : E) : nndist 1 a = ‖a‖₊ := by simp [nndist_eq_nnnorm_div] + +@[to_additive (attr := simp)] +theorem edist_one_left (a : E) : edist 1 a = ‖a‖₊ := by + rw [edist_nndist, nndist_one_left] + open scoped symmDiff in @[to_additive] theorem nndist_mulIndicator (s t : Set α) (f : α → E) (x : α) : diff --git a/Mathlib/MeasureTheory/Function/L1Space.lean b/Mathlib/MeasureTheory/Function/L1Space.lean index 9994ae4d6e8b1..87c029742d760 100644 --- a/Mathlib/MeasureTheory/Function/L1Space.lean +++ b/Mathlib/MeasureTheory/Function/L1Space.lean @@ -1375,12 +1375,10 @@ theorem edist_toL1_toL1 (f g : α → β) (hf : Integrable f μ) (hg : Integrabl ENNReal.rpow_one, ne_eq, not_false_eq_true, div_self, ite_false] simp [edist_eq_coe_nnnorm_sub] -@[simp] theorem edist_toL1_zero (f : α → β) (hf : Integrable f μ) : edist (hf.toL1 f) 0 = ∫⁻ a, edist (f a) 0 ∂μ := by - simp only [toL1, Lp.edist_toLp_zero, eLpNorm, one_ne_zero, eLpNorm', one_toReal, ENNReal.rpow_one, - ne_eq, not_false_eq_true, div_self, ite_false] - simp [edist_eq_coe_nnnorm] + simp only [edist_zero_right, Lp.nnnorm_coe_ennreal, toL1_eq_mk, eLpNorm_aeeqFun] + apply eLpNorm_one_eq_lintegral_nnnorm variable {𝕜 : Type*} [NormedRing 𝕜] [Module 𝕜 β] [BoundedSMul 𝕜 β]