feat(library/theories/analysis/normed_space): start theory of normed spaces for analysis

library/algebra/module.lean

@@ -16,10 +16,10 @@ infixl ` • `:73 := has_scalar.smul
 
 structure left_module [class] (R M : Type) [ringR : ring R]
   extends has_scalar R M, add_comm_group M :=
-(smul_distrib_left : ∀ (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
-(smul_distrib_right : ∀ (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x)))
+(smul_left_distrib : ∀ (r : R) (x y : M), smul r (add x y) = (add (smul r x) (smul r y)))
+(smul_right_distrib : ∀ (r s : R) (x : M), smul (ring.add r s) x = (add (smul r x) (smul s x)))
 (smul_mul : ∀ r s x, smul (mul r s) x = smul r (smul s x))
-(smul_one : ∀ x, smul one x = x)
+(one_smul : ∀ x, smul one x = x)
 
 section left_module
   variables {R M : Type}
@@ -29,27 +29,27 @@ section left_module
 
   -- Note: the anonymous include does not work in the propositions below.
 
-  proposition smul_distrib_left (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
-  !left_module.smul_distrib_left
+  proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v :=
+  !left_module.smul_left_distrib
 
-  proposition smul_distrib_right (a b : R) (u : M) : (a + b)•u = a•u + b•u :=
-  !left_module.smul_distrib_right
+  proposition smul_right_distrib (a b : R) (u : M) : (a + b)•u = a•u + b•u :=
+  !left_module.smul_right_distrib
 
   proposition smul_mul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) :=
   !left_module.smul_mul
 
-  proposition one_smul (u : M) : (1 : R) • u = u := !left_module.smul_one
+  proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul
 
   proposition zero_smul (u : M) : (0 : R) • u = 0 :=
-  have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_distrib_right, *add_zero],
+  have (0 : R) • u + 0 • u = 0 • u + 0, by rewrite [-smul_right_distrib, *add_zero],
   !add.left_cancel this
 
   proposition smul_zero (a : R) : a • (0 : M) = 0 :=
-  have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_distrib_left, *add_zero],
+  have a • 0 + a • 0 = a • 0 + 0, by rewrite [-smul_left_distrib, *add_zero],
   !add.left_cancel this
 
   proposition neg_smul (a : R) (u : M) : (-a) • u = - (a • u) :=
-  eq_neg_of_add_eq_zero (by rewrite [-smul_distrib_right, add.left_inv, zero_smul])
+  eq_neg_of_add_eq_zero (by rewrite [-smul_right_distrib, add.left_inv, zero_smul])
 
   proposition neg_one_smul (u : M) : -(1 : R) • u = -u :=
   by rewrite [neg_smul, one_smul]

library/theories/analysis/analysis.md

@@ -3,3 +3,4 @@ theories.analysis
 
 * [metric_space](metric_space.lean)
 * [real_limit](real_limit.lean)
+* [normed_space](normed_space.lean)

library/theories/analysis/metric_space.lean

@@ -244,3 +244,7 @@ open metric_space
 
 structure complete_metric_space [class] (M : Type) extends metricM : metric_space M : Type :=
 (complete : ∀ X, @cauchy M metricM X → @converges_seq M metricM X)
+
+proposition complete (M : Type) [cmM : complete_metric_space M] {X : ℕ → M} (H : cauchy X) :
+  converges_seq X :=
+complete_metric_space.complete X H

library/theories/analysis/normed_space.lean

