[Merged by Bors] - feat(normed_space): second countability for linear maps

src/analysis/normed_space/basic.lean

@@ -175,6 +175,16 @@ le_trans (le_abs_self _) (abs_norm_sub_norm_le g h)
 lemma dist_norm_norm_le (g h : α) : dist ∥g∥ ∥h∥ ≤ ∥g - h∥ :=
 abs_norm_sub_norm_le g h
 
+lemma eq_of_norm_sub_eq_zero {u v : α} (h : ∥u - v∥ = 0) : u = v :=
+begin
+  apply eq_of_dist_eq_zero,
+  rwa dist_eq_norm
+end
+
+lemma norm_le_insert (u v : α) : ∥v∥ ≤ ∥u∥ + ∥u - v∥ :=
+calc ∥v∥ = ∥u - (u - v)∥ : by abel
+... ≤ ∥u∥ + ∥u - v∥ : norm_sub_le u _
+
 lemma ball_0_eq (ε : ℝ) : ball (0:α) ε = {x | ∥x∥ < ε} :=
 set.ext $ assume a, by simp
 
@@ -196,6 +206,10 @@ theorem normed_group.tendsto_nhds_zero {f : γ → α} {l : filter γ} :
   tendsto f l (𝓝 0) ↔ ∀ ε > 0, ∀ᶠ x in l, ∥ f x ∥ < ε :=
 metric.tendsto_nhds.trans $ by simp only [dist_zero_right]
 
+lemma normed_group.tendsto_nhds_nhds {f : α → β} {x : α} {y : β} :
+  tendsto f (𝓝 x) (𝓝 y) ↔ ∀ ε > 0, ∃ δ > 0, ∀ x', ∥x' - x∥ < δ → ∥f x' - y∥ < ε :=
+by simp_rw [metric.tendsto_nhds_nhds, dist_eq_norm]
+
 /-- A homomorphism `f` of normed groups is Lipschitz, if there exists a constant `C` such that for
 all `x`, one has `∥f x∥ ≤ C * ∥x∥`.
 The analogous condition for a linear map of normed spaces is in `normed_space.operator_norm`. -/
@@ -779,6 +793,9 @@ lemma nndist_smul [normed_space α β] (s : α) (x y : β) :
   nndist (s • x) (s • y) = nnnorm s * nndist x y :=
 nnreal.eq $ dist_smul s x y
 
+lemma norm_smul_of_nonneg [normed_space ℝ α] {t : ℝ} (ht : 0 ≤ t) (x : α) : ∥t • x∥ = t * ∥x∥ :=
+by rw [norm_smul, real.norm_eq_abs, abs_of_nonneg ht]
+
 variables {E : Type*} {F : Type*}
 [normed_group E] [normed_space α E] [normed_group F] [normed_space α F]
 

src/analysis/normed_space/finite_dimension.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Sébastien Gouëzel
 -/
 import analysis.normed_space.operator_norm
+import topology.bases
 import linear_algebra.finite_dimensional
 import tactic.omega
 
@@ -39,9 +40,11 @@ then the identities from `E` to `E'` and from `E'`to `E` are continuous thanks t
 
 universes u v w x
 
-open set finite_dimensional
+open set finite_dimensional topological_space
 open_locale classical big_operators
 
+noncomputable theory
+
 /-- A linear map on `ι → 𝕜` (where `ι` is a fintype) is continuous -/
 lemma linear_map.continuous_on_pi {ι : Type w} [fintype ι] {𝕜 : Type u} [normed_field 𝕜]
   {E : Type v}  [add_comm_group E] [vector_space 𝕜 E] [topological_space E]
@@ -174,6 +177,122 @@ def linear_equiv.to_continuous_linear_equiv [finite_dimensional 𝕜 E] (e : E 
   end,
   ..e }
 
