feat(analysis/matrix): add frobenius_norm_conj_transpose (#13883)

This also moves the existing lemmas about the elementwise norm to the same file.

src/analysis/matrix.lean

@@ -88,17 +88,27 @@ lemma nnnorm_entry_le_entrywise_sup_nnnorm (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_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_conj_transpose [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
+  ∥Aᴴ∥₊ = ∥A∥₊ :=
+(nnnorm_map_eq _ _ nnnorm_star).trans A.nnnorm_transpose
+@[simp] lemma norm_conj_transpose [star_add_monoid α] [normed_star_group α] (A : matrix m n α) :
+  ∥Aᴴ∥ = ∥A∥ :=
+congr_arg coe $ nnnorm_conj_transpose A
+
+instance [star_add_monoid α] [normed_star_group α] : normed_star_group (matrix m m α) :=
+⟨norm_conj_transpose⟩
+
 @[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
 
@@ -360,18 +370,29 @@ lemma frobenius_norm_def (A : matrix m n α) :
   ∥A∥ = (∑ i j, ∥A i j∥ ^ (2 : ℝ)) ^ (1/2 : ℝ) :=
 (congr_arg coe (frobenius_nnnorm_def A)).trans $ by simp [nnreal.coe_sum]
 
-@[simp] lemma frobenius_nnnorm_transpose (A : matrix m n α) : ∥Aᵀ∥₊ = ∥A∥₊ :=
-by { rw [frobenius_nnnorm_def, frobenius_nnnorm_def, finset.sum_comm], refl }
-@[simp] lemma frobenius_norm_transpose (A : matrix m n α) : ∥Aᵀ∥ = ∥A∥ :=
-congr_arg coe $ frobenius_nnnorm_transpose A
-
 @[simp] lemma frobenius_nnnorm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥₊ = ∥a∥₊) :
   ∥A.map f∥₊ = ∥A∥₊ :=
 by simp_rw [frobenius_nnnorm_def, matrix.map, hf]
 @[simp] lemma frobenius_norm_map_eq (A : matrix m n α) (f : α → β) (hf : ∀ a, ∥f a∥ = ∥a∥) :
   ∥A.map f∥ = ∥A∥ :=
 (congr_arg (coe : ℝ≥0 → ℝ) $ frobenius_nnnorm_map_eq A f $ λ a, subtype.ext $ hf a : _)
 
+@[simp] lemma frobenius_nnnorm_transpose (A : matrix m n α) : ∥Aᵀ∥₊ = ∥A∥₊ :=
+by { rw [frobenius_nnnorm_def, frobenius_nnnorm_def, finset.sum_comm], refl }
+@[simp] lemma frobenius_norm_transpose (A : matrix m n α) : ∥Aᵀ∥ = ∥A∥ :=
+congr_arg coe $ frobenius_nnnorm_transpose A
+
+@[simp] lemma frobenius_nnnorm_conj_transpose [star_add_monoid α] [normed_star_group α]
+  (A : matrix m n α) : ∥Aᴴ∥₊ = ∥A∥₊ :=
+(frobenius_nnnorm_map_eq _ _ nnnorm_star).trans A.frobenius_nnnorm_transpose
+@[simp] lemma frobenius_norm_conj_transpose [star_add_monoid α] [normed_star_group α]
+  (A : matrix m n α) : ∥Aᴴ∥ = ∥A∥ :=
+congr_arg coe $ frobenius_nnnorm_conj_transpose A
+
+instance frobenius_normed_star_group [star_add_monoid α] [normed_star_group α] :
+  normed_star_group (matrix m m α) :=
+⟨frobenius_norm_conj_transpose⟩
+
 @[simp] lemma frobenius_norm_row (v : m → α) : ∥row v∥ = ∥(pi_Lp.equiv 2 _).symm v∥ :=
 by { rw [frobenius_norm_def, fintype.sum_unique], refl }
 @[simp] lemma frobenius_nnnorm_row (v : m → α) : ∥row v∥₊ = ∥(pi_Lp.equiv 2 _).symm v∥₊ :=

src/analysis/normed_space/star/matrix.lean

@@ -18,22 +18,6 @@ open_locale big_operators matrix
 
 variables {𝕜 m n E : Type*}
 
-namespace matrix
-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 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
-
-instance : normed_star_group (matrix n n E) :=
-⟨matrix.norm_conj_transpose⟩
-
-end matrix
-
 section entrywise_sup_norm
 variables [is_R_or_C 𝕜] [fintype n] [decidable_eq n]