From 796e16bdb7fa7595b83d3debee1b28e2d23b1729 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 28 Jan 2016 17:24:39 -0500 Subject: [PATCH] feat(library/theories/analysis): add theorems about convergent functions in metric spaces --- library/theories/analysis/metric_space.lean | 143 +++++++++++++++++++- 1 file changed, 141 insertions(+), 2 deletions(-) diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index b3c3fbee5b..fdf4104d52 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -5,7 +5,7 @@ Author: Jeremy Avigad Metric spaces. -/ -import data.real.division +import data.real.complete data.pnat open nat real eq.ops classical structure metric_space [class] (M : Type) : Type := @@ -44,6 +44,11 @@ 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 ne_of_dist_pos {x y : M} (H : dist x y > 0) : x ≠ y := +suppose x = y, +have H1 [visible] : dist x x > 0, by rewrite this at {2}; exact H, +by rewrite dist_self at H1; apply not_lt_self _ H1 + 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) @@ -189,7 +194,7 @@ 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') (f x) < ε +∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ dist x' x < δ → dist (f x') y < ε notation f `⟶` y `at` x := converges_to_at f y x @@ -231,6 +236,128 @@ exists.intro δ (and.intro assume H : x' ≠ x ∧ dist x' x < δ, show dist (f x') (f x) < ε, from and.right Hδ x' (and.right H))) +section +omit strucN +set_option pp.coercions true +--set_option pp.all true + +open pnat rat + +section +omit strucM + +theorem of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat {p : pnat} : of_rat (rat_of_pnat p) = of_nat (nat_of_pnat p) := + rfl + +end + +theorem cnv_real_of_cnv_nat {X : ℕ → M} {c : M} (H : ∀ n : ℕ, dist (X n) c < 1 / (real.of_nat n + 1)) : + ∀ ε : ℝ, ε > 0 → ∃ N : ℕ, ∀ n : ℕ, n ≥ N → dist (X n) c < ε := + begin + intros ε Hε, + cases ex_rat_pos_lower_bound_of_pos Hε with q Hq, + cases Hq with Hq1 Hq2, + cases pnat_bound Hq1 with p Hp, + existsi nat_of_pnat p, + intros n Hn, + apply lt_of_lt_of_le, + apply H, + apply le.trans, + rotate 1, + apply Hq2, + have Hrat : of_rat (inv p) ≤ of_rat q, from of_rat_le_of_rat_of_le Hp, + apply le.trans, + rotate 1, + exact Hrat, + change 1 / (of_nat n + 1) ≤ of_rat ((1 : ℚ) / (rat_of_pnat p)), + rewrite [of_rat_divide, of_rat_one], + eapply one_div_le_one_div_of_le, + krewrite -of_rat_zero, + apply of_rat_lt_of_rat_of_lt, + apply rat_of_pnat_is_pos, + krewrite [of_rat_rat_of_pnat_eq_of_nat_nat_of_pnat, -real.of_nat_add], + apply real.of_nat_le_of_nat_of_le, + apply le_add_of_le_right, + assumption + end +end + +theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) + (Hseq : ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ)) → ((λ n : ℕ, f (X n)) ⟶ l in ℕ))) + : f ⟶ l at c := + by_contradiction + (assume Hnot : ¬ (f ⟶ l at c), + obtain ε Hε, from exists_not_of_not_forall Hnot, + let Hε' := iff.mp not_implies_iff_and_not Hε in + obtain (H1 : ε > 0) H2, from Hε', + have H3 [visible] : ∀ δ : ℝ, (δ > 0 → ∃ x' : M, x' ≠ c ∧ dist x' c < δ ∧ dist (f x') l ≥ ε), begin -- tedious!! + intros δ Hδ, + note Hε'' := forall_not_of_not_exists H2, + note H4 := forall_not_of_not_exists H2 δ, + have ¬ (∀ x' : M, x' ≠ c ∧ dist x' c < δ → dist (f x') l < ε), from λ H', H4 (and.intro Hδ H'), + note H5 := exists_not_of_not_forall this, + cases H5 with x' Hx', + existsi x', + note H6 := iff.mp not_implies_iff_and_not Hx', + rewrite and.assoc at H6, + cases H6, + split, + assumption, + cases a_1, + split, + assumption, + apply le_of_not_gt, + assumption + end, + let S : ℕ → M → Prop := λ n x, 0 < dist x c ∧ dist x c < 1 / (of_nat n + 1) ∧ dist (f x) l ≥ ε in + have HS [visible] : ∀ n : ℕ, ∃ m : M, S n m, begin + intro k, + have Hpos : 0 < of_nat k + 1, from of_nat_succ_pos k, + cases H3 (1 / (k + 1)) (one_div_pos_of_pos Hpos) with x' Hx', + cases Hx' with Hne Hx', + cases Hx' with Hdistl Hdistg, + existsi x', + esimp, + split, + apply dist_pos_of_ne, + assumption, + split, + repeat assumption + end, + let X : ℕ → M := λ n, some (HS n) in + have H4 [visible] : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ), from + (take n, and.intro + (begin + note Hspec := some_spec (HS n), + esimp, esimp at Hspec, + cases Hspec, + apply ne_of_dist_pos, + assumption + end) + (begin + apply cnv_real_of_cnv_nat, + intro m, + note Hspec := some_spec (HS m), + esimp, esimp at Hspec, + cases Hspec with Hspec1 Hspec2, + cases Hspec2, + assumption + end)), + have H5 [visible] : (λ n : ℕ, f (X n)) ⟶ l in ℕ, from Hseq X H4, + begin + note H6 := H5 H1, + cases H6 with Q HQ, + note HQ' := HQ !le.refl, + esimp at HQ', + apply absurd HQ', + apply not_lt_of_ge, + note H7 := some_spec (HS Q), + esimp at H7, + cases H7 with H71 H72, + cases H72, + assumption + end) + definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x theorem converges_seq_of_comp [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N} @@ -253,6 +380,18 @@ theorem converges_seq_of_comp [instance] (X : ℕ → M) [HX : converges_seq X] apply HB Hn end +omit strucN + +theorem id_continuous : continuous (λ x : M, x) := + begin + intros x ε Hε, + existsi ε, + split, + assumption, + intros, + assumption + end + end metric_space_M_N end analysis