feat(analysis/normed_space/star/basic): `matrix.entrywise_sup_norm_st…

…ar_eq_norm` (#12201)

This is precisely the statement needed for a `normed_star_monoid`
instance on matrices using the entrywise sup norm.





Co-authored-by: Hans Parshall <hparshall@users.noreply.github.com>
Co-authored-by: Johan Commelin <johan@commelin.net>

src/analysis/normed_space/basic.lean

@@ -288,7 +288,7 @@ def matrix.normed_space {α : Type*} [normed_field α] {n m : Type*} [fintype n]
   normed_space α (matrix n m α) :=
 pi.normed_space
 
-lemma matrix.norm_entry_le_entrywise_sup_norm {α : Type*} [normed_field α] {n m : Type*} [fintype n]
+lemma matrix.norm_entry_le_entrywise_sup_norm {α : Type*} [normed_ring α] {n m : Type*} [fintype n]
   [fintype m] (M : (matrix n m α)) {i : n} {j : m} :
   ∥M i j∥ ≤ ∥M∥ :=
 (norm_le_pi_norm (M i) j).trans (norm_le_pi_norm M i)

src/analysis/normed_space/star/basic.lean

@@ -218,3 +218,25 @@ variables {𝕜}
 lemma starₗᵢ_apply {x : E} : starₗᵢ 𝕜 x = star x := rfl
 
 end starₗᵢ
+
+section matrix
+
+local attribute [instance] matrix.normed_group
+
+open_locale matrix
+
+@[simp] lemma matrix.entrywise_sup_norm_star_eq_norm {n : Type*} [normed_ring E] [star_add_monoid E]
+  [normed_star_group E] [fintype n] (M : (matrix n n E)) : ∥star M∥ = ∥M∥ :=
+begin
+  refine le_antisymm (by simp [norm_matrix_le_iff, M.norm_entry_le_entrywise_sup_norm]) _,
+  refine ((norm_matrix_le_iff (norm_nonneg _)).mpr (λ i j, _)).trans
+    (congr_arg _ M.star_eq_conj_transpose).ge,
+  exact (normed_star_group.norm_star).symm.le.trans Mᴴ.norm_entry_le_entrywise_sup_norm
+end
+
+@[priority 100] -- see Note [lower instance priority]
+instance matrix.to_normed_star_group {n : Type*} [normed_ring E] [star_add_monoid E]
+  [normed_star_group E] [fintype n] : normed_star_group (matrix n n E) :=
+⟨matrix.entrywise_sup_norm_star_eq_norm⟩
+
+end matrix