feat(library/theories/{metric_space,real_limit}): define metric spaces, limits, instantiate reals

library/theories/analysis/analysis.md

@@ -0,0 +1,5 @@
+theories.analysis
+=================
+
+* [metric_space](metric_space.lean)
+* [real_limit](real_limit.lean)

library/theories/analysis/metric_space.lean

@@ -0,0 +1,141 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Metric spaces.
+-/
+import data.real.division
+open real eq.ops classical
+
+structure metric_space [class] (M : Type) : Type :=
+  (dist : M → M → ℝ)
+  (dist_self : ∀ x : M, dist x x = 0)
+  (eq_of_dist_eq_zero : ∀ {x y : M}, dist x y = 0 → x = y)
+  (dist_comm : ∀ x y : M, dist x y = dist y x)
+  (dist_triangle : ∀ x y z : M, dist x y + dist y z ≥ dist x z)
+
+namespace metric_space
+
+section metric_space_M
+variables {M : Type} [strucM : metric_space M]
+include strucM
+
+proposition dist_eq_zero_iff (x y : M) : dist x y = 0 ↔ x = y :=
+iff.intro eq_of_dist_eq_zero (suppose x = y, this ▸ !dist_self)
+
+proposition dist_nonneg (x y : M) : 0 ≤ dist x y :=
+have dist x y + dist y x ≥ 0, by rewrite -(dist_self x); apply dist_triangle,
+have 2 * dist x y ≥ 0, using this,
+  by rewrite [-real.one_add_one, right_distrib, +one_mul, dist_comm at {2}]; apply this,
+nonneg_of_mul_nonneg_left this two_pos
+
+proposition dist_pos_of_ne {x y : M} (H : x ≠ y) : dist x y > 0 :=
+lt_of_le_of_ne !dist_nonneg (suppose 0 = dist x y, H (iff.mp !dist_eq_zero_iff this⁻¹))
+
+proposition eq_of_forall_dist_le {x y : M} (H : ∀ ε, ε > 0 → dist x y ≤ ε) : x = y :=
+eq_of_dist_eq_zero (eq_zero_of_nonneg_of_forall_le !dist_nonneg H)
+
+open nat
+
+definition converges_to_seq (X : ℕ → M) (y : M) : Prop :=
+∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y < ε
+
+-- the same, with ≤ in place of <; easier to prove, harder to use
+definition converges_to_seq.intro {X : ℕ → M} {y : M}
+    (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y ≤ ε) :
+  converges_to_seq X y :=
+take ε, assume epos : ε > 0,
+  have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
+  obtain N HN, from H e2pos,
+  exists.intro N
+    (take n, suppose n ≥ N,
+      calc
+        dist (X n) y ≤ ε / 2 : HN _ `n ≥ N`
+                 ... < ε     : div_two_lt_of_pos epos)
+
+notation X `⟶` y `in` `ℕ` := converges_to_seq X y
+
+definition converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y in ℕ
+
+noncomputable definition limit_seq (X : ℕ → M) [H : converges_seq X] : M := some H
+
+proposition converges_to_limit_seq (X : ℕ → M) [H : converges_seq X] :
+  (X ⟶ limit_seq X in ℕ) :=
+some_spec H
+
+proposition converges_to_seq_unique {X : ℕ → M} {y₁ y₂ : M}
+  (H₁ : X ⟶ y₁ in ℕ) (H₂ : X ⟶ y₂ in ℕ) : y₁ = y₂ :=
+eq_of_forall_dist_le
+  (take ε, suppose ε > 0,
+    have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
+    obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → dist (X n) y₁ < ε / 2), from H₁ e2pos,
+    obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → dist (X n) y₂ < ε / 2), from H₂ e2pos,
+    let N := max N₁ N₂ in
+    have dN₁ : dist (X N) y₁ < ε / 2, from HN₁ !le_max_left,
+    have dN₂ : dist (X N) y₂ < ε / 2, from HN₂ !le_max_right,
+    have dist y₁ y₂ < ε, from calc
+      dist y₁ y₂ ≤ dist y₁ (X N) + dist (X N) y₂ : dist_triangle
+             ... = dist (X N) y₁ + dist (X N) y₂ : dist_comm
+             ... < ε / 2 + ε / 2                 : add_lt_add dN₁ dN₂
+             ... = ε                             : add_halves,
+    show dist y₁ y₂ ≤ ε, from le_of_lt this)
+
+proposition eq_limit_of_converges_to_seq {X : ℕ → M} (y : M) (H : X ⟶ y in ℕ) :
+  y = @limit_seq M _ X (exists.intro y H) :=
+converges_to_seq_unique H (@converges_to_limit_seq M _ X (exists.intro y H))
+
+proposition converges_to_seq_constant (y : M) : (λn, y) ⟶ y in ℕ :=
+take ε, assume egt0 : ε > 0,
+  exists.intro 0
+    (take n, suppose n ≥ 0,
+      calc
+        dist y y = 0 : !dist_self
+             ... < ε : egt0)
+
+definition cauchy (X : ℕ → M) : Prop :=
+∀ ε : ℝ, ε > 0 → ∃ N, ∀ m n, m ≥ N → n ≥ N → dist (X m) (X n) < ε
+
+proposition cauchy_of_converges_seq (X : ℕ → M) [H : converges_seq X] : cauchy X :=
+take ε, suppose ε > 0,
+  obtain y (Hy : converges_to_seq X y), from H,
+  have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos,
+  obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → dist (X n) y < ε / 2), from Hy e2pos,
+  obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → dist (X n) y < ε / 2), from Hy e2pos,
+  let N := max N₁ N₂ in
+    exists.intro N
+      (take m n, suppose m ≥ N, suppose n ≥ N,
+        have m ≥ N₁, from le.trans !le_max_left `m ≥ N`,
+        have n ≥ N₂, from le.trans !le_max_right `n ≥ N`,
+        have dN₁ : dist (X m) y < ε / 2, from HN₁ `m ≥ N₁`,
+        have dN₂ : dist (X n) y < ε / 2, from HN₂ `n ≥ N₂`,
+        show dist (X m) (X n) < ε, from calc
+          dist (X m) (X n) ≤ dist (X m) y + dist y (X n) : dist_triangle
+                       ... = dist (X m) y + dist (X n) y : dist_comm
+                       ... < ε / 2 + ε / 2               : add_lt_add dN₁ dN₂
+                       ... = ε                           : add_halves)
+
+end metric_space_M
+
+section metric_space_M_N
+variables {M N : Type} [strucM : metric_space M] [strucN : metric_space N]
+include strucM strucN
+
+definition converges_to_at (f : M → N) (y : N) (x : M) :=
+∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ x', x ≠ x' ∧ dist x x' < δ → dist (f x') y < ε
+
+notation f `⟶` y `at` x := converges_to_at f y x
+
+definition converges_at [class] (f : M → N) (x : M) :=
+∃ y, converges_to_at f y x
+
+noncomputable definition limit_at (f : M → N) (x : M) [H : converges_at f x] : N :=
+some H
+
+proposition converges_to_limit_at (f : M → N) (x : M) [H : converges_at f x] :
+  (f ⟶ limit_at f x at x) :=
+some_spec H
+
+end metric_space_M_N
+
+end metric_space

