refactor(analysis/normed_space/bounded_linear_maps): nondiscrete normed field

Author: sgouezel

src/analysis/normed_space/operator_norm.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Jan-David Salchow. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Jan-David Salchow
+Authors: Jan-David Salchow, Sébastien Gouëzel
 
 The space of bounded linear maps
 
@@ -20,8 +20,10 @@ variables {k : Type*}
 variables {E : Type*} {F : Type*}
 
 
--- Define the subspace of bounded linear maps, introduce the notation L(E,F) for the set of bounded linear maps.
+-- Define the subspace of bounded linear maps.
 section bounded_linear_maps
+set_option class.instance_max_depth 50
+
 
 variables [hnfk : normed_field k] [normed_space k E] [normed_space k F]
 include hnfk
@@ -32,6 +34,7 @@ def bounded_linear_maps : subspace k (E → F) :=
   add := assume A B, is_bounded_linear_map.add,
   smul := assume c A, is_bounded_linear_map.smul c }
 
+-- introduce the local notation L(E,F) for the set of bounded linear maps.
 local notation `L(` E `,` F `)` := @bounded_linear_maps k E F _ _ _
 
 /-- Coerce bounded linear maps to functions. -/
@@ -41,117 +44,102 @@ instance bounded_linear_maps.to_fun : has_coe_to_fun $ L(E,F) :=
 @[extensionality] theorem ext {A B : L(E,F)} (H : ∀ x, A x = B x) : A = B :=
 set_coe.ext $ funext H
 
-/-- Bounded linear maps are ... bounded -/
-lemma exists_bound (A : L(E,F)) : ∃ c, c > 0 ∧ ∀ x : E, ∥A x∥ ≤ c * ∥x∥ := A.property.bound
+def to_linear_map (A : L(E, F)) : linear_map _ E F :=
+{to_fun := A.val, ..A.property}
+
+@[simp] lemma bounded_linear_maps.map_zero {A : L(E, F)} : A (0 : E) = 0 :=
+(to_linear_map A).map_zero
+
+@[simp] lemma bounded_linear_maps.coe_zero {x : E} : (0 : L(E, F)) x = 0 := rfl
+
+@[simp] lemma bounded_linear_maps.smul_coe {A : L(E, F)} {x : E} {c : k} :
+  (c • A) x = c • (A x) := rfl
+
+@[simp] lemma bounded_linear_maps.zero_smul {A : L(E, F)} : (0 : k) • A = 0 :=
+by ext; simp
 
-/-- Bounded linear maps are conveniently bounded on the unit ball. -/
-lemma exists_bound' (A : L(E,F)) : ∃ c, c > 0 ∧ ∀ x : E, ∥x∥ ≤ 1 → ∥A x∥ ≤ c :=
-let ⟨c, _, H⟩ := exists_bound A in
-exists.intro c ⟨‹c > 0›,
-  assume x _,
-  calc ∥A x∥ ≤ c * ∥x∥ : H x
-        ... ≤ c * 1 : (mul_le_mul_left ‹c > 0›).mpr ‹∥x∥ ≤ 1›
-        ... = c : mul_one c⟩
+@[simp] lemma bounded_linear_maps.one_smul {A : L(E, F)} : (1 : k) • A = A :=
+by ext; simp
+
+/-- Bounded linear maps are ... bounded -/
+lemma exists_bound (A : L(E,F)) : ∃ c, 0 < c ∧ ∀ x : E, ∥A x∥ ≤ c * ∥x∥ := A.property.bound
 
 end bounded_linear_maps
 
 /-
-Now define the operator norm. We only do this for normed spaces over ℝ, since we need a
-scalar multiplication with reals to prove that ∥A x∥ ≤ ∥A∥ * ∥x∥. It would be enough to
-have a vector space over a normed field k with a real scalar multiplication and certain
-compatibility conditions.
+Now define the operator norm.
 
 The main task is to show that the operator norm is definite, homogeneous, and satisfies the
