refactor(analysis/normed_space/operator_norm): topological modules (#1085)

* refactor(analysis/normed_space/operator_norm): topological modules

* remove useless typeclass in definition of topological module

* refactor(analysis/normed_space/operator_norm): style

Author: sgouezel

src/analysis/normed_space/basic.lean

@@ -9,6 +9,8 @@ Authors: Patrick Massot, Johannes Hölzl
 import algebra.pi_instances
 import linear_algebra.basic
 import topology.instances.nnreal topology.instances.complex
+import topology.algebra.module
+
 variables {α : Type*} {β : Type*} {γ : Type*} {ι : Type*}
 
 noncomputable theory
@@ -415,10 +417,9 @@ lemma tendsto_smul_const {g : γ → F} {e : filter γ} (s : α) {b : F} :
   (tendsto g e (nhds b)) → tendsto (λ x, s • (g x)) e (nhds (s • b)) :=
 tendsto_smul tendsto_const_nhds
 
-lemma continuous_smul [topological_space γ] {f : γ → α} {g : γ → E}
-  (hf : continuous f) (hg : continuous g) : continuous (λc, f c • g c) :=
-continuous_iff_continuous_at.2 $ assume c,
-  tendsto_smul (continuous_iff_continuous_at.1 hf _) (continuous_iff_continuous_at.1 hg _)
+instance normed_space.topological_vector_space : topological_vector_space α E :=
+{ continuous_smul := continuous_iff_continuous_at.2 $ λp, tendsto_smul
+    (continuous_iff_continuous_at.1 continuous_fst _) (continuous_iff_continuous_at.1 continuous_snd _) }
 
 /-- If there is a scalar `c` with `∥c∥>1`, then any element can be moved by scalar multiplication to
 any shell of width `∥c∥`. Also recap information on the norm of the rescaling element that shows

src/analysis/normed_space/bounded_linear_maps.lean

@@ -16,11 +16,14 @@ local notation f ` →_{`:50 a `} `:0 b := filter.tendsto f (nhds a) (nhds b)
 open filter (tendsto)
 open metric
 
-variables {k : Type*} [normed_field k]
+variables {k : Type*} [nondiscrete_normed_field k]
 variables {E : Type*} [normed_space k E]
 variables {F : Type*} [normed_space k F]
 variables {G : Type*} [normed_space k G]
 
+
+set_option class.instance_max_depth 80
+
 structure is_bounded_linear_map (k : Type*) [normed_field k] {E : Type*}
   [normed_space k E] {F : Type*} [normed_space k F] (f : E → F)
   extends is_linear_map k f : Prop :=
@@ -34,25 +37,27 @@ lemma is_linear_map.with_bound
     le_trans (h x) $ mul_le_mul_of_nonneg_right (le_trans this zero_le_one) (norm_nonneg x)⟩)
   (assume : ¬ M ≤ 0, ⟨M, lt_of_not_ge this, h⟩)⟩
 
-/-- A bounded linear map satisfies `is_bounded_linear_map` -/
-lemma bounded_linear_map.is_bounded_linear_map (f : E →L[k] F) : is_bounded_linear_map k f := {..f}
+/-- A continuous linear map satisfies `is_bounded_linear_map` -/
+lemma continuous_linear_map.is_bounded_linear_map (f : E →L[k] F) : is_bounded_linear_map k f :=
+{ bound := f.bound,
+  ..f.to_linear_map }
 
 namespace is_bounded_linear_map
 
 def to_linear_map (f : E → F) (h : is_bounded_linear_map k f) : E →ₗ[k] F :=
 (is_linear_map.mk' _ h.to_is_linear_map)
 
-/-- Construct a bounded linear map from is_bounded_linear_map -/
-def to_bounded_linear_map {f : E → F} (hf : is_bounded_linear_map k f) : E →L[k] F :=
-{ bound := hf.bound, ..is_bounded_linear_map.to_linear_map f hf }
+/-- Construct a continuous linear map from is_bounded_linear_map -/
+def to_continuous_linear_map {f : E → F} (hf : is_bounded_linear_map k f) : E →L[k] F :=
+{ cont := let ⟨C, Cpos, hC⟩ := hf.bound in linear_map.continuous_of_bound _ C hC,
+  ..to_linear_map f hf}
 
 lemma zero : is_bounded_linear_map k (λ (x:E), (0:F)) :=
 (0 : E →ₗ F).is_linear.with_bound 0 $ by simp [le_refl]
 
 lemma id : is_bounded_linear_map k (λ (x:E), x) :=
 linear_map.id.is_linear.with_bound 1 $ by simp [le_refl]
 
-set_option class.instance_max_depth 43
 variables { f g : E → F }
 
 lemma smul (c : k) (hf : is_bounded_linear_map k f) :
@@ -129,82 +134,51 @@ end
 
 end is_bounded_linear_map
 
-set_option class.instance_max_depth 60
+section
+set_option class.instance_max_depth 250
 
 lemma is_bounded_linear_map_prod_iso :
   is_bounded_linear_map k (λ(p : (E →L[k] F) × (E →L[k] G)),
-                            (bounded_linear_map.prod p.1 p.2 : (E →L[k] (F × G)))) :=
+                            (continuous_linear_map.prod p.1 p.2 : (E →L[k] (F × G)))) :=
 begin
   refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ 1 (λp, _),
   simp only [norm, one_mul],
