feat(analysis/normed): more lemmas about the sup norm on pi types and…

… matrices (#13536)

For now we name the matrix lemmas as `matrix.norm_*` and `matrix.nnnorm_*` to match `matrix.norm_le_iff` and `matrix.nnnorm_le_iff`.

We should consider renaming these in future to indicate which norm they refer to, but should probably deal with agreeing on a name in a separate PR.

src/analysis/matrix.lean

@@ -20,16 +20,16 @@ of a matrix.
 
 noncomputable theory
 
-open_locale nnreal
+open_locale nnreal matrix
 
 namespace matrix
 
-variables {R m n α : Type*} [fintype m] [fintype n]
+variables {R m n α β : Type*} [fintype m] [fintype n]
 
 section semi_normed_group
-variables [semi_normed_group α]
+variables [semi_normed_group α] [semi_normed_group β]
 
-/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed ring. Not
+/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed group. Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
 protected def semi_normed_group : semi_normed_group (matrix m n α) :=
@@ -61,9 +61,47 @@ lemma nnnorm_entry_le_entrywise_sup_nnorm (A : matrix m n α) {i : m} {j : n} :
   ∥A i j∥₊ ≤ ∥A∥₊ :=
 (nnnorm_le_pi_nnnorm (A i) j).trans (nnnorm_le_pi_nnnorm A i)
 
+@[simp] lemma nnnorm_transpose (A : matrix m n α) : ∥Aᵀ∥₊ = ∥A∥₊ :=
+by { simp_rw [pi.nnnorm_def], exact finset.sup_comm _ _ _ }
+@[simp] lemma norm_transpose (A : matrix m n α) : ∥Aᵀ∥ = ∥A∥ := congr_arg coe $ nnnorm_transpose A
+
+@[simp] lemma nnnorm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥₊ = ∥a∥₊) :
+  ∥A.map f∥₊ = ∥A∥₊ :=
+by simp_rw [pi.nnnorm_def, matrix.map, hf]
+@[simp] lemma norm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥ = ∥a∥) :
+  ∥A.map f∥ = ∥A∥ :=
+(congr_arg (coe : ℝ≥0 → ℝ) $ nnnorm_map_eq A f $ λ a, subtype.ext $ hf a : _)
+
+@[simp] lemma nnnorm_col (v : m → α) : ∥col v∥₊ = ∥v∥₊ := by simp [pi.nnnorm_def]
+@[simp] lemma norm_col (v : m → α) : ∥col v∥ = ∥v∥ := congr_arg coe $ nnnorm_col v
+
+@[simp] lemma nnnorm_row (v : n → α) : ∥row v∥₊ = ∥v∥₊ := by simp [pi.nnnorm_def]
+@[simp] lemma norm_row (v : n → α) : ∥row v∥ = ∥v∥ := congr_arg coe $ nnnorm_row v
+
+@[simp] lemma nnnorm_diagonal [decidable_eq n] (v : n → α) : ∥diagonal v∥₊ = ∥v∥₊ :=
+begin
+  simp_rw pi.nnnorm_def,
+  congr' 1 with i : 1,
+  refine le_antisymm (finset.sup_le $ λ j hj, _) _,
+  { obtain rfl | hij := eq_or_ne i j,
+    { rw diagonal_apply_eq },
+    { rw [diagonal_apply_ne hij, nnnorm_zero],
+      exact zero_le _ }, },
+  { refine eq.trans_le _ (finset.le_sup (finset.mem_univ i)),
+    rw diagonal_apply_eq }
+end
+
+@[simp] lemma norm_diagonal [decidable_eq n] (v : n → α) : ∥diagonal v∥ = ∥v∥ :=
+congr_arg coe $ nnnorm_diagonal v
+
+/-- Note this is safe as an instance as it carries no data. -/
+instance [nonempty n] [decidable_eq n] [has_one α] [norm_one_class α] :
+  norm_one_class (matrix n n α) :=
+⟨(norm_diagonal _).trans $ norm_one⟩
+
 end semi_normed_group
 
-/-- Normed group instance (using sup norm of sup norm) for matrices over a normed ring.  Not
+/-- Normed group instance (using sup norm of sup norm) for matrices over a normed group.  Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
 protected def normed_group [normed_group α] : normed_group (matrix m n α) :=