-triangle inequality. This is done after a few preliminary lemmas necessary to deal with cSup.
+triangle inequality. This is done after a few preliminary lemmas necessary to deal with csupr.
 -/
 section operator_norm
 
-variables [normed_space ℝ E] [normed_space ℝ F]
+variables [normed_field k] [normed_space k E] [normed_space k F]
 open lattice set
 
-local notation `L(` E `,` F `)` := @bounded_linear_maps ℝ E F _ _ _
-
-noncomputable def to_linear_map (A : L(E, F)) : linear_map _ E F :=
-{to_fun := A.val, ..A.property}
+local notation `L(` E `,` F `)` := @bounded_linear_maps k E F _ _ _
 
-/-- The operator norm of a bounded linear map A : E → F is the sup of
-    the set ∥A x∥ with ∥x∥ ≤ 1. If E = {0} we set ∥A∥ = 0. -/
+/-- The operator norm of a bounded linear map A : E → F is the sup of ∥A x∥/∥x∥. -/
 noncomputable def operator_norm (A : L(E, F)) : ℝ :=
-Sup (image (λ x, ∥A x∥) {x | ∥x∥ ≤ 1})
+supr (λ x, ∥A x∥/∥x∥)
 
 noncomputable instance bounded_linear_maps.to_has_norm : has_norm L(E,F) :=
 {norm := operator_norm}
 
