/- 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 Banach space. -/ 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 open set private definition exists_is_sup {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) : ∃ y, is_sup X y := let x := some (and.left H), b := some (and.right H) in exists_is_sup_of_inh_of_bdd X x (some_spec (and.left H)) b (some_spec (and.right H)) private definition sup_aux {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) := some (exists_is_sup H) private definition sup_aux_spec {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b)) : is_sup X (sup_aux H) := some_spec (exists_is_sup H) definition sup (X : set ℝ) : ℝ := if H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b) then sup_aux H else 0 proposition le_sup {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) : x ≤ sup X := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b), from and.intro (exists.intro x Hx) (exists.intro b Hb), by+ rewrite [↑sup, dif_pos H]; exact and.left (sup_aux_spec H) x Hx proposition sup_le {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) : sup X ≤ b := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → x ≤ b), from and.intro HX (exists.intro b Hb), by+ rewrite [↑sup, dif_pos H]; exact and.right (sup_aux_spec H) b Hb proposition exists_mem_and_lt_of_lt_sup {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : b < sup X) : ∃ x, x ∈ X ∧ b < x := have ¬ ∀ x, x ∈ X → x ≤ b, from assume H, not_le_of_gt Hb (sup_le HX H), obtain x (Hx : ¬ (x ∈ X → x ≤ b)), from exists_not_of_not_forall this, exists.intro x (have x ∈ X ∧ ¬ x ≤ b, by rewrite [-not_implies_iff_and_not]; apply Hx, and.intro (and.left this) (lt_of_not_ge (and.right this))) private definition exists_is_inf {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) : ∃ y, is_inf X y := let x := some (and.left H), b := some (and.right H) in exists_is_inf_of_inh_of_bdd X x (some_spec (and.left H)) b (some_spec (and.right H)) private definition inf_aux {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) := some (exists_is_inf H) private definition inf_aux_spec {X : set ℝ} (H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x)) : is_inf X (inf_aux H) := some_spec (exists_is_inf H) definition inf (X : set ℝ) : ℝ := if H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x) then inf_aux H else 0 proposition inf_le {x : ℝ} {X : set ℝ} (Hx : x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) : inf X ≤ x := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x), from and.intro (exists.intro x Hx) (exists.intro b Hb), by+ rewrite [↑inf, dif_pos H]; exact and.left (inf_aux_spec H) x Hx proposition le_inf {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) : b ≤ inf X := have H : (∃ x, x ∈ X) ∧ (∃ b, ∀ x, x ∈ X → b ≤ x), from and.intro HX (exists.intro b Hb), by+ rewrite [↑inf, dif_pos H]; exact and.right (inf_aux_spec H) b Hb proposition exists_mem_and_lt_of_inf_lt {X : set ℝ} (HX : ∃ x, x ∈ X) {b : ℝ} (Hb : inf X < b) : ∃ x, x ∈ X ∧ x < b := have ¬ ∀ x, x ∈ X → b ≤ x, from assume H, not_le_of_gt Hb (le_inf HX H), obtain x (Hx : ¬ (x ∈ X → b ≤ x)), from exists_not_of_not_forall this, exists.intro x (have x ∈ X ∧ ¬ b ≤ x, by rewrite [-not_implies_iff_and_not]; apply Hx, and.intro (and.left this) (lt_of_not_ge (and.right this))) section local attribute mem [quasireducible] -- TODO: is there a better place to put this? proposition image_neg_eq (X : set ℝ) : (λ x, -x) ' X = {x | -x ∈ X} := set.ext (take x, iff.intro (assume H, obtain y [(Hy₁ : y ∈ X) (Hy₂ : -y = x)], from H, show -x ∈ X, by rewrite [-Hy₂, neg_neg]; exact Hy₁) (assume H : -x ∈ X, exists.intro (-x) (and.intro H !neg_neg))) proposition sup_neg {X : set ℝ} (nonempty_X : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → b ≤ x) : sup {x | -x ∈ X} = - inf X := let negX := {x | -x ∈ X} in have nonempty_negX : ∃ x, x ∈ negX, from obtain x Hx, from nonempty_X, have -(-x) ∈ X, by rewrite neg_neg; apply Hx, exists.intro (-x) this, have H₁ : ∀ x, x ∈ negX → x ≤ - inf X, from take x, assume H, have inf X ≤ -x, from inf_le H Hb, show x ≤ - inf X, from le_neg_of_le_neg this, have H₂ : ∀ x, x ∈ X → -sup negX ≤ x, from take x, assume H, have -(-x) ∈ X, by rewrite neg_neg; apply H, have -x ≤ sup negX, from le_sup this H₁, show -sup negX ≤ x, from !neg_le_of_neg_le this, eq_of_le_of_ge (show sup negX ≤ - inf X, from sup_le nonempty_negX H₁) (show -inf X ≤ sup negX, from !neg_le_of_neg_le (le_inf nonempty_X H₂)) proposition inf_neg {X : set ℝ} (nonempty_X : ∃ x, x ∈ X) {b : ℝ} (Hb : ∀ x, x ∈ X → x ≤ b) : inf {x | -x ∈ X} = - sup X := let negX := {x | -x ∈ X} in have nonempty_negX : ∃ x, x ∈ negX, from obtain x Hx, from nonempty_X, have -(-x) ∈ X, by rewrite neg_neg; apply Hx, exists.intro (-x) this, have Hb' : ∀ x, x ∈ negX → -b ≤ x, from take x, assume H, !neg_le_of_neg_le (Hb _ H), have HX : X = {x | -x ∈ negX}, from set.ext (take x, by rewrite [↑set_of, ↑mem, +neg_neg]), 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 variables {X Y : ℕ → ℝ} variables {x y : ℝ} proposition mul_left_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : (λ n, c * X n) ⟶ c * x in ℕ := smul_converges_to_seq c HX proposition mul_right_converges_to_seq (c : ℝ) (HX : X ⟶ x in ℕ) : (λ n, X n * c) ⟶ x * c in ℕ := 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 ℕ := begin 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, existsi max N1 N2, intro n Hn, have HXY : abs (Y n - X n) < ε / 2, begin apply lt_of_le_of_lt, apply abs_sub_le _ x, have Hε24 : ε / 2 = ε / 4 + ε / 4, from eq.symm !add_quarters, rewrite Hε24, apply add_lt_add, apply HN2, apply ge.trans Hn !le_max_right, rewrite abs_sub, apply HN1, apply ge.trans Hn !le_max_left end, have HZX : abs (Z n - X n) < ε / 2, begin have HZXnp : Z n - X n ≥ 0, from sub_nonneg_of_le !HZX, have HXYnp : Y n - X n ≥ 0, from sub_nonneg_of_le (le.trans !HZX !HZY), rewrite [abs_of_nonneg HZXnp, abs_of_nonneg HXYnp at HXY], note Hgt := lt_add_of_sub_lt_right HXY, have Hlt : Z n < ε / 2 + X n, from calc Z n ≤ Y n : HZY ... < ε / 2 + X n : Hgt, apply sub_lt_right_of_lt_add Hlt end, have H : abs (Z n - x) < ε, begin apply lt_of_le_of_lt, apply abs_sub_le _ (X n), apply lt.trans, apply add_lt_add, apply HZX, apply HN1, apply ge.trans Hn !le_max_left, apply div_two_add_div_four_lt Hε end, exact H end proposition converges_to_seq_of_abs_sub_converges_to_seq (Habs : (λ n, abs (X n - x)) ⟶ 0 in ℕ) : X ⟶ x in ℕ := begin intros ε Hε, cases Habs Hε with N HN, existsi N, intro n Hn, have Hn' : abs (abs (X n - x) - 0) < ε, from HN Hn, rewrite [sub_zero at Hn', abs_abs at Hn'], exact Hn' end proposition abs_sub_converges_to_seq_of_converges_to_seq (HX : X ⟶ x in ℕ) : (λ n, abs (X n - x)) ⟶ 0 in ℕ := begin intros ε Hε, cases 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 ℕ := have Hbd : ∃ K : ℝ, ∀ n : ℕ, abs (X n) ≤ K, begin cases bounded_of_converges_seq HX with K HK, existsi K + abs x, intro n, note Habs := le.trans (abs_abs_sub_abs_le_abs_sub (X n) x) !HK, apply le_add_of_sub_right_le, apply le.trans, apply le_abs_self, assumption end, obtain K HK, from Hbd, have Habsle [visible] : ∀ n, abs (X n * Y n - x * y) ≤ K * abs (Y n - y) + abs y * abs (X n - x), begin intro, have Heq : X n * Y n - x * y = (X n * Y n - X n * y) + (X n * y - x * y), by rewrite [-sub_add_cancel (X n * Y n) (X n * y) at {1}, sub_eq_add_neg, *add.assoc], apply le.trans, rewrite Heq, apply abs_add_le_abs_add_abs, apply add_le_add, rewrite [-mul_sub_left_distrib, abs_mul], apply mul_le_mul_of_nonneg_right, apply HK, apply abs_nonneg, rewrite [-mul_sub_right_distrib, abs_mul, mul.comm], apply le.refl end, have Hdifflim [visible] : (λ n, abs (X n * Y n - x * y)) ⟶ 0 in ℕ, begin apply converges_to_seq_squeeze, rotate 2, intro, apply abs_nonneg, apply Habsle, apply converges_to_seq_constant, rewrite -{0}zero_add, apply add_converges_to_seq, krewrite -(mul_zero K), apply mul_left_converges_to_seq, apply abs_sub_converges_to_seq_of_converges_to_seq, exact HY, krewrite -(mul_zero (abs y)), apply mul_left_converges_to_seq, apply abs_sub_converges_to_seq_of_converges_to_seq, exact HX end, converges_to_seq_of_abs_sub_converges_to_seq Hdifflim -- 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 ℕ := 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 ℕ := 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 ℕ) := 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 end limit_operations /- properties of converges_to_at -/ 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 := 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 end end limit_operations_continuous /- monotone sequences -/ section monotone_sequences open real set variable {X : ℕ → ℝ} definition nondecreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≤ X j proposition nondecreasing_of_forall_le_succ (H : ∀ i, X i ≤ X (succ i)) : nondecreasing X := take i j, suppose i ≤ j, have ∀ n, X i ≤ X (i + n), from take n, nat.induction_on n (by rewrite nat.add_zero; apply le.refl) (take n, assume ih, le.trans ih (H (i + n))), have X i ≤ X (i + (j - i)), from !this, by+ rewrite [add_sub_of_le `i ≤ j` at this]; exact this 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 have Xle : ∀ i, X i ≤ sX, from take i, have ∀ x, x ∈ X ' univ → x ≤ b, from (take x, assume H, obtain i [H' (Hi : X i = x)], from H, by rewrite -Hi; exact Hb i), show X i ≤ sX, from le_sup (mem_image_of_mem X !mem_univ) this, have exX : ∃ x, x ∈ X ' univ, from exists.intro (X 0) (mem_image_of_mem X !mem_univ), take ε, assume epos : ε > 0, have sX - ε < sX, from !sub_lt_of_pos epos, obtain x' [(H₁x' : x' ∈ X ' univ) (H₂x' : sX - ε < x')], from exists_mem_and_lt_of_lt_sup exX this, obtain i [H' (Hi : X i = x')], from H₁x', have Hi' : ∀ j, j ≥ i → sX - ε < X j, from take j, assume Hj, lt_of_lt_of_le (by rewrite Hi; apply H₂x') (nondecX Hj), exists.intro i (take j, assume Hj : j ≥ i, have X j - sX ≤ 0, from sub_nonpos_of_le (Xle j), have eq₁ : abs (X j - sX) = sX - X j, using this, by rewrite [abs_of_nonpos this, neg_sub], 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)) < ε, using eq₁ this, by rewrite eq₁; exact this) definition nonincreasing (X : ℕ → ℝ) : Prop := ∀ ⦃i j⦄, i ≤ j → X i ≥ X j proposition nodecreasing_of_nonincreasing_neg (nonincX : nonincreasing (λ n, - X n)) : nondecreasing (λ n, X n) := take i j, suppose i ≤ j, show X i ≤ X j, from le_of_neg_le_neg (nonincX this) proposition noincreasing_neg_of_nondecreasing (nondecX : nondecreasing X) : nonincreasing (λ n, - X n) := take i j, suppose i ≤ j, show - X i ≥ - X j, from neg_le_neg (nondecX this) proposition nonincreasing_neg_iff (X : ℕ → ℝ) : nonincreasing (λ n, - X n) ↔ nondecreasing X := iff.intro nodecreasing_of_nonincreasing_neg noincreasing_neg_of_nondecreasing proposition nonincreasing_of_nondecreasing_neg (nondecX : nondecreasing (λ n, - X n)) : nonincreasing (λ n, X n) := take i j, suppose i ≤ j, show X i ≥ X j, from le_of_neg_le_neg (nondecX this) proposition nodecreasing_neg_of_nonincreasing (nonincX : nonincreasing X) : nondecreasing (λ n, - X n) := take i j, suppose i ≤ j, show - X i ≤ - X j, from neg_le_neg (nonincX this) proposition nondecreasing_neg_iff (X : ℕ → ℝ) : nondecreasing (λ n, - X n) ↔ nonincreasing X := iff.intro nonincreasing_of_nondecreasing_neg nodecreasing_neg_of_nonincreasing proposition nonincreasing_of_forall_succ_le (H : ∀ i, X (succ i) ≤ X i) : nonincreasing X := begin rewrite -nondecreasing_neg_iff, show nondecreasing (λ n : ℕ, - X n), from nondecreasing_of_forall_le_succ (take i, neg_le_neg (H i)) end proposition converges_to_seq_inf_of_nonincreasing (nonincX : nonincreasing X) {b : ℝ} (Hb : ∀ i, b ≤ X i) : X ⟶ inf (X ' univ) in ℕ := 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, obtain i [Hi₁ (Hi₂ : X i = x)], from H, show b ≤ x, by rewrite -Hi₂; apply Hb i), have H₃ : {x : ℝ | -x ∈ X ' univ} = {x : ℝ | x ∈ (λ n, -X n) ' univ}, from calc {x : ℝ | -x ∈ X ' univ} = (λ y, -y) ' (X ' univ) : by rewrite image_neg_eq ... = {x : ℝ | x ∈ (λ n, -X n) ' univ} : image_compose, have H₄ : ∀ i, - X i ≤ - b, from take i, neg_le_neg (Hb i), begin+ -- 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 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 have (λ n, (abs x)^n) = (λ n, abs (x^n)), from funext (take n, eq.symm !abs_pow), 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 := real.inf (aX ' univ), asX := (λ n, (abs x)^(succ n)) in have noninc_aX : nonincreasing aX, from nonincreasing_of_forall_succ_le (take i, assert (abs x) * (abs x)^i ≤ 1 * (abs x)^i, from mul_le_mul_of_nonneg_right (le_of_lt H) (!pow_nonneg_of_nonneg !abs_nonneg), 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 ℕ, 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), show aX ⟶ 0 in ℕ, begin rewrite -this, exact aXconv end --from this ▸ aXconv end xn /- continuity on the reals -/ section continuous theorem continuous_real_elim {f : ℝ → ℝ} (H : continuous f) : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε := take x, continuous_at_elim (H x) theorem continuous_real_intro {f : ℝ → ℝ} (H : ∀ x : ℝ, ∀ ⦃ε : ℝ⦄, ε > 0 → ∃ δ : ℝ, δ > 0 ∧ ∀ x' : ℝ, abs (x' - x) < δ → abs (f x' - f x) < ε) : continuous f := take x, continuous_at_intro (H x) theorem pos_on_nbhd_of_cts_of_pos {f : ℝ → ℝ} (Hf : continuous f) {b : ℝ} (Hb : f b > 0) : ∃ δ : ℝ, δ > 0 ∧ ∀ y, abs (y - b) < δ → f y > 0 := begin 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_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 (y - b) < δ → f y < 0 := begin 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_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 continuous_neg_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) : continuous (λ x, - f x) := begin apply continuous_real_intro, intros x ε Hε, cases continuous_real_elim Hcon x Hε with δ Hδ, cases Hδ with Hδ₁ Hδ₂, existsi δ, split, assumption, intros x' Hx', let HD := Hδ₂ x' Hx', rewrite [-abs_neg, neg_neg_sub_neg], exact HD end theorem continuous_offset_of_continuous {f : ℝ → ℝ} (Hcon : continuous f) (a : ℝ) : continuous (λ x, (f x) + a) := begin apply continuous_real_intro, intros x ε Hε, cases continuous_real_elim Hcon x Hε with δ Hδ, cases Hδ with Hδ₁ Hδ₂, existsi δ, split, assumption, intros x' Hx', rewrite [add_sub_comm, sub_self, add_zero], apply Hδ₂, assumption end theorem continuous_mul_of_continuous {f g : ℝ → ℝ} (Hconf : continuous f) (Hcong : continuous g) : continuous (λ x, f x * g x) := begin intro x, apply continuous_at_of_converges_to_at, apply mul_converges_to_at, all_goals apply converges_to_at_of_continuous_at, apply Hconf, apply Hcong end end continuous