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 06:55:06 +00:00
|
|
|
|
import data.real.basic data.real.order data.real.division data.rat data.nat data.pnat
|
2015-07-29 20:30:18 +00:00
|
|
|
|
import logic.choice
|
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 eq.ops
|
2015-06-16 04:55:02 +00:00
|
|
|
|
open pnat
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
local notation 2 := subtype.tag (nat.of_num 2) dec_trivial
|
|
|
|
|
local notation 3 := subtype.tag (nat.of_num 3) dec_trivial
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
namespace s
|
|
|
|
|
|
|
|
|
|
|
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)
|
|
|
|
|
|
2015-06-23 12:17:50 +00:00
|
|
|
|
theorem const_bound {s : seq} (Hs : regular s) (n : ℕ+) :
|
|
|
|
|
s_le (s_abs (sadd s (sneg (const (s n))))) (const n⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
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
|
|
|
|
|
|
|
|
|
|
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-23 12:17:50 +00:00
|
|
|
|
open [classes] s
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
theorem p_add_fractions (n : ℕ+) : (2 * n)⁻¹ + (2 * 3 * n)⁻¹ + (3 * n)⁻¹ = n⁻¹ :=
|
|
|
|
|
assert T : 2⁻¹ + 2⁻¹ * 3⁻¹ + 3⁻¹ = 1, from dec_trivial,
|
|
|
|
|
by rewrite[*inv_mul_eq_mul_inv,-*rat.right_distrib,T,rat.one_mul]
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
theorem rewrite_helper9 (a b c : ℝ) : b - c = (b - a) - (c - a) :=
|
|
|
|
|
by rewrite[-sub_add_eq_sub_sub_swap,sub_add_cancel]
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
theorem rewrite_helper10 (a b c d : ℝ) : c - d = (c - a) + (a - b) + (b - d) :=
|
|
|
|
|
by rewrite[*add_sub,*sub_add_cancel]
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition rep (x : ℝ) : s.reg_seq := some (quot.exists_rep x)
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-29 15:28:40 +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))
|
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
theorem r_abs_nonneg {x : ℝ} : zero ≤ x → re_abs x = x :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_abs_of_ge_zero Ha))
|
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
theorem r_abs_nonpos {x : ℝ} : x ≤ zero → re_abs x = -x :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
quot.induction_on x (λ a Ha, quot.sound (s.r_equiv_neg_abs_of_le_zero Ha))
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem abs_const' (a : ℚ) : of_rat (rat.abs a) = re_abs (of_rat a) := quot.sound (s.r_abs_const a)
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
theorem re_abs_is_abs : re_abs = real.abs := funext
|
2015-06-09 05:39:28 +00:00
|
|
|
|
(begin
|
|
|
|
|
intro x,
|
|
|
|
|
apply eq.symm,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
let Hor := decidable.em (zero ≤ x),
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply or.elim Hor,
|
|
|
|
|
intro Hor1,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
rewrite [abs_of_nonneg Hor1, r_abs_nonneg Hor1],
|
2015-06-09 05:39:28 +00:00
|
|
|
|
intro Hor2,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
have Hor2' : x ≤ zero, from le_of_lt (lt_of_not_ge Hor2),
|
|
|
|
|
rewrite [abs_of_neg (lt_of_not_ge Hor2), r_abs_nonpos Hor2']
|
2015-06-09 05:39:28 +00:00
|
|
|
|
end)
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem abs_const (a : ℚ) : of_rat (rat.abs a) = abs (of_rat a) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
by rewrite -re_abs_is_abs -- ????
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem rat_approx' (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, re_abs (x - of_rat q) ≤ of_rat n⁻¹ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
quot.induction_on x (λ s n, s.r_rat_approx s n)
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem rat_approx (x : ℝ) : ∀ n : ℕ+, ∃ q : ℚ, abs (x - of_rat q) ≤ of_rat n⁻¹ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
by rewrite -re_abs_is_abs; apply rat_approx'
|
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition approx (x : ℝ) (n : ℕ+) := some (rat_approx x n)
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (of_rat (approx x n))) ≤ of_rat n⁻¹ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
some_spec (rat_approx x n)
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((of_rat (approx x n)) - x) ≤ of_rat n⁻¹ :=
|
2015-06-24 07:14:31 +00:00
|
|
|
|
by rewrite abs_sub; apply approx_spec
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
notation `r_seq` := ℕ+ → ℝ
|
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition converges_to (X : r_seq) (a : ℝ) (N : ℕ+ → ℕ+) :=
|
2015-07-16 17:18:35 +00:00
|
|
|
|
∀ k : ℕ+, ∀ n : ℕ+, n ≥ N k → abs (X n - a) ≤ of_rat k⁻¹
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition cauchy (X : r_seq) (M : ℕ+ → ℕ+) :=
|
2015-07-16 17:18:35 +00:00
|
|
|
|
∀ k : ℕ+, ∀ m n : ℕ+, m ≥ M k → n ≥ M k → abs (X m - X n) ≤ of_rat k⁻¹
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-06-09 05:39:28 +00:00
|
|
|
|
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),
|
2015-06-24 07:14:31 +00:00
|
|
|
|
apply le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply le.trans,
|
|
|
|
|
apply add_le_add,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hc,
|
|
|
|
|
apply Hm,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
krewrite abs_neg,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply Hc,
|
|
|
|
|
apply Hn,
|
2015-07-16 17:18:35 +00:00
|
|
|
|
xrewrite of_rat_add,
|
|
|
|
|
apply of_rat_le_of_rat_of_le,
|
|
|
|
|
rewrite pnat.add_halves,
|
|
|
|
|
apply rat.le.refl
|
2015-06-09 05:39:28 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
definition Nb (M : ℕ+ → ℕ+) := λ k, pnat.max (3 * k) (M (2 * k))
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
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
|
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℕ+ → ℚ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
λ 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)) :
|
2015-07-16 17:18:35 +00:00
|
|
|
|
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⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
2015-06-24 07:14:31 +00:00
|
|
|
|
apply le.trans,
|
|
|
|
|
apply 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-07-16 17:18:35 +00:00
|
|
|
|
rewrite [*of_rat_add, rat.add.assoc, pnat.add_halves],
|
|
|
|
|
apply of_rat_le_of_rat_of_le,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply inv_ge_of_le,
|
|
|
|
|
apply pnat.mul_le_mul_left
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
theorem lim_seq_reg {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.regular (lim_seq Hc) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
2015-06-23 12:17:50 +00:00
|
|
|
|
rewrite ↑s.regular,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
intro m n,
|
2015-07-16 17:18:35 +00:00
|
|
|
|
apply le_of_rat_le_of_rat,
|
2015-07-27 21:49:26 +00:00
|
|
|
|
rewrite [abs_const, -of_rat_sub, (rewrite_helper10 (X (Nb M m)) (X (Nb M n)))],
|
2015-06-23 12:17:50 +00:00
|
|
|
|
apply real.le.trans,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
apply 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),
|
2015-06-24 07:14:31 +00:00
|
|
|
|
rewrite [real.abs_sub (X (Nb M n)), abs_sub (X (Nb M m)), abs_sub, -- ???
|
|
|
|
|
rat.add.comm, 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-23 12:17:50 +00:00
|
|
|
|
s.s_le (s.s_abs (s.sadd (lim_seq Hc) (s.sneg (s.const (lim_seq Hc k))) )) (s.const k⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
begin
|
|
|
|
|
apply s.const_bound,
|
|
|
|
|
apply lim_seq_reg
|
|
|
|
|
end
|
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition r_lim_seq {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : s.reg_seq :=
|
2015-06-23 12:17:50 +00:00
|
|
|
|
s.reg_seq.mk (lim_seq Hc) (lim_seq_reg Hc)
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
|
|
|
|
theorem r_lim_seq_spec {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) (k : ℕ+) :
|
2015-06-23 12:17:50 +00:00
|
|
|
|
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)⁻¹) :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
lim_seq_spec Hc k
|
|
|
|
|
|
2015-07-29 04:56:35 +00:00
|
|
|
|
noncomputable definition lim {X : r_seq} {M : ℕ+ → ℕ+} (Hc : cauchy X M) : ℝ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
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-07-16 17:18:35 +00:00
|
|
|
|
re_abs ((lim Hc) - (of_rat ((lim_seq Hc) k))) ≤ of_rat 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-07-16 17:18:35 +00:00
|
|
|
|
abs ((lim Hc) - (of_rat ((lim_seq Hc) k))) ≤ of_rat k⁻¹ :=
|
2015-06-09 05:39:28 +00:00
|
|
|
|
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-07-16 17:18:35 +00:00
|
|
|
|
abs ((of_rat ((lim_seq Hc) k)) - (lim Hc)) ≤ of_rat (k)⁻¹ :=
|
2015-06-24 07:14:31 +00:00
|
|
|
|
by rewrite abs_sub; apply lim_spec'
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
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,
|
2015-07-16 17:18:35 +00:00
|
|
|
|
rewrite (rewrite_helper10 (X (Nb M n)) (of_rat (lim_seq Hc n))),
|
2015-06-24 07:14:31 +00:00
|
|
|
|
apply le.trans,
|
|
|
|
|
apply abs_add_three,
|
|
|
|
|
apply le.trans,
|
|
|
|
|
apply 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,
|
2015-07-16 17:18:35 +00:00
|
|
|
|
rewrite 2 of_rat_add,
|
|
|
|
|
apply of_rat_le_of_rat_of_le,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
apply rat.le.trans,
|
2015-06-24 07:14:31 +00:00
|
|
|
|
apply rat.add_le_add_three,
|
2015-06-09 05:39:28 +00:00
|
|
|
|
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
|
2015-06-24 07:14:31 +00:00
|
|
|
|
end
|
2015-06-09 05:39:28 +00:00
|
|
|
|
|
2015-07-27 15:11:14 +00:00
|
|
|
|
--------------------------------------------------
|
|
|
|
|
-- archimedean property
|
|
|
|
|
|
|
|
|
|
theorem archimedean (x y : ℝ) (Hx : x > 0) (Hy : y > 0) : ∃ n : ℕ, (of_rat (of_nat n)) * x ≥ y := sorry
|
|
|
|
|
|
|
|
|
|
--------------------------------------------------
|
|
|
|
|
-- supremum property
|
|
|
|
|
|
|
|
|
|
section supremum
|
|
|
|
|
open prod nat
|
2015-07-27 21:49:26 +00:00
|
|
|
|
local postfix `~` := nat_of_pnat
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
local notation 2 := (1 : ℚ) + 1
|
|
|
|
|
parameter X : ℝ → Prop
|
|
|
|
|
|
|
|
|
|
definition rpt {A : Type} (op : A → A) : ℕ → A → A
|
|
|
|
|
| rpt 0 := λ a, a
|
|
|
|
|
| rpt (succ k) := λ a, ((rpt k) (op a))
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
definition ub (x : ℝ) := ∀ y : ℝ, X y → y ≤ x
|
|
|
|
|
definition bounded := ∃ x : ℝ, ub x
|
2015-07-27 21:49:26 +00:00
|
|
|
|
definition sup (x : ℝ) := ub x ∧ ∀ y : ℝ, ub y → x ≤ y
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
|
|
|
|
|
parameter elt : ℝ
|
|
|
|
|
hypothesis inh : X elt
|
|
|
|
|
parameter bound : ℝ
|
|
|
|
|
hypothesis bdd : ub bound
|
|
|
|
|
|
|
|
|
|
parameter floor : ℝ → int
|
|
|
|
|
parameter ceil : ℝ → int
|
2015-07-28 03:28:35 +00:00
|
|
|
|
hypothesis floor_spec : ∀ x : ℝ, of_rat (of_int (floor x)) ≤ x
|
|
|
|
|
hypothesis ceil_spec : ∀ x : ℝ, of_rat (of_int (ceil x)) ≥ x
|
|
|
|
|
hypothesis floor_succ : ∀ x : ℝ, int.lt (floor (x - 1)) (floor x)
|
|
|
|
|
hypothesis ceil_succ : ∀ x : ℝ, int.lt (ceil x) (ceil (x + 1))
|
|
|
|
|
|
|
|
|
|
include inh bdd floor_spec ceil_spec floor_succ ceil_succ
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
definition avg (a b : ℚ) := a / 2 + b / 2
|
|
|
|
|
|
|
|
|
|
definition bisect (ab : ℚ × ℚ) :=
|
|
|
|
|
if ub (avg (pr1 ab) (pr2 ab)) then
|
|
|
|
|
(pr1 ab, (avg (pr1 ab) (pr2 ab)))
|
|
|
|
|
else
|
|
|
|
|
(avg (pr1 ab) (pr2 ab), pr2 ab)
|
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
set_option pp.coercions true
|
|
|
|
|
|
2015-07-27 15:11:14 +00:00
|
|
|
|
definition under : ℚ := of_int (floor (elt - 1))
|
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem under_spec1 : of_rat under < elt :=
|
|
|
|
|
let fs := floor_succ in
|
|
|
|
|
have H : of_rat under < of_rat (of_int (floor elt)), begin
|
|
|
|
|
apply of_rat_lt_of_rat_of_lt,
|
|
|
|
|
apply iff.mpr !of_int_lt_of_int,
|
|
|
|
|
apply fs
|
|
|
|
|
end,
|
|
|
|
|
lt_of_lt_of_le H !floor_spec
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
theorem not_forall_of_exists_not {A : Type} {P : A → Prop} (H : ∃ a : A, ¬ P a) : ¬ ∀ a : A, P a := sorry
|
|
|
|
|
|
|
|
|
|
theorem under_spec : ¬ ub under :=
|
|
|
|
|
using inh,
|
|
|
|
|
using floor_spec,
|
|
|
|
|
using floor_succ,
|
|
|
|
|
begin
|
|
|
|
|
rewrite ↑ub,
|
|
|
|
|
apply not_forall_of_exists_not,
|
|
|
|
|
existsi elt,
|
|
|
|
|
apply iff.mpr not_implies_iff_and_not,
|
|
|
|
|
apply and.intro,
|
|
|
|
|
apply inh,
|
|
|
|
|
apply not_le_of_gt under_spec1
|
|
|
|
|
end
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
definition over : ℚ := of_int (ceil (bound + 1)) -- b
|
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem over_spec1 : bound < of_rat over :=
|
|
|
|
|
let cs := ceil_succ in
|
|
|
|
|
have H : of_rat (of_int (ceil bound)) < of_rat over, begin
|
|
|
|
|
apply of_rat_lt_of_rat_of_lt,
|
|
|
|
|
apply iff.mpr !of_int_lt_of_int,
|
|
|
|
|
apply cs
|
|
|
|
|
end,
|
|
|
|
|
lt_of_le_of_lt !ceil_spec H
|
|
|
|
|
|
|
|
|
|
theorem over_spec : ub over :=
|
|
|
|
|
using bdd,
|
|
|
|
|
using ceil_spec,
|
|
|
|
|
using ceil_succ,
|
|
|
|
|
begin
|
|
|
|
|
rewrite ↑ub,
|
|
|
|
|
intro y Hy,
|
|
|
|
|
apply le_of_lt,
|
|
|
|
|
apply lt_of_le_of_lt,
|
|
|
|
|
apply bdd,
|
|
|
|
|
apply Hy,
|
|
|
|
|
apply over_spec1
|
|
|
|
|
end
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
definition under_seq := λ n : ℕ, pr1 (rpt bisect n (under, over)) -- A
|
|
|
|
|
|
|
|
|
|
definition over_seq := λ n : ℕ, pr2 (rpt bisect n (under, over)) -- B
|
|
|
|
|
|
|
|
|
|
definition avg_seq := λ n : ℕ, avg (over_seq n) (under_seq n) -- C
|
|
|
|
|
|
|
|
|
|
theorem over_0 : over_seq 0 = over := rfl
|
|
|
|
|
theorem under_0 : under_seq 0 = under := rfl
|
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem under_succ (n : ℕ) : under_seq (succ n) =
|
|
|
|
|
(if ub (avg_seq n) then under_seq n else avg_seq n) := sorry
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem over_succ (n : ℕ) : over_seq (succ n) =
|
|
|
|
|
(if ub (avg_seq n) then avg_seq n else over_seq n) := sorry
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
theorem rat.pow_zero (a : ℚ) : rat.pow a 0 = 1 := sorry
|
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem rat.pow_pos {a : ℚ} (H : a > 0) (n : ℕ) : rat.pow a n > 0 := sorry
|
|
|
|
|
|
2015-07-27 15:11:14 +00:00
|
|
|
|
theorem width (n : ℕ) : over_seq n - under_seq n = (over - under) / (rat.pow 2 n) :=
|
|
|
|
|
nat.induction_on n
|
|
|
|
|
(by rewrite [over_0, under_0, rat.pow_zero, rat.div_one])
|
|
|
|
|
(begin
|
|
|
|
|
intro a Ha,
|
|
|
|
|
rewrite [over_succ, under_succ],
|
|
|
|
|
cases (decidable.em (ub (avg_seq a))),
|
|
|
|
|
rewrite [*if_pos a_1],
|
|
|
|
|
apply sorry,
|
|
|
|
|
rewrite [*if_neg a_1],
|
|
|
|
|
apply sorry
|
|
|
|
|
end)
|
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem binary_bound (a : ℚ) : ∃ n : ℕ, a ≤ rat.pow 2 n := sorry
|
|
|
|
|
|
|
|
|
|
theorem width_narrows : ∃ n : ℕ, over_seq n - under_seq n ≤ 1 :=
|
|
|
|
|
begin
|
|
|
|
|
cases binary_bound (over - under) with [a, Ha],
|
|
|
|
|
existsi a,
|
|
|
|
|
rewrite (width a),
|
|
|
|
|
apply rat.div_le_of_le_mul,
|
|
|
|
|
apply rat.pow_pos dec_trivial,
|
|
|
|
|
rewrite rat.mul_one,
|
|
|
|
|
apply Ha
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition over' := over_seq (some width_narrows)
|
|
|
|
|
|
|
|
|
|
definition under' := under_seq (some width_narrows)
|
|
|
|
|
|
|
|
|
|
definition over_seq' := λ n, over_seq (n + some width_narrows)
|
|
|
|
|
|
|
|
|
|
definition under_seq' := λ n, under_seq (n + some width_narrows)
|
|
|
|
|
|
|
|
|
|
theorem width' (n : ℕ) : over_seq' n - under_seq' n ≤ 1 / rat.pow 2 n := sorry
|
|
|
|
|
|
2015-07-27 22:33:34 +00:00
|
|
|
|
--theorem twos (y r : ℚ) (H : 0 < r) : ∃ n : ℕ, y / (rat.pow 2 n) < r := sorry
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
|
|
|
|
theorem PA (n : ℕ) : ¬ ub (under_seq n) :=
|
|
|
|
|
nat.induction_on n
|
|
|
|
|
(by rewrite under_0; apply under_spec)
|
|
|
|
|
(begin
|
|
|
|
|
intro a Ha,
|
|
|
|
|
rewrite under_succ,
|
|
|
|
|
cases (decidable.em (ub (avg_seq a))),
|
|
|
|
|
rewrite (if_pos a_1),
|
|
|
|
|
assumption,
|
|
|
|
|
rewrite (if_neg a_1),
|
|
|
|
|
assumption
|
|
|
|
|
end)
|
|
|
|
|
|
|
|
|
|
theorem PB (n : ℕ) : ub (over_seq n) :=
|
|
|
|
|
nat.induction_on n
|
|
|
|
|
(by rewrite over_0; apply over_spec)
|
|
|
|
|
(begin
|
|
|
|
|
intro a Ha,
|
|
|
|
|
rewrite over_succ,
|
|
|
|
|
cases (decidable.em (ub (avg_seq a))),
|
|
|
|
|
rewrite (if_pos a_1),
|
|
|
|
|
assumption,
|
|
|
|
|
rewrite (if_neg a_1),
|
|
|
|
|
assumption
|
|
|
|
|
end)
|
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem under_lt_over : under < over :=
|
|
|
|
|
begin
|
|
|
|
|
cases (exists_not_of_not_forall under_spec) with [x, Hx],
|
|
|
|
|
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,
|
|
|
|
|
apply over_spec _ HXx
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
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],
|
|
|
|
|
apply lt_of_rat_lt_of_rat,
|
|
|
|
|
apply lt_of_lt_of_le,
|
|
|
|
|
apply lt_of_not_ge Hxu,
|
|
|
|
|
apply PB,
|
|
|
|
|
apply HXx
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem under_seq_lt_over_seq_single : ∀ n : ℕ, under_seq n < over_seq n :=
|
|
|
|
|
by intros; apply under_seq_lt_over_seq
|
|
|
|
|
|
|
|
|
|
theorem under_seq'_lt_over_seq' : ∀ m n : ℕ, under_seq' m < over_seq' n :=
|
|
|
|
|
by intros; apply under_seq_lt_over_seq
|
|
|
|
|
|
|
|
|
|
theorem under_seq'_lt_over_seq'_single : ∀ n : ℕ, under_seq' n < over_seq' n :=
|
|
|
|
|
by intros; apply under_seq_lt_over_seq
|
|
|
|
|
|
|
|
|
|
--theorem over_dist (n : ℕ) : abs (over - over_seq n) ≤ (over - under) / rat.pow 2 n := sorry
|
|
|
|
|
|
2015-07-27 22:33:34 +00:00
|
|
|
|
theorem under_seq_mono_helper (i k : ℕ) : under_seq i ≤ under_seq (i + k) :=
|
|
|
|
|
(nat.induction_on k
|
|
|
|
|
(by rewrite nat.add_zero; apply rat.le.refl)
|
|
|
|
|
(begin
|
|
|
|
|
intros a Ha,
|
|
|
|
|
rewrite [add_succ, under_succ],
|
|
|
|
|
cases (decidable.em (ub (avg_seq (i + a)))) with [Havg, Havg],
|
|
|
|
|
rewrite (if_pos Havg),
|
|
|
|
|
apply Ha,
|
|
|
|
|
rewrite [if_neg Havg, ↑avg_seq, ↑avg],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply Ha,
|
|
|
|
|
rewrite -rat.add_halves at {1},
|
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply rat.div_le_div_of_le_of_pos,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply under_seq_lt_over_seq,
|
|
|
|
|
apply dec_trivial
|
|
|
|
|
end))
|
|
|
|
|
|
|
|
|
|
theorem under_seq_mono (i j : ℕ) (H : i ≤ j) : under_seq i ≤ under_seq j :=
|
|
|
|
|
begin
|
|
|
|
|
cases le.elim H with [k, Hk'],
|
|
|
|
|
rewrite -Hk',
|
|
|
|
|
apply under_seq_mono_helper
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem over_seq_mono_helper (i k : ℕ) : over_seq (i + k) ≤ over_seq i :=
|
|
|
|
|
nat.induction_on k
|
|
|
|
|
(by rewrite nat.add_zero; apply rat.le.refl)
|
|
|
|
|
(begin
|
|
|
|
|
intros a Ha,
|
|
|
|
|
rewrite [add_succ, over_succ],
|
|
|
|
|
cases (decidable.em (ub (avg_seq (i + a)))) with [Havg, Havg],
|
|
|
|
|
rewrite [if_pos Havg, ↑avg_seq, ↑avg],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply Ha,
|
|
|
|
|
rotate 1,
|
|
|
|
|
rewrite -{over_seq (i + a)}rat.add_halves at {2},
|
|
|
|
|
apply rat.add_le_add_left,
|
|
|
|
|
apply rat.div_le_div_of_le_of_pos,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply under_seq_lt_over_seq,
|
|
|
|
|
apply dec_trivial,
|
|
|
|
|
rewrite [if_neg Havg],
|
|
|
|
|
apply Ha
|
|
|
|
|
end)
|
|
|
|
|
|
|
|
|
|
theorem over_seq_mono (i j : ℕ) (H : i ≤ j) : over_seq j ≤ over_seq i :=
|
|
|
|
|
begin
|
|
|
|
|
cases le.elim H with [k, Hk'],
|
|
|
|
|
rewrite -Hk',
|
|
|
|
|
apply over_seq_mono_helper
|
|
|
|
|
end
|
2015-07-27 21:49:26 +00:00
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem rat_of_pnat_add {k : ℕ} (H : succ k > 0) : rat_of_pnat (subtype.tag (succ k) H) = (rat.of_nat k) + 1 := sorry
|
|
|
|
|
|
|
|
|
|
theorem rat_power_two_le (k : ℕ+) : rat_of_pnat k ≤ rat.pow 2 k~ :=
|
|
|
|
|
begin
|
|
|
|
|
apply subtype.rec_on k,
|
|
|
|
|
intros n Hn,
|
|
|
|
|
induction n,
|
|
|
|
|
apply absurd Hn !nat.not_lt_self,
|
|
|
|
|
rewrite (rat_of_pnat_add Hn),
|
|
|
|
|
apply sorry
|
|
|
|
|
end
|
2015-07-27 21:49:26 +00:00
|
|
|
|
|
2015-07-28 03:28:35 +00:00
|
|
|
|
theorem rat_power_two_inv_ge (k : ℕ+) : 1 / rat.pow 2 k~ ≤ k⁻¹ :=
|
|
|
|
|
rat.div_le_div_of_le !rat_of_pnat_is_pos !rat_power_two_le
|
2015-07-27 21:49:26 +00:00
|
|
|
|
|
|
|
|
|
open s
|
|
|
|
|
theorem regular_lemma_helper {s : seq} {m n : ℕ+} (Hm : m ≤ n)
|
2015-07-28 03:28:35 +00:00
|
|
|
|
(H : ∀ n i : ℕ+, i ≥ n → under_seq' n~ ≤ s i ∧ s i ≤ over_seq' n~) :
|
|
|
|
|
rat.abs (s m - s n) ≤ m⁻¹ + n⁻¹ :=
|
2015-07-27 21:49:26 +00:00
|
|
|
|
begin
|
|
|
|
|
cases (H m n Hm) with [T1under, T1over],
|
|
|
|
|
cases (H m m (!pnat.le.refl)) with [T2under, T2over],
|
|
|
|
|
apply rat.le.trans,
|
2015-07-28 04:49:51 +00:00
|
|
|
|
apply rat.dist_bdd_within_interval,
|
2015-07-27 21:49:26 +00:00
|
|
|
|
apply under_seq'_lt_over_seq'_single,
|
|
|
|
|
rotate 1,
|
|
|
|
|
repeat assumption,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply width',
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat_power_two_inv_ge,
|
|
|
|
|
apply rat.le_add_of_nonneg_right,
|
|
|
|
|
apply rat.le_of_lt (!inv_pos)
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem regular_lemma (s : seq) (H : ∀ n i : ℕ+, i ≥ n → under_seq' n~ ≤ s i ∧ s i ≤ over_seq' n~) :
|
|
|
|
|
regular s :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite ↑regular,
|
|
|
|
|
intros,
|
|
|
|
|
cases (decidable.em (m ≤ n)) with [Hm, Hn],
|
|
|
|
|
apply regular_lemma_helper Hm H,
|
|
|
|
|
let T := regular_lemma_helper (pnat.le_of_lt (pnat.lt_of_not_le Hn)) H,
|
|
|
|
|
rewrite [rat.abs_sub at T, {n⁻¹ + _}rat.add.comm at T],
|
|
|
|
|
exact T
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition p_under_seq : seq := λ n : ℕ+, under_seq' n~
|
|
|
|
|
|
|
|
|
|
definition p_over_seq : seq := λ n : ℕ+, over_seq' n~
|
|
|
|
|
|
|
|
|
|
theorem under_seq_regular : regular p_under_seq :=
|
|
|
|
|
begin
|
|
|
|
|
apply regular_lemma,
|
|
|
|
|
intros n i Hni,
|
|
|
|
|
apply and.intro,
|
|
|
|
|
apply under_seq_mono,
|
|
|
|
|
apply nat.add_le_add_right Hni,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply under_seq_lt_over_seq
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem over_seq_regular : regular p_over_seq :=
|
|
|
|
|
begin
|
|
|
|
|
apply regular_lemma,
|
|
|
|
|
intros n i Hni,
|
|
|
|
|
apply and.intro,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply under_seq_lt_over_seq,
|
|
|
|
|
apply over_seq_mono,
|
|
|
|
|
apply nat.add_le_add_right Hni
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition sup_over : ℝ := quot.mk (reg_seq.mk p_over_seq over_seq_regular)
|
|
|
|
|
|
|
|
|
|
definition sup_under : ℝ := quot.mk (reg_seq.mk p_under_seq under_seq_regular)
|
|
|
|
|
|
|
|
|
|
theorem over_bound : ub sup_over :=
|
2015-07-27 15:11:14 +00:00
|
|
|
|
begin
|
2015-07-27 21:49:26 +00:00
|
|
|
|
rewrite ↑ub,
|
|
|
|
|
intros y Hy,
|
|
|
|
|
apply le_of_le_reprs,
|
|
|
|
|
intro n,
|
|
|
|
|
apply PB,
|
|
|
|
|
apply Hy
|
|
|
|
|
end
|
|
|
|
|
set_option pp.coercions true
|
2015-07-27 15:11:14 +00:00
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem under_lowest_bound : ∀ y : ℝ, ub y → sup_under ≤ y :=
|
|
|
|
|
begin
|
|
|
|
|
intros y Hy,
|
|
|
|
|
apply le_of_reprs_le,
|
|
|
|
|
intro n,
|
|
|
|
|
cases (exists_not_of_not_forall (PA _)) with [x, Hx],
|
|
|
|
|
cases (iff.mp not_implies_iff_and_not Hx) with [HXx, Hxn],
|
|
|
|
|
apply le.trans,
|
|
|
|
|
apply le_of_lt,
|
|
|
|
|
apply lt_of_not_ge Hxn,
|
|
|
|
|
apply Hy,
|
|
|
|
|
apply HXx
|
2015-07-27 15:11:14 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem under_over_equiv : p_under_seq ≡ p_over_seq :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite ↑equiv,
|
|
|
|
|
intros,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
have H : p_under_seq n < p_over_seq n, from !under_seq_lt_over_seq,
|
|
|
|
|
rewrite [rat.abs_of_neg (iff.mpr !rat.sub_neg_iff_lt H), rat.neg_sub],
|
|
|
|
|
apply width',
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat_power_two_inv_ge,
|
|
|
|
|
apply rat.le_add_of_nonneg_left,
|
|
|
|
|
apply rat.le_of_lt !inv_pos
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem under_over_eq : sup_under = sup_over := quot.sound under_over_equiv
|
|
|
|
|
|
|
|
|
|
theorem supremum_of_complete : ∃ x : ℝ, sup x :=
|
|
|
|
|
exists.intro sup_over (and.intro over_bound (under_over_eq ▸ under_lowest_bound))
|
|
|
|
|
|
2015-07-27 15:11:14 +00:00
|
|
|
|
end supremum
|
|
|
|
|
|
2015-06-09 05:39:28 +00:00
|
|
|
|
end real
|