From 86fc326e083329abf148473e14cc4248ac7613e2 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 14 Jan 2016 23:57:27 -0500 Subject: [PATCH] refactor/feat(library/theories/analysis/*): reorganize analysis library and add some theorems --- library/algebra/module.lean | 17 +- library/theories/analysis/analysis.md | 3 +- library/theories/analysis/ivt.lean | 237 +++++++ library/theories/analysis/metric_space.lean | 84 ++- library/theories/analysis/normed_space.lean | 192 ++++-- library/theories/analysis/real_limit.lean | 652 +++++--------------- 6 files changed, 603 insertions(+), 582 deletions(-) create mode 100644 library/theories/analysis/ivt.lean diff --git a/library/algebra/module.lean b/library/algebra/module.lean index edb5eedf88..7e14635c6a 100644 --- a/library/algebra/module.lean +++ b/library/algebra/module.lean @@ -18,7 +18,7 @@ structure left_module [class] (R M : Type) [ringR : ring R] extends has_scalar R M, add_comm_group M := (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)) +(mul_smul : ∀ r s x, smul (mul r s) x = smul r (smul s x)) (one_smul : ∀ x, smul one x = x) section left_module @@ -32,11 +32,11 @@ section left_module proposition smul_left_distrib (a : R) (u v : M) : a • (u + v) = a • u + a • v := !left_module.smul_left_distrib - proposition smul_right_distrib (a b : R) (u : M) : (a + b)•u = a•u + b•u := + 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 mul_smul (a : R) (b : R) (u : M) : (a * b) • u = a • (b • u) := + !left_module.mul_smul proposition one_smul (u : M) : (1 : R) • u = u := !left_module.one_smul @@ -53,6 +53,15 @@ section left_module proposition neg_one_smul (u : M) : -(1 : R) • u = -u := by rewrite [neg_smul, one_smul] + + proposition smul_neg (a : R) (u : M) : a • (-u) = -(a • u) := + by rewrite [-neg_one_smul, -mul_smul, mul_neg_one_eq_neg, neg_smul] + + proposition smul_sub_left_distrib (a : R) (u v : M) : a • (u - v) = a • u - a • v := + by rewrite [sub_eq_add_neg, smul_left_distrib, smul_neg] + + proposition sub_smul_right_distrib (a b : R) (v : M) : (a - b) • v = a • v - b • v := + by rewrite [sub_eq_add_neg, smul_right_distrib, neg_smul] end left_module /- linear maps -/ diff --git a/library/theories/analysis/analysis.md b/library/theories/analysis/analysis.md index 5a6d9b6400..c209f43d7d 100644 --- a/library/theories/analysis/analysis.md +++ b/library/theories/analysis/analysis.md @@ -2,5 +2,6 @@ theories.analysis ================= * [metric_space](metric_space.lean) +* [normed_space](normed_space.lean) * [real_limit](real_limit.lean) -* [normed_space](normed_space.lean) \ No newline at end of file +* [ivt](ivt.lean) : the intermediate value theorem diff --git a/library/theories/analysis/ivt.lean b/library/theories/analysis/ivt.lean new file mode 100644 index 0000000000..5f5de7fd7c --- /dev/null +++ b/library/theories/analysis/ivt.lean @@ -0,0 +1,237 @@ +/- +Copyright (c) 2015 Robert Y. Lewis. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Robert Y. Lewis + +The intermediate value theorem. +-/ +import .real_limit +open real analysis set classical +noncomputable theory + +private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0} + +section +parameters {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) (Ha : f a < 0) (Hb : f b > 0) +include Hf Ha Hb Hab + +private theorem Hinh : ∃ x, x ∈ {x | x < b ∧ f x < 0} := exists.intro a (and.intro Hab Ha) + +private theorem Hmem : ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ b := λ x Hx, le_of_lt (and.left Hx) + +private theorem Hsupleb : inter_sup a b f ≤ b := sup_le (Hinh) Hmem + +local notation 2 := of_num 1 + of_num 1 + +private theorem ex_delta_lt {x : ℝ} (Hx : f x < 0) (Hxb : x < b) : ∃ δ : ℝ, δ > 0 ∧ x + δ < b ∧ f (x + δ) < 0 := + begin + let Hcont := neg_on_nbhd_of_cts_of_neg Hf Hx, + cases Hcont with δ Hδ, + {cases em (x + δ < b) with Haδ Haδ, + existsi δ / 2, + split, + {exact div_pos_of_pos_of_pos (and.left Hδ) two_pos}, + split, + {apply lt.trans, + apply add_lt_add_left, + exact div_two_lt_of_pos (and.left Hδ), + exact Haδ}, + {apply and.right Hδ, + krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, + abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)], + exact div_two_lt_of_pos (and.left Hδ)}, + existsi (b - x) / 2, + split, + {apply div_pos_of_pos_of_pos, + exact sub_pos_of_lt Hxb, + exact two_pos}, + split, + {apply add_midpoint Hxb}, + {apply and.right Hδ, + krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, + abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hxb) two_pos)], + apply lt_of_lt_of_le, + apply div_two_lt_of_pos (sub_pos_of_lt Hxb), + apply sub_left_le_of_le_add, + apply le_of_not_gt Haδ}} + end + +private lemma sup_near_b {δ : ℝ} (Hpos : 0 < δ) + (Hgeb : inter_sup a b f + δ / 2 ≥ b) : abs (inter_sup a b f - b) < δ := + begin + apply abs_lt_of_lt_of_neg_lt, + apply sub_lt_left_of_lt_add, + apply lt_of_le_of_lt, + apply Hsupleb, + apply lt_add_of_pos_right Hpos, + rewrite neg_sub, + apply sub_lt_left_of_lt_add, + apply lt_of_le_of_lt, + apply Hgeb, + apply add_lt_add_left, + apply div_two_lt_of_pos Hpos + end + +private lemma delta_of_lt (Hflt : f (inter_sup a b f) < 0) : + ∃ δ : ℝ, δ > 0 ∧ inter_sup a b f + δ < b ∧ f (inter_sup a b f + δ) < 0 := + if Hlt : inter_sup a b f < b then ex_delta_lt Hflt Hlt else + begin + let Heq := eq_of_le_of_ge Hsupleb (le_of_not_gt Hlt), + apply absurd Hflt, + apply not_lt_of_ge, + apply le_of_lt, + rewrite Heq, + exact Hb + end + +private theorem sup_fn_interval_aux1 : f (inter_sup a b f) ≥ 0 := + have ¬ f (inter_sup a b f) < 0, from + (suppose f (inter_sup a b f) < 0, + obtain δ Hδ, from delta_of_lt this, + have inter_sup a b f + δ ∈ {x | x < b ∧ f x < 0}, + from and.intro (and.left (and.right Hδ)) (and.right (and.right Hδ)), + have ¬ inter_sup a b f < inter_sup a b f + δ, + from not_lt_of_ge (le_sup this Hmem), + show false, from this (lt_add_of_pos_right (and.left Hδ))), + le_of_not_gt this + +private theorem sup_fn_interval_aux2 : f (inter_sup a b f) ≤ 0 := + have ¬ f (inter_sup a b f) > 0, from + (assume Hfsup : f (inter_sup a b f) > 0, + obtain δ Hδ, from pos_on_nbhd_of_cts_of_pos Hf Hfsup, + have ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ inter_sup a b f - δ / 2, from + (take x, assume Hxset : x ∈ {x | x < b ∧ f x < 0}, + have ¬ x > inter_sup a b f - δ / 2, from + (assume Hngt, + have Habs : abs (x - inter_sup a b f) < δ, begin + rewrite abs_sub, + apply abs_lt_of_lt_of_neg_lt, + apply sub_lt_of_sub_lt, + apply gt.trans, + exact Hngt, + apply sub_lt_sub_left, + exact div_two_lt_of_pos (and.left Hδ), + rewrite neg_sub, + apply lt_of_le_of_lt, + rotate 1, + apply and.left Hδ, + apply sub_nonpos_of_le, + apply le_sup, + exact Hxset, + exact Hmem + end, + have f x > 0, from and.right Hδ x Habs, + show false, from (not_lt_of_gt this) (and.right Hxset)), + le_of_not_gt this), + have Hle : inter_sup a b f ≤ inter_sup a b f - δ / 2, from sup_le Hinh this, + show false, from not_le_of_gt + (sub_lt_of_pos _ (div_pos_of_pos_of_pos (and.left Hδ) (two_pos))) Hle), + le_of_not_gt this + +private theorem sup_fn_interval : f (inter_sup a b f) = 0 := + eq_of_le_of_ge sup_fn_interval_aux2 sup_fn_interval_aux1 + + +private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ < b ∧ f (a + δ) < 0 := + begin + let Hcont := neg_on_nbhd_of_cts_of_neg Hf Ha, + cases Hcont with δ Hδ, + {cases em (a + δ < b) with Haδ Haδ, + existsi δ / 2, + split, + {exact div_pos_of_pos_of_pos (and.left Hδ) two_pos}, + split, + {apply lt.trans, + apply add_lt_add_left, + exact div_two_lt_of_pos (and.left Hδ), + exact Haδ}, + {apply and.right Hδ, + krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, + abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)], + exact div_two_lt_of_pos (and.left Hδ)}, + existsi (b - a) / 2, + split, + {apply div_pos_of_pos_of_pos, + exact sub_pos_of_lt Hab, + exact two_pos}, + split, + {apply add_midpoint Hab}, + {apply and.right Hδ, + krewrite [abs_sub, sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, + abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hab) two_pos)], + apply lt_of_lt_of_le, + apply div_two_lt_of_pos (sub_pos_of_lt Hab), + apply sub_left_le_of_le_add, + apply le_of_not_gt Haδ}} + end + +theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 := + begin + existsi inter_sup a b f, + split, + {cases intermediate_value_incr_aux2 with δ Hδ, + apply lt_of_lt_of_le, + apply lt_add_of_pos_right, + exact and.left Hδ, + apply le_sup, + exact and.right Hδ, + intro x Hx, + apply le_of_lt, + exact and.left Hx}, + split, + {cases pos_on_nbhd_of_cts_of_pos Hf Hb with δ Hδ, + apply lt_of_le_of_lt, + rotate 1, + apply sub_lt_of_pos, + exact and.left Hδ, + rotate_right 1, + apply sup_le, + exact exists.intro a (and.intro Hab Ha), + intro x Hx, + apply le_of_not_gt, + intro Hxgt, + have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt, + krewrite [-(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt', abs_sub at Hxgt'], + note Hxgt'' := and.right Hδ _ Hxgt', + exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)}, + {exact sup_fn_interval} + end + +end + +theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) + (Ha : f a > 0) (Hb : f b < 0) : ∃ c, a < c ∧ c < b ∧ f c = 0 := + begin + have Ha' : - f a < 0, from neg_neg_of_pos Ha, + have Hb' : - f b > 0, from neg_pos_of_neg Hb, + have Hcon : continuous (λ x, - f x), from continuous_neg_of_continuous Hf, + let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb', + cases Hiv with c Hc, + existsi c, + split, + exact and.left Hc, + split, + exact and.left (and.right Hc), + apply eq_zero_of_neg_eq_zero, + apply and.right (and.right Hc) + end + +theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ} + (Hav : f a < v) (Hbv : f b > v) : ∃ c, a < c ∧ c < b ∧ f c = v := + have Hav' : f a - v < 0, from sub_neg_of_lt Hav, + have Hbv' : f b - v > 0, from sub_pos_of_lt Hbv, + have Hcon : continuous (λ x, f x - v), from continuous_offset_of_continuous Hf _, + have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_incr_zero Hcon Hab Hav' Hbv', + obtain c Hc, from Hiv, + exists.intro c + (and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc))))) + +theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ} + (Hav : f a > v) (Hbv : f b < v) : ∃ c, a < c ∧ c < b ∧ f c = v := + have Hav' : f a - v > 0, from sub_pos_of_lt Hav, + have Hbv' : f b - v < 0, from sub_neg_of_lt Hbv, + have Hcon : continuous (λ x, f x - v), from continuous_offset_of_continuous Hf _, + have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_decr_zero Hcon Hab Hav' Hbv', + obtain c Hc, from Hiv, + exists.intro c + (and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc))))) diff --git a/library/theories/analysis/metric_space.lean b/library/theories/analysis/metric_space.lean index c5e89957b8..b3c3fbee5b 100644 --- a/library/theories/analysis/metric_space.lean +++ b/library/theories/analysis/metric_space.lean @@ -6,24 +6,35 @@ Author: Jeremy Avigad Metric spaces. -/ import data.real.division -open real eq.ops classical +open nat 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) + (dist_triangle : ∀ x y z : M, dist x z ≤ dist x y + dist y z) -namespace metric_space +namespace analysis section metric_space_M -variables {M : Type} [strucM : metric_space M] -include strucM +variables {M : Type} [metric_space M] + +definition dist (x y : M) : ℝ := metric_space.dist x y + +proposition dist_self (x : M) : dist x x = 0 := metric_space.dist_self x + +proposition eq_of_dist_eq_zero {x y : M} (H : dist x y = 0) : x = y := +metric_space.eq_of_dist_eq_zero H + +proposition dist_comm (x y : M) : dist x y = dist y x := metric_space.dist_comm x y 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_triangle (x y z : M) : dist x z ≤ dist x y + dist y z := +metric_space.dist_triangle x y z + 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, @@ -36,8 +47,6 @@ lt_of_le_of_ne !dist_nonneg (suppose 0 = dist x y, H (iff.mp !dist_eq_zero_iff t 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 - /- convergence of a sequence -/ definition converges_to_seq (X : ℕ → M) (y : M) : Prop := @@ -133,7 +142,7 @@ 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 strucM X y 1 H +@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 ℕ) := @@ -180,7 +189,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') y < ε +∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, x' ≠ x ∧ dist x' x < δ → dist (f x') (f x) < ε notation f `⟶` y `at` x := converges_to_at f y x @@ -194,25 +203,38 @@ 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 -definition continuous_at (f : M → N) (x : M) := converges_to_at f (f x) x +/- continuity at a point -/ -definition continuous (f : M → N) := ∀ x, continuous_at f x +definition continuous_at (f : M → N) (x : M) := +∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ ⦃x'⦄, dist x' x < δ → dist (f x') (f x) < ε -theorem continuous_at_spec {f : M → N} {x : M} (Hf : continuous_at f x) : - ∀ ⦃ε⦄, ε > 0 → ∃ δ, δ > 0 ∧ ∀ x', dist x x' < δ → dist (f x') (f x) < ε := +theorem continuous_at_of_converges_to_at {f : M → N} {x : M} (Hf : f ⟶ f x at x) : + continuous_at f x := take ε, suppose ε > 0, obtain δ Hδ, from 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 + (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' (and.intro Heq this), this))) -theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : converges_seq X] {f : M → N} - (Hf : continuous f) : +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 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))) + +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} + (Hf : continuous f) : converges_seq (λ n, f (X n)) := begin cases HX with xlim Hxlim, @@ -228,23 +250,33 @@ theorem image_seq_converges_of_converges [instance] (X : ℕ → M) [HX : conver rewrite [a, dist_self], assumption, apply and.right Hδ, - split, - exact a, - rewrite dist_comm, apply HB Hn end end metric_space_M_N -end metric_space +end analysis /- complete metric spaces -/ -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) +(complete : ∀ X, @analysis.cauchy M metricM X → @analysis.converges_seq M metricM X) + +namespace analysis proposition complete (M : Type) [cmM : complete_metric_space M] {X : ℕ → M} (H : cauchy X) : converges_seq X := complete_metric_space.complete X H + +end analysis + +/- the reals form a metris space -/ + +noncomputable definition metric_space_real [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 := λ x y, eq_of_abs_sub_eq_zero, + dist_comm := abs_sub, + dist_triangle := abs_sub_le +⦄ diff --git a/library/theories/analysis/normed_space.lean b/library/theories/analysis/normed_space.lean index c8612cfa4f..bd114ae5e1 100644 --- a/library/theories/analysis/normed_space.lean +++ b/library/theories/analysis/normed_space.lean @@ -5,17 +5,18 @@ Author: Jeremy Avigad Normed spaces. -/ -import algebra.module .real_limit -open real - +import algebra.module .metric_space +open real nat classical 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 +namespace analysis + definition norm {M : Type} [has_normM : has_norm M] (v : M) : ℝ := has_norm.norm v -notation `∥`v`∥` := norm v + notation `∥`v`∥` := norm v +end analysis -- where is the right place to put this? structure real_vector_space [class] (V : Type) extends vector_space ℝ V @@ -26,9 +27,7 @@ structure normed_vector_space [class] (V : Type) extends real_vector_space V, ha (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 +namespace analysis variable {V : Type} variable [normed_vector_space V] @@ -46,28 +45,33 @@ section normed_vector_space 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] +end analysis - section - private definition nvs_dist (u v : V) := ∥ u - v ∥ +section + open analysis + variable {V : Type} + variable [normed_vector_space V] - private lemma nvs_dist_self (u : V) : nvs_dist u u = 0 := - by rewrite [↑nvs_dist, sub_self, norm_zero] + private definition nvs_dist [reducible] (u v : V) := ∥ u - v ∥ - 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_self (u : V) : nvs_dist u u = 0 := + by rewrite [↑nvs_dist, sub_self, norm_zero] - 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 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_comm (u v : V) : nvs_dist u v = nvs_dist v u := - by rewrite [↑nvs_dist, -norm_neg, neg_sub] - end + 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] - definition normed_vector_space_to_metric_space [reducible] [trans_instance] : metric_space V := + definition normed_vector_space_to_metric_space [reducible] [trans_instance] + (V : Type) [nvsV : normed_vector_space V] : + metric_space V := ⦃ metric_space, dist := nvs_dist, dist_self := nvs_dist_self, @@ -75,42 +79,126 @@ section normed_vector_space dist_comm := nvs_dist_comm, dist_triangle := nvs_dist_triangle ⦄ -end normed_vector_space + + 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 dist_eq_norm_sub (u v : V) : dist u v = ∥ u - v ∥ := rfl + + proposition norm_eq_dist_zero (u : V) : ∥ u ∥ = dist u 0 := + by rewrite [dist_eq_norm_sub, sub_zero] + + proposition norm_nonneg (u : V) : ∥ u ∥ ≥ 0 := + by rewrite norm_eq_dist_zero; apply !dist_nonneg +end 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) +(complete : ∀ X, @analysis.cauchy V (@normed_vector_space_to_metric_space V nvsV) X → + @analysis.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] : +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_metric_space, normed_vector_space_to_metric_space V, complete := banach_space.complete ⦄ -section - open metric_space +namespace analysis +variable {V : Type} +variable [normed_vector_space V] - example (V : Type) (vsV : banach_space V) (X : ℕ → V) (H : cauchy X) : converges_seq X := - complete V H -end +variables {X Y : ℕ → V} +variables {x y : V} -/- the real numbers themselves can be viewed as a banach space -/ +proposition add_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : + (λ n, X n + Y n) ⟶ x + y in ℕ := +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), + from converges_to_seq_norm_elim HX e2pos, +obtain (N₂ : ℕ) (HN₂ : ∀ {n}, n ≥ N₂ → ∥ Y n - y ∥ < ε / 2), + from converges_to_seq_norm_elim HY e2pos, +let N := max N₁ N₂ in +exists.intro N + (take n, + suppose n ≥ N, + have ngtN₁ : n ≥ N₁, from nat.le_trans !le_max_left `n ≥ N`, + have ngtN₂ : n ≥ N₂, from nat.le_trans !le_max_right `n ≥ N`, + show ∥ (X n + Y n) - (x + y) ∥ < ε, from calc + ∥ (X n + Y n) - (x + y) ∥ + = ∥ (X n - x) + (Y n - y) ∥ : by rewrite [sub_add_eq_sub_sub, *sub_eq_add_neg, + *add.assoc, add.left_comm (-x)] + ... ≤ ∥ X n - x ∥ + ∥ Y n - y ∥ : norm_triangle + ... < ε / 2 + ε / 2 : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂) + ... = ε : add_halves) -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 -⦄ +private lemma smul_converges_to_seq_aux {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x in ℕ) : + (λ n, c • X n) ⟶ c • x in ℕ := +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, +obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε / abs c), from converges_to_seq_norm_elim HX epos, +exists.intro N + (take n, + suppose n ≥ N, + have H : norm (X n - x) < ε / abs c, from HN this, + show norm (c • X n - c • x) < ε, from calc + norm (c • X n - c • x) + = abs c * norm (X n - x) : by rewrite [-smul_sub_left_distrib, norm_smul] + ... < abs c * (ε / abs c) : mul_lt_mul_of_pos_left H abscpos + ... = ε : mul_div_cancel' (ne_of_gt abscpos)) -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 -⦄ +proposition smul_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : + (λ n, c • X n) ⟶ c • x in ℕ := +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) + (suppose c ≠ 0, smul_converges_to_seq_aux this HX) + +proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) : + (λ n, - X n) ⟶ - x in ℕ := +take ε, suppose ε > 0, +obtain N (HN : ∀ {n}, n ≥ N → norm (X n - x) < ε), from converges_to_seq_norm_elim HX this, +exists.intro N + (take n, + suppose n ≥ 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 ℕ) := +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) + neg_converges_to_seq + +proposition norm_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, norm (X n)) ⟶ 0 in ℕ := +take ε, suppose ε > 0, +obtain N (HN : ∀ n, n ≥ N → norm (X n - 0) < ε), from 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, + show abs (norm (X n) - 0) < ε, using this, + 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 ℕ := +take ε, suppose ε > 0, +obtain N (HN : ∀ n, n ≥ N → abs (norm (X n) - 0) < ε), from HX `ε > 0`, +exists.intro (N : ℕ) + (take n : ℕ, assume Hn : n ≥ N, + have HN' : abs (norm (X n) - 0) < ε, from HN n Hn, + have norm (X n) < ε, + by+ rewrite [sub_zero at HN', abs_of_nonneg !norm_nonneg at HN']; apply HN', + show norm (X n - 0) < ε, using this, + by rewrite sub_zero; apply this) + +proposition norm_converges_to_seq_zero_iff (X : ℕ → V) : + ((λ n, norm (X n)) ⟶ 0 in ℕ) ↔ (X ⟶ 0 in ℕ) := +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 d4c605a87f..8ea6b3f079 100644 --- a/library/theories/analysis/real_limit.lean +++ b/library/theories/analysis/real_limit.lean @@ -3,178 +3,21 @@ Copyright (c) 2015 Jeremy Avigad. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Jeremy Avigad, Robert Y. Lewis -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. +Instantiates the reals as a Banach space. -/ -import .metric_space data.real.complete data.set -open real classical +import .metric_space data.real.complete data.set .normed_space +open real classical analysis nat noncomputable theory +/- sup and inf -/ + +-- 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. + +-- Issue: real.sup and real.inf conflict with sup and inf in lattice. +-- Perhaps put algebra sup and inf into a namespace? + namespace real -local postfix ⁻¹ := pnat.inv -/- the reals form a metric space -/ - -protected definition 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 := λ x y, eq_of_abs_sub_eq_zero, - dist_comm := abs_sub, - dist_triangle := abs_sub_le -⦄ - -open nat -open [class] rat - -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 - -proposition converges_to_seq_offset {X : ℕ → ℝ} {y : ℝ} (k : ℕ) (H : X ⟶ y in ℕ) : - (λ n, X (n + k)) ⟶ y in ℕ := -metric_space.converges_to_seq_offset k H - -proposition converges_to_seq_offset_left {X : ℕ → ℝ} {y : ℝ} (k : ℕ) (H : X ⟶ y in ℕ) : - (λ n, X (k + n)) ⟶ y in ℕ := -metric_space.converges_to_seq_offset_left k H - -proposition converges_to_set_offset_succ {X : ℕ → ℝ} {y : ℝ} (H : X ⟶ y in ℕ) : - (λ n, X (succ n)) ⟶ y in ℕ := -metric_space.converges_to_seq_offset_succ H - -proposition converges_to_seq_of_converges_to_seq_offset - {X : ℕ → ℝ} {y : ℝ} {k : ℕ} (H : (λ n, X (n + k)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -metric_space.converges_to_seq_of_converges_to_seq_offset H - -proposition converges_to_seq_of_converges_to_seq_offset_left - {X : ℕ → ℝ} {y : ℝ} {k : ℕ} (H : (λ n, X (k + n)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -metric_space.converges_to_seq_of_converges_to_seq_offset_left H - -proposition converges_to_seq_of_converges_to_seq_offset_succ - {X : ℕ → ℝ} {y : ℝ} (H : (λ n, X (succ n)) ⟶ y in ℕ) : - X ⟶ y in ℕ := -metric_space.converges_to_seq_of_converges_to_seq_offset_succ H - -proposition converges_to_seq_offset_iff (X : ℕ → ℝ) (y : ℝ) (k : ℕ) : - ((λ n, X (n + k)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -metric_space.converges_to_seq_offset_iff X y k - -proposition converges_to_seq_offset_left_iff (X : ℕ → ℝ) (y : ℝ) (k : ℕ) : - ((λ n, X (k + n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -metric_space.converges_to_seq_offset_left_iff X y k - -proposition converges_to_seq_offset_succ_iff (X : ℕ → ℝ) (y : ℝ) : - ((λ n, X (succ n)) ⟶ y in ℕ) ↔ (X ⟶ y in ℕ) := -metric_space.converges_to_seq_offset_succ_iff X 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 : (k⁻¹ > (rat.of_num 0)), from !pnat.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, begin apply le.trans, apply le_succ, apply Hm end, - have Hn' : elt_of n ≥ N, begin apply le.trans, apply le_succ, apply Hn end, - 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⁻¹, by apply conv k n' Hn, - show abs (X n - l) < ε, from lt_of_le_of_lt this Hk)) - -protected definition complete_metric_space [reducible] [trans_instance] : - complete_metric_space ℝ := -⦃complete_metric_space, real.metric_space, - complete := @converges_seq_of_cauchy -⦄ - open set private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) : @@ -299,58 +142,121 @@ have HX : X = {x | -x ∈ negX}, show inf {x | -x ∈ X} = - sup X, using HX Hb' nonempty_negX, by rewrite [HX at {2}, sup_neg nonempty_negX Hb', neg_neg] end +end real + +/- the reals form a complete metric space -/ + +namespace analysis + +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 + +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_intro' {X : ℕ → ℝ} {y : ℝ} + (H : ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ N : ℕ, ∀ {n}, n ≥ N → abs (X n - y) ≤ ε) : + converges_to_seq X y := +converges_to_seq.intro H + +open pnat subtype +local postfix ⁻¹ := pnat.inv + +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 : (k⁻¹ >[rat] (rat.of_num 0)), from !pnat.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, begin apply le.trans, apply le_succ, apply Hm end, + have Hn' : elt_of n ≥ N, begin apply le.trans, apply le_succ, apply Hn end, + 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⁻¹, by apply conv k n' Hn, + show abs (X n - l) < ε, from lt_of_le_of_lt this Hk)) + +end analysis + +definition complete_metric_space_real [reducible] [trans_instance] : + complete_metric_space ℝ := +⦃complete_metric_space, metric_space_real, + complete := @analysis.converges_seq_of_cauchy +⦄ + +/- the real numbers can be viewed as a banach space -/ + +definition real_vector_space_real : real_vector_space ℝ := +⦃ real_vector_space, real.discrete_linear_ordered_field, + smul := mul, + smul_left_distrib := left_distrib, + smul_right_distrib := right_distrib, + mul_smul := mul.assoc, + one_smul := one_mul +⦄ + +definition banach_space_real [trans_instance] [reducible] : banach_space ℝ := +⦃ banach_space, real_vector_space_real, + 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, analysis.complete ℝ H +⦄ + /- limits under pointwise operations -/ section limit_operations -open nat - variables {X Y : ℕ → ℝ} variables {x y : ℝ} -proposition add_converges_to_seq (HX : X ⟶ x in ℕ) (HY : Y ⟶ y in ℕ) : - (λ n, X n + Y n) ⟶ x + y in ℕ := -take ε, suppose ε > 0, -have e2pos : ε / 2 > 0, from div_pos_of_pos_of_pos `ε > 0` two_pos, -obtain N₁ (HN₁ : ∀ {n}, n ≥ N₁ → abs (X n - x) < ε / 2), from HX e2pos, -obtain N₂ (HN₂ : ∀ {n}, n ≥ N₂ → abs (Y n - y) < ε / 2), from HY e2pos, -let N := max N₁ N₂ in -exists.intro N - (take n, - suppose n ≥ N, - have ngtN₁ : n ≥ N₁, from nat.le_trans !le_max_left `n ≥ N`, - have ngtN₂ : n ≥ N₂, from nat.le_trans !le_max_right `n ≥ N`, - show abs ((X n + Y n) - (x + y)) < ε, from calc - abs ((X n + Y n) - (x + y)) - = abs ((X n - x) + (Y n - y)) : by rewrite [sub_add_eq_sub_sub, *sub_eq_add_neg, - *add.assoc, add.left_comm (-x)] - ... ≤ abs (X n - x) + abs (Y n - y) : abs_add_le_abs_add_abs - ... < ε / 2 + ε / 2 : add_lt_add (HN₁ ngtN₁) (HN₂ ngtN₂) - ... = ε : add_halves) - -private lemma mul_left_converges_to_seq_of_pos {c : ℝ} (cnz : c ≠ 0) (HX : X ⟶ x in ℕ) : - (λ n, c * X n) ⟶ c * x in ℕ := -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, -obtain N (HN : ∀ {n}, n ≥ N → abs (X n - x) < ε / abs c), from HX epos, -exists.intro N - (take n, - suppose n ≥ N, - have H : abs (X n - x) < ε / abs c, from HN this, - show abs (c * X n - c * x) < ε, from calc - abs (c * X n - c * x) = abs c * abs (X n - x) : by rewrite [-mul_sub_left_distrib, abs_mul] - ... < abs c * (ε / abs c) : mul_lt_mul_of_pos_left H abscpos - ... = ε : mul_div_cancel' (ne_of_gt abscpos)) - proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : (λ n, c * X n) ⟶ c * x in ℕ := -by_cases - (assume cz : c = 0, - have (λ n, c * X n) = (λ n, 0), from funext (take x, by rewrite [cz, zero_mul]), - by+ rewrite [this, cz, zero_mul]; apply converges_to_seq_constant) - (suppose c ≠ 0, mul_left_converges_to_seq_of_pos this HX) +smul_converges_to_seq c HX proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : (λ n, X n * c) ⟶ x * c in ℕ := @@ -359,44 +265,12 @@ by+ rewrite [this, mul.comm]; apply mul_left_converges_to_seq c HX -- TODO: converges_to_seq_div, converges_to_seq_mul_left_iff, etc. -proposition neg_converges_to_seq (HX : X ⟶ x in ℕ) : - (λ n, - X n) ⟶ - x in ℕ := -take ε, suppose ε > 0, -obtain N (HN : ∀ {n}, n ≥ N → abs (X n - x) < ε), from HX this, -exists.intro N - (take n, - suppose n ≥ N, - show abs (- X n - (- x)) < ε, - by rewrite [-neg_neg_sub_neg, *neg_neg, abs_neg]; exact HN `n ≥ N`) - -proposition neg_converges_to_seq_iff (X : ℕ → ℝ) : - ((λ n, - X n) ⟶ - x in ℕ) ↔ (X ⟶ x in ℕ) := -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) - neg_converges_to_seq - proposition abs_converges_to_seq_zero (HX : X ⟶ 0 in ℕ) : (λ n, abs (X n)) ⟶ 0 in ℕ := -take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → abs (X n - 0) < ε), from HX `ε > 0`, -exists.intro N - (take n, assume Hn : n ≥ N, - have abs (X n) < ε, begin rewrite -(sub_zero (X n)), apply HN n Hn end, - show abs (abs (X n) - 0) < ε, using this, - by rewrite [sub_zero, abs_of_nonneg !abs_nonneg]; apply this) +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 ℕ := -take ε, suppose ε > 0, -obtain N (HN : ∀ n, n ≥ N → abs (abs (X n) - 0) < ε), from HX `ε > 0`, -exists.intro (N : ℕ) - (take n : ℕ, assume Hn : n ≥ N, - have HN' : abs (abs (X n) - 0) < ε, from HN n Hn, - have abs (X n) < ε, - by+ rewrite [sub_zero at HN', abs_of_nonneg !abs_nonneg at HN']; apply HN', - show abs (X n - 0) < ε, using this, - by rewrite sub_zero; apply this) +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 ℕ) := @@ -409,8 +283,7 @@ end limit_operations /- monotone sequences -/ section monotone_sequences -open nat set - +open real set variable {X : ℕ → ℝ} definition nondecreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≤ X j @@ -499,12 +372,15 @@ have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_compose, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), begin+ - rewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], + -- need krewrite here + krewrite [-neg_converges_to_seq_iff, -sup_neg H₁ H₂, H₃, -nondecreasing_neg_iff at nonincX], apply converges_to_seq_sup_of_nondecreasing nonincX H₄ end end monotone_sequences +/- x^n converges to 0 if abs x < 1 -/ + section xn open nat set @@ -515,7 +391,7 @@ suffices H' : (λ n, (abs x)^n) ⟶ 0 in ℕ, from using this, by rewrite this at H'; exact converges_to_seq_zero_of_abs_converges_to_seq_zero H', let aX := (λ n, (abs x)^n), - iaX := inf (aX ' univ), + iaX := real.inf (aX ' univ), asX := (λ n, (abs x)^(succ n)) in have noninc_aX : nonincreasing aX, from nonincreasing_of_forall_succ_le @@ -525,8 +401,8 @@ have noninc_aX : nonincreasing aX, from assert (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, -assert aXconv : aX ⟶ iaX in ℕ, from converges_to_seq_inf_of_nonincreasing noninc_aX bdd_aX, -have asXconv : asX ⟶ iaX in ℕ, from metric_space.converges_to_seq_offset_succ aXconv, +assert 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', assert iaX = 0, from eq_zero_of_mul_eq_self_left (ne_of_lt H) (eq.symm this), @@ -534,47 +410,57 @@ show aX ⟶ 0 in ℕ, begin rewrite -this, exact aXconv end --from this ▸ aXco end xn +/- continuity on the reals -/ + section continuous --- this definition should be inherited from metric_space once a migrate is done. -definition continuous (f : ℝ → ℝ) := - ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x - x') < δ → abs (f x - f x') < ε +theorem continuous_real_elim {f : ℝ → ℝ} (H : continuous f) : + ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε := +H + +theorem continuous_real_intro {f : ℝ → ℝ} + (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, + abs (x' - x) < δ → abs (f x' - f x) < ε) : + continuous f := +H theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b > 0) : - ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (b - y) < δ → f y > 0 := + ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y > 0 := begin - let Hcont := Hf b Hb, + let Hcont := continuous_real_elim Hf b Hb, cases Hcont with δ Hδ, existsi δ, split, exact and.left Hδ, intro y Hy, let Hy' := and.right Hδ y Hy, - note Hlt := sub_lt_of_abs_sub_lt_right Hy', + note Hlt := sub_lt_of_abs_sub_lt_left Hy', rewrite sub_self at Hlt, assumption end theorem neg_on_nbhd_of_cts_of_neg {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b < 0) : - ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (b - y) < δ → f y < 0 := + ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y < 0 := begin - let Hcont := Hf b (neg_pos_of_neg Hb), + let Hcont := continuous_real_elim Hf b (neg_pos_of_neg Hb), cases Hcont with δ Hδ, existsi δ, split, exact and.left Hδ, intro y Hy, let Hy' := and.right Hδ y Hy, - let Hlt := sub_lt_of_abs_sub_lt_left Hy', - note Hlt' := lt_add_of_sub_lt_right Hlt, - rewrite [-sub_eq_add_neg at Hlt', sub_self at Hlt'], + let Hlt := sub_lt_of_abs_sub_lt_right Hy', + note Hlt' := lt_add_of_sub_lt_left Hlt, + rewrite [add.comm at Hlt', -sub_eq_add_neg at Hlt', sub_self at Hlt'], assumption end -theorem neg_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) := +theorem continuous_neg_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) := begin + apply continuous_real_intro, intros x ε Hε, - cases Hcon x Hε with δ Hδ, + cases continuous_real_elim Hcon x Hε with δ Hδ, cases Hδ with Hδ₁ Hδ₂, existsi δ, split, @@ -585,11 +471,12 @@ theorem neg_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : c exact HD end -theorem translate_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) : +theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) : continuous (λ x, (f x) + a) := begin + apply continuous_real_intro, intros x ε Hε, - cases Hcon x Hε with δ Hδ, + cases continuous_real_elim Hcon x Hε with δ Hδ, cases Hδ with Hδ₁ Hδ₂, existsi δ, split, @@ -599,239 +486,9 @@ theorem translate_continuous_of_continuous {f : ℝ → ℝ} (Hcon : continuous apply Hδ₂, assumption end + end continuous -section inter_val -open set - -private definition inter_sup (a b : ℝ) (f : ℝ → ℝ) := sup {x | x < b ∧ f x < 0} - -section -parameters {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) (Ha : f a < 0) (Hb : f b > 0) -include Hf Ha Hb Hab - -private theorem Hinh : ∃ x, x ∈ {x | x < b ∧ f x < 0} := exists.intro a (and.intro Hab Ha) - -private theorem Hmem : ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ b := λ x Hx, le_of_lt (and.left Hx) - -private theorem Hsupleb : inter_sup a b f ≤ b := sup_le (Hinh) Hmem - -local notation 2 := of_num 1 + of_num 1 - -private theorem ex_delta_lt {x : ℝ} (Hx : f x < 0) (Hxb : x < b) : ∃ δ : ℝ, δ > 0 ∧ x + δ < b ∧ f (x + δ) < 0 := - begin - let Hcont := neg_on_nbhd_of_cts_of_neg Hf Hx, - cases Hcont with δ Hδ, - {cases em (x + δ < b) with Haδ Haδ, - existsi δ / 2, - split, - {exact div_pos_of_pos_of_pos (and.left Hδ) two_pos}, - split, - {apply lt.trans, - apply add_lt_add_left, - exact div_two_lt_of_pos (and.left Hδ), - exact Haδ}, - {apply and.right Hδ, - krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, - abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)], - exact div_two_lt_of_pos (and.left Hδ)}, - existsi (b - x) / 2, - split, - {apply div_pos_of_pos_of_pos, - exact sub_pos_of_lt Hxb, - exact two_pos}, - split, - {apply add_midpoint Hxb}, - {apply and.right Hδ, - krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, - abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hxb) two_pos)], - apply lt_of_lt_of_le, - apply div_two_lt_of_pos (sub_pos_of_lt Hxb), - apply sub_left_le_of_le_add, - apply le_of_not_gt Haδ}} - end - -private lemma sup_near_b {δ : ℝ} (Hpos : 0 < δ) - (Hgeb : inter_sup a b f + δ / 2 ≥ b) : abs (inter_sup a b f - b) < δ := - begin - apply abs_lt_of_lt_of_neg_lt, - apply sub_lt_left_of_lt_add, - apply lt_of_le_of_lt, - apply Hsupleb, - apply lt_add_of_pos_right Hpos, - rewrite neg_sub, - apply sub_lt_left_of_lt_add, - apply lt_of_le_of_lt, - apply Hgeb, - apply add_lt_add_left, - apply div_two_lt_of_pos Hpos - end - -private lemma delta_of_lt (Hflt : f (inter_sup a b f) < 0) : - ∃ δ : ℝ, δ > 0 ∧ inter_sup a b f + δ < b ∧ f (inter_sup a b f + δ) < 0 := - if Hlt : inter_sup a b f < b then ex_delta_lt Hflt Hlt else - begin - let Heq := eq_of_le_of_ge Hsupleb (le_of_not_gt Hlt), - apply absurd Hflt, - apply not_lt_of_ge, - apply le_of_lt, - rewrite Heq, - exact Hb - end - -private theorem sup_fn_interval_aux1 : f (inter_sup a b f) ≥ 0 := - have ¬ f (inter_sup a b f) < 0, from - (suppose f (inter_sup a b f) < 0, - obtain δ Hδ, from delta_of_lt this, - have inter_sup a b f + δ ∈ {x | x < b ∧ f x < 0}, - from and.intro (and.left (and.right Hδ)) (and.right (and.right Hδ)), - have ¬ inter_sup a b f < inter_sup a b f + δ, - from not_lt_of_ge (le_sup this Hmem), - show false, from this (lt_add_of_pos_right (and.left Hδ))), - le_of_not_gt this - -private theorem sup_fn_interval_aux2 : f (inter_sup a b f) ≤ 0 := - have ¬ f (inter_sup a b f) > 0, from - (assume Hfsup : f (inter_sup a b f) > 0, - obtain δ Hδ, from pos_on_nbhd_of_cts_of_pos Hf Hfsup, - have ∀ x, x ∈ {x | x < b ∧ f x < 0} → x ≤ inter_sup a b f - δ / 2, from - (take x, assume Hxset : x ∈ {x | x < b ∧ f x < 0}, - have ¬ x > inter_sup a b f - δ / 2, from - (assume Hngt, - have Habs : abs (inter_sup a b f - x) < δ, begin - apply abs_lt_of_lt_of_neg_lt, - apply sub_lt_of_sub_lt, - apply gt.trans, - exact Hngt, - apply sub_lt_sub_left, - exact div_two_lt_of_pos (and.left Hδ), - rewrite neg_sub, - apply lt_of_le_of_lt, - rotate 1, - apply and.left Hδ, - apply sub_nonpos_of_le, - apply le_sup, - exact Hxset, - exact Hmem - end, - have f x > 0, from and.right Hδ x Habs, - show false, from (not_lt_of_gt this) (and.right Hxset)), - le_of_not_gt this), - have Hle : inter_sup a b f ≤ inter_sup a b f - δ / 2, from sup_le Hinh this, - show false, from not_le_of_gt - (sub_lt_of_pos _ (div_pos_of_pos_of_pos (and.left Hδ) (two_pos))) Hle), - le_of_not_gt this - -private theorem sup_fn_interval : f (inter_sup a b f) = 0 := - eq_of_le_of_ge sup_fn_interval_aux2 sup_fn_interval_aux1 - - -private theorem intermediate_value_incr_aux2 : ∃ δ : ℝ, δ > 0 ∧ a + δ < b ∧ f (a + δ) < 0 := - begin - let Hcont := neg_on_nbhd_of_cts_of_neg Hf Ha, - cases Hcont with δ Hδ, - {cases em (a + δ < b) with Haδ Haδ, - existsi δ / 2, - split, - {exact div_pos_of_pos_of_pos (and.left Hδ) two_pos}, - split, - {apply lt.trans, - apply add_lt_add_left, - exact div_two_lt_of_pos (and.left Hδ), - exact Haδ}, - {apply and.right Hδ, - krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, - abs_of_pos (div_pos_of_pos_of_pos (and.left Hδ) two_pos)], - exact div_two_lt_of_pos (and.left Hδ)}, - existsi (b - a) / 2, - split, - {apply div_pos_of_pos_of_pos, - exact sub_pos_of_lt Hab, - exact two_pos}, - split, - {apply add_midpoint Hab}, - {apply and.right Hδ, - krewrite [sub_add_eq_sub_sub, sub_self, zero_sub, abs_neg, - abs_of_pos (div_pos_of_pos_of_pos (sub_pos_of_lt Hab) two_pos)], - apply lt_of_lt_of_le, - apply div_two_lt_of_pos (sub_pos_of_lt Hab), - apply sub_left_le_of_le_add, - apply le_of_not_gt Haδ}} - end - -theorem intermediate_value_incr_zero : ∃ c, a < c ∧ c < b ∧ f c = 0 := - begin - existsi inter_sup a b f, - split, - {cases intermediate_value_incr_aux2 with δ Hδ, - apply lt_of_lt_of_le, - apply lt_add_of_pos_right, - exact and.left Hδ, - apply le_sup, - exact and.right Hδ, - intro x Hx, - apply le_of_lt, - exact and.left Hx}, - split, - {cases pos_on_nbhd_of_cts_of_pos Hf Hb with δ Hδ, - apply lt_of_le_of_lt, - rotate 1, - apply sub_lt_of_pos, - exact and.left Hδ, - rotate_right 1, - apply sup_le, - exact exists.intro a (and.intro Hab Ha), - intro x Hx, - apply le_of_not_gt, - intro Hxgt, - have Hxgt' : b - x < δ, from sub_lt_of_sub_lt Hxgt, - krewrite -(abs_of_pos (sub_pos_of_lt (and.left Hx))) at Hxgt', - note Hxgt'' := and.right Hδ _ Hxgt', - exact not_lt_of_ge (le_of_lt Hxgt'') (and.right Hx)}, - {exact sup_fn_interval} - end - -end - -theorem intermediate_value_decr_zero {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) - (Ha : f a > 0) (Hb : f b < 0) : ∃ c, a < c ∧ c < b ∧ f c = 0 := - begin - have Ha' : - f a < 0, from neg_neg_of_pos Ha, - have Hb' : - f b > 0, from neg_pos_of_neg Hb, - have Hcon : continuous (λ x, - f x), from neg_continuous_of_continuous Hf, - let Hiv := intermediate_value_incr_zero Hcon Hab Ha' Hb', - cases Hiv with c Hc, - existsi c, - split, - exact and.left Hc, - split, - exact and.left (and.right Hc), - apply eq_zero_of_neg_eq_zero, - apply and.right (and.right Hc) - end - -theorem intermediate_value_incr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ} - (Hav : f a < v) (Hbv : f b > v) : ∃ c, a < c ∧ c < b ∧ f c = v := - have Hav' : f a - v < 0, from sub_neg_of_lt Hav, - have Hbv' : f b - v > 0, from sub_pos_of_lt Hbv, - have Hcon : continuous (λ x, f x - v), from translate_continuous_of_continuous Hf _, - have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_incr_zero Hcon Hab Hav' Hbv', - obtain c Hc, from Hiv, - exists.intro c - (and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc))))) - -theorem intermediate_value_decr {f : ℝ → ℝ} (Hf : continuous f) {a b : ℝ} (Hab : a < b) {v : ℝ} - (Hav : f a > v) (Hbv : f b < v) : ∃ c, a < c ∧ c < b ∧ f c = v := - have Hav' : f a - v > 0, from sub_pos_of_lt Hav, - have Hbv' : f b - v < 0, from sub_neg_of_lt Hbv, - have Hcon : continuous (λ x, f x - v), from translate_continuous_of_continuous Hf _, - have Hiv : ∃ c, a < c ∧ c < b ∧ f c - v = 0, from intermediate_value_decr_zero Hcon Hab Hav' Hbv', - obtain c Hc, from Hiv, - exists.intro c - (and.intro (and.left Hc) (and.intro (and.left (and.right Hc)) (eq_of_sub_eq_zero (and.right (and.right Hc))))) - -end inter_val - /- 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₂ := @@ -844,7 +501,4 @@ eq_of_forall_dist_le from H₂ e2pos, let δ := min δ₁ δ₂ in have δ > 0, from lt_min δ₁pos δ₂pos, - -/ - -end real