From 5c2fe1c3affc6ceea5eb8ad1cc26d7cf3675b6d4 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Mon, 3 Aug 2015 11:12:56 -0400 Subject: [PATCH] refactor(real/complete): put limit sequence construction in a section --- library/data/real/complete.lean | 78 ++++++++++++++++++--------------- 1 file changed, 43 insertions(+), 35 deletions(-) diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 8e560f2a04..fd015722ec 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -229,7 +229,7 @@ theorem re_abs_is_abs : re_abs = real.abs := funext end) theorem abs_const (a : ℚ) : of_rat (rat.abs a) = abs (of_rat a) := - by rewrite -re_abs_is_abs -- ???? + by rewrite -re_abs_is_abs theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - of_rat q) ≤ of_rat n⁻¹ := quot.induction_on x (λ s n, s.r_rat_approx s n) @@ -279,13 +279,18 @@ theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := ! theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_left -noncomputable definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℕ+ → ℚ := +section lim_seq +parameter {X : r_seq} +parameter {M : ℕ+ → ℕ+} +hypothesis Hc : cauchy X M +include Hc + +noncomputable definition lim_seq : ℕ+ → ℚ := λ k, approx (X (Nb M k)) (2 * k) -theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+} - (Hmn : M (2 * n) ≤M (2 * m)) : - abs (of_rat (lim_seq Hc m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs - (X (Nb M n) - of_rat (lim_seq Hc n)) ≤ of_rat (m⁻¹ + n⁻¹) := +theorem lim_seq_reg_helper {m n : ℕ+} (Hmn : M (2 * n) ≤M (2 * m)) : + abs (of_rat (lim_seq m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs + (X (Nb M n) - of_rat (lim_seq n)) ≤ of_rat (m⁻¹ + n⁻¹) := begin apply le.trans, apply add_le_add_three, @@ -307,7 +312,7 @@ theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m apply pnat.mul_le_mul_left end -theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.regular (lim_seq Hc) := +theorem lim_seq_reg : s.regular lim_seq := begin rewrite ↑s.regular, intro m n, @@ -318,48 +323,46 @@ theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.regula let Hor := em (M (2 * m) ≥ M (2 * n)), apply or.elim Hor, intro Hor1, - apply lim_seq_reg_helper Hc Hor1, + apply lim_seq_reg_helper Hor1, intro Hor2, let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2), rewrite [real.abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub, -- ??? rat.add.comm, add_comm_three], - apply lim_seq_reg_helper Hc Hor2' + apply lim_seq_reg_helper Hor2' end -theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : - s.s_le (s.s_abs (s.sadd (lim_seq Hc) (s.sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) := +theorem lim_seq_spec (k : ℕ+) : + s.s_le (s.s_abs (s.sadd lim_seq (s.sneg (s.const (lim_seq k))))) (s.const k⁻¹) := begin apply s.const_bound, apply lim_seq_reg end -noncomputable definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.reg_seq := - s.reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc) +noncomputable definition r_lim_seq : s.reg_seq := + s.reg_seq.mk lim_seq lim_seq_reg -theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) : - s.r_le (s.r_abs (( s.radd (r_lim_seq Hc) (s.rneg (s.r_const ((s.reg_seq.sq (r_lim_seq Hc)) k)))))) (s.r_const (k)⁻¹) := - lim_seq_spec Hc k +theorem r_lim_seq_spec (k : ℕ+) : s.r_le + (s.r_abs ((s.radd r_lim_seq (s.rneg (s.r_const ((s.reg_seq.sq r_lim_seq) k)))))) + (s.r_const k⁻¹) := + lim_seq_spec k -noncomputable definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ := - quot.mk (r_lim_seq Hc) +noncomputable definition lim : ℝ := + quot.mk r_lim_seq -theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : - re_abs ((lim Hc) - (of_rat ((lim_seq Hc) k))) ≤ of_rat k⁻¹ := - r_lim_seq_spec Hc k +theorem re_lim_spec (k : ℕ+) : re_abs (lim - (of_rat (lim_seq k))) ≤ of_rat k⁻¹ := + r_lim_seq_spec k -theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : - abs ((lim Hc) - (of_rat ((lim_seq Hc) k))) ≤ of_rat k⁻¹ := +theorem lim_spec' (k : ℕ+) : abs (lim - (of_rat (lim_seq k))) ≤ of_rat k⁻¹ := by rewrite -re_abs_is_abs; apply re_lim_spec -theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) : - abs ((of_rat ((lim_seq Hc) k)) - (lim Hc)) ≤ of_rat (k)⁻¹ := +theorem lim_spec (k : ℕ+) : + abs ((of_rat (lim_seq k)) - lim) ≤ of_rat k⁻¹ := by rewrite abs_sub; apply lim_spec' -theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : - converges_to X (lim Hc) (Nb M) := +theorem converges_of_cauchy : converges_to X lim (Nb M) := begin intro k n Hn, - rewrite (rewrite_helper10 (X (Nb M n)) (of_rat (lim_seq Hc n))), + rewrite (rewrite_helper10 (X (Nb M n)) (of_rat (lim_seq n))), apply le.trans, apply abs_add_three, apply le.trans, @@ -405,10 +408,10 @@ theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : apply rat.le.refl end +end lim_seq ------------------------------------------- -- int embedding theorems -- archimedean properties, integer floor and ceiling - section ints open int @@ -714,7 +717,8 @@ theorem avg_symm (n : ℕ) : avg_seq n = avg (under_seq n) (over_seq n) := theorem over_0 : over_seq 0 = over := rfl theorem under_0 : under_seq 0 = under := rfl -theorem succ_helper (n : ℕ) : avg (pr1 (rpt bisect n (under, over))) (pr2 (rpt bisect n (under, over))) = avg_seq n := +theorem succ_helper (n : ℕ) : + avg (pr1 (rpt bisect n (under, over))) (pr2 (rpt bisect n (under, over))) = avg_seq n := by rewrite avg_symm theorem under_succ (n : ℕ) : under_seq (succ n) = @@ -752,12 +756,15 @@ theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2 intro a Ha, rewrite [over_succ, under_succ], let Hou := calc - (over_seq a) / 2 - (under_seq a) / 2 = ((over - under) / rat.pow 2 a) / 2 : by rewrite [rat.div_sub_div_same, Ha] - ... = (over - under) / (rat.pow 2 a * 2) : rat.div_div_eq_div_mul (rat.ne_of_gt (rat.pow_pos dec_trivial _)) dec_trivial + (over_seq a) / 2 - (under_seq a) / 2 = ((over - under) / rat.pow 2 a) / 2 : + by rewrite [rat.div_sub_div_same, Ha] + ... = (over - under) / (rat.pow 2 a * 2) : + rat.div_div_eq_div_mul (rat.ne_of_gt (rat.pow_pos dec_trivial _)) dec_trivial ... = (over - under) / rat.pow 2 (a + 1) : by rewrite rat.pow_add, cases em (ub (avg_seq a)), rewrite [*if_pos a_1, -add_one, -Hou, ↑avg_seq, ↑avg, rat.add.assoc, rat.div_two_sub_self], - rewrite [*if_neg a_1, -add_one, -Hou, ↑avg_seq, ↑avg, rat.sub_add_eq_sub_sub, rat.sub_self_div_two] + rewrite [*if_neg a_1, -add_one, -Hou, ↑avg_seq, ↑avg, rat.sub_add_eq_sub_sub, + rat.sub_self_div_two] end) theorem binary_nat_bound (a : ℕ) : of_nat a ≤ (rat.pow 2 a) := @@ -766,7 +773,8 @@ theorem binary_nat_bound (a : ℕ) : of_nat a ≤ (rat.pow 2 a) := calc of_nat (succ n) = (of_nat n) + 1 : of_nat_add ... ≤ rat.pow 2 n + 1 : rat.add_le_add_right Hn - ... ≤ rat.pow 2 n + rat.pow 2 n : rat.add_le_add_left (rat.pow_ge_one_of_ge_one rat.two_ge_one _) + ... ≤ rat.pow 2 n + rat.pow 2 n : + rat.add_le_add_left (rat.pow_ge_one_of_ge_one rat.two_ge_one _) ... = rat.pow 2 (succ n) : rat.pow_two_add) theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ rat.pow 2 n := @@ -857,7 +865,7 @@ theorem under_seq_lt_over_seq : ∀ m n : ℕ, under_seq m < over_seq n := begin intros, cases exists_not_of_not_forall (PA m) with [x, Hx], - cases (iff.mp not_implies_iff_and_not) Hx with [HXx, Hxu], + cases iff.mp not_implies_iff_and_not Hx with [HXx, Hxu], apply lt_of_rat_lt_of_rat, apply lt_of_lt_of_le, apply lt_of_not_ge Hxu,