From 2f1f7b9c5ff87506a38b2ead588636117fe9a13c Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Mon, 6 Jan 2025 22:50:54 +0000 Subject: [PATCH] feat: add @[simp] lemma Prod.norm_mk (#20411) --- Mathlib/Analysis/Normed/Group/Constructions.lean | 14 ++++++++++++-- Mathlib/Analysis/Normed/Lp/ProdLp.lean | 2 +- .../Analysis/NormedSpace/Multilinear/Basic.lean | 2 +- .../NumberField/CanonicalEmbedding/Basic.lean | 2 +- 4 files changed, 15 insertions(+), 5 deletions(-) diff --git a/Mathlib/Analysis/Normed/Group/Constructions.lean b/Mathlib/Analysis/Normed/Group/Constructions.lean index 95eb19382e965..5a2a7e261e62b 100644 --- a/Mathlib/Analysis/Normed/Group/Constructions.lean +++ b/Mathlib/Analysis/Normed/Group/Constructions.lean @@ -229,6 +229,8 @@ instance Prod.toNorm : Norm (E × F) where norm x := ‖x.1‖ ⊔ ‖x.2‖ lemma Prod.norm_def (x : E × F) : ‖x‖ = max ‖x.1‖ ‖x.2‖ := rfl +@[simp] lemma Prod.norm_mk (x : E) (y : F) : ‖(x, y)‖ = max ‖x‖ ‖y‖ := rfl + lemma norm_fst_le (x : E × F) : ‖x.1‖ ≤ ‖x‖ := le_max_left _ _ lemma norm_snd_le (x : E × F) : ‖x.2‖ ≤ ‖x‖ := le_max_right _ _ @@ -246,8 +248,16 @@ instance Prod.seminormedGroup : SeminormedGroup (E × F) where dist_eq x y := by simp only [Prod.norm_def, Prod.dist_eq, dist_eq_norm_div, Prod.fst_div, Prod.snd_div] -@[to_additive Prod.nnnorm_def'] -lemma Prod.nnorm_def (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ := rfl +/-- Multiplicative version of `Prod.nnnorm_def`. +Earlier, this names was used for the additive version. -/ +@[to_additive Prod.nnnorm_def] +lemma Prod.nnnorm_def' (x : E × F) : ‖x‖₊ = max ‖x.1‖₊ ‖x.2‖₊ := rfl + +@[deprecated (since := "2025-01-02")] alias Prod.nnorm_def := Prod.nnnorm_def' + +/-- Multiplicative version of `Prod.nnnorm_mk`. -/ +@[to_additive (attr := simp) Prod.nnnorm_mk] +lemma Prod.nnnorm_mk' (x : E) (y : F) : ‖(x, y)‖₊ = max ‖x‖₊ ‖y‖₊ := rfl end SeminormedGroup diff --git a/Mathlib/Analysis/Normed/Lp/ProdLp.lean b/Mathlib/Analysis/Normed/Lp/ProdLp.lean index d94faf96a1d7e..be6e704e2ad40 100644 --- a/Mathlib/Analysis/Normed/Lp/ProdLp.lean +++ b/Mathlib/Analysis/Normed/Lp/ProdLp.lean @@ -616,7 +616,7 @@ theorem prod_nnnorm_eq_sup (f : WithLp ∞ (α × β)) : ‖f‖₊ = ‖f.fst norm_cast @[simp] theorem prod_nnnorm_equiv (f : WithLp ∞ (α × β)) : ‖WithLp.equiv ⊤ _ f‖₊ = ‖f‖₊ := by - rw [prod_nnnorm_eq_sup, Prod.nnnorm_def', equiv_fst, equiv_snd] + rw [prod_nnnorm_eq_sup, Prod.nnnorm_def, equiv_fst, equiv_snd] @[simp] theorem prod_nnnorm_equiv_symm (f : α × β) : ‖(WithLp.equiv ⊤ _).symm f‖₊ = ‖f‖₊ := (prod_nnnorm_equiv _).symm diff --git a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean index c6c4a0ad92ef2..d7bef54d16d58 100644 --- a/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean +++ b/Mathlib/Analysis/NormedSpace/Multilinear/Basic.lean @@ -535,7 +535,7 @@ theorem isLeast_opNNNorm (f : ContinuousMultilinearMap 𝕜 E G) : theorem opNNNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') : ‖f.prod g‖₊ = max ‖f‖₊ ‖g‖₊ := eq_of_forall_ge_iff fun _ ↦ by - simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def', max_le_iff, forall_and] + simp only [opNNNorm_le_iff, prod_apply, Prod.nnnorm_def, max_le_iff, forall_and] theorem opNorm_prod (f : ContinuousMultilinearMap 𝕜 E G) (g : ContinuousMultilinearMap 𝕜 E G') : ‖f.prod g‖ = max ‖f‖ ‖g‖ := diff --git a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean index 3b10a1368dea7..4101379ae8266 100644 --- a/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean +++ b/Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean @@ -388,7 +388,7 @@ theorem nnnorm_eq_sup_normAtPlace (x : mixedSpace K) : (univ.image (fun w : {w : InfinitePlace K // IsComplex w} ↦ w.1)) := by ext; simp [isReal_or_isComplex] rw [this, sup_union, univ.sup_image, univ.sup_image, - Prod.nnnorm_def', Pi.nnnorm_def, Pi.nnnorm_def] + Prod.nnnorm_def, Pi.nnnorm_def, Pi.nnnorm_def] congr · ext w simp [normAtPlace_apply_isReal w.prop]