-lemma norm_of_unit_ball_bdd_above (A : L(E,F)) : bdd_above (image (norm ∘ A) {x | ∥x∥ ≤ 1}) :=
-let ⟨c, _, H⟩ := (exists_bound' A : ∃ c, c > 0 ∧ ∀ x : E, ∥x∥ ≤ 1 → ∥A x∥ ≤ c) in
-bdd_above.mk c
-  (assume r ⟨x, (_ : ∥x∥ ≤ 1), (_ : ∥A x∥ = r)⟩,
-    show r ≤ c, from
-      calc r = ∥A x∥ : eq.symm ‹∥A x∥ = r›
-         ... ≤ c : H x ‹∥x∥ ≤ 1›)
-
-lemma zero_in_im_ball (A : L(E,F)) : (0:ℝ) ∈ {r : ℝ | ∃ (x : E), ∥x∥ ≤ 1 ∧ ∥A x∥ = r} :=
-have A 0 = 0, from (to_linear_map A).map_zero,
-exists.intro (0:E) $ and.intro (by rw[norm_zero]; exact zero_le_one) (by rw[‹A 0 = 0›]; simp)
+lemma bdd_above_range_norm_image_div_norm (A : L(E,F)) : bdd_above (range (λ x, ∥A x∥/∥x∥)) :=
+let ⟨c, _, H⟩ := (exists_bound A : ∃ c, 0 < c ∧ ∀ x : E, ∥A x∥ ≤ c * ∥x∥) in
+bdd_above.mk c $ forall_range_iff.2 $ λx, begin
+  by_cases h : ∥x∥ = 0,
+  { simp [h, le_of_lt ‹0 < c›] },
+  { refine (div_le_iff _).2 (H x),
+    simpa [ne.symm h] using le_iff_eq_or_lt.1 (norm_nonneg x) }
+end
 
 lemma operator_norm_nonneg (A : L(E,F)) : 0 ≤ ∥A∥ :=
-have (0:ℝ) ∈ _, from zero_in_im_ball A,
-show 0 ≤ Sup (image (norm ∘ A) {x | ∥x∥ ≤ 1}), from
-let ⟨c, _, H⟩ := (exists_bound' A : ∃ c, c > 0 ∧ ∀ x : E, ∥x∥ ≤ 1 → ∥A x∥ ≤ c) in
-le_cSup (norm_of_unit_ball_bdd_above A) ‹(0:ℝ) ∈ _›
-
-lemma bounded_by_operator_norm_on_unit_vector (A : L(E, F)) {x : E} (_ : ∥x∥ = 1) : ∥A x∥ ≤ ∥A∥ :=
-show ∥A x∥ ≤ Sup (image (norm ∘ A) {x | ∥x∥ ≤ 1}), from
-let ⟨c, _, _⟩ := (exists_bound A : ∃ c, c > 0 ∧ ∀ x : E, ∥ A x ∥ ≤ c * ∥ x ∥) in
-have ∥A x∥ ∈ (image (norm ∘ A) {x | ∥x∥ ≤ 1}), from mem_image_of_mem _ $ le_of_eq ‹∥x∥ = 1›,
-le_cSup (norm_of_unit_ball_bdd_above A) ‹∥A x∥ ∈ _›
+begin
+  have : (0 : ℝ) = (λ x, ∥A x∥/∥x∥) 0, by simp,
+  rw this,
+  exact le_csupr (bdd_above_range_norm_image_div_norm A),
+end
 
 set_option class.instance_max_depth 34
 
 /-- This is the fundamental property of the operator norm: ∥A x∥ ≤ ∥A∥ * ∥x∥. -/
 theorem bounded_by_operator_norm {A : L(E,F)} {x : E} : ∥A x∥ ≤ ∥A∥ * ∥x∥ :=
-have A 0 = 0, from (to_linear_map A).map_zero,
-classical.by_cases
-  (assume : x = (0:E),
-    show ∥A x∥ ≤ ∥A∥ * ∥x∥, by rw[‹x = 0›, ‹A 0 = 0›, norm_zero, norm_zero, mul_zero]; exact le_refl 0)
-  (assume : x ≠ (0:E),
-    have ∥x∥ ≠ 0, from ne_of_gt $ (norm_pos_iff x).mpr ‹x ≠ 0›,
-    have ∥∥x∥⁻¹∥ = ∥x∥⁻¹, from abs_of_nonneg $ inv_nonneg.mpr $ norm_nonneg x,
-    have ∥∥x∥⁻¹•x∥ = 1, begin rw[norm_smul, ‹∥∥x∥⁻¹∥ = ∥x∥⁻¹›], exact inv_mul_cancel ‹∥x∥ ≠ 0› end,
-    calc ∥A x∥ = (∥x∥ * ∥x∥⁻¹) * ∥A x∥ : by rw[mul_inv_cancel ‹∥x∥ ≠ 0›]; ring
-          ... = ∥∥x∥⁻¹∥ * ∥A x∥ * ∥x∥  : by rw[‹∥∥x∥⁻¹∥ = ∥x∥⁻¹›]; ring
-          ... = ∥∥x∥⁻¹• A x ∥ * ∥x∥    : by rw[←normed_space.norm_smul ∥x∥⁻¹ (A x)]
-          ... = ∥A (∥x∥⁻¹• x)∥ * ∥x∥   : by {
-                                          change  ∥∥x∥⁻¹ • A.val x∥ * ∥x∥ = ∥A.val (∥x∥⁻¹ • x)∥ * ∥x∥,
-                                          rw A.property.smul}
-          ... ≤ ∥A∥ * ∥x∥              : (mul_le_mul_right ((norm_pos_iff x).mpr ‹x ≠ 0›)).mpr
-                                          (bounded_by_operator_norm_on_unit_vector A ‹∥∥x∥⁻¹•x∥ = 1›))
-
-lemma bounded_by_operator_norm_on_unit_ball (A : L(E, F)) {x : E} (_ : ∥x∥ ≤ 1) : ∥A x∥ ≤ ∥A∥ :=
-calc ∥A x∥ ≤ ∥A∥ * ∥x∥ : bounded_by_operator_norm
-        ... ≤ ∥A∥ * 1 : mul_le_mul_of_nonneg_left ‹∥x∥ ≤ 1› (operator_norm_nonneg A)
-        ... = ∥A∥ : mul_one ∥A∥
-
-lemma operator_norm_bounded_by {A : L(E,F)} (c : nnreal) :
-  (∀ x : E, ∥x∥ ≤ 1 → ∥A x∥ ≤ (c:ℝ)) → ∥A∥ ≤ c :=
-assume H : ∀ x : E, ∥x∥ ≤ 1 → ∥A x∥ ≤ c,
-suffices Sup (image (norm ∘ A) {x | ∥x∥ ≤ 1}) ≤ c, by assumption,
-cSup_le (set.ne_empty_of_mem $ zero_in_im_ball A)
-  (show ∀ (r : ℝ), r ∈ (image (norm ∘ A) {x | ∥x∥ ≤ 1}) → r ≤ c, from
-    assume r ⟨x, _, _⟩,
-      calc r = ∥A x∥ : eq.symm ‹_›
-         ... ≤ c : H x ‹_›)
-
-theorem operator_norm_triangle (A : L(E,F)) (B : L(E,F)) : ∥A + B∥ ≤ ∥A∥ + ∥B∥ :=
-operator_norm_bounded_by (⟨∥A∥, operator_norm_nonneg A⟩ + ⟨∥B∥, operator_norm_nonneg B⟩)
-  (assume x _, by exact
+begin
+  classical, by_cases h : x = 0,
+  { simp [h] },
+  { have : ∥A x∥/∥x∥ ≤ ∥A∥, from le_csupr (bdd_above_range_norm_image_div_norm A),
+    rwa (div_le_iff _) at this,
+    have : ∥x∥ ≠ 0, from ne_of_gt ((norm_pos_iff x).mpr h),
+    have I := le_iff_eq_or_lt.1 (norm_nonneg x),
+    simpa [ne.symm this] using I }
+end
+
+/-- If one controls the norm of every A x, then one controls the norm of A. -/
+lemma operator_norm_bounded_by {A : L(E,F)} {c : ℝ} (hc : 0 ≤ c) (H : ∀ x, ∥A x∥ ≤ c * ∥x∥) :
+  ∥A∥ ≤ c :=
+begin
+  haveI : nonempty E := ⟨0⟩,
+  refine csupr_le (λx, _),
+  by_cases h : ∥x∥ = 0,
+  { simp [h, hc] },
+  { refine (div_le_iff _).2 (H x),
+    simpa [ne.symm h] using le_iff_eq_or_lt.1 (norm_nonneg x) }
+end
+
+/-- The operator norm satisfies the triangle inequality. -/
+theorem operator_norm_triangle (A B : L(E,F)) : ∥A + B∥ ≤ ∥A∥ + ∥B∥ :=
+operator_norm_bounded_by (add_nonneg (operator_norm_nonneg A) (operator_norm_nonneg B))
+  (assume x,
     calc ∥(A + B) x∥ = ∥A x + B x∥ : by refl
                 ... ≤ ∥A x∥ + ∥B x∥ : by exact norm_triangle _ _
-                ... ≤ ∥A∥ + ∥B∥ : by exact add_le_add (bounded_by_operator_norm_on_unit_ball A ‹_›)
-                                            (bounded_by_operator_norm_on_unit_ball B ‹_›))
+                ... ≤ ∥A∥ * ∥x∥ + ∥B∥ * ∥x∥ :
+                  add_le_add bounded_by_operator_norm bounded_by_operator_norm
+                ... = (∥A∥ + ∥B∥) * ∥x∥ : by ring)
 
+/-- An operator is zero iff its norm vanishes. -/
 theorem operator_norm_zero_iff (A : L(E,F)) : ∥A∥ = 0 ↔ A = 0 :=
-have A 0 = 0, from (to_linear_map A).map_zero,
 iff.intro
   (assume : ∥A∥ = 0,
     suffices ∀ x, A x = 0, from ext this,
@@ -161,62 +149,45 @@ iff.intro
               ... = 0 : by rw[‹∥A∥ = 0›]; ring,
       (norm_le_zero_iff (A x)).mp this)
   (assume : A = 0,
-    let M := {r : ℝ | ∃ (x : E), ∥x∥ ≤ 1 ∧ ∥A x∥ = r} in
-    -- note that we have M = (image (norm ∘ A) {x | ∥x∥ ≤ 1}), from rfl
-    suffices Sup M = 0, by assumption,
-    suffices M = {0}, by rw[this]; exact cSup_singleton 0,
-    (set.ext_iff M {0}).mpr $ assume r, iff.intro
-      (assume : ∃ (x : E), ∥x∥ ≤ 1 ∧ ∥A x∥ = r,
-        let ⟨x, _, _⟩ := this in
-          have h : ∥(0:F)∥ = r, by rwa[‹A=0›] at *,
-          by finish)
-      (assume : r ∈ {0},
-        have r = 0, from set.eq_of_mem_singleton this,
-        exists.intro (0:E) $ ⟨by rw[norm_zero]; exact zero_le_one, by rw[this, ‹A 0 = 0›]; simp⟩))
-
-theorem operator_norm_homogeneous (c : ℝ) (A : L(E, F)) : ∥c • A∥ = ∥c∥ * ∥A∥ :=
--- ∥c • A∥ is the supremum of the image of the map x ↦ ∥c • A x∥ on the unit ball in E
--- we show that this is the same as ∥c∥ * ∥A∥ by showing 1) and 2):
--- 1) ∥c∥ * ∥A∥ is an upper bound for the image of x ↦ ∥c • A x∥ on the unit ball
--- 2) any w < ∥c∥ * ∥A∥ is not an upper bound (this is equivalent to showing that every upper bound is ≥ ∥c∥ * ∥A∥)
-suffices (∀ a ∈ _, a ≤ ∥c∥ * ∥A∥) ∧ (∀ (ub : ℝ), (∀ a ∈ _, a ≤ ub) → ∥c∥ * ∥A∥ ≤ ub), from
-  cSup_intro' (show _ ≠ ∅, from set.ne_empty_of_mem $ zero_in_im_ball _) this.1 this.2,
-and.intro
-  (show ∀ a ∈ image (λ x, ∥(c • A) x∥) {x : E | ∥x∥ ≤ 1}, a ≤ ∥c∥ * ∥A∥, from
-    assume a (hₐ : ∃ (x : E), ∥x∥ ≤ 1 ∧ ∥(c • A) x∥ = a),
-      let ⟨x, _, _⟩ := hₐ in
-        calc a = ∥c • A x∥    : eq.symm ‹_›
-           ... = ∥c∥ * ∥A x∥   : by rw[←norm_smul c (A x)]; refl
-           ... ≤ ∥c∥ * ∥A∥     : mul_le_mul_of_nonneg_left
-                                   (bounded_by_operator_norm_on_unit_ball A ‹∥x∥ ≤ 1›)
-                                   (norm_nonneg c))
-  (show ∀ (ub : ℝ), (∀ a ∈ image (λ (x : E), ∥(c • A) x∥) {x : E | ∥x∥ ≤ 1}, a ≤ ub) → ∥c∥ * ∥A∥ ≤ ub, from
-    assume u u_is_ub,
-      classical.by_cases
-        (assume : c = 0,
-          calc ∥c∥ * ∥A∥ = 0 : by rw[‹c=0›, norm_zero, zero_mul]
-                    ... ≤ u : u_is_ub (0:ℝ) $ zero_in_im_ball _)
-        (assume : c ≠ 0,
-          have ∥c∥ ≠ 0, from ne_of_gt $ (norm_pos_iff c).mpr ‹c ≠ 0›,
-          have bla : u = ∥c∥ * (∥c∥⁻¹ * u), by rw[←mul_assoc, mul_inv_cancel ‹∥c∥ ≠ 0›, one_mul],
-          suffices ∥A∥ ≤ ∥c∥⁻¹ * u, from
-            have u = ∥c∥ * (∥c∥⁻¹ * u), by rw[←mul_assoc, mul_inv_cancel ‹∥c∥ ≠ 0›, one_mul],
-            by rw[this]; exact mul_le_mul_of_nonneg_left ‹_› (norm_nonneg c),
-          cSup_le
-            (set.ne_empty_of_mem $ zero_in_im_ball _)
-            (assume n (H : ∃ (x : E), ∥x∥ ≤ 1 ∧ ∥A x∥ = n),
-              let ⟨x, _, _⟩ := H in
-              calc n = ∥A x∥             : eq.symm ‹∥A x∥ = n›
-                 ... = ∥c∥⁻¹ * ∥c • A x∥ : by rw[norm_smul, ←mul_assoc, inv_mul_cancel ‹∥c∥ ≠ 0›, one_mul]
-                 ... ≤ ∥c∥⁻¹ * u         : mul_le_mul_of_nonneg_left (u_is_ub ∥c • A x∥ ⟨x, ‹∥x∥ ≤ 1›, rfl⟩) $
-                                                                     inv_nonneg.mpr $ norm_nonneg c)))
+    have ∥A∥ ≤ 0, from operator_norm_bounded_by (le_refl 0) $ by rw this; simp [le_refl],
+    le_antisymm this (operator_norm_nonneg A))
+
+section instance_70
+-- one needs to increase the max_depth for the following proof
+set_option class.instance_max_depth 70
+
+/-- Auxiliary lemma to prove that the operator norm is homogeneous. -/
+lemma operator_norm_homogeneous_le (c : k) (A : L(E, F)) : ∥c • A∥ ≤ ∥c∥ * ∥A∥ :=
+begin
+  apply operator_norm_bounded_by (mul_nonneg (norm_nonneg _) (operator_norm_nonneg _)) (λx, _),
+  erw [norm_smul _ _, mul_assoc],
+  exact mul_le_mul_of_nonneg_left bounded_by_operator_norm (norm_nonneg _)
+end
+
+theorem operator_norm_homogeneous (c : k) (A : L(E, F)) : ∥c • A∥ = ∥c∥ * ∥A∥ :=
+begin
+  refine le_antisymm (operator_norm_homogeneous_le c A) _,
+  by_cases h : ∥c∥ = 0,
+  { have : c = 0, from (norm_eq_zero _).1 h,
+    have I : ∥(0 : L(E, F))∥ = 0, by rw operator_norm_zero_iff,
+    simp only [h],
+    simp [this, I] },
+  { have h' : c ≠ 0, by simpa [norm_eq_zero] using h,
+    have : ∥A∥ ≤ ∥c • A∥ / ∥c∥, from calc
+      ∥A∥ = ∥(1 : k) • A∥ : by rw bounded_linear_maps.one_smul
+      ... = ∥c⁻¹ • c • A∥ : by rw [smul_smul, inv_mul_cancel h']
+      ... ≤ ∥c⁻¹∥ * ∥c • A∥ : operator_norm_homogeneous_le _ _
+      ... = ∥c • A∥ / ∥c∥ : by rw [norm_inv, div_eq_inv_mul],
+    rwa [le_div_iff, mul_comm] at this,
+    simpa [ne.symm h] using le_iff_eq_or_lt.1 (norm_nonneg c) }
+end
+end instance_70
 
 /-- Expose L(E,F) equipped with the operator norm as normed space. -/
-noncomputable instance bounded_linear_maps.to_normed_space : normed_space ℝ L(E,F) :=
-normed_space.of_core ℝ L(E,F) {
+noncomputable instance bounded_linear_maps.to_normed_space : normed_space k L(E,F) :=
+normed_space.of_core k L(E,F) {
   norm_eq_zero_iff := operator_norm_zero_iff,
   norm_smul := operator_norm_homogeneous,
-  triangle := operator_norm_triangle
-}
+  triangle := operator_norm_triangle }
 
 end operator_norm