-  refine bounded_linear_map.op_norm_le_bound _ (le_trans (norm_nonneg _) (le_max_left _ _)) (λu, _),
-  simp only [norm, bounded_linear_map.prod, max_le_iff],
+  refine continuous_linear_map.op_norm_le_bound _ (le_trans (norm_nonneg _) (le_max_left _ _)) (λu, _),
+  simp only [norm, continuous_linear_map.prod, max_le_iff],
   split,
-  { calc ∥p.1 u∥ ≤ ∥p.1∥ * ∥u∥ : bounded_linear_map.le_op_norm _ _
+  { calc ∥p.1 u∥ ≤ ∥p.1∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
     ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
       mul_le_mul_of_nonneg_right (le_max_left _ _) (norm_nonneg _) },
-  { calc ∥p.2 u∥ ≤ ∥p.2∥ * ∥u∥ : bounded_linear_map.le_op_norm _ _
+  { calc ∥p.2 u∥ ≤ ∥p.2∥ * ∥u∥ : continuous_linear_map.le_op_norm _ _
     ... ≤ max (∥p.1∥) (∥p.2∥) * ∥u∥ :
       mul_le_mul_of_nonneg_right (le_max_right _ _) (norm_nonneg _) }
 end
 
-lemma bounded_linear_map.is_bounded_linear_map_comp_left (g : bounded_linear_map k F G) :
-  is_bounded_linear_map k (λ(f : E →L[k] F), bounded_linear_map.comp g f) :=
+lemma continuous_linear_map.is_bounded_linear_map_comp_left (g : continuous_linear_map k F G) :
+  is_bounded_linear_map k (λ(f : E →L[k] F), continuous_linear_map.comp g f) :=
 begin
   refine is_linear_map.with_bound ⟨λu v, _, λc u, _⟩
-    (∥g∥) (λu, bounded_linear_map.op_norm_comp_le _ _),
+    (∥g∥) (λu, continuous_linear_map.op_norm_comp_le _ _),
   { ext x,
     change g ((u+v) x) = g (u x) + g (v x),
     have : (u+v) x = u x + v x := rfl,
     rw [this, g.map_add] },
   { ext x,
     change g ((c • u) x) = c • g (u x),
     have : (c • u) x = c • u x := rfl,
-    rw [this, bounded_linear_map.map_smul] }
+    rw [this, continuous_linear_map.map_smul] }
 end
 
-lemma bounded_linear_map.is_bounded_linear_map_comp_right (f : bounded_linear_map k E F) :
-  is_bounded_linear_map k (λ(g : F →L[k] G), bounded_linear_map.comp g f) :=
+lemma continuous_linear_map.is_bounded_linear_map_comp_right (f : continuous_linear_map k E F) :
+  is_bounded_linear_map k (λ(g : F →L[k] G), continuous_linear_map.comp g f) :=
 begin
   refine is_linear_map.with_bound ⟨λu v, rfl, λc u, rfl⟩ (∥f∥) (λg, _),
   rw mul_comm,
-  exact bounded_linear_map.op_norm_comp_le _ _
+  exact continuous_linear_map.op_norm_comp_le _ _
 end
 
-/-- A continuous linear map between normed spaces is bounded when the field is nondiscrete.
-The continuity ensures boundedness on a ball of some radius δ. The nondiscreteness is then
-used to rescale any element into an element of norm in [δ/C, δ], whose image has a controlled norm.
-The norm control for the original element follows by rescaling. -/
-theorem is_linear_map.bounded_of_continuous_at {k : Type*} [nondiscrete_normed_field k]
-  {E : Type*} [normed_space k E] {F : Type*} [normed_space k F] {f : E → F} {x₀ : E}
-  (lin : is_linear_map k f) (cont : continuous_at f x₀) : is_bounded_linear_map k f :=
-begin
-  rcases tendsto_nhds_nhds.1 cont 1 zero_lt_one with ⟨ε, ε_pos, hε⟩,
-  let δ := ε/2,
-  have δ_pos : δ > 0 := half_pos ε_pos,
-  have H : ∀{a}, ∥a∥ ≤ δ → ∥f a∥ ≤ 1,
-  { assume a ha,
-    have : dist (f (x₀+a)) (f x₀) ≤ 1,
-    { apply le_of_lt (hε _),
-      have : dist x₀ (x₀ + a) = ∥a∥, by { rw dist_eq_norm, simp },
-      rw [dist_comm, this],
-      exact lt_of_le_of_lt ha (half_lt_self ε_pos) },
-    simpa [dist_eq_norm, lin.add] using this },
-  rcases exists_one_lt_norm k with ⟨c, hc⟩,
-  refine lin.with_bound (δ⁻¹ * ∥c∥) (λx, _),
-  by_cases h : x = 0,
-  { simp only [h, lin.map_zero, norm_zero, mul_zero] },
-  { rcases rescale_to_shell hc δ_pos h with ⟨d, hd, dxle, ledx, dinv⟩,
-    calc ∥f x∥
-      = ∥f ((d⁻¹ * d) • x)∥ : by rwa [inv_mul_cancel, one_smul]
-      ... = ∥d∥⁻¹ * ∥f (d • x)∥ :
-        by rw [mul_smul, lin.smul, norm_smul, norm_inv]
-      ... ≤ ∥d∥⁻¹ * 1 :
-        mul_le_mul_of_nonneg_left (H dxle) (by { rw ← norm_inv, exact norm_nonneg _ })
-      ... ≤ δ⁻¹ * ∥c∥ * ∥x∥ : by { rw mul_one, exact dinv } }
 end
 
-
 section bilinear_map
 
 variable (k)
@@ -253,21 +227,23 @@ lemma is_bounded_bilinear_map_comp :
   smul_left := λc x y, begin
       ext z,
       change y (c • (x z)) = c • y (x z),
-      rw bounded_linear_map.map_smul
+      rw continuous_linear_map.map_smul
     end,
   add_right := λx y₁ y₂, rfl,
   smul_right := λc x y, rfl,
   bound := ⟨1, zero_lt_one, λx y, calc
-    ∥bounded_linear_map.comp ((x, y).snd) ((x, y).fst)∥
-      ≤ ∥y∥ * ∥x∥ : bounded_linear_map.op_norm_comp_le _ _
+    ∥continuous_linear_map.comp ((x, y).snd) ((x, y).fst)∥
+      ≤ ∥y∥ * ∥x∥ : continuous_linear_map.op_norm_comp_le _ _
     ... = 1 * ∥x∥ * ∥ y∥ : by ring ⟩ }
 
 /-- Definition of the derivative of a bilinear map `f`, given at a point `p` by
 `q ↦ f(p.1, q.2) + f(q.1, p.2)` as in the standard formula for the derivative of a product.
 We define this function here a bounded linear map from `E × F` to `G`. The fact that this
 is indeed the derivative of `f` is proved in `is_bounded_bilinear_map.has_fderiv_at` in
 `deriv.lean`-/
