2015-06-09 05:39:28 +00:00
|
|
|
|
/-
|
|
|
|
|
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
|
|
|
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
|
|
|
Author: Robert Y. Lewis
|
|
|
|
|
The real numbers, constructed as equivalence classes of Cauchy sequences of rationals.
|
|
|
|
|
This construction follows Bishop and Bridges (1985).
|
|
|
|
|
|
|
|
|
|
At this point, we no longer proceed constructively: this file makes heavy use of decidability,
|
|
|
|
|
excluded middle, and Hilbert choice.
|
|
|
|
|
|
|
|
|
|
Here, we show that ℝ is complete.
|
|
|
|
|
-/
|
2015-06-10 02:46:30 +00:00
|
|
|
|
|
2015-06-16 04:55:02 +00:00
|
|
|
|
import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat logic.axioms.classical
|
2015-06-10 02:46:30 +00:00
|
|
|
|
open -[coercions] rat
|
|
|
|
|
local notation 0 := rat.of_num 0
|
|
|
|
|
local notation 1 := rat.of_num 1
|
2015-06-09 05:39:28 +00:00
|
|
|
|
open -[coercions] nat
|
|
|
|
|
open algebra
|
|
|
|
|
open eq.ops
|
2015-06-16 04:55:02 +00:00
|
|
|
|
open pnat
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
local notation 2 := pnat.pos (nat.of_num 2) dec_trivial
|
|
|
|
|
local notation 3 := pnat.pos (nat.of_num 3) dec_trivial
|
|
|
|
|
|
|
|
|
|
namespace s
|
|
|
|
|
|
|
|
|
|
theorem nonneg_of_ge_neg_invs (a : ℚ) (H : ∀ n : ℕ+, -n⁻¹ ≤ a) : 0 ≤ a := sorry
|
|
|
|
|
|
|
|
|
|
definition const (a : ℚ) : seq := λ n, a
|
|
|
|
|
|
|
|
|
|
theorem const_reg (a : ℚ) : regular (const a) :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [↑const, sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a)
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem rat_approx_l1 {s : seq} (H : regular s) :
|
2015-06-09 05:39:28 +00:00
|
|
|
|
∀ n : ℕ+, ∃ q : ℚ, ∃ N : ℕ+, ∀ m : ℕ+, m ≥ N → abs (s m - q) ≤ n⁻¹ :=
|
|
|
|
|
begin
|
|
|
|
|
intro n,
|
|
|
|
|
existsi (s (2 * n)),
|
|
|
|
|
existsi 2 * n,
|
|
|
|
|
intro m Hm,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply H,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite -(add_halves n),
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply inv_ge_of_le Hm
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem rat_approx {s : seq} (H : regular s) :
|
|
|
|
|
∀ n : ℕ+, ∃ q : ℚ, s_le (s_abs (sadd s (sneg (const q)))) (const n⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
intro m,
|
|
|
|
|
rewrite ↑s_le,
|
|
|
|
|
apply exists.elim (rat_approx_l1 H m),
|
|
|
|
|
intro q Hq,
|
|
|
|
|
apply exists.elim Hq,
|
|
|
|
|
intro N HN,
|
|
|
|
|
existsi q,
|
|
|
|
|
apply nonneg_of_bdd_within,
|
|
|
|
|
repeat (apply reg_add_reg | apply reg_neg_reg | apply abs_reg_of_reg | apply const_reg
|
|
|
|
|
| assumption),
|
|
|
|
|
intro n,
|
|
|
|
|
existsi N,
|
|
|
|
|
intro p Hp,
|
|
|
|
|
rewrite ↑[sadd, sneg, s_abs, const],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply rat.sub_le_sub_left,
|
|
|
|
|
apply HN,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hp,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite -*pnat.mul.assoc,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply pnat.mul_le_mul_left,
|
|
|
|
|
rewrite [sub_self, -neg_zero],
|
|
|
|
|
apply neg_le_neg,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
definition r_abs (s : reg_seq) : reg_seq :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
reg_seq.mk (s_abs (reg_seq.sq s)) (abs_reg_of_reg (reg_seq.is_reg s))
|
|
|
|
|
|
|
|
|
|
theorem abs_well_defined {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
|
2015-06-10 02:46:30 +00:00
|
|
|
|
s_abs s ≡ s_abs t :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
rewrite [↑equiv at *],
|
|
|
|
|
intro n,
|
|
|
|
|
rewrite ↑s_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_abs_sub_abs_le_abs_sub,
|
|
|
|
|
apply Heq
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem r_abs_well_defined {s t : reg_seq} (H : requiv s t) : requiv (r_abs s) (r_abs t) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
abs_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) H
|
|
|
|
|
|
|
|
|
|
theorem r_rat_approx (s : reg_seq) :
|
2015-06-10 02:46:30 +00:00
|
|
|
|
∀ n : ℕ+, ∃ q : ℚ, r_le (r_abs (radd s (rneg (r_const q)))) (r_const n⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rat_approx (reg_seq.is_reg s)
|
|
|
|
|
|
|
|
|
|
theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) : s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite ↑[s_le, nonneg, s_abs, sadd, sneg, const],
|
|
|
|
|
intro m,
|
2015-06-09 06:14:52 +00:00
|
|
|
|
apply iff.mp !rat.le_add_iff_neg_le_sub_left,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply rat.add_le_add_right,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite -*pnat.mul.assoc,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply inv_ge_of_le,
|
|
|
|
|
apply pnat.mul_le_mul_left
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem abs_const (a : ℚ) : const (abs a) ≡ s_abs (const a) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑s_abs, ↑const],
|
|
|
|
|
apply equiv.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem r_abs_const (a : ℚ) : requiv (r_const (abs a) ) (r_abs (r_const a)) := abs_const a
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑const],
|
|
|
|
|
apply equiv.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem r_add_consts (a b : ℚ) : requiv (r_const a + r_const b) (r_const (a + b)) := add_consts a b
|
|
|
|
|
|
|
|
|
|
theorem const_le_const_of_le {a b : ℚ} (H : a ≤ b) : s_le (const a) (const b) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑s_le, ↑nonneg],
|
|
|
|
|
intro n,
|
|
|
|
|
rewrite [↑sadd, ↑sneg, ↑const],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.neg_nonpos_of_nonneg,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos,
|
|
|
|
|
apply iff.mp' !rat.sub_nonneg_iff_le,
|
|
|
|
|
apply H
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem le_of_const_le_const {a b : ℚ} (H : s_le (const a) (const b)) : a ≤ b :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑s_le at H, ↑nonneg at H, ↑sadd at H, ↑sneg at H, ↑const at H],
|
|
|
|
|
apply iff.mp !rat.sub_nonneg_iff_le,
|
|
|
|
|
apply nonneg_of_ge_neg_invs _ H
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem r_const_le_const_of_le {a b : ℚ} (H : a ≤ b) : r_le (r_const a) (r_const b) :=
|
|
|
|
|
const_le_const_of_le H
|
|
|
|
|
|
|
|
|
|
theorem r_le_of_const_le_const {a b : ℚ} (H : r_le (r_const a) (r_const b)) : a ≤ b :=
|
|
|
|
|
le_of_const_le_const H
|
|
|
|
|
|
|
|
|
|
theorem equiv_abs_of_ge_zero {s : seq} (Hs : regular s) (Hz : s_le zero s) : s_abs s ≡ s :=
|
2015-06-10 02:46:30 +00:00
|
|
|
|
begin
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply eq_of_bdd,
|
|
|
|
|
apply abs_reg_of_reg Hs,
|
|
|
|
|
apply Hs,
|
|
|
|
|
intro j,
|
|
|
|
|
rewrite ↑s_abs,
|
|
|
|
|
let Hz' := s_nonneg_of_ge_zero Hs Hz,
|
|
|
|
|
existsi 2 * j,
|
|
|
|
|
intro n Hn,
|
|
|
|
|
apply or.elim (decidable.em (s n ≥ 0)),
|
|
|
|
|
intro Hpos,
|
|
|
|
|
rewrite [rat.abs_of_nonneg Hpos, sub_self, abs_zero],
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos,
|
|
|
|
|
intro Hneg,
|
|
|
|
|
let Hneg' := lt_of_not_ge Hneg,
|
2015-06-10 02:46:30 +00:00
|
|
|
|
have Hsn : -s n - s n > 0, from add_pos (neg_pos_of_neg Hneg') (neg_pos_of_neg Hneg'),
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rewrite [rat.abs_of_neg Hneg', rat.abs_of_pos Hsn],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
repeat (apply rat.neg_le_neg; apply Hz'),
|
|
|
|
|
rewrite *rat.neg_neg,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
repeat (apply inv_ge_of_le; apply Hn),
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite pnat.add_halves,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem equiv_neg_abs_of_le_zero {s : seq} (Hs : regular s) (Hz : s_le s zero) : s_abs s ≡ sneg s :=
|
|
|
|
|
begin
|
|
|
|
|
apply eq_of_bdd,
|
|
|
|
|
apply abs_reg_of_reg Hs,
|
|
|
|
|
apply reg_neg_reg Hs,
|
|
|
|
|
intro j,
|
|
|
|
|
rewrite [↑s_abs, ↑s_le at Hz],
|
|
|
|
|
have Hz' : nonneg (sneg s), begin
|
|
|
|
|
apply nonneg_of_nonneg_equiv,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply Hz,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply s_zero_add,
|
|
|
|
|
repeat (apply Hs | apply zero_is_reg | apply reg_neg_reg | apply reg_add_reg)
|
|
|
|
|
end,
|
|
|
|
|
existsi 2 * j,
|
|
|
|
|
intro n Hn,
|
|
|
|
|
apply or.elim (decidable.em (s n ≥ 0)),
|
|
|
|
|
intro Hpos,
|
|
|
|
|
have Hsn : s n + s n ≥ 0, from add_nonneg Hpos Hpos,
|
|
|
|
|
rewrite [rat.abs_of_nonneg Hpos, ↑sneg, rat.sub_neg_eq_add, rat.abs_of_nonneg Hsn],
|
|
|
|
|
rewrite [↑nonneg at Hz', ↑sneg at Hz'],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
repeat apply (rat.le_of_neg_le_neg !Hz'),
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
repeat (apply inv_ge_of_le; apply Hn),
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite pnat.add_halves,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le.refl,
|
|
|
|
|
intro Hneg,
|
|
|
|
|
let Hneg' := lt_of_not_ge Hneg,
|
|
|
|
|
rewrite [rat.abs_of_neg Hneg', ↑sneg, rat.sub_neg_eq_add, rat.neg_add_eq_sub, rat.sub_self,
|
2015-06-10 02:46:30 +00:00
|
|
|
|
abs_zero],
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem r_equiv_abs_of_ge_zero {s : reg_seq} (Hz : r_le r_zero s) : requiv (r_abs s) s :=
|
2015-06-10 02:46:30 +00:00
|
|
|
|
equiv_abs_of_ge_zero (reg_seq.is_reg s) Hz
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
theorem r_equiv_neg_abs_of_le_zero {s : reg_seq} (Hz : r_le s r_zero) : requiv (r_abs s) (-s) :=
|
|
|
|
|
equiv_neg_abs_of_le_zero (reg_seq.is_reg s) Hz
|
|
|
|
|
|
|
|
|
|
end s
|
|
|
|
|
|
|
|
|
|
namespace real
|
|
|
|
|
|
2015-06-11 07:01:55 +00:00
|
|
|
|
theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ := sorry
|
|
|
|
|
|
2015-06-09 05:39:28 +00:00
|
|
|
|
theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) := sorry
|
|
|
|
|
|
|
|
|
|
theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) := sorry
|
|
|
|
|
|
|
|
|
|
definition rep (x : ℝ) : reg_seq := some (quot.exists_rep x)
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
definition const (a : ℚ) : ℝ := quot.mk (s.r_const a)
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem add_consts (a b : ℚ) : const a + const b = const (a + b) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
quot.sound (s.r_add_consts a b)
|
|
|
|
|
|
|
|
|
|
theorem sub_consts (a b : ℚ) : const a - const b = const (a - b) := !add_consts
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem add_half_const (n : ℕ+) : const (2 * n)⁻¹ + const (2 * n)⁻¹ = const (n⁻¹) :=
|
2015-06-16 04:55:02 +00:00
|
|
|
|
by rewrite [add_consts, pnat.add_halves]
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem const_le_const_of_le (a b : ℚ) : a ≤ b → const a ≤ const b :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
s.r_const_le_const_of_le
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem le_of_const_le_const (a b : ℚ) : const a ≤ const b → a ≤ b :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
s.r_le_of_const_le_const
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
definition re_abs (x : ℝ) : ℝ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
quot.lift_on x (λ a, quot.mk (s.r_abs a)) (take a b Hab, quot.sound (s.r_abs_well_defined Hab))
|
|
|
|
|
|
|
|
|
|
theorem r_abs_nonneg {x : ℝ} : 0 ≤ x → re_abs x = x :=
|
|
|
|
|
quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_abs_of_ge_zero Ha))
|
|
|
|
|
|
|
|
|
|
theorem r_abs_nonpos {x : ℝ} : x ≤ 0 → re_abs x = -x :=
|
|
|
|
|
quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_neg_abs_of_le_zero Ha))
|
|
|
|
|
|
|
|
|
|
theorem abs_const' (a : ℚ) : const (rat.abs a) = re_abs (const a) := quot.sound (s.r_abs_const a)
|
|
|
|
|
|
|
|
|
|
theorem re_abs_is_abs : re_abs = algebra.abs := funext
|
|
|
|
|
(begin
|
|
|
|
|
intro x,
|
|
|
|
|
rewrite ↑abs,
|
|
|
|
|
apply eq.symm,
|
|
|
|
|
let Hor := decidable.em (0 ≤ x),
|
|
|
|
|
apply or.elim Hor,
|
|
|
|
|
intro Hor1,
|
|
|
|
|
rewrite [(if_pos Hor1), r_abs_nonneg Hor1],
|
|
|
|
|
intro Hor2,
|
|
|
|
|
let Hor2' := algebra.le_of_lt (algebra.lt_of_not_ge Hor2),
|
|
|
|
|
rewrite [(if_neg Hor2), r_abs_nonpos Hor2']
|
|
|
|
|
end)
|
|
|
|
|
|
|
|
|
|
theorem abs_const (a : ℚ) : const (rat.abs a) = abs (const a) :=
|
|
|
|
|
by rewrite -re_abs_is_abs -- ????
|
|
|
|
|
|
|
|
|
|
theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - const q) ≤ const n⁻¹ :=
|
|
|
|
|
quot.induction_on x (λ s n, s.r_rat_approx s n)
|
|
|
|
|
|
|
|
|
|
theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - const q) ≤ const n⁻¹ :=
|
|
|
|
|
by rewrite -re_abs_is_abs; apply rat_approx'
|
|
|
|
|
|
|
|
|
|
definition approx (x : ℝ) (n : ℕ+) := some (rat_approx x n)
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (const (approx x n))) ≤ const n⁻¹ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
some_spec (rat_approx x n)
|
|
|
|
|
|
|
|
|
|
theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((const (approx x n)) - x) ≤ const n⁻¹ :=
|
|
|
|
|
by rewrite algebra.abs_sub; apply approx_spec
|
|
|
|
|
|
|
|
|
|
notation `r_seq` := ℕ+ → ℝ
|
|
|
|
|
|
|
|
|
|
definition converges_to (X : r_seq) (a : ℝ) (N : ℕ+ → ℕ+) :=
|
|
|
|
|
∀ k : ℕ+, ∀ n : ℕ+, n ≥ N k → abs (X n - a) ≤ const k⁻¹
|
|
|
|
|
|
|
|
|
|
definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) :=
|
|
|
|
|
∀ k : ℕ+, ∀ m n : ℕ+, m ≥ M k → n ≥ M k → abs (X m - X n) ≤ const k⁻¹
|
|
|
|
|
|
|
|
|
|
theorem cauchy_of_converges_to {X : r_seq} {a : ℝ} {N : ℕ+ → ℕ+} (Hc : converges_to X a N) :
|
|
|
|
|
cauchy X (λ k, N (2 * k)) :=
|
|
|
|
|
begin
|
2015-06-10 02:46:30 +00:00
|
|
|
|
intro k m n Hm Hn,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rewrite (rewrite_helper9 a),
|
|
|
|
|
apply algebra.le.trans,
|
|
|
|
|
apply algebra.abs_add_le_abs_add_abs,
|
|
|
|
|
apply algebra.le.trans,
|
|
|
|
|
apply algebra.add_le_add,
|
|
|
|
|
apply Hc,
|
|
|
|
|
apply Hm,
|
|
|
|
|
rewrite algebra.abs_neg,
|
|
|
|
|
apply Hc,
|
|
|
|
|
apply Hn,
|
|
|
|
|
rewrite add_half_const,
|
|
|
|
|
apply !algebra.le.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition Nb (M : ℕ+ → ℕ+) := λ k, max (3 * k) (M (2 * k))
|
|
|
|
|
|
|
|
|
|
theorem Nb_spec_right (M : ℕ+ → ℕ+) (k : ℕ+) : M (2 * k) ≤ Nb M k := !max_right
|
|
|
|
|
|
|
|
|
|
theorem Nb_spec_left (M : ℕ+ → ℕ+) (k : ℕ+) : 3 * k ≤ Nb M k := !max_left
|
|
|
|
|
|
|
|
|
|
definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : seq :=
|
|
|
|
|
λ k, approx (X (Nb M k)) (2 * k)
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem lim_seq_reg_helper {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) {m n : ℕ+}
|
2015-06-09 05:39:28 +00:00
|
|
|
|
(Hmn : M (2 * n) ≤M (2 * m)) :
|
|
|
|
|
abs (const (lim_seq Hc m) - X (Nb M m)) + abs (X (Nb M m) - X (Nb M n)) + abs
|
|
|
|
|
(X (Nb M n) - const (lim_seq Hc n)) ≤ const (m⁻¹ + n⁻¹) :=
|
|
|
|
|
begin
|
|
|
|
|
apply algebra.le.trans,
|
2015-06-10 02:46:30 +00:00
|
|
|
|
apply algebra.add_le_add_three,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply approx_spec',
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply approx_spec,
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply Hc,
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply Nb_spec_right,
|
|
|
|
|
rotate 1,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hmn,
|
|
|
|
|
apply Nb_spec_right,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [*add_consts, rat.add.assoc, pnat.add_halves],
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply const_le_const_of_le,
|
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply inv_ge_of_le,
|
|
|
|
|
apply pnat.mul_le_mul_left
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : regular (lim_seq Hc) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
rewrite ↑regular,
|
|
|
|
|
intro m n,
|
|
|
|
|
apply le_of_const_le_const,
|
|
|
|
|
rewrite [abs_const, -sub_consts, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
|
|
|
|
|
apply algebra.le.trans,
|
2015-06-10 02:46:30 +00:00
|
|
|
|
apply algebra.abs_add_three,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
let Hor := decidable.em (M (2 * m) ≥ M (2 * n)),
|
|
|
|
|
apply or.elim Hor,
|
|
|
|
|
intro Hor1,
|
|
|
|
|
apply lim_seq_reg_helper Hc Hor1,
|
|
|
|
|
intro Hor2,
|
|
|
|
|
let Hor2' := pnat.le_of_lt (pnat.lt_of_not_le Hor2),
|
|
|
|
|
rewrite [algebra.abs_sub (X (Nb M n)), algebra.abs_sub (X (Nb M m)), algebra.abs_sub, -- ???
|
2015-06-09 06:14:52 +00:00
|
|
|
|
rat.add.comm, algebra.add_comm_three],
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply lim_seq_reg_helper Hc Hor2'
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
|
2015-06-09 05:39:28 +00:00
|
|
|
|
s.s_le (s.s_abs (sadd (lim_seq Hc) (sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) :=
|
|
|
|
|
begin
|
|
|
|
|
apply s.const_bound,
|
|
|
|
|
apply lim_seq_reg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : reg_seq :=
|
|
|
|
|
reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc)
|
|
|
|
|
|
|
|
|
|
theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
|
2015-06-10 02:46:30 +00:00
|
|
|
|
s.r_le (s.r_abs (((r_lim_seq Hc) + -s.r_const ((reg_seq.sq (r_lim_seq Hc)) k)))) (s.r_const (k)⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
lim_seq_spec Hc k
|
|
|
|
|
|
|
|
|
|
definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ :=
|
|
|
|
|
quot.mk (r_lim_seq Hc)
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem re_lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
2015-06-09 05:39:28 +00:00
|
|
|
|
re_abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
|
2015-06-10 02:46:30 +00:00
|
|
|
|
r_lim_seq_spec Hc k
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem lim_spec' {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
2015-06-09 05:39:28 +00:00
|
|
|
|
abs ((lim Hc) - (const ((lim_seq Hc) k))) ≤ const k⁻¹ :=
|
|
|
|
|
by rewrite -re_abs_is_abs; apply re_lim_spec
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem lim_spec {x : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy x M) (k : ℕ+) :
|
2015-06-09 05:39:28 +00:00
|
|
|
|
abs ((const ((lim_seq Hc) k)) - (lim Hc)) ≤ const (k)⁻¹ :=
|
|
|
|
|
by rewrite algebra.abs_sub; apply lim_spec'
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem converges_of_cauchy {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) :
|
|
|
|
|
converges_to X (lim Hc) (Nb M) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
intro k n Hn,
|
|
|
|
|
rewrite (rewrite_helper10 (X (Nb M n)) (const (lim_seq Hc n))),
|
|
|
|
|
apply algebra.le.trans,
|
2015-06-09 06:14:52 +00:00
|
|
|
|
apply algebra.abs_add_three,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply algebra.le.trans,
|
2015-06-09 06:14:52 +00:00
|
|
|
|
apply algebra.add_le_add_three,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hc,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rotate 1,
|
|
|
|
|
apply Hn,
|
|
|
|
|
rotate_right 1,
|
|
|
|
|
apply Nb_spec_right,
|
|
|
|
|
have HMk : M (2 * k) ≤ Nb M n, begin
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Nb_spec_right,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hn,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
|
|
|
|
apply mul_le_mul_left 3,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Nb_spec_left
|
|
|
|
|
end,
|
|
|
|
|
apply HMk,
|
|
|
|
|
rewrite ↑lim_seq,
|
|
|
|
|
apply approx_spec,
|
|
|
|
|
apply lim_spec,
|
|
|
|
|
rewrite 2 add_consts,
|
|
|
|
|
apply const_le_const_of_le,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply add_le_add_three,
|
|
|
|
|
apply rat.le.refl,
|
|
|
|
|
apply inv_ge_of_le,
|
|
|
|
|
apply pnat_mul_le_mul_left',
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rotate 1,
|
|
|
|
|
apply Hn,
|
|
|
|
|
rotate_right 1,
|
|
|
|
|
apply Nb_spec_left,
|
|
|
|
|
apply inv_ge_of_le,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply pnat.le.trans,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
rotate 1,
|
|
|
|
|
apply Hn,
|
|
|
|
|
rotate_right 1,
|
|
|
|
|
apply Nb_spec_left,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [-*pnat.mul.assoc, p_add_fractions],
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
end real
|