+variables {ι : Type*} [fintype ι]
+
+/-- Construct a continuous linear map given the value at a finite basis. -/
+def is_basis.constrL {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) :
+  E →L[𝕜] F :=
+⟨hv.constr f, begin
+  haveI : finite_dimensional 𝕜 E := finite_dimensional.of_finite_basis hv,
+  exact (hv.constr f).continuous_of_finite_dimensional,
+end⟩
+
+@[simp, norm_cast] lemma is_basis.coe_constrL {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) :
+  (hv.constrL f : E →ₗ[𝕜] F) = hv.constr f := rfl
+
+/-- The continuous linear equivalence between a vector space over `𝕜` with a finite basis and
+functions from its basis indexing type to `𝕜`. -/
+def is_basis.equiv_funL {v : ι → E} (hv : is_basis 𝕜 v) : E ≃L[𝕜] (ι → 𝕜) :=
+{ continuous_to_fun := begin
+    haveI : finite_dimensional 𝕜 E := finite_dimensional.of_finite_basis hv,
+    apply linear_map.continuous_of_finite_dimensional,
+  end,
+  continuous_inv_fun := begin
+    change continuous hv.equiv_fun.symm.to_fun,
+    apply linear_map.continuous_of_finite_dimensional,
+  end,
+  ..hv.equiv_fun }
+
+
+@[simp] lemma is_basis.constrL_apply {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) (e : E) :
+  (hv.constrL f) e = ∑ i, (hv.equiv_fun e i) • f i :=
+hv.constr_apply_fintype _ _
+
+@[simp] lemma is_basis.constrL_basis {v : ι → E} (hv : is_basis 𝕜 v) (f : ι → F) (i : ι) :
+  (hv.constrL f) (v i) = f i :=
+constr_basis _
+
+lemma is_basis.sup_norm_le_norm {v : ι → E} (hv : is_basis 𝕜 v) :
+  ∃ C > (0 : ℝ), ∀ e : E, ∑ i, ∥hv.equiv_fun e i∥ ≤ C * ∥e∥ :=
+begin
+  set φ := hv.equiv_funL.to_continuous_linear_map,
+  set C := ∥φ∥ * (fintype.card ι),
+  use [max C 1, lt_of_lt_of_le (zero_lt_one) (le_max_right C 1)],
+  intros e,
+  calc ∑ i, ∥φ e i∥ ≤ ∑ i : ι, ∥φ e∥ : by { apply finset.sum_le_sum,
+                                           exact λ i hi, norm_le_pi_norm (φ e) i }
+  ... = ∥φ e∥*(fintype.card ι) : by simpa only [mul_comm, finset.sum_const, nsmul_eq_mul]
+  ... ≤ ∥φ∥ * ∥e∥ * (fintype.card ι) : mul_le_mul_of_nonneg_right (φ.le_op_norm e)
+                                                                 (fintype.card ι).cast_nonneg
+  ... = ∥φ∥ * (fintype.card ι) * ∥e∥ : by ring
+  ... ≤ max C 1 * ∥e∥ :  mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _)
+end
+
+lemma is_basis.op_norm_le  {ι : Type*} [fintype ι] {v : ι → E} (hv : is_basis 𝕜 v) :
+  ∃ C > (0 : ℝ), ∀ {u : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥u (v i)∥ ≤ M) → ∥u∥ ≤ C*M :=
+begin
+  obtain ⟨C, C_pos, hC⟩ : ∃ C > (0 : ℝ), ∀ (e : E), ∑ i, ∥hv.equiv_fun e i∥ ≤ C * ∥e∥,
+    from hv.sup_norm_le_norm,
+  use [C, C_pos],
+  intros u M hM hu,
+  apply u.op_norm_le_bound (mul_nonneg (le_of_lt C_pos) hM),
+  intros e,
+  calc
+  ∥u e∥ = ∥u (∑ i, hv.equiv_fun e i • v i)∥ :  by conv_lhs { rw ← hv.equiv_fun_total e }
+  ... = ∥∑ i, (hv.equiv_fun e i) • (u $ v i)∥ :  by simp [u.map_sum, linear_map.map_smul]
+  ... ≤ ∑ i, ∥(hv.equiv_fun e i) • (u $ v i)∥ : norm_sum_le _ _
+  ... = ∑ i, ∥hv.equiv_fun e i∥ * ∥u (v i)∥ : by simp only [norm_smul]
+  ... ≤ ∑ i, ∥hv.equiv_fun e i∥ * M : finset.sum_le_sum (λ i hi,
+                                                  mul_le_mul_of_nonneg_left (hu i) (norm_nonneg _))
+  ... = (∑ i, ∥hv.equiv_fun e i∥) * M : finset.sum_mul.symm
+  ... ≤ C * ∥e∥ * M : mul_le_mul_of_nonneg_right (hC e) hM
+  ... = C * M * ∥e∥ : by ring
+end
+
+instance [finite_dimensional 𝕜 E] [second_countable_topology F] :
+  second_countable_topology (E →L[𝕜] F) :=
+begin
+  set d := finite_dimensional.findim 𝕜 E,
+  suffices :
+    ∀ ε > (0 : ℝ), ∃ n : (E →L[𝕜] F) → fin d → ℕ, ∀ (f g : E →L[𝕜] F), n f = n g → dist f g ≤ ε,
+  from metric.second_countable_of_countable_discretization
+    (λ ε ε_pos, ⟨fin d → ℕ, by apply_instance, this ε ε_pos⟩),
+  intros ε ε_pos,
+  obtain ⟨u : ℕ → F, hu : closure (range u) = univ⟩ := exists_dense_seq F,
+  obtain ⟨v : fin d → E, hv : is_basis 𝕜 v⟩ := finite_dimensional.fin_basis 𝕜 E,
+  obtain ⟨C : ℝ, C_pos : 0 < C,
+          hC : ∀ {φ : E →L[𝕜] F} {M : ℝ}, 0 ≤ M → (∀ i, ∥φ (v i)∥ ≤ M) → ∥φ∥ ≤ C * M⟩ := hv.op_norm_le,
+  have h_2C : 0 < 2*C := mul_pos two_pos C_pos,
+  have hε2C : 0 < ε/(2*C) := div_pos ε_pos h_2C,
+  have : ∀ φ : E →L[𝕜] F, ∃ n : fin d → ℕ, ∥φ - (hv.constrL $ u ∘ n)∥ ≤ ε/2,
+  { intros φ,
+    have : ∀ i, ∃ n, ∥φ (v i) - u n∥ ≤ ε/(2*C),
+    { simp only [norm_sub_rev],
+      intro i,
+      have : φ (v i) ∈ closure (range u), by simp [hu],
+      obtain ⟨n, hn⟩ : ∃ n, ∥u n - φ (v i)∥ < ε / (2 * C),
+      { rw mem_closure_iff_nhds_basis metric.nhds_basis_ball at this,
+        specialize this (ε/(2*C)) hε2C,
+        simpa [dist_eq_norm] },
+      exact ⟨n, le_of_lt hn⟩ },
+    choose n hn using this,
+    use n,
+    replace hn : ∀ i : fin d, ∥(φ - (hv.constrL $ u ∘ n)) (v i)∥ ≤ ε / (2 * C), by simp [hn],
+    have : C * (ε / (2 * C)) = ε/2,
+    { rw [eq_div_iff (two_ne_zero : (2 : ℝ) ≠ 0), mul_comm, ← mul_assoc,
+          mul_div_cancel' _ (ne_of_gt h_2C)] },
+    specialize hC (le_of_lt hε2C) hn,
+    rwa this at hC },
+  choose n hn using this,
+  set Φ := λ φ : E →L[𝕜] F, (hv.constrL $ u ∘ (n φ)),
+  change ∀ z, dist z (Φ z) ≤ ε/2 at hn,
+  use n,
+  intros x y hxy,
+  calc dist x y ≤ dist x (Φ x) + dist (Φ x) y : dist_triangle _ _ _
+  ... = dist x (Φ x) + dist y (Φ y) : by simp [Φ, hxy, dist_comm]
+  ... ≤ ε : by linarith [hn x, hn y]
+end
+
 /-- Any finite-dimensional vector space over a complete field is complete.
 We do not register this as an instance to avoid an instance loop when trying to prove the
 completeness of `𝕜`, and the search for `𝕜` as an unknown metavariable. Declare the instance

src/analysis/normed_space/operator_norm.lean

@@ -73,6 +73,11 @@ follow automatically in `linear_map.mk_continuous_norm_le`. -/
 def linear_map.mk_continuous_of_exists_bound (h : ∃C, ∀x, ∥f x∥ ≤ C * ∥x∥) : E →L[𝕜] F :=
 ⟨f, let ⟨C, hC⟩ := h in linear_map.continuous_of_bound f C hC⟩
 
+lemma continuous_of_linear_of_bound {f : E → F} (h_add : ∀ x y, f (x + y) = f x + f y)
+  (h_smul : ∀ (c : 𝕜) x, f (c • x) = c • f x) {C : ℝ} (h_bound : ∀ x, ∥f x∥ ≤ C*∥x∥) :
+  continuous f :=
+let φ : E →ₗ[𝕜] F := ⟨f, h_add, h_smul⟩ in φ.continuous_of_bound C h_bound
+
 @[simp, norm_cast] lemma linear_map.mk_continuous_coe (C : ℝ) (h : ∀x, ∥f x∥ ≤ C * ∥x∥) :
   ((f.mk_continuous C h) : E →ₗ[𝕜] F) = f := rfl
 
@@ -279,6 +284,31 @@ theorem op_norm_le_of_lipschitz {f : E →L[𝕜] F} {K : nnreal} (hf : lipschit
   ∥f∥ ≤ K :=
 f.op_norm_le_bound K.2 $ λ x, by simpa only [dist_zero_right, f.map_zero] using hf.dist_le_mul x 0
 
+lemma op_norm_le_of_ball {f : E →L[𝕜] F} {ε : ℝ} {C : ℝ} (ε_pos : 0 < ε) (hC : 0 ≤ C)
+  (hf : ∀ x ∈ ball (0 : E) ε, ∥f x∥ ≤ C * ∥x∥) : ∥f∥ ≤ C :=
+begin
+  apply f.op_norm_le_bound hC,
+  intros x,
+  rcases normed_field.exists_one_lt_norm 𝕜 with ⟨c, hc⟩,
+  by_cases hx : x = 0, { simp [hx] },
+  rcases rescale_to_shell hc (half_pos ε_pos) hx with ⟨δ, hδ, δxle, leδx, δinv⟩,
+  have δx_in : δ • x ∈ ball (0 : E) ε,
+  { rw [mem_ball, dist_eq_norm, sub_zero],
+    linarith },
+  calc ∥f x∥ = ∥f ((1/δ) • δ • x)∥ : by simp [hδ, smul_smul]
+  ... = ∥1/δ∥ * ∥f (δ • x)∥ : by simp [norm_smul]
+  ... ≤ ∥1/δ∥ * (C*∥δ • x∥) : mul_le_mul_of_nonneg_left _ (norm_nonneg _)
+  ... = C * ∥x∥ : by { rw norm_smul, field_simp [hδ], ring },
+  exact hf _ δx_in
+end
+
+lemma op_norm_eq_of_bounds {φ : E →L[𝕜] F} {M : ℝ} (M_nonneg : 0 ≤ M)
+  (h_above : ∀ x, ∥φ x∥ ≤ M*∥x∥) (h_below : ∀ N ≥ 0, (∀ x, ∥φ x∥ ≤ N*∥x∥) → M ≤ N) :
+  ∥φ∥ = M :=
+le_antisymm (φ.op_norm_le_bound M_nonneg h_above)
+  ((le_cInf_iff continuous_linear_map.bounds_bdd_below ⟨M, M_nonneg, h_above⟩).mpr $
+   λ N ⟨N_nonneg, hN⟩, h_below N N_nonneg hN)
+
 /-- The operator norm satisfies the triangle inequality. -/
 theorem op_norm_add_le : ∥f + g∥ ≤ ∥f∥ + ∥g∥ :=
 show ∥f + g∥ ≤ (coe : nnreal → ℝ) (⟨_, f.op_norm_nonneg⟩ + ⟨_, g.op_norm_nonneg⟩),

src/linear_algebra/basis.lean

@@ -787,7 +787,7 @@ def is_basis.constr (f : ι → M') : M →ₗ[R] M' :=
 
 theorem is_basis.constr_apply (f : ι → M') (x : M) :
   (hv.constr f : M → M') x = (hv.repr x).sum (λb a, a • f b) :=
-by dsimp [is_basis.constr];
+by dsimp [is_basis.constr] ;
    rw [finsupp.total_apply, finsupp.sum_map_domain_index]; simp [add_smul]
 
 lemma is_basis.ext {f g : M →ₗ[R] M'} (hv : is_basis R v) (h : ∀i, f (v i) = g (v i)) : f = g :=
@@ -1024,6 +1024,10 @@ end
 lemma is_basis.equiv_fun_self (i j : ι) : h.equiv_fun (v i) j = if i = j then 1 else 0 :=
 by { rw [h.equiv_fun_apply, h.repr_self_apply] }
 
+@[simp] theorem is_basis.constr_apply_fintype (f : ι → M') (x : M) :
+  (h.constr f : M → M') x = ∑ i, (h.equiv_fun x i) • f i :=
+by simp [h.constr_apply, h.equiv_fun_apply, finsupp.sum_fintype]
+
 end module
 
 section vector_space

src/topology/algebra/module.lean

@@ -231,6 +231,9 @@ variables (c : R) (f g : M →L[R] M₂) (h : M₂ →L[R] M₃) (x y z : M)
 @[simp] lemma map_add  : f (x + y) = f x + f y := (to_linear_map _).map_add _ _
 @[simp] lemma map_smul : f (c • x) = c • f x := (to_linear_map _).map_smul _ _
 
+lemma map_sum {ι : Type*} (s : finset ι) (g : ι → M) :
+  f (∑ i in s, g i) = ∑ i in s, f (g i) := f.to_linear_map.map_sum
+
 @[simp, norm_cast] lemma coe_coe : ((f : M →ₗ[R] M₂) : (M → M₂)) = (f : M → M₂) := rfl
 
 /-- The continuous map that is constantly zero. -/