From e17c5c4f0803af09ea39c845d408e24c4e752f04 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Wed, 18 May 2016 21:21:49 -0400 Subject: [PATCH] feat(library/theories/analysis/*): install new limits --- library/theories/analysis/metric_space.lean | 920 ++++++++++---------- library/theories/analysis/normed_space.lean | 48 +- library/theories/analysis/real_limit.lean | 100 ++- library/theories/topology/limit.lean | 50 +- 4 files changed, 575 insertions(+), 543 deletions(-) diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index eb81196f9..3d0225752 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -1,12 +1,12 @@ /- Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad +Authors: Jeremy Avigad, Robert Lewis Metric spaces. -/ -import data.real.complete data.pnat data.list.sort ..topology.continuous data.set -open nat real eq.ops classical +import data.real.complete data.pnat ..topology.continuous ..topology.limit data.set +open nat real eq.ops classical set prod set.filter topology interval structure metric_space [class] (M : Type) : Type := (dist : M → M → ℝ) @@ -52,396 +52,20 @@ 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) -/- convergence of a sequence -/ -definition converges_to_seq (X : ℕ → M) (y : M) : Prop := -∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ ⦃n⦄, n ≥ N → dist (X n) y < ε +/- instantiate metric space as a topology -/ --- 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) +definition open_ball (x : M) (ε : ℝ) := {y | dist y x < ε} -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) - -proposition converges_to_seq_offset {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) : - (λ n, X (n + k)) ⟶ y in ℕ := -take ε, suppose ε > 0, -obtain N HN, from H `ε > 0`, -exists.intro N - (take n : ℕ, assume ngtN : n ≥ N, - show dist (X (n + k)) y < ε, from HN (n + k) (le.trans ngtN !le_add_right)) - -proposition converges_to_seq_offset_left {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) : - (λ n, X (k + n)) ⟶ y in ℕ := -have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), -by rewrite aux; exact converges_to_seq_offset k H - -proposition converges_to_seq_offset_succ {X : ℕ → M} {y : M} (H : X ⟶ y in ℕ) : - (λ n, X (succ n)) ⟶ y in ℕ := -converges_to_seq_offset 1 H - -proposition converges_to_seq_of_converges_to_seq_offset - {X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (n + k)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -take ε, suppose ε > 0, -obtain N HN, from H `ε > 0`, -exists.intro (N + k) - (take n : ℕ, assume nge : n ≥ N + k, - have n - k ≥ N, from nat.le_sub_of_add_le nge, - have dist (X (n - k + k)) y < ε, from HN (n - k) this, - show dist (X n) y < ε, - by rewrite [(nat.sub_add_cancel (le.trans !le_add_left nge)) at this]; exact this) - -proposition converges_to_seq_of_converges_to_seq_offset_left - {X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), -by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H - -proposition converges_to_seq_of_converges_to_seq_offset_succ - {X : ℕ → M} {y : M} (H : (λ n, X (succ n)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -@converges_to_seq_of_converges_to_seq_offset M _ X y 1 H - -proposition converges_to_seq_offset_iff (X : ℕ → M) (y : M) (k : ℕ) : - ((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -iff.intro converges_to_seq_of_converges_to_seq_offset !converges_to_seq_offset - -proposition converges_to_seq_offset_left_iff (X : ℕ → M) (y : M) (k : ℕ) : - ((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -iff.intro converges_to_seq_of_converges_to_seq_offset_left !converges_to_seq_offset_left - -proposition converges_to_seq_offset_succ_iff (X : ℕ → M) (y : M) : - ((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -iff.intro converges_to_seq_of_converges_to_seq_offset_succ !converges_to_seq_offset_succ - -section -open list -definition r_trans : transitive (@le ℝ _) := λ a b c, !le.trans -definition r_refl : reflexive (@le ℝ _) := λ a, !le.refl - -theorem dec_prf_eq (P : Prop) (H1 H2 : decidable P) : H1 = H2 := - begin - induction H1, - induction H2, - reflexivity, - apply absurd a a_1, - induction H2, - apply absurd a_1 a, - reflexivity - end - --- there's a very ugly part of this proof. - -proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x in ℕ) : - ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K := - begin - cases H zero_lt_one with N HN, - cases em (N = 0), - existsi 1, - intro n, - apply le_of_lt, - apply HN, - rewrite a, - apply zero_le, - let l := map (λ n : ℕ, -dist (X n) x) (upto N), - have Hnenil : l ≠ nil, from (map_ne_nil_of_ne_nil _ (upto_ne_nil_of_ne_zero a)), - existsi max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, - intro n, - have Hsmn : ∀ m : ℕ, m < N → dist (X m) x ≤ max (-list.min (λ a b : ℝ, le a b) l Hnenil) 1, begin - intro m Hm, - apply le.trans, - rotate 1, - apply le_max_left, - note Hall := min_lemma real.le_total r_trans r_refl Hnenil, - have Hmem : -dist (X m) x ∈ (map (λ (n : ℕ), -dist (X n) x) (upto N)), from mem_map _ (mem_upto_of_lt Hm), - note Hallm' := of_mem_of_all Hmem Hall, - apply le_neg_of_le_neg, - esimp, esimp at Hallm', -/- - have Heqs : (λ (a b : real), classical.prop_decidable (@le.{1} real real.real_has_le a b)) - = - (@decidable_le.{1} real - (@decidable_linear_ordered_comm_group.to_decidable_linear_order.{1} real - (@decidable_linear_ordered_comm_ring.to_decidable_linear_ordered_comm_group.{1} real - (@discrete_linear_ordered_field.to_decidable_linear_ordered_comm_ring.{1} real - real.discrete_linear_ordered_field)))), - begin - apply funext, intro, apply funext, intro, - apply dec_prf_eq - end, - rewrite -Heqs, --/ - exact Hallm' - end, - cases em (n < N) with Elt Ege, - apply Hsmn, - exact Elt, - apply le_of_lt, - apply lt_of_lt_of_le, - apply HN, - apply le_of_not_gt Ege, - apply le_max_right - end -end - -/- cauchy sequences -/ - -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 - -/- convergence of a function at a point -/ - -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 - -section -omit strucN -set_option pp.coercions true ---set_option pp.all true - -open pnat rat - -section -omit strucM - -private lemma 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 all_conv_seqs_of_converges_to_at {f : M → N} {c : M} {l : N} (Hconv : f ⟶ l at c) : - ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c in ℕ)) → ((λ n : ℕ, f (X n)) ⟶ l in ℕ)) := - begin - intros X HX, - rewrite [↑converges_to_at at Hconv, ↑converges_to_seq], - intros ε Hε, - cases Hconv Hε with δ Hδ, - cases Hδ with Hδ1 Hδ2, - cases HX 0 with _ HXlim, - cases HXlim Hδ1 with N1 HN1, - existsi N1, - intro n Hn, - apply Hδ2, - split, - apply and.left (HX _), - exact HN1 Hn - 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ε' := and_not_of_not_implies Hε in - obtain (H1 : ε > 0) H2, from Hε', - have H3 : ∀ δ : ℝ, (δ > 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 := and_not_of_not_implies 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 : ∀ 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 : ∀ 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 : (λ 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) - - -end metric_space_M_N - -section topology -/- A metric space is a topological space. -/ - -open set prod topology - -variables {V : Type} [Vmet : metric_space V] -include Vmet - -definition open_ball (x : V) (ε : ℝ) := {y ∈ univ | dist x y < ε} - -theorem open_ball_empty_of_nonpos (x : V) {ε : ℝ} (Hε : ε ≤ 0) : open_ball x ε = ∅ := +theorem open_ball_empty_of_nonpos (x : M) {ε : ℝ} (Hε : ε ≤ 0) : open_ball x ε = ∅ := begin apply eq_empty_of_forall_not_mem, - intro y Hy, - note Hlt := and.right Hy, - apply not_lt_of_ge (dist_nonneg x y), + intro y Hlt, + apply not_lt_of_ge (dist_nonneg y x), apply lt_of_lt_of_le Hlt Hε end -theorem radius_pos_of_nonempty {x : V} {ε : ℝ} {u : V} (Hu : u ∈ open_ball x ε) : ε > 0 := +theorem radius_pos_of_nonempty {x : M} {ε : ℝ} {u : M} (Hu : u ∈ open_ball x ε) : ε > 0 := begin apply lt_of_not_ge, intro Hge, @@ -450,108 +74,93 @@ theorem radius_pos_of_nonempty {x : V} {ε : ℝ} {u : V} (Hu : u ∈ open_ball apply not_mem_empty _ Hu end -theorem mem_open_ball (x : V) {ε : ℝ} (H : ε > 0) : x ∈ open_ball x ε := - suffices x ∈ univ ∧ dist x x < ε, from this, - and.intro !mem_univ (by rewrite dist_self; assumption) +theorem mem_open_ball (x : M) {ε : ℝ} (H : ε > 0) : x ∈ open_ball x ε := + show dist x x < ε, by rewrite dist_self; assumption -definition closed_ball (x : V) (ε : ℝ) := {y ∈ univ | dist x y ≤ ε} +definition closed_ball (x : M) (ε : ℝ) := {y | dist x y ≤ ε} -theorem closed_ball_eq_compl (x : V) (ε : ℝ) : closed_ball x ε = -{y ∈ univ | dist x y > ε} := +theorem closed_ball_eq_compl (x : M) (ε : ℝ) : closed_ball x ε = - {y | dist x y > ε} := begin apply ext, intro y, apply iff.intro, - intro Hx, + intro Hle, apply mem_compl, - intro Hxmem, - cases Hxmem with _ Hgt, - cases Hx with _ Hle, + intro Hgt, apply not_le_of_gt Hgt Hle, intro Hx, note Hx' := not_mem_of_mem_compl Hx, - split, - apply mem_univ, apply le_of_not_gt, intro Hgt, apply Hx', - split, - apply mem_univ, - assumption + exact Hgt end -omit Vmet +variable (M) -definition open_sets_basis (V : Type) [metric_space V] := - image (λ pair : V × ℝ, open_ball (pr1 pair) (pr2 pair)) univ +definition open_sets_basis := + image (λ pair : M × ℝ, open_ball (pr1 pair) (pr2 pair)) univ -definition metric_topology [instance] (V : Type) [metric_space V] : topology V := - topology.generated_by (open_sets_basis V) +definition metric_topology [instance] : topology M := + topology.generated_by (open_sets_basis M) -include Vmet +variable {M} -theorem open_ball_mem_open_sets_basis (x : V) (ε : ℝ) : (open_ball x ε) ∈ (open_sets_basis V) := +theorem open_ball_mem_open_sets_basis (x : M) (ε : ℝ) : open_ball x ε ∈ open_sets_basis M := mem_image !mem_univ rfl -theorem open_ball_open (x : V) (ε : ℝ) : Open (open_ball x ε) := +theorem open_ball_open (x : M) (ε : ℝ) : Open (open_ball x ε) := by apply generators_mem_topology_generated_by; apply open_ball_mem_open_sets_basis -theorem closed_ball_closed (x : V) {ε : ℝ} (H : ε > 0) : closed (closed_ball x ε) := +theorem closed_ball_closed (x : M) {ε : ℝ} (H : ε > 0) : closed (closed_ball x ε) := begin apply iff.mpr !closed_iff_Open_compl, rewrite closed_ball_eq_compl, rewrite compl_compl, apply Open_of_forall_exists_Open_nbhd, - intro y Hy, - cases Hy with _ Hxy, + intro y Hxy, existsi open_ball y (dist x y - ε), split, apply open_ball_open, split, apply mem_open_ball, apply sub_pos_of_lt Hxy, - intros y' Hy', - cases Hy' with _ Hxy'd, - rewrite dist_comm at Hxy'd, - split, - apply mem_univ, + intros y' Hxy'd, apply lt_of_not_ge, intro Hxy', apply not_lt_self (dist x y), exact calc - dist x y ≤ dist x y' + dist y' y : dist_triangle - ... ≤ ε + dist y' y : add_le_add_right Hxy' - ... < ε + (dist x y - ε) : add_lt_add_left Hxy'd - ... = dist x y : by rewrite [add.comm, sub_add_cancel] + dist x y ≤ dist x y' + dist y' y : dist_triangle + ... ≤ ε + dist y' y : add_le_add_right Hxy' + ... < ε + (dist x y - ε) : add_lt_add_left Hxy'd + ... = dist x y : by rewrite [add.comm, sub_add_cancel] end -private theorem not_mem_open_basis_of_boundary_pt {s : set V} (a : s ∈ open_sets_basis V) {x : V} - (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : V, v ∉ s ∧ dist x v < ε) : ¬ x ∈ s := +private theorem not_mem_open_basis_of_boundary_pt {s : set M} (a : s ∈ open_sets_basis M) {x : M} + (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : M, v ∉ s ∧ dist x v < ε) : ¬ x ∈ s := begin intro HxU, cases a with pr Hpr, cases pr with y r, cases Hpr with _ Hs, rewrite -Hs at HxU, - have H : dist y x < r, from and.right HxU, + have H : dist x y < r, from HxU, cases Hbd _ (sub_pos_of_lt H) with v Hv, cases Hv with Hv Hvdist, apply Hv, rewrite -Hs, - apply and.intro, - apply mem_univ, apply lt_of_le_of_lt, apply dist_triangle, exact x, esimp, - exact calc - dist y x + dist x v < dist y x + (r - dist y x) : add_lt_add_left Hvdist - ... = r : by rewrite [add.comm, sub_add_cancel] + rewrite dist_comm, + exact add_lt_of_lt_sub_right Hvdist end -private theorem not_mem_intersect_of_boundary_pt {s t : set V} (a : Open s) (a_1 : Open t) {x : V} - (v_0 : (x ∈ s → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : V), v ∉ s ∧ dist x v < ε)))) - (v_1 : (x ∈ t → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : V), v ∉ t ∧ dist x v < ε)))) - (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : V), v ∉ s ∩ t ∧ dist x v < ε)) : ¬ (x ∈ s ∩ t) := +private theorem not_mem_intersect_of_boundary_pt {s t : set M} (a : Open s) (a_1 : Open t) {x : M} + (v_0 : (x ∈ s → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ s ∧ dist x v < ε)))) + (v_1 : (x ∈ t → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ t ∧ dist x v < ε)))) + (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ s ∩ t ∧ dist x v < ε)) : ¬ (x ∈ s ∩ t) := begin intro HxU, have Hxs : x ∈ s, from mem_of_mem_inter_left HxU, @@ -586,10 +195,10 @@ private theorem not_mem_intersect_of_boundary_pt {s t : set V} (a : Open s) (a_1 apply min_le_right end -private theorem not_mem_sUnion_of_boundary_pt {S : set (set V)} (a : ∀₀ s ∈ S, Open s) {x : V} - (v_0 : ∀ ⦃x_1 : set V⦄, - x_1 ∈ S → x ∈ x_1 → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : V), v ∉ x_1 ∧ dist x v < ε))) - (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : V), v ∉ ⋃₀ S ∧ dist x v < ε)) : ¬ x ∈ ⋃₀ S := +private theorem not_mem_sUnion_of_boundary_pt {S : set (set M)} (a : ∀₀ s ∈ S, Open s) {x : M} + (v_0 : ∀ ⦃x_1 : set M⦄, + x_1 ∈ S → x ∈ x_1 → ¬ (∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ x_1 ∧ dist x v < ε))) + (Hbd : ∀ (ε : ℝ), ε > 0 → (∃ (v : M), v ∉ ⋃₀ S ∧ dist x v < ε)) : ¬ x ∈ ⋃₀ S := begin intro HxU, have Hex : ∃₀ s ∈ S, x ∈ s, from HxU, @@ -606,15 +215,14 @@ private theorem not_mem_sUnion_of_boundary_pt {S : set (set V)} (a : ∀₀ s exact Hdist end - /- this should be doable by showing that the open-ball boundary definition is equivalent to topology.on_boundary, and applying topology.not_open_of_on_boundary. But the induction hypotheses don't work out nicely. -/ -theorem not_open_of_ex_boundary_pt {U : set V} {x : V} (HxU : x ∈ U) - (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : V, v ∉ U ∧ dist x v < ε) : ¬ Open U := +theorem not_open_of_ex_boundary_pt {U : set M} {x : M} (HxU : x ∈ U) + (Hbd : ∀ ε : ℝ, ε > 0 → ∃ v : M, v ∉ U ∧ dist x v < ε) : ¬ Open U := begin intro HUopen, induction HUopen, @@ -626,12 +234,12 @@ theorem not_open_of_ex_boundary_pt {U : set V} {x : V} (HxU : x ∈ U) {apply not_mem_sUnion_of_boundary_pt a v_0 Hbd HxU} end -theorem ex_Open_ball_subset_of_Open_of_nonempty {U : set V} (HU : Open U) {x : V} (Hx : x ∈ U) : +theorem exists_Open_ball_subset_of_Open_of_mem {U : set M} (HU : Open U) {x : M} (Hx : x ∈ U) : ∃ (r : ℝ), r > 0 ∧ open_ball x r ⊆ U := begin let balloon := {r ∈ univ | r > 0 ∧ open_ball x r ⊆ U}, cases em (balloon = ∅), - have H : ∀ r : ℝ, r > 0 → ∃ v : V, v ∉ U ∧ dist x v < r, begin + have H : ∀ r : ℝ, r > 0 → ∃ v : M, v ∉ U ∧ dist x v < r, begin intro r Hr, note Hor := not_or_not_of_not_and (forall_not_of_sep_empty a (mem_univ r)), note Hor' := or.neg_resolve_left Hor Hr, @@ -641,7 +249,8 @@ theorem ex_Open_ball_subset_of_Open_of_nonempty {U : set V} (HU : Open U) {x : V intro y Hy, cases not_or_not_of_not_and (Hall y) with Hmem Hge, apply not_not_elim Hmem, - apply absurd (and.right Hy) Hge + rewrite dist_comm at Hge, + apply absurd Hy Hge end, apply absurd HU, apply not_open_of_ex_boundary_pt Hx H, @@ -653,7 +262,392 @@ theorem ex_Open_ball_subset_of_Open_of_nonempty {U : set V} (HU : Open U) {x : V repeat assumption end -end topology + +/- limits in metric spaces -/ + +proposition eventually_nhds_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M} + (H : ∀ x', dist x' x < ε → P x') : + eventually P (nhds x) := +topology.eventually_nhds_intro (open_ball_open x ε) (mem_open_ball x εpos) H + +proposition eventually_nhds_dest {P : M → Prop} {x : M} (H : eventually P (nhds x)) : + ∃ ε, ε > 0 ∧ ∀ x', dist x' x < ε → P x' := +obtain s [(Os : Open s) [(xs : x ∈ s) (Hs : ∀₀ x' ∈ s, P x')]], + from topology.eventually_nhds_dest H, +obtain ε [(εpos : ε > 0) (Hε : open_ball x ε ⊆ s)], + from exists_Open_ball_subset_of_Open_of_mem Os xs, +exists.intro ε (and.intro εpos + (take x', suppose dist x' x < ε, + have x' ∈ s, from Hε this, + show P x', from Hs this)) + +proposition eventually_nhds_iff (P : M → Prop) (x : M) : + eventually P (nhds x) ↔ (∃ ε, ε > 0 ∧ ∀ x', dist x' x < ε → P x') := +iff.intro eventually_nhds_dest + (assume H, obtain ε [εpos Hε], from H, eventually_nhds_intro εpos Hε) + +proposition eventually_dist_lt_nhds (x : M) {ε : ℝ} (εpos : ε > 0) : + eventually (λ x', dist x' x < ε) (nhds x) := +eventually_nhds_intro εpos (λ x' H, H) + +proposition eventually_at_within_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M} {s : set M} + (H : ∀₀ x' ∈ s, dist x' x < ε → x' ≠ x → P x') : + eventually P [at x within s] := +topology.eventually_at_within_intro (open_ball_open x ε) (mem_open_ball x εpos) + (λ x' x'mem x'ne x's, H x's x'mem x'ne) + +proposition eventually_at_within_dest {P : M → Prop} {x : M} {s : set M} + (H : eventually P [at x within s]) : + ∃ ε, ε > 0 ∧ ∀₀ x' ∈ s, dist x' x < ε → x' ≠ x → P x' := +obtain t [(Ot : Open t) [(xt : x ∈ t) (Ht : ∀₀ x' ∈ t, x' ≠ x → x' ∈ s → P x')]], + from topology.eventually_at_within_dest H, +obtain ε [(εpos : ε > 0) (Hε : open_ball x ε ⊆ t)], + from exists_Open_ball_subset_of_Open_of_mem Ot xt, +exists.intro ε (and.intro εpos + (take x', assume x's distx'x x'nex, + have x' ∈ t, from Hε distx'x, + show P x', from Ht this x'nex x's)) + +proposition eventually_at_within_iff (P : M → Prop) (x : M) (s : set M) : + eventually P [at x within s] ↔ ∃ ε, ε > 0 ∧ ∀₀ x' ∈ s, dist x' x < ε → x' ≠ x → P x' := +iff.intro eventually_at_within_dest + (λ H, obtain ε [εpos Hε], from H, eventually_at_within_intro εpos Hε) + +proposition eventually_at_intro {P : M → Prop} {ε : ℝ} (εpos : ε > 0) {x : M} + (H : ∀ x', dist x' x < ε → x' ≠ x → P x') : + eventually P [at x] := +topology.eventually_at_intro (open_ball_open x ε) (mem_open_ball x εpos) + (λ x' x'mem x'ne, H x' x'mem x'ne) + +proposition eventually_at_dest {P : M → Prop} {x : M} (H : eventually P [at x]) : + ∃ ε, ε > 0 ∧ ∀ ⦃x'⦄, dist x' x < ε → x' ≠ x → P x' := +obtain ε [εpos Hε], from eventually_at_within_dest H, +exists.intro ε (and.intro εpos (λ x', Hε x' (mem_univ x'))) + +proposition eventually_at_iff (P : M → Prop) (x : M) : + eventually P [at x] ↔ ∃ ε, ε > 0 ∧ ∀ ⦃x'⦄, dist x' x < ε → x' ≠ x → P x' := +iff.intro eventually_at_dest (λ H, obtain ε [εpos Hε], from H, eventually_at_intro εpos Hε) + +section approaches + variables {X : Type} {F : filter X} {f : X → M} {y : M} + + proposition approaches_intro (H : ∀ ε, ε > 0 → eventually (λ x, dist (f x) y < ε) F) : + (f ⟶ y) F := + tendsto_intro + (take P, assume eventuallyP, + obtain ε [(εpos : ε > 0) (Hε : ∀ x', dist x' y < ε → P x')], + from eventually_nhds_dest eventuallyP, + show eventually (λ x, P (f x)) F, + from eventually_mono (H ε εpos) (λ x Hx, Hε (f x) Hx)) + + proposition approaches_dest (H : (f ⟶ y) F) {ε : ℝ} (εpos : ε > 0) : + eventually (λ x, dist (f x) y < ε) F := + tendsto_dest H (eventually_dist_lt_nhds y εpos) + + variables (F f y) + + proposition approaches_iff : (f ⟶ y) F ↔ (∀ ε, ε > 0 → eventually (λ x, dist (f x) y < ε) F) := + iff.intro approaches_dest approaches_intro + + -- TODO: prove this in greater generality in topology.limit + proposition approaches_constant : ((λ x, y) ⟶ y) F := + approaches_intro (λ ε εpos, eventually_of_forall F (λ x, + show dist y y < ε, by rewrite dist_self; apply εpos)) +end approaches + +-- here we full unwrap two particular kinds of convergence3 + +proposition approaches_at_infty_intro {f : ℕ → M} {y : M} + (H : ∀ ε, ε > 0 → ∃ N, ∀ n, n ≥ N → dist (f n) y < ε) : + f ⟶ y [at ∞] := +approaches_intro (λ ε εpos, obtain N HN, from H ε εpos, + eventually_at_infty_intro HN) + +proposition approaches_at_infty_dest {f : ℕ → M} {y : M} + (H : f ⟶ y [at ∞]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ N, ∀ ⦃n⦄, n ≥ N → dist (f n) y < ε := +have eventually (λ x, dist (f x) y < ε) [at ∞], from approaches_dest H εpos, +eventually_at_infty_dest this + +proposition approaches_at_infty_iff (f : ℕ → M) (y : M) : + f ⟶ y [at ∞] ↔ (∀ ε, ε > 0 → ∃ N, ∀ ⦃n⦄, n ≥ N → dist (f n) y < ε) := +iff.intro approaches_at_infty_dest approaches_at_infty_intro + +section metric_space_N +variables {N : Type} [metric_space N] + +proposition approaches_at_dest {f : M → N} {y : N} {x : M} + (H : f ⟶ y [at x]) ⦃ε : ℝ⦄ (εpos : ε > 0) : + ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → x' ≠ x → dist (f x') y < ε := +have eventually (λ x, dist (f x) y < ε) [at x], + from approaches_dest H εpos, +eventually_at_dest this + +proposition approaches_at_intro {f : M → N} {y : N} {x : M} + (H : ∀ ε, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → x' ≠ x → dist (f x') y < ε) : + f ⟶ y [at x] := +approaches_intro (λ ε εpos, + obtain δ [δpos Hδ], from H ε εpos, + eventually_at_intro δpos Hδ) + +proposition approaches_at_iff (f : M → N) (y : N) (x : M) : f ⟶ y [at x] ↔ + (∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → x' ≠ x → dist (f x') y < ε) := +iff.intro approaches_at_dest approaches_at_intro + +end metric_space_N + +-- TODO: remove this. It is only here temporarily, because it is used in normed_space +abbreviation converges_seq [class] (X : ℕ → M) : Prop := ∃ y, X ⟶ y [at ∞] + +-- TODO: refactor +-- the same, with ≤ in place of <; easier to prove, harder to use +definition approaches_at_infty_intro' {X : ℕ → M} {y : M} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → dist (X n) y ≤ ε) : + (X ⟶ y) [at ∞] := +approaches_at_infty_intro +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) + +-- TODO: prove more generally +proposition approaches_at_infty_unique {X : ℕ → M} {y₁ y₂ : M} + (H₁ : X ⟶ y₁ [at ∞]) (H₂ : X ⟶ y₂ [at ∞]) : 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 approaches_at_infty_dest H₁ e2pos, + obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → dist (X n) y₂ < ε / 2), + from approaches_at_infty_dest 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) + +/- TODO: revise + +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 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_offset_left {X : ℕ → M} {y : M} (k : ℕ) (H : X ⟶ y in ℕ) : + (λ n, X (k + n)) ⟶ y in ℕ := +have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), +by rewrite aux; exact converges_to_seq_offset k H + +proposition converges_to_seq_of_converges_to_seq_offset_left + {X : ℕ → M} {y : M} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) : + X ⟶ y in ℕ := +have aux : (λ n, X (k + n)) = (λ n, X (n + k)), from funext (take n, by rewrite add.comm), +by rewrite aux at H; exact converges_to_seq_of_converges_to_seq_offset H +-/ + +proposition bounded_of_converges_seq {X : ℕ → M} {x : M} (H : X ⟶ x [at ∞]) : + ∃ K : ℝ, ∀ n : ℕ, dist (X n) x ≤ K := + have eventually (λ n, dist (X n) x < 1) [at ∞], + from approaches_dest H zero_lt_one, + obtain N (HN : ∀ n, n ≥ N → dist (X n) x < 1), + from eventually_at_infty_dest this, + let K := max 1 (Max i ∈ '(-∞, N), dist (X i) x) in + exists.intro K + (take n, + if Hn : n < N then + show dist (X n) x ≤ K, + from le.trans (le_Max _ Hn) !le_max_right + else + show dist (X n) x ≤ K, + from le.trans (le_of_lt (HN n (le_of_not_gt Hn))) !le_max_left) + +/- cauchy sequences -/ + +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 : ∃ y, X ⟶ y [at ∞]) : cauchy X := +take ε, suppose ε > 0, + obtain y (Hy : X ⟶ y [at ∞]), from H, + have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, + have eventually (λ n, dist (X n) y < ε / 2) [at ∞], from approaches_dest Hy e2pos, + obtain N (HN : ∀ {n}, n ≥ N → dist (X n) y < ε / 2), from eventually_at_infty_dest this, + exists.intro N + (take m n, suppose m ≥ N, suppose 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 + +/- convergence of a function at a point -/ + +section metric_space_M_N +variables {M N : Type} [metric_space M] [metric_space N] + +/- +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 + +-/ + +-- TODO: refactor +section +open pnat rat +private lemma 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 + +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 pnat.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 + +-- a nice illustration of the limit library: [at c] and [at ∞] can be replaced by any filters +theorem comp_approaches_at_infty {f : M → N} {c : M} {l : N} (Hf : f ⟶ l [at c]) + {X : ℕ → M} (HX₁ : X ⟶ c [at ∞]) (HX₂ : eventually (λ n, X n ≠ c) [at ∞]) : + (λ n, f (X n)) ⟶ l [at ∞] := + tendsto_comp_of_approaches_of_tendsto_at HX₁ HX₂ Hf + +-- TODO: refactor + +theorem converges_to_at_of_all_conv_seqs {f : M → N} (c : M) (l : N) + (Hseq : ∀ X : ℕ → M, ((∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞])) → ((λ n : ℕ, f (X n)) ⟶ l [at ∞]))) + : f ⟶ l [at c] := + by_contradiction + (assume Hnot : ¬ (f ⟶ l [at c]), + obtain ε Hε, from exists_not_of_not_forall (λ H, Hnot (approaches_at_intro H)), + let Hε' := and_not_of_not_implies Hε in + obtain (H1 : ε > 0) H2, from Hε', + have H3 : ∀ δ : ℝ, (δ > 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, dist x' c < δ → 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 := and_not_of_not_implies Hx', +-- rewrite and.assoc at H6, + cases H6 with H6a H6b, + split, + cases (and_not_of_not_implies H6b), + assumption, + split, + assumption, + apply le_of_not_gt, + cases (and_not_of_not_implies H6b), + 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 : ∀ 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 : ∀ n : ℕ, ((X n) ≠ c) ∧ (X ⟶ c [at ∞]), 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 approaches_at_infty_intro, + 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 : (λ n : ℕ, f (X n)) ⟶ l [at ∞], from Hseq X H4, + begin + note H6 := approaches_at_infty_dest 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) + +end metric_space_M_N section continuity variables {M N : Type} [Hm : metric_space M] [Hn : metric_space N] @@ -668,7 +662,7 @@ theorem continuous_at_intro {f : M → N} {x : M} begin rewrite ↑continuous_at, intros U Uopen HfU, - cases ex_Open_ball_subset_of_Open_of_nonempty Uopen HfU with r Hr, + cases exists_Open_ball_subset_of_Open_of_mem Uopen HfU with r Hr, cases Hr with Hr HUr, cases H Hr with δ Hδ, cases Hδ with Hδ Hx'δ, @@ -681,11 +675,7 @@ theorem continuous_at_intro {f : M → N} {x : M} intro y Hy, apply mem_preimage, apply HUr, - cases Hy with y' Hy', - rewrite dist_comm at Hy', - note Hy'' := Hx'δ Hy', - apply and.intro !mem_univ, - rewrite dist_comm, + note Hy'' := Hx'δ Hy, exact Hy'' end @@ -697,59 +687,51 @@ theorem continuous_at_elim {f : M → N} {x : M} (Hfx : continuous_at f x) : cases @Hfx (open_ball (f x) ε) !open_ball_open (mem_open_ball _ Hε) with V HV, cases HV with HV HVx, cases HVx with HVx HVf, - cases ex_Open_ball_subset_of_Open_of_nonempty HV HVx with δ Hδ, + cases exists_Open_ball_subset_of_Open_of_mem HV HVx with δ Hδ, cases Hδ with Hδ Hδx, existsi δ, split, exact Hδ, intro x' Hx', - rewrite dist_comm, - apply and.right, apply HVf, apply Hδx, - apply and.intro !mem_univ, - rewrite dist_comm, apply Hx', end -theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) : +theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x [at x]) : continuous_at f x := continuous_at_intro (take ε, suppose ε > 0, -obtain δ Hδ, from Hf this, +obtain δ Hδ, from approaches_at_dest Hf this, exists.intro δ (and.intro (and.left Hδ) (take x', suppose dist x' x < δ, if Heq : x' = x then by rewrite [-Heq, dist_self]; assumption else - (suffices dist x' x < δ, from and.right Hδ x' (and.intro Heq this), + (suffices dist x' x < δ, from and.right Hδ x' this Heq, this)))) theorem converges_to_at_of_continuous_at {f : M → N} {x : M} (Hf : continuous_at f x) : - f ⟶ f x at x := -take ε, suppose ε > 0, -obtain δ Hδ, from continuous_at_elim Hf this, -exists.intro δ (and.intro - (and.left Hδ) - (take x', - assume H : x' ≠ x ∧ dist x' x < δ, - show dist (f x') (f x) < ε, from and.right Hδ x' (and.right H))) - + f ⟶ f x [at x] := +approaches_at_intro + (take ε, suppose ε > 0, + obtain δ [δpos Hδ], from continuous_at_elim Hf this, + exists.intro δ (and.intro δpos (λ x' Hx' xnex', Hδ x' Hx'))) definition continuous (f : M → N) : Prop := ∀ x, continuous_at f x -theorem converges_seq_comp_of_converges_seq_of_cts [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N} +theorem converges_seq_comp_of_converges_seq_of_cts (X : ℕ → M) [HX : converges_seq X] {f : M → N} (Hf : continuous f) : converges_seq (λ n, f (X n)) := begin cases HX with xlim Hxlim, existsi f xlim, - rewrite ↑converges_to_seq at *, + apply approaches_at_infty_intro, intros ε Hε, let Hcont := (continuous_at_elim (Hf xlim)) Hε, cases Hcont with δ Hδ, - cases Hxlim (and.left Hδ) with B HB, + cases approaches_at_infty_dest Hxlim (and.left Hδ) with B HB, existsi B, intro n Hn, apply and.right Hδ, @@ -773,6 +755,7 @@ end continuity end analysis + /- complete metric spaces -/ structure complete_metric_space [class] (M : Type) extends metricM : metric_space M : Type := @@ -786,6 +769,7 @@ complete_metric_space.complete X H end analysis + /- the reals form a metric space -/ noncomputable definition metric_space_real [instance] : metric_space ℝ := diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index 6329f0b6f..3e555f2fd 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -6,7 +6,7 @@ Author: Jeremy Avigad Normed spaces. -/ import algebra.module .metric_space -open real nat classical +open real nat classical topology analysis noncomputable theory structure has_norm [class] (M : Type) : Type := @@ -116,8 +116,9 @@ section open nat - proposition converges_to_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x in ℕ) : - ∀ {ε : ℝ}, ε > 0 → ∃ N₁ : ℕ, ∀ {n : ℕ}, n ≥ N₁ → ∥ X n - x ∥ < ε := H + proposition converges_to_seq_norm_elim {X : ℕ → V} {x : V} (H : X ⟶ x [at ∞]) : + ∀ {ε : ℝ}, ε > 0 → ∃ N₁ : ℕ, ∀ {n : ℕ}, n ≥ N₁ → ∥ X n - x ∥ < ε := + approaches_at_infty_dest H proposition dist_eq_norm_sub (u v : V) : dist u v = ∥ u - v ∥ := rfl @@ -145,8 +146,9 @@ variable [normed_vector_space V] variables {X Y : ℕ → V} variables {x y : V} -proposition add_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : - (λ n, X n + Y n) ⟶ x + y in ℕ := +proposition add_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) : + (λ n, X n + Y n) ⟶ x + y [at ∞] := +approaches_at_infty_intro take ε : ℝ, suppose ε > 0, have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, obtain (N₁ : ℕ) (HN₁ : ∀ {n}, n ≥ N₁ → ∥ X n - x ∥ < ε / 2), @@ -167,8 +169,9 @@ exists.intro N ... < ε / 2 + ε / 2 : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂) ... = ε : add_halves) -private lemma smul_converges_to_seq_aux {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x in ℕ) : - (λ n, c • X n) ⟶ c • x in ℕ := +private lemma smul_converges_to_seq_aux {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x [at ∞]) : + (λ n, c • X n) ⟶ c • x [at ∞] := +approaches_at_infty_intro take ε : ℝ, suppose ε > 0, have abscpos : abs c > 0, from abs_pos_of_ne_zero cnz, have epos : ε / abs c > 0, from div_pos_of_pos_of_pos `ε > 0` abscpos, @@ -183,16 +186,17 @@ exists.intro N ... < abs c * (ε / abs c) : mul_lt_mul_of_pos_left H abscpos ... = ε : mul_div_cancel' (ne_of_gt abscpos)) -proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : - (λ n, c • X n) ⟶ c • x in ℕ := +proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : + (λ n, c • X n) ⟶ c • x [at ∞] := by_cases (assume cz : c = 0, have (λ n, c • X n) = (λ n, 0), from funext (take x, by rewrite [cz, zero_smul]), - begin rewrite [this, cz, zero_smul], apply converges_to_seq_constant end) + begin rewrite [this, cz, zero_smul], apply approaches_constant end) (suppose c ≠ 0, smul_converges_to_seq_aux this HX) -proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) : - (λ n, - X n) ⟶ - x in ℕ := +proposition neg_converges_to_seq (HX : X ⟶ x [at ∞]) : + (λ n, - X n) ⟶ - x [at ∞] := +approaches_at_infty_intro take ε, suppose ε > 0, obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε), from converges_to_seq_norm_elim HX this, exists.intro N @@ -201,16 +205,17 @@ exists.intro N show norm (- X n - (- x)) < ε, by rewrite [-neg_neg_sub_neg, *neg_neg, norm_neg]; exact HN `n ≥ N`) -proposition neg_converges_to_seq_iff : ((λ n, - X n) ⟶ - x in ℕ) ↔ (X ⟶ x in ℕ) := +proposition neg_converges_to_seq_iff : ((λ n, - X n) ⟶ - x [at ∞]) ↔ (X ⟶ x [at ∞]) := have aux : X = λ n, (- (- X n)), from funext (take n, by rewrite neg_neg), iff.intro - (assume H : (λ n, -X n)⟶ -x in ℕ, - show X ⟶ x in ℕ, by rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H) + (assume H : (λ n, -X n)⟶ -x [at ∞], + show X ⟶ x [at ∞], by rewrite [aux, -neg_neg x]; exact neg_converges_to_seq H) neg_converges_to_seq -proposition norm_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, norm (X n)) ⟶ 0 in ℕ := +proposition norm_converges_to_seq_zero (HX : X ⟶ 0 [at ∞]) : (λ n, norm (X n)) ⟶ 0 [at ∞] := +approaches_at_infty_intro take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from HX `ε > 0`, +obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from approaches_at_infty_dest HX `ε > 0`, exists.intro N (take n, assume Hn : n ≥ N, have norm (X n) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end, @@ -218,10 +223,11 @@ exists.intro N by rewrite [sub_zero, abs_of_nonneg !norm_nonneg]; apply this) proposition converges_to_seq_zero_of_norm_converges_to_seq_zero - (HX : (λ n, norm (X n)) ⟶ 0 in ℕ) : - X ⟶ 0 in ℕ := + (HX : (λ n, norm (X n)) ⟶ 0 [at ∞]) : + X ⟶ 0 [at ∞] := +approaches_at_infty_intro take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from HX `ε > 0`, +obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from approaches_at_infty_dest HX `ε > 0`, exists.intro (N : ℕ) (take n : ℕ, assume Hn : n ≥ N, have HN' : abs (norm (X n) - 0) < ε, from HN n Hn, @@ -231,7 +237,7 @@ exists.intro (N : ℕ) by rewrite sub_zero; apply this) proposition norm_converges_to_seq_zero_iff (X : ℕ → V) : - ((λ n, norm (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) := + ((λ n, norm (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) := iff.intro converges_to_seq_zero_of_norm_converges_to_seq_zero norm_converges_to_seq_zero end analysis diff --git a/library/theories/analysis/real_limit.lean b/library/theories/analysis/real_limit.lean index 011518a08..abb0061bf 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -6,7 +6,7 @@ Authors: Jeremy Avigad, Robert Y. Lewis Instantiates the reals as a Banach space. -/ import .metric_space data.real.complete data.set .normed_space -open real classical analysis nat +open real classical analysis nat topology noncomputable theory /- sup and inf -/ @@ -152,15 +152,15 @@ theorem dist_eq_abs (x y : real) : dist x y = abs (x - y) := rfl proposition converges_to_seq_real_intro {X : ℕ → ℝ} {y : ℝ} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε) : - (X ⟶ y in ℕ) := H + (X ⟶ y [at ∞]) := approaches_at_infty_intro H -proposition converges_to_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y in ℕ) : - ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := H +proposition converges_to_seq_real_elim {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y [at ∞]) : + ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) < ε := approaches_at_infty_dest H proposition converges_to_seq_real_intro' {X : ℕ → ℝ} {y : ℝ} (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) : - converges_to_seq X y := -converges_to_seq.intro H + (X ⟶ y [at ∞]) := +approaches_at_infty_intro' H open pnat subtype local postfix ⁻¹ := pnat.inv @@ -205,7 +205,8 @@ theorem converges_seq_of_cauchy {X : ℕ → ℝ} (H : cauchy X) : converges_seq 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 ε : ℝ, + (approaches_at_infty_intro + take ε : ℝ, suppose ε > 0, obtain (k' : ℕ) (Hn : 1 / succ k' < ε), from archimedean_small `ε > 0`, let k : ℕ+ := tag (succ k') !succ_pos, @@ -254,22 +255,23 @@ section limit_operations variables {X Y : ℕ → ℝ} variables {x y : ℝ} -proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : - (λ n, c * X n) ⟶ c * x in ℕ := +proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : + (λ n, c * X n) ⟶ c * x [at ∞] := smul_converges_to_seq c HX -proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : - (λ n, X n * c) ⟶ x * c in ℕ := +proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x [at ∞]) : + (λ n, X n * c) ⟶ x * c [at ∞] := have (λ n, X n * c) = (λ n, c * X n), from funext (take x, !mul.comm), by rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX -theorem converges_to_seq_squeeze (HX : X ⟶ x in ℕ) (HY : Y ⟶ x in ℕ) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n) - (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x in ℕ := +theorem converges_to_seq_squeeze (HX : X ⟶ x [at ∞]) (HY : Y ⟶ x [at ∞]) {Z : ℕ → ℝ} (HZX : ∀ n, X n ≤ Z n) + (HZY : ∀ n, Z n ≤ Y n) : Z ⟶ x [at ∞] := begin + apply approaches_at_infty_intro, intros ε Hε, have Hε4 : ε / 4 > 0, from div_pos_of_pos_of_pos Hε four_pos, - cases HX Hε4 with N1 HN1, - cases HY Hε4 with N2 HN2, + cases approaches_at_infty_dest HX Hε4 with N1 HN1, + cases approaches_at_infty_dest HY Hε4 with N2 HN2, existsi max N1 N2, intro n Hn, have HXY : abs (Y n - X n) < ε / 2, begin @@ -307,11 +309,12 @@ theorem converges_to_seq_squeeze (HX : X ⟶ x in ℕ) (HY : Y ⟶ x in ℕ) {Z exact H end -proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 in ℕ) : - X ⟶ x in ℕ := +proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 [at ∞]) : + X ⟶ x [at ∞] := begin + apply approaches_at_infty_intro, intros ε Hε, - cases Habs Hε with N HN, + cases approaches_at_infty_dest Habs Hε with N HN, existsi N, intro n Hn, have Hn' : abs (abs (X n - x) - 0) < ε, from HN Hn, @@ -319,19 +322,20 @@ proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n exact Hn' end -proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x in ℕ) : - (λ n, abs (X n - x)) ⟶ 0 in ℕ := +proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x [at ∞]) : + (λ n, abs (X n - x)) ⟶ 0 [at ∞] := begin + apply approaches_at_infty_intro, intros ε Hε, - cases HX Hε with N HN, + cases approaches_at_infty_dest HX Hε with N HN, existsi N, intro n Hn, have Hn' : abs (abs (X n - x) - 0) < ε, by rewrite [sub_zero, abs_abs]; apply HN Hn, exact Hn' end -proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : - (λ n, X n * Y n) ⟶ x * y in ℕ := +proposition mul_converges_to_seq (HX : X ⟶ x [at ∞]) (HY : Y ⟶ y [at ∞]) : + (λ n, X n * Y n) ⟶ x * y [at ∞] := have Hbd : ∃ K : ℝ, ∀ n : ℕ, abs (X n) ≤ K, begin cases bounded_of_converges_seq HX with K HK, existsi K + abs x, @@ -358,12 +362,12 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : rewrite [-mul_sub_right_distrib, abs_mul, mul.comm], apply le.refl end, - have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 in ℕ, begin + have Hdifflim : (λ n, abs (X n * Y n - x * y)) ⟶ 0 [at ∞], begin apply converges_to_seq_squeeze, rotate 2, intro, apply abs_nonneg, apply Habsle, - apply converges_to_seq_constant, + apply approaches_constant, rewrite -{0}zero_add, apply add_converges_to_seq, krewrite -(mul_zero K), @@ -380,15 +384,15 @@ proposition mul_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : -- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc. -proposition abs_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, abs (X n)) ⟶ 0 in ℕ := +proposition abs_converges_to_seq_zero (HX : X ⟶ 0 [at ∞]) : (λ n, abs (X n)) ⟶ 0 [at ∞] := norm_converges_to_seq_zero HX -proposition converges_to_seq_zero_of_abs_converges_to_seq_zero (HX : (λ n, abs (X n)) ⟶ 0 in ℕ) : - X ⟶ 0 in ℕ := +proposition converges_to_seq_zero_of_abs_converges_to_seq_zero (HX : (λ n, abs (X n)) ⟶ 0 [at ∞]) : + X ⟶ 0 [at ∞] := converges_to_seq_zero_of_norm_converges_to_seq_zero HX proposition abs_converges_to_seq_zero_iff (X : ℕ → ℝ) : - ((λ n, abs (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) := + ((λ n, abs (X n)) ⟶ 0 [at ∞]) ↔ (X ⟶ 0 [at ∞]) := iff.intro converges_to_seq_zero_of_abs_converges_to_seq_zero abs_converges_to_seq_zero -- TODO: products of two sequences, converges_seq, limit_seq @@ -401,15 +405,17 @@ section limit_operations_continuous variables {f g : ℝ → ℝ} variables {a b x y : ℝ} -theorem mul_converges_to_at (Hf : f ⟶ a at x) (Hg : g ⟶ b at x) : (λ z, f z * g z) ⟶ a * b at x := +theorem mul_converges_to_at (Hf : f ⟶ a [at x]) (Hg : g ⟶ b [at x]) : (λ z, f z * g z) ⟶ a * b [at x] := begin apply converges_to_at_of_all_conv_seqs, intro X HX, apply mul_converges_to_seq, - note Hfc := all_conv_seqs_of_converges_to_at Hf, - apply Hfc _ HX, - note Hgb := all_conv_seqs_of_converges_to_at Hg, - apply Hgb _ HX + apply comp_approaches_at_infty Hf, + apply and.right (HX 0), + apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n))), + apply comp_approaches_at_infty Hg, + apply and.right (HX 0), + apply (set.filter.eventually_of_forall _ (λ n, and.left (HX n))) end end limit_operations_continuous @@ -421,8 +427,9 @@ open real set variable {X : ℕ → ℝ} proposition converges_to_seq_sup_of_nondecreasing (nondecX : nondecreasing X) {b : ℝ} - (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) in ℕ := -let sX := sup (X ' univ) in + (Hb : ∀ i, X i ≤ b) : X ⟶ sup (X ' univ) [at ∞] := +approaches_at_infty_intro +(let sX := sup (X ' univ) in have Xle : ∀ i, X i ≤ sX, from take i, have ∀ x, x ∈ X ' univ → x ≤ b, from @@ -446,10 +453,10 @@ exists.intro i have sX - ε < X j, from lt_of_lt_of_le (by rewrite Hi; apply H₂x') (nondecX Hj), have sX < X j + ε, from lt_add_of_sub_lt_right this, have sX - X j < ε, from sub_lt_left_of_lt_add this, - show (abs (X j - sX)) < ε, by rewrite eq₁; exact this) + show (abs (X j - sX)) < ε, by rewrite eq₁; exact this)) proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ} - (Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) in ℕ := + (Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) [at ∞] := have H₁ : ∃ x, x ∈ X ' univ, from exists.intro (X 0) (mem_image_of_mem X !mem_univ), have H₂ : ∀ x, x ∈ X ' univ → b ≤ x, from (take x, assume H, @@ -460,8 +467,9 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_comp, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), begin + apply iff.mp !neg_converges_to_seq_iff, -- need krewrite here - krewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], + krewrite [-sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], apply converges_to_seq_sup_of_nondecreasing nonincX H₄ end @@ -473,8 +481,8 @@ section xn open nat set theorem pow_converges_to_seq_zero {x : ℝ} (H : abs x < 1) : - (λ n, x^n) ⟶ 0 in ℕ := -suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from + (λ n, x^n) ⟶ 0 [at ∞] := +suffices H' : (λ n, (abs x)^n) ⟶ 0 [at ∞], from have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, eq.symm !abs_pow), by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H', let aX := (λ n, (abs x)^n), @@ -488,12 +496,12 @@ have noninc_aX : nonincreasing aX, from have (abs x) * (abs x)^i ≤ (abs x)^i, by krewrite one_mul at this; exact this, show (abs x) ^ (succ i) ≤ (abs x)^i, by rewrite pow_succ; apply this), have bdd_aX : ∀ i, 0 ≤ aX i, from take i, !pow_nonneg_of_nonneg !abs_nonneg, -have aXconv : aX ⟶ iaX in ℕ, proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed, -have asXconv : asX ⟶ iaX in ℕ, from converges_to_seq_offset_succ aXconv, -have asXconv' : asX ⟶ (abs x) * iaX in ℕ, from mul_left_converges_to_seq (abs x) aXconv, -have iaX = (abs x) * iaX, from converges_to_seq_unique asXconv asXconv', +have aXconv : aX ⟶ iaX [at ∞], proof converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX qed, +have asXconv : asX ⟶ iaX [at ∞], from tendsto_succ_at_infty aXconv, +have asXconv' : asX ⟶ (abs x) * iaX [at ∞], from mul_left_converges_to_seq (abs x) aXconv, +have iaX = (abs x) * iaX, from sorry, -- converges_to_seq_unique asXconv asXconv', have iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this), -show aX ⟶ 0 in ℕ, begin rewrite -this, exact aXconv end --from this ▸ aXconv +show aX ⟶ 0 [at ∞], begin rewrite -this, exact aXconv end --from this ▸ aXconv end xn diff --git a/library/theories/topology/limit.lean b/library/theories/topology/limit.lean index 13b490eb2..690d23f1e 100644 --- a/library/theories/topology/limit.lean +++ b/library/theories/topology/limit.lean @@ -52,17 +52,17 @@ In terms of sets, this is equivalent to ∀ s : set Y, s ∈ sets F₂ → f '- s ∈ sets F₁ so one option is to use "tendsto_intro" "tendsto_dest" and "tendsto_iff" to unpack meanings -in terms of "eventually", and then use the intro and elim rules of "eventually". For specific +in terms of "eventually", and then use the intro and dest rules of "eventually". For specific topologies -- for example, those given by a metric space or norm -- see the specialized -intro and elim rules for eventually in those files. +intro and dest rules for eventually in those files. -For "approaches", "approaches_infty", and "approaches_ninfty", there are specific intro, elim, +For "approaches", "approaches_infty", and "approaches_ninfty", there are specific intro, dest, and iff rules. Again, see also specific versions for metric spaces, normed spaces, etc. Note that the filters at_infty and at_ninfty don't rely on topological notions at all, only the existence of a suitable order. -We mark tendsto as irreducible after defining the intro and elim rules, because otherwise +We mark tendsto as irreducible after defining the intro and dest rules, because otherwise tactics seem to unfold too much. -/ import data.set data.nat algebra.interval .basic @@ -245,6 +245,21 @@ theorem tendsto_comp_iff_tendsto_mapfilter (f : X → Y) (g : Y → Z) (F₁ : f tendsto (g ∘ f) F₂ F₁ ↔ tendsto g F₂ (mapfilter f F₁) := !iff.refl +theorem eventually_of_tendsto_principal {f : X → Y} {F : filter X} {s : set Y} + (H : tendsto f (principal s) F) : + eventually (λ x, f x ∈ s) F := +tendsto_dest H (eventually_principal (subset.refl _)) + +theorem tendsto_principal {f : X → Y} {F : filter X} {s : set Y} (H : eventually (λ x, f x ∈ s) F) : + tendsto f (principal s) F := +tendsto_intro (take P, assume ePF, + have ∀₀ x ∈ s, P x, from subset_of_eventually_principal ePF, + eventually_mono H (λ x Hfx, this Hfx)) + +theorem tendsto_principal_iff (f : X → Y) (F : filter X) (s : set Y) : + tendsto f (principal s) F ↔ eventually (λ x, f x ∈ s) F := +iff.intro eventually_of_tendsto_principal tendsto_principal + attribute tendsto [irreducible] @@ -471,7 +486,7 @@ section nhds_filter eventually (λ x, x ∈ s) (nhds x) := eventually_nhds_intro Os xs (λ x Hx, Hx) - proposition eventually_nhds_elim {x : X} (H : eventually P (nhds x)) : + proposition eventually_nhds_dest {x : X} (H : eventually P (nhds x)) : ∃ s, Open s ∧ x ∈ s ∧ ∀₀ x ∈ s, P x := let princS := principal ' {s | Open s ∧ x ∈ s} in have principal univ ∈ princS, @@ -494,7 +509,7 @@ section nhds_filter proposition eventually_nhds_iff (x : X) : eventually P (nhds x) ↔ ∃ s, Open s ∧ x ∈ s ∧ ∀₀ x ∈ s, P x := - iff.intro eventually_nhds_elim + iff.intro eventually_nhds_dest (assume H, obtain s [Os [xs Hs]], from H, eventually_nhds_intro Os xs Hs) end nhds_filter @@ -533,7 +548,7 @@ section at_within (H : eventually P [at x within t]) : ∃ s, Open s ∧ x ∈ s ∧ ∀₀ y ∈ s, y ≠ x → y ∈ t → P y := obtain P₁ [eP₁nhds [P₂ [eP₂princ (H' : P ⊇ P₁ ∩ P₂)]]], from exists_of_eventually_inf H, - obtain s [Os [xs Hs]], from eventually_nhds_elim eP₁nhds, + obtain s [Os [xs Hs]], from eventually_nhds_dest eP₁nhds, have Ht : ∀₀ y ∈ t \ '{x}, P₂ y, from subset_of_eventually_principal eP₂princ, exists.intro s (and.intro Os (and.intro xs (take y, assume ys ynex yt, @@ -659,7 +674,7 @@ section approaches tendsto_intro (take P, assume eventuallyP, obtain s [Os [(ys : y ∈ s) (H' : ∀₀ y' ∈ s, P y')]], - from eventually_nhds_elim eventuallyP, + from eventually_nhds_dest eventuallyP, show eventually (λ x, P (f x)) F, from eventually_mono (H s Os ys) (λ x Hx, H' Hx)) proposition approaches_elim (H : (f ⟶ y) F) {s : set Y} (Os : Open s) (ys : y ∈ s) : @@ -669,6 +684,25 @@ section approaches variables (F f y) proposition approaches_iff : (f ⟶ y) F ↔ (∀ s, Open s → y ∈ s → eventually (λ x, f x ∈ s) F) := iff.intro approaches_elim approaches_intro + + proposition tendsto_comp_of_approaches_of_tendsto_at_within + {f : X → Y} {g : Y → Z} {s : set Y} {y : Y} {F₁ : filter X} {F₃ : filter Z} + (Hf₁ : (f ⟶ y) F₁) (Hf₂ : eventually (λ x, f x ∈ s ∧ f x ≠ y) F₁) + (Hg : tendsto g F₃ [at y within s]) : + tendsto (g ∘ f) F₃ F₁ := + have eventually (λ x, f x ∈ s \ '{y}) F₁, + from eventually_congr (take x, by rewrite [mem_diff_iff, mem_singleton_iff]) Hf₂, + have tendsto f [at y within s] F₁, from tendsto_inf Hf₁ (tendsto_principal this), + tendsto_comp this Hg + + proposition tendsto_comp_of_approaches_of_tendsto_at + {f : X → Y} {g : Y → Z} {y : Y} {F₁ : filter X} {F₃ : filter Z} + (Hf₁ : (f ⟶ y) F₁) (Hf₂ : eventually (λ x, f x ≠ y) F₁) + (Hg : tendsto g F₃ [at y]) : + tendsto (g ∘ f) F₃ F₁ := + have eventually (λ x, f x ∈ univ ∧ f x ≠ y) F₁, + from eventually_congr (take x, by rewrite [mem_univ_iff, true_and]) Hf₂, + tendsto_comp_of_approaches_of_tendsto_at_within Hf₁ this Hg end approaches /-