@@ -74,7 +112,7 @@ local attribute [instance] matrix.semi_normed_group
 
 variables [normed_field R] [semi_normed_group α] [normed_space R α]
 
-/-- Normed space instance (using sup norm of sup norm) for matrices over a normed field.  Not
+/-- Normed space instance (using sup norm of sup norm) for matrices over a normed space.  Not
 declared as an instance because there are several natural choices for defining the norm of a
 matrix. -/
 protected def normed_space : normed_space R (matrix m n α) :=

src/analysis/normed/group/basic.lean

@@ -765,6 +765,12 @@ noncomputable instance pi.semi_normed_group {π : ι → Type*} [fintype ι]
     congr_arg (coe : ℝ≥0 → ℝ) $ congr_arg (finset.sup finset.univ) $ funext $ assume a,
     show nndist (x a) (y a) = ∥x a - y a∥₊, from nndist_eq_nnnorm _ _ }
 
+lemma pi.norm_def {π : ι → Type*} [fintype ι] [Π i, semi_normed_group (π i)] (f : Π i, π i) :
+  ∥f∥ = ↑(finset.univ.sup (λ b, ∥f b∥₊)) := rfl
+
+lemma pi.nnnorm_def {π : ι → Type*} [fintype ι] [Π i, semi_normed_group (π i)] (f : Π i, π i) :
+  ∥f∥₊ = finset.univ.sup (λ b, ∥f b∥₊) := subtype.eta _ _
+
 /-- The seminorm of an element in a product space is `≤ r` if and only if the norm of each
 component is. -/
 lemma pi_norm_le_iff {π : ι → Type*} [fintype ι] [∀i, semi_normed_group (π i)] {r : ℝ}

src/analysis/normed/normed_field.lean

@@ -127,6 +127,11 @@ instance prod.norm_one_class [semi_normed_group α] [has_one α] [norm_one_class
   norm_one_class (α × β) :=
 ⟨by simp [prod.norm_def]⟩
 
+instance pi.norm_one_class {ι : Type*} {α : ι → Type*} [nonempty ι] [fintype ι]
+  [Π i, semi_normed_group (α i)] [Π i, has_one (α i)] [∀ i, norm_one_class (α i)] :
+  norm_one_class (Π i, α i) :=
+⟨by simp [pi.norm_def, finset.sup_const finset.univ_nonempty]⟩
+
 section non_unital_semi_normed_ring
 variables [non_unital_semi_normed_ring α]
 

src/analysis/normed_space/star/matrix.lean

@@ -16,24 +16,21 @@ This file collects facts about the unitary matrices over `𝕜` (either `ℝ` or
 
 open_locale big_operators matrix
 
-variables {𝕜 n E : Type*}
+variables {𝕜 m n E : Type*}
 
 namespace matrix
-variables [fintype n] [semi_normed_group E] [star_add_monoid E] [normed_star_group E]
+variables [fintype m] [fintype n] [semi_normed_group E] [star_add_monoid E] [normed_star_group E]
 
 local attribute [instance] matrix.semi_normed_group
 
-@[simp] lemma entrywise_sup_norm_star_eq_norm (M : matrix n n E) : ∥star M∥ = ∥M∥ :=
-begin
-  refine le_antisymm (by simp [matrix.norm_le_iff, M.norm_entry_le_entrywise_sup_norm]) _,
-  refine ((matrix.norm_le_iff (norm_nonneg _)).mpr (λ i j, _)).trans
-    (congr_arg _ M.star_eq_conj_transpose).ge,
-  exact (norm_star _).ge.trans Mᴴ.norm_entry_le_entrywise_sup_norm
-end
+@[simp] lemma norm_conj_transpose (M : matrix m n E) : ∥Mᴴ∥ = ∥M∥ :=
+(norm_map_eq _ _ norm_star).trans M.norm_transpose
+
+@[simp] lemma nnnorm_conj_transpose (M : matrix m n E) : ∥Mᴴ∥₊ = ∥M∥₊ :=
+subtype.ext M.norm_conj_transpose
 
-@[priority 100] -- see Note [lower instance priority]
-instance to_normed_star_group : normed_star_group (matrix n n E) :=
-⟨matrix.entrywise_sup_norm_star_eq_norm⟩
+instance : normed_star_group (matrix n n E) :=
+⟨matrix.norm_conj_transpose⟩
 
 end matrix