library/theories/analysis/real_limit.lean

@@ -0,0 +1,207 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Instantiates the reals as a metric space, and expresses completeness, sup, and inf in
+a manner that is less constructive, but more convenient, than the way it is done in
+data.real.complete.
+
+The definitions here are noncomputable, for various reasons:
+
+(1) We rely on the nonconstructive definition of abs.
+(2) The theory of the reals uses the "some" operator e.g. to define the ceiling function.
+    This can't be defined constructively as an operation on the quotient, because
+    such a function is not continuous.
+(3) We use "forall" and "exists" to say that a series converges, rather than carrying
+    around rates of convergence explicitly. We then use "some" whenever we need to extract
+    information, such as the limit.
+
+These could be avoided in a constructive theory of analysis, but here we will not
+follow that route.
+-/
+import .metric_space data.real.complete
+open real eq.ops classical
+noncomputable theory
+
+namespace real
+
+/- the reals form a metric space -/
+
+protected definition to_metric_space [instance] : metric_space ℝ :=
+⦃ metric_space,
+  dist               := λ x y, abs (x - y),
+  dist_self          := λ x, abstract by rewrite [sub_self, abs_zero] end,
+  eq_of_dist_eq_zero := @eq_of_abs_sub_eq_zero,
+  dist_comm          := abs_sub,
+  dist_triangle      := abs_sub_le
+⦄
+
+open nat
+
+definition converges_to_seq (X : ℕ → ℝ) (y : ℝ) : Prop :=
+∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε
+
+proposition converges_to_seq.intro {X : ℕ → ℝ} {y : ℝ}
+    (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) :
+  converges_to_seq X y :=
+metric_space.converges_to_seq.intro H
+
+notation X `⟶` y `in` `ℕ` := converges_to_seq X y
+
+definition converges_seq [class] (X : ℕ → ℝ) : Prop := ∃ y, X ⟶ y in ℕ
+
+definition limit_seq (X : ℕ → ℝ) [H : converges_seq X] : ℝ := some H
+
+proposition converges_to_limit_seq (X : ℕ → ℝ) [H : converges_seq X] :
+  (X ⟶ limit_seq X in ℕ) :=
+some_spec H
+
+proposition converges_to_seq_unique {X : ℕ → ℝ} {y₁ y₂ : ℝ}
+  (H₁ : X ⟶ y₁ in ℕ) (H₂ : X ⟶ y₂ in ℕ) : y₁ = y₂ :=
+metric_space.converges_to_seq_unique H₁ H₂
+
+proposition eq_limit_of_converges_to_seq {X : ℕ → ℝ} (y : ℝ) (H : X ⟶ y in ℕ) :
+  y = @limit_seq X (exists.intro y H) :=
+converges_to_seq_unique H (@converges_to_limit_seq X (exists.intro y H))
+
+proposition converges_to_seq_constant (y : ℝ) : (λn, y) ⟶ y in ℕ :=
+metric_space.converges_to_seq_constant y
+
+/- the completeness of the reals, "translated" from data.real.complete -/
+
+definition cauchy (X : ℕ → ℝ) := metric_space.cauchy X
+
+section
+  open pnat subtype
+
+  private definition pnat.succ (n : ℕ) : ℕ+ := tag (succ n) !succ_pos
+
+  private definition r_seq_of (X : ℕ → ℝ) : r_seq := λ n, X (elt_of n)
+
+  private lemma rate_of_cauchy_aux {X : ℕ → ℝ} (H : cauchy X) :
+    ∀ k : ℕ+, ∃ N : ℕ+, ∀ m n : ℕ+,
+      m ≥ N → n ≥ N → abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹ :=
+  take k : ℕ+,
+  have H1 : (rat.gt k⁻¹ (rat.of_num 0)), from !inv_pos,
+  have H2 : (of_rat k⁻¹ > of_rat (rat.of_num 0)), from !of_rat_lt_of_rat_of_lt H1,
+  obtain (N : ℕ) (H : ∀ m n, m ≥ N → n ≥ N → abs (X m - X n) < of_rat k⁻¹), from H _ H2,
+  exists.intro (pnat.succ N)
+    (take m n : ℕ+,
+      assume Hm : m ≥ (pnat.succ N),
+      assume Hn : n ≥ (pnat.succ N),
+      have Hm' : elt_of m ≥ N, from nat.le.trans !le_succ Hm,
+      have Hn' : elt_of n ≥ N, from nat.le.trans !le_succ Hn,
+      show abs (X (elt_of m) - X (elt_of n)) ≤ of_rat k⁻¹, from le_of_lt (H _ _ Hm' Hn'))
+
+  private definition rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) (k : ℕ+) : ℕ+ :=
+  some (rate_of_cauchy_aux H k)
+
+  private lemma cauchy_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
+    cauchy_with_rate (r_seq_of X) (rate_of_cauchy H) :=
+  take k : ℕ+,
+  some_spec (rate_of_cauchy_aux H k)
+
+  private lemma converges_to_with_rate_of_cauchy {X : ℕ → ℝ} (H : cauchy X) :
+    ∃ l Nb, converges_to_with_rate (r_seq_of X) l Nb :=
+  begin
+    apply exists.intro,
+    apply exists.intro,
+    apply converges_to_with_rate_of_cauchy_with_rate,
+    exact cauchy_with_rate_of_cauchy H
+  end
+
+theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq X :=
+obtain l Nb (conv : converges_to_with_rate (r_seq_of X) l Nb),
+  from converges_to_with_rate_of_cauchy H,
+exists.intro l
+  (take ε : ℝ,
+    suppose ε > 0,
+    obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`,
+    let k : ℕ+ := tag (succ k') !succ_pos,
+        N : ℕ+ := Nb k in
+    have Hk : real.of_rat k⁻¹ < ε,
+      by rewrite [↑pnat.inv, of_rat_divide]; exact Hn,
+    exists.intro (elt_of N)
+      (take n : ℕ,
+        assume Hn : n ≥ elt_of N,
+        let n' : ℕ+ := tag n (nat.lt_of_lt_of_le (has_property N) Hn) in
+        have abs (X n - l) ≤ real.of_rat k⁻¹, from conv k n' Hn,
+        show abs (X n - l) < ε, from lt_of_le_of_lt this Hk))
+
+/- sup and inf -/
+
+open set
+
+private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :
+  ∃ y, is_sup X y :=
+let x := some (and.left H), b := some (and.right H) in
+  exists_is_sup_of_inh_of_bdd X x (some_spec (and.left H)) b (some_spec (and.right H))
+
+private definition sup_aux {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :=
+some (exists_is_sup H)
+
+private definition sup_aux_spec {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) :
+  is_sup X (sup_aux H) :=
+some_spec (exists_is_sup H)
+
+definition sup (X : set ℝ) : ℝ :=
+if H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b) then sup_aux H else 0
+
+proposition le_sup {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) :
+  x ≤ sup X :=
+have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b),
+  from and.intro (exists.intro x Hx) (exists.intro b Hb),
+by+ rewrite [↑sup, dif_pos H]; exact and.left (sup_aux_spec H) x Hx
+
+proposition sup_le {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) :
+  sup X ≤ b :=
+have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b),
+  from and.intro HX (exists.intro b Hb),
+by+ rewrite [↑sup, dif_pos H]; exact and.right (sup_aux_spec H) b Hb
+
+private definition exists_is_inf {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) :
+  ∃ y, is_inf X y :=
+let x := some (and.left H), b := some (and.right H) in
+  exists_is_inf_of_inh_of_bdd X x (some_spec (and.left H)) b (some_spec (and.right H))
+
+private definition inf_aux {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) :=
+some (exists_is_inf H)
+
+private definition inf_aux_spec {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) :
+  is_inf X (inf_aux H) :=
+some_spec (exists_is_inf H)
+
+definition inf (X : set ℝ) : ℝ :=
+if H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x) then inf_aux H else 0
+
+proposition inf_le {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) :
+  inf X ≤ x :=
+have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x),
+  from and.intro (exists.intro x Hx) (exists.intro b Hb),
+by+ rewrite [↑inf, dif_pos H]; exact and.left (inf_aux_spec H) x Hx
+
+proposition le_inf {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) :
+  b ≤ inf X :=
+have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x),
+  from and.intro HX (exists.intro b Hb),
+by+ rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb
+
+end
+
+/-
+proposition converges_to_at_unique {f : M → N} {y₁ y₂ : N} {x : M}
+  (H₁ : f ⟶ y₁ '[at x]) (H₂ : f ⟶ y₂ '[at x]) : y₁ = y₂ :=
+eq_of_forall_dist_le
+  (take ε, suppose ε > 0,
+    have e2pos : ε / 2 > 0, from  div_pos_of_pos_of_pos `ε > 0` two_pos,
+    obtain δ₁ [(δ₁pos : δ₁ > 0) (Hδ₁ : ∀ x', x ≠ x' ∧ dist x x' < δ₁ → dist (f x') y₁ < ε / 2)],
+      from H₁ e2pos,
+    obtain δ₂ [(δ₂pos : δ₂ > 0) (Hδ₂ : ∀ x', x ≠ x' ∧ dist x x' < δ₂ → dist (f x') y₂ < ε / 2)],
+      from H₂ e2pos,
+    let δ := min δ₁ δ₂ in
+    have δ > 0, from lt_min δ₁pos δ₂pos,
+
+-/
+
+end real

library/theories/group_theory/group_theory.md

@@ -3,16 +3,10 @@ theories.group_theory
 
 Group theory (especially finite group theory).
 
-[subgroup](subgroup.lean) : general subgroup theories, quotient group using quot
+* [subgroup](subgroup.lean) : general subgroup theories, quotient group using quot
-
+* [finsubg](finsubg.lean) : finite subgroups (finset and fintype), Lagrange theorem, finite cosets and lcoset_type, normalizer for finite groups, coset product and quotient group based on lcoset_type, semidirect product
-[finsubg](finsubg.lean)   : finite subgroups (finset and fintype), Lagrange theorem, finite cosets and lcoset_type, normalizer for finite groups, coset product and quotient group based on lcoset_type, semidirect product
+* [hom](hom.lean) : homomorphism and isomorphism, kernel, first isomorphism theorem
-
+* [perm](perm.lean) : permutation group
-[hom](hom.lean) 	  : homomorphism and isomorphism, kernel, first isomorphism theorem
+* [cyclic](cyclic.lean) : cyclic subgroup, finite generator, order of generator, sequence and rotation
-
+* [action](action.lean)	: fixed point, action, stabilizer, orbit stabilizer theorem, orbit partition, Cayley theorem, action on lcoset, cardinality of permutation group
-[perm](perm.lean)	  : permutation group
+* [pgroup](pgroup.lean)	: subgroup with order of prime power, Cauchy theorem, first Sylow theorem
-
-[cyclic](cyclic.lean)	  : cyclic subgroup, finite generator, order of generator, sequence and rotation
-
-[action](action.lean)	  : fixed point, action, stabilizer, orbit stabilizer theorem, orbit partition, Cayley theorem, action on lcoset, cardinality of permutation group
-
-[pgroup](pgroup.lean)	  : subgroup with order of prime power, Cauchy theorem, first Sylow theorem

library/theories/theories.md

@@ -3,3 +3,5 @@ theories
 
 * [number_theory](number_theory.md)
 * [combinatorics](combinatorics.md)
+* [group_theory](group_theory.md)
+* [analysis](analysis.md)