@@ -0,0 +1,116 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Normed spaces.
+-/
+import algebra.module .real_limit
+open real
+
+noncomputable theory
+
+structure has_norm [class] (M : Type) : Type :=
+(norm : M → ℝ)
+
+definition norm {M : Type} [has_normM : has_norm M] (v : M) : ℝ := has_norm.norm v
+
+notation `∥`v`∥` := norm v
+
+-- where is the right place to put this?
+structure real_vector_space [class] (V : Type) extends vector_space ℝ V
+
+structure normed_vector_space [class] (V : Type) extends real_vector_space V, has_norm V :=
+(norm_zero : norm zero = 0)
+(eq_zero_of_norm_eq_zero : ∀ u : V, norm u = 0 → u = zero)
+(norm_triangle : ∀ u v, norm (add u v) ≤ norm u + norm v)
+(norm_smul : ∀ (a : ℝ) (v : V), norm (smul a v) = abs a * norm v)
+
+-- what namespace should we put this in?
+
+section normed_vector_space
+  variable {V : Type}
+  variable [normed_vector_space V]
+
+  proposition norm_zero : ∥ (0 : V) ∥ = 0 := !normed_vector_space.norm_zero
+
+  proposition eq_zero_of_norm_eq_zero {u : V} (H : ∥ u ∥ = 0) : u = 0 :=
+  !normed_vector_space.eq_zero_of_norm_eq_zero H
+
+  proposition norm_triangle (u v : V) : ∥ u + v ∥ ≤ ∥ u ∥ + ∥ v ∥ :=
+  !normed_vector_space.norm_triangle
+
+  proposition norm_smul (a : ℝ) (v : V) : ∥ a • v ∥ = abs a * ∥ v ∥ :=
+  !normed_vector_space.norm_smul
+
+  proposition norm_neg (v : V) : ∥ -v ∥ = ∥ v ∥ :=
+  have abs (1 : ℝ) = 1, from abs_of_nonneg zero_le_one,
+  by+ rewrite [-@neg_one_smul ℝ V, norm_smul, abs_neg, this, one_mul]
+
+  section
+    private definition nvs_dist (u v : V) := ∥ u - v ∥
+
+    private lemma nvs_dist_self (u : V) : nvs_dist u u = 0 :=
+    by rewrite [↑nvs_dist, sub_self, norm_zero]
+
+    private lemma eq_of_nvs_dist_eq_zero (u v : V) (H : nvs_dist u v = 0) : u = v :=
+    have u - v = 0, from eq_zero_of_norm_eq_zero H,
+    eq_of_sub_eq_zero this
+
+    private lemma nvs_dist_triangle (u v w : V) : nvs_dist u w ≤ nvs_dist u v + nvs_dist v w :=
+    calc
+      nvs_dist u w = ∥ (u - v) + (v - w) ∥       : by rewrite [↑nvs_dist, *sub_eq_add_neg, add.assoc,
+                                                               neg_add_cancel_left]
+               ... ≤ ∥ u - v ∥ + ∥ v - w ∥       : norm_triangle
+
+    private lemma nvs_dist_comm  (u v : V) : nvs_dist u v = nvs_dist v u :=
+    by rewrite [↑nvs_dist, -norm_neg, neg_sub]
+  end
+
+  definition normed_vector_space_to_metric_space [reducible] [trans_instance] : metric_space V :=
+  ⦃ metric_space,
+    dist               := nvs_dist,
+    dist_self          := nvs_dist_self,
+    eq_of_dist_eq_zero := eq_of_nvs_dist_eq_zero,
+    dist_comm          := nvs_dist_comm,
+    dist_triangle      := nvs_dist_triangle
+  ⦄
+end normed_vector_space
+
+structure banach_space [class] (V : Type) extends nvsV : normed_vector_space V :=
+(complete : ∀ X, @metric_space.cauchy V (@normed_vector_space_to_metric_space V nvsV) X →
+    @metric_space.converges_seq V (@normed_vector_space_to_metric_space V nvsV) X)
+
+definition banach_space_to_metric_space [reducible] [trans_instance] (V : Type) [bsV : banach_space V] :
+  complete_metric_space V :=
+⦃ complete_metric_space, normed_vector_space_to_metric_space,
+  complete := banach_space.complete
+⦄
+
+section
+  open metric_space
+
+  example (V : Type) (vsV : banach_space V) (X : ℕ → V) (H : cauchy X) : converges_seq X :=
+  complete V H
+end
+
+/- the real numbers themselves can be viewed as a banach space -/
+
+definition real_is_real_vector_space [trans_instance] [reducible] : real_vector_space ℝ :=
+⦃ real_vector_space, real.discrete_linear_ordered_field,
+  smul               := mul,
+  smul_left_distrib  := left_distrib,
+  smul_right_distrib := right_distrib,
+  smul_mul           := mul.assoc,
+  one_smul           := one_mul
+⦄
+
+definition real_is_banach_space [trans_instance] [reducible] : banach_space ℝ :=
+⦃ banach_space, real_is_real_vector_space,
+  norm                    := abs,
+  norm_zero               := abs_zero,
+  eq_zero_of_norm_eq_zero := λ a H, eq_zero_of_abs_eq_zero H,
+  norm_triangle           := abs_add_le_abs_add_abs,
+  norm_smul               := abs_mul,
+  complete                := λ X H, complete ℝ H
+⦄