-def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map k f) (p : E × F) : (E × F) →L[k] G :=
+
+def is_bounded_bilinear_map.linear_deriv (h : is_bounded_bilinear_map k f) (p : E × F) :
+  (E × F) →ₗ[k] G :=
 { to_fun := λq, f (p.1, q.2) + f (q.1, p.2),
   add := λq₁ q₂, begin
     change f (p.1, q₁.2 + q₂.2) + f (q₁.1 + q₂.1, p.2) =
@@ -277,22 +253,28 @@ def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map k f) (p : E × F)
   smul := λc q, begin
     change f (p.1, c • q.2) + f (c • q.1, p.2) = c • (f (p.1, q.2) + f (q.1, p.2)),
     simp [h.smul_left, h.smul_right, smul_add]
-  end,
-  bound := begin
-    rcases h.bound with ⟨C, Cpos, hC⟩,
-    refine exists_pos_bound_of_bound (C * ∥p.1∥ + C * ∥p.2∥) (λq, _),
-    calc ∥f (p.1, q.2) + f (q.1, p.2)∥
-      ≤ ∥f (p.1, q.2)∥ + ∥f (q.1, p.2)∥ : norm_triangle _ _
-    ... ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : add_le_add (hC _ _) (hC _ _)
-    ... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
-       apply add_le_add,
-       exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
-       apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
-       exact mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt Cpos),
-    end
-    ... = (C * ∥p.1∥ + C * ∥p.2∥) * ∥q∥ : by ring
   end }
 
