From d7abdff7d5abd82d0fbdf795e2a0766150e06c42 Mon Sep 17 00:00:00 2001
From: hrmacbeth <25316162+hrmacbeth@users.noreply.github.com>
Date: Wed, 29 Sep 2021 04:03:07 +0000
Subject: [PATCH] chore(analysis/normed_space/*): prereqs for #8611 (#9379)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

The functions `abs` and `norm_sq` on `ℂ` are proper.

A matrix with entries in a {seminormed group, normed group, normed space} is itself a {seminormed group, normed group, normed space}.

An injective linear map with finite-dimensional domain is a closed embedding.
---
 src/analysis/complex/basic.lean               | 10 ++++++
 src/analysis/normed_space/basic.lean          | 33 +++++++++++++++++++
 .../normed_space/finite_dimension.lean        | 22 +++++++------
 3 files changed, 55 insertions(+), 10 deletions(-)

diff --git a/src/analysis/complex/basic.lean b/src/analysis/complex/basic.lean
index 813761ab73f10..4fcf1b122c5ee 100644
--- a/src/analysis/complex/basic.lean
+++ b/src/analysis/complex/basic.lean
@@ -84,6 +84,16 @@ by rw [norm_int, _root_.abs_of_nonneg]; exact int.cast_nonneg.2 hn
 @[continuity] lemma continuous_norm_sq : continuous norm_sq :=
 by simpa [← norm_sq_eq_abs] using continuous_abs.pow 2
 
+/-- The `abs` function on `ℂ` is proper. -/
+lemma tendsto_abs_cocompact_at_top : filter.tendsto abs (filter.cocompact ℂ) filter.at_top :=
+tendsto_norm_cocompact_at_top
+
+/-- The `norm_sq` function on `ℂ` is proper. -/
+lemma tendsto_norm_sq_cocompact_at_top :
+  filter.tendsto norm_sq (filter.cocompact ℂ) filter.at_top :=
+by simpa [mul_self_abs] using
+  tendsto_abs_cocompact_at_top.at_top_mul_at_top tendsto_abs_cocompact_at_top
+
 open continuous_linear_map
 
 /-- Continuous linear map version of the real part function, from `ℂ` to `ℝ`. -/
diff --git a/src/analysis/normed_space/basic.lean b/src/analysis/normed_space/basic.lean
index a2f2b6f6c6eea..b2af2758de2aa 100644
--- a/src/analysis/normed_space/basic.lean
+++ b/src/analysis/normed_space/basic.lean
@@ -5,6 +5,7 @@ Authors: Patrick Massot, Johannes Hölzl
 -/
 import algebra.algebra.restrict_scalars
 import algebra.algebra.subalgebra
+import data.matrix.basic
 import order.liminf_limsup
 import topology.algebra.group_completion
 import topology.instances.ennreal
@@ -1180,6 +1181,20 @@ instance prod.semi_normed_ring [semi_normed_ring β] : semi_normed_ring (α × 
         ... = (∥x∥*∥y∥) : rfl,
   ..prod.semi_normed_group }
 
+/-- Seminormed group instance (using sup norm of sup norm) for matrices over a seminormed ring. Not
+declared as an instance because there are several natural choices for defining the norm of a
+matrix. -/
+def matrix.semi_normed_group {n m : Type*} [fintype n] [fintype m] :
+  semi_normed_group (matrix n m α) :=
+pi.semi_normed_group
+
+local attribute [instance] matrix.semi_normed_group
+
+lemma semi_norm_matrix_le_iff {n m : Type*} [fintype n] [fintype m] {r : ℝ} (hr : 0 ≤ r)
+  {A : matrix n m α} :
+  ∥A∥ ≤ r ↔ ∀ i j, ∥A i j∥ ≤ r :=
+by simp [pi_semi_norm_le_iff hr]
+
 end semi_normed_ring
 
 section normed_ring
@@ -1194,6 +1209,12 @@ instance prod.normed_ring [normed_ring β] : normed_ring (α × β) :=
 { norm_mul := norm_mul_le,
   ..prod.semi_normed_group }
 
+/-- Normed group instance (using sup norm of sup norm) for matrices over a normed ring.  Not
+declared as an instance because there are several natural choices for defining the norm of a
+matrix. -/
+def matrix.normed_group {n m : Type*} [fintype n] [fintype m] : normed_group (matrix n m α) :=
+pi.normed_group
+
 end normed_ring
 
 @[priority 100] -- see Note [lower instance priority]
@@ -1755,6 +1776,18 @@ instance pi.normed_space {E : ι → Type*} [fintype ι] [∀i, normed_group (E
   [∀i, normed_space α (E i)] : normed_space α (Πi, E i) :=
 { ..pi.semi_normed_space }
 
+section
+local attribute [instance] matrix.normed_group
+
+/-- Normed space instance (using sup norm of sup norm) for matrices over a normed field.  Not
+declared as an instance because there are several natural choices for defining the norm of a
+matrix. -/
+def matrix.normed_space {α : Type*} [normed_field α] {n m : Type*} [fintype n] [fintype m] :
+  normed_space α (matrix n m α) :=
+pi.normed_space
+
+end
+
 /-- A subspace of a normed space is also a normed space, with the restriction of the norm. -/
 instance submodule.normed_space {𝕜 R : Type*} [has_scalar 𝕜 R] [normed_field 𝕜] [ring R]
   {E : Type*} [normed_group E] [normed_space 𝕜 E] [module R E]
diff --git a/src/analysis/normed_space/finite_dimension.lean b/src/analysis/normed_space/finite_dimension.lean
index c596227d74706..f03c00355af6c 100644
--- a/src/analysis/normed_space/finite_dimension.lean
+++ b/src/analysis/normed_space/finite_dimension.lean
@@ -550,6 +550,17 @@ end
 
 end riesz
 
+/-- An injective linear map with finite-dimensional domain is a closed embedding. -/
+lemma linear_equiv.closed_embedding_of_injective {f : E →ₗ[𝕜] F} (hf : f.ker = ⊥)
+  [finite_dimensional 𝕜 E] :
+  closed_embedding ⇑f :=
+let g := linear_equiv.of_injective f (linear_map.ker_eq_bot.mp hf) in
+{ closed_range := begin
+    haveI := f.finite_dimensional_range,
+    simpa [f.range_coe] using f.range.closed_of_finite_dimensional
+  end,
+  .. embedding_subtype_coe.comp g.to_continuous_linear_equiv.to_homeomorph.embedding }
+
 lemma continuous_linear_map.exists_right_inverse_of_surjective [finite_dimensional 𝕜 F]
   (f : E →L[𝕜] F) (hf : f.range = ⊤) :
   ∃ g : F →L[𝕜] E, f.comp g = continuous_linear_map.id 𝕜 F :=
@@ -557,16 +568,7 @@ let ⟨g, hg⟩ := (f : E →ₗ[𝕜] F).exists_right_inverse_of_surjective hf
 ⟨g.to_continuous_linear_map, continuous_linear_map.ext $ linear_map.ext_iff.1 hg⟩
 
 lemma closed_embedding_smul_left {c : E} (hc : c ≠ 0) : closed_embedding (λ x : 𝕜, x • c) :=
-begin
-  haveI : finite_dimensional 𝕜 (submodule.span 𝕜 {c}) :=
-    finite_dimensional.span_of_finite 𝕜 (finite_singleton c),
-  have m1 : closed_embedding (coe : submodule.span 𝕜 {c} → E) :=
-  (submodule.span 𝕜 {c}).closed_of_finite_dimensional.closed_embedding_subtype_coe,
-  have m2 : closed_embedding
-    (linear_equiv.to_span_nonzero_singleton 𝕜 E c hc : 𝕜 → submodule.span 𝕜 {c}) :=
-  (continuous_linear_equiv.to_span_nonzero_singleton 𝕜 c hc).to_homeomorph.closed_embedding,
-  exact m1.comp m2
-end
+linear_equiv.closed_embedding_of_injective (linear_equiv.ker_to_span_singleton 𝕜 E hc)
 
 /- `smul` is a closed map in the first argument. -/
 lemma is_closed_map_smul_left (c : E) : is_closed_map (λ x : 𝕜, x • c) :=