+def is_bounded_bilinear_map.deriv (h : is_bounded_bilinear_map k f) (p : E × F) : (E × F) →L[k] G :=
+(h.linear_deriv p).with_bound $ begin
+  rcases h.bound with ⟨C, Cpos, hC⟩,
+  refine ⟨C * ∥p.1∥ + C * ∥p.2∥, λq, _⟩,
+  calc ∥f (p.1, q.2) + f (q.1, p.2)∥
+    ≤ ∥f (p.1, q.2)∥ + ∥f (q.1, p.2)∥ : norm_triangle _ _
+  ... ≤ C * ∥p.1∥ * ∥q.2∥ + C * ∥q.1∥ * ∥p.2∥ : add_le_add (hC _ _) (hC _ _)
+  ... ≤ C * ∥p.1∥ * ∥q∥ + C * ∥q∥ * ∥p.2∥ : begin
+      apply add_le_add,
+      exact mul_le_mul_of_nonneg_left (le_max_right _ _) (mul_nonneg (le_of_lt Cpos) (norm_nonneg _)),
+      apply mul_le_mul_of_nonneg_right _ (norm_nonneg _),
+      exact mul_le_mul_of_nonneg_left (le_max_left _ _) (le_of_lt Cpos),
+  end
+  ... = (C * ∥p.1∥ + C * ∥p.2∥) * ∥q∥ : by ring
+end
+
+set_option class.instance_max_depth 150
+@[simp] lemma is_bounded_bilinear_map_deriv_coe (h : is_bounded_bilinear_map k f) (p q : E × F) :
+  h.deriv p q = f (p.1, q.2) + f (q.1, p.2) := rfl
+
 /-- Given a bounded bilinear map `f`, the map associating to a point `p` the derivative of `f` at
 `p` is itself a bounded linear map. -/
 lemma is_bounded_bilinear_map.is_bounded_linear_map_deriv (h : is_bounded_bilinear_map k f) :
@@ -301,14 +283,10 @@ begin
   rcases h.bound with ⟨C, Cpos, hC⟩,
   refine is_linear_map.with_bound ⟨λp₁ p₂, _, λc p, _⟩ (C + C) (λp, _),
   { ext q,
-    change f (p₁.1 + p₂.1, q.2) + f (q.1, p₁.2 + p₂.2) =
-      (f (p₁.1, q.2) + f (q.1, p₁.2)) + ((f (p₂.1, q.2) + f (q.1, p₂.2))),
     simp [h.add_left, h.add_right] },
   { ext q,
-    change f (c • p.1, q.2) + f (q.1, c • p.2) = c • (f (p.1, q.2) + f (q.1, p.2)),
     simp [h.smul_left, h.smul_right, smul_add] },
-  { dunfold is_bounded_bilinear_map.deriv,
-    refine bounded_linear_map.op_norm_le_bound _
+  { refine continuous_linear_map.op_norm_le_bound _
       (mul_nonneg (add_nonneg (le_of_lt Cpos) (le_of_lt Cpos)) (norm_nonneg _)) (λq, _),
     calc ∥f (p.1, q.2) + f (q.1, p.2)∥
       ≤ ∥f (p.1, q.2)∥ + ∥f (q.1, p.2)∥ : norm_triangle _ _