2015-05-26 02:05:53 +00:00
|
|
|
|
/-
|
2015-06-01 11:57:11 +00:00
|
|
|
|
Copyright (c) 2015 Robert Y. Lewis. All rights reserved.
|
2015-05-26 02:05:53 +00:00
|
|
|
|
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).
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
The construction of the reals is arranged in four files.
|
|
|
|
|
|
|
|
|
|
- basic.lean proves properties about regular sequences of rationals in the namespace rat_seq,
|
|
|
|
|
defines ℝ to be the quotient type of regular sequences mod equivalence, and shows ℝ is a ring
|
|
|
|
|
in namespace real. No classical axioms are used.
|
|
|
|
|
|
|
|
|
|
- order.lean defines an order on regular sequences and lifts the order to ℝ. In the namespace real,
|
|
|
|
|
ℝ is shown to be an ordered ring. No classical axioms are used.
|
|
|
|
|
|
|
|
|
|
- division.lean defines the inverse of a regular sequence and lifts this to ℝ. If a sequence is
|
|
|
|
|
equivalent to the 0 sequence, its inverse is the zero sequence. In the namespace real, ℝ is shown
|
|
|
|
|
to be an ordered field. This construction is classical.
|
|
|
|
|
|
|
|
|
|
- complete.lean
|
2015-05-26 02:05:53 +00:00
|
|
|
|
-/
|
2015-06-16 02:48:57 +00:00
|
|
|
|
import data.nat data.rat.order data.pnat
|
2015-06-11 07:01:55 +00:00
|
|
|
|
open nat eq eq.ops pnat
|
2015-05-26 03:22:37 +00:00
|
|
|
|
open -[coercions] rat
|
2015-06-10 02:46:30 +00:00
|
|
|
|
local notation 0 := rat.of_num 0
|
|
|
|
|
local notation 1 := rat.of_num 1
|
2015-08-27 17:29:19 +00:00
|
|
|
|
|
2015-08-03 19:02:03 +00:00
|
|
|
|
-- small helper lemmas
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem s_mul_assoc_lemma_3 (a b n : ℕ+) (p : ℚ) :
|
2015-08-03 19:02:03 +00:00
|
|
|
|
p * ((a * n)⁻¹ + (b * n)⁻¹) = p * (a⁻¹ + b⁻¹) * n⁻¹ :=
|
|
|
|
|
by rewrite [rat.mul.assoc, rat.right_distrib, *inv_mul_eq_mul_inv]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem s_mul_assoc_lemma_4 {n : ℕ+} {ε q : ℚ} (Hε : ε > 0) (Hq : q > 0) (H : n ≥ pceil (q / ε)) :
|
2015-05-26 03:22:37 +00:00
|
|
|
|
q * n⁻¹ ≤ ε :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
2015-08-27 14:24:48 +00:00
|
|
|
|
let H2 := pceil_helper H (div_pos_of_pos_of_pos Hq Hε),
|
|
|
|
|
let H3 := mul_le_of_le_div (div_pos_of_pos_of_pos Hq Hε) H2,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite -(one_mul ε),
|
|
|
|
|
apply mul_le_mul_of_mul_div_le,
|
2015-06-16 06:55:06 +00:00
|
|
|
|
repeat assumption
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
2015-06-16 03:14:05 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem find_thirds (a b : ℚ) (H : b > 0) : ∃ n : ℕ+, a + n⁻¹ + n⁻¹ + n⁻¹ < a + b :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
let n := pceil (of_nat 4 / b) in
|
|
|
|
|
have of_nat 3 * n⁻¹ < b, from calc
|
|
|
|
|
of_nat 3 * n⁻¹ < of_nat 4 * n⁻¹
|
|
|
|
|
: rat.mul_lt_mul_of_pos_right dec_trivial !inv_pos
|
|
|
|
|
... ≤ of_nat 4 * (b / of_nat 4)
|
|
|
|
|
: rat.mul_le_mul_of_nonneg_left (!inv_pceil_div dec_trivial H) !of_nat_nonneg
|
|
|
|
|
... = b / of_nat 4 * of_nat 4 : rat.mul.comm
|
2015-08-27 17:29:19 +00:00
|
|
|
|
... = b : !rat.div_mul_cancel dec_trivial,
|
2015-07-24 15:56:18 +00:00
|
|
|
|
exists.intro n (calc
|
|
|
|
|
a + n⁻¹ + n⁻¹ + n⁻¹ = a + (1 + 1 + 1) * n⁻¹ : by rewrite[*rat.right_distrib,*rat.one_mul,-*rat.add.assoc]
|
|
|
|
|
... = a + of_nat 3 * n⁻¹ : {show 1+1+1=of_nat 3, from dec_trivial}
|
|
|
|
|
... < a + b : rat.add_lt_add_left this a)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem squeeze {a b : ℚ} (H : ∀ j : ℕ+, a ≤ b + j⁻¹ + j⁻¹ + j⁻¹) : a ≤ b :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
apply rat.le_of_not_gt,
|
|
|
|
|
intro Hb,
|
2015-08-27 14:24:48 +00:00
|
|
|
|
cases exists_add_lt_and_pos_of_lt Hb with [c, Hc],
|
2015-08-05 16:44:13 +00:00
|
|
|
|
cases find_thirds b c (and.right Hc) with [j, Hbj],
|
2015-06-16 08:33:18 +00:00
|
|
|
|
have Ha : a > b + j⁻¹ + j⁻¹ + j⁻¹, from lt.trans Hbj (and.left Hc),
|
2015-08-05 16:44:13 +00:00
|
|
|
|
apply (not_le_of_gt Ha) !H
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem rewrite_helper (a b c d : ℚ) : a * b - c * d = a * (b - d) + (a - c) * d :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
by rewrite[rat.mul_sub_left_distrib, rat.mul_sub_right_distrib, add_sub, rat.sub_add_cancel]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem rewrite_helper3 (a b c d e f g: ℚ) : a * (b + c) - (d * e + f * g) =
|
2015-07-24 15:56:18 +00:00
|
|
|
|
(a * b - d * e) + (a * c - f * g) :=
|
|
|
|
|
by rewrite[rat.mul.left_distrib, add_sub_comm]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem rewrite_helper4 (a b c d : ℚ) : a * b - c * d = (a * b - a * d) + (a * d - c * d) :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
by rewrite[add_sub, rat.sub_add_cancel]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem rewrite_helper5 (a b x y : ℚ) : a - b = (a - x) + (x - y) + (y - b) :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
by rewrite[*add_sub, *rat.sub_add_cancel]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem rewrite_helper7 (a b c d x : ℚ) :
|
2015-07-24 15:56:18 +00:00
|
|
|
|
a * b * c - d = (b * c) * (a - x) + (x * b * c - d) :=
|
|
|
|
|
by rewrite[rat.mul_sub_left_distrib, add_sub]; exact (calc
|
|
|
|
|
a * b * c - d = a * b * c - x * b * c + x * b * c - d : rat.sub_add_cancel
|
|
|
|
|
... = b * c * a - b * c * x + x * b * c - d :
|
|
|
|
|
have ∀ {a b c : ℚ}, a * b * c = b * c * a, from
|
|
|
|
|
λa b c, !rat.mul.comm ▸ !rat.mul.right_comm,
|
|
|
|
|
this ▸ this ▸ rfl)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem ineq_helper (a b : ℚ) (k m n : ℕ+) (H : a ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(H2 : b ≤ (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹) :
|
2015-07-24 15:56:18 +00:00
|
|
|
|
(rat_of_pnat k) * a + b * (rat_of_pnat k) ≤ m⁻¹ + n⁻¹ :=
|
|
|
|
|
have (k * 2 * m)⁻¹ + (k * 2 * n)⁻¹ = (2 * k)⁻¹ * (m⁻¹ + n⁻¹),
|
|
|
|
|
by rewrite[rat.mul.left_distrib,*inv_mul_eq_mul_inv]; exact !rat.mul.comm ▸ rfl,
|
|
|
|
|
have a + b ≤ k⁻¹ * (m⁻¹ + n⁻¹), from calc
|
|
|
|
|
a + b ≤ (2 * k)⁻¹ * (m⁻¹ + n⁻¹) + (2 * k)⁻¹ * (m⁻¹ + n⁻¹) : rat.add_le_add (this ▸ H) (this ▸ H2)
|
|
|
|
|
... = ((2 * k)⁻¹ + (2 * k)⁻¹) * (m⁻¹ + n⁻¹) : rat.mul.right_distrib
|
|
|
|
|
... = k⁻¹ * (m⁻¹ + n⁻¹) : (pnat.add_halves k) ▸ rfl,
|
|
|
|
|
calc (rat_of_pnat k) * a + b * (rat_of_pnat k)
|
|
|
|
|
= (rat_of_pnat k) * a + (rat_of_pnat k) * b : rat.mul.comm
|
|
|
|
|
... = (rat_of_pnat k) * (a + b) : rat.left_distrib
|
|
|
|
|
... ≤ (rat_of_pnat k) * (k⁻¹ * (m⁻¹ + n⁻¹)) :
|
|
|
|
|
iff.mp (!rat.le_iff_mul_le_mul_left !rat_of_pnat_is_pos) this
|
|
|
|
|
... = m⁻¹ + n⁻¹ : by rewrite[-rat.mul.assoc, inv_cancel_left, rat.one_mul]
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem factor_lemma (a b c d e : ℚ) : abs (a + b + c - (d + (b + e))) = abs ((a - d) + (c - e)) :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
!congr_arg (calc
|
|
|
|
|
a + b + c - (d + (b + e)) = a + b + c - (d + b + e) : rat.add.assoc
|
|
|
|
|
... = a + b - (d + b) + (c - e) : add_sub_comm
|
|
|
|
|
... = a + b - b - d + (c - e) : sub_add_eq_sub_sub_swap
|
|
|
|
|
... = a - d + (c - e) : rat.add_sub_cancel)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem factor_lemma_2 (a b c d : ℚ) : (a + b) + (c + d) = (a + c) + (d + b) :=
|
2015-07-24 15:56:18 +00:00
|
|
|
|
!rat.add.comm ▸ (binary.comm4 rat.add.comm rat.add.assoc a b c d)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
--------------------------------------
|
|
|
|
|
-- define cauchy sequences and equivalence. show equivalence actually is one
|
2015-09-11 03:00:18 +00:00
|
|
|
|
namespace rat_seq
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
notation `seq` := ℕ+ → ℚ
|
|
|
|
|
|
|
|
|
|
definition regular (s : seq) := ∀ m n : ℕ+, abs (s m - s n) ≤ m⁻¹ + n⁻¹
|
|
|
|
|
|
|
|
|
|
definition equiv (s t : seq) := ∀ n : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹
|
|
|
|
|
infix `≡` := equiv
|
|
|
|
|
|
|
|
|
|
theorem equiv.refl (s : seq) : s ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem equiv.symm (s t : seq) (H : s ≡ t) : t ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [-abs_neg, neg_sub],
|
|
|
|
|
exact H n
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem bdd_of_eq {s t : seq} (H : s ≡ t) :
|
2015-05-26 03:22:37 +00:00
|
|
|
|
∀ j : ℕ+, ∀ n : ℕ+, n ≥ 2 * j → abs (s n - t n) ≤ j⁻¹ :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
intros [j, n, Hn],
|
|
|
|
|
apply rat.le.trans,
|
2015-08-05 16:44:13 +00:00
|
|
|
|
apply H,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite -(add_halves j),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply inv_ge_of_le Hn,
|
|
|
|
|
apply inv_ge_of_le Hn
|
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem eq_of_bdd {s t : seq} (Hs : regular s) (Ht : regular t)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(H : ∀ j : ℕ+, ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ j⁻¹) : s ≡ t :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
have Hj : (∀ j : ℕ+, abs (s n - t n) ≤ n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹), begin
|
|
|
|
|
intros,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
cases H j with [Nj, HNj],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite [-(rat.sub_add_cancel (s n) (s (max j Nj))), rat.add.assoc (s n + -s (max j Nj)),
|
|
|
|
|
↑regular at *],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply Hs,
|
|
|
|
|
rewrite [-(rat.sub_add_cancel (s (max j Nj)) (t (max j Nj))), rat.add.assoc],
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add_left,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply HNj (max j Nj) (max_right j Nj),
|
|
|
|
|
apply Ht,
|
2015-07-24 15:56:18 +00:00
|
|
|
|
have hsimp : ∀ m : ℕ+, n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹),
|
|
|
|
|
from λm, calc
|
|
|
|
|
n⁻¹ + m⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) = n⁻¹ + (j⁻¹ + (m⁻¹ + n⁻¹)) + m⁻¹ : rat.add.right_comm
|
|
|
|
|
... = n⁻¹ + (j⁻¹ + m⁻¹ + n⁻¹) + m⁻¹ : rat.add.assoc
|
|
|
|
|
... = n⁻¹ + (n⁻¹ + (j⁻¹ + m⁻¹)) + m⁻¹ : rat.add.comm
|
|
|
|
|
... = n⁻¹ + n⁻¹ + j⁻¹ + (m⁻¹ + m⁻¹) : by rewrite[-*rat.add.assoc],
|
2015-07-14 13:54:53 +00:00
|
|
|
|
rewrite hsimp,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
have Hms : (max j Nj)⁻¹ + (max j Nj)⁻¹ ≤ j⁻¹ + j⁻¹, begin
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply inv_ge_of_le (max_left j Nj),
|
|
|
|
|
apply inv_ge_of_le (max_left j Nj),
|
|
|
|
|
end,
|
|
|
|
|
apply (calc
|
|
|
|
|
n⁻¹ + n⁻¹ + j⁻¹ + ((max j Nj)⁻¹ + (max j Nj)⁻¹) ≤ n⁻¹ + n⁻¹ + j⁻¹ + (j⁻¹ + j⁻¹) :
|
|
|
|
|
rat.add_le_add_left Hms
|
|
|
|
|
... = n⁻¹ + n⁻¹ + j⁻¹ + j⁻¹ + j⁻¹ : by rewrite *rat.add.assoc)
|
|
|
|
|
end,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
apply squeeze Hj
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem eq_of_bdd_var {s t : seq} (Hs : regular s) (Ht : regular t)
|
|
|
|
|
(H : ∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε) : s ≡ t :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
apply eq_of_bdd,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat assumption,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros,
|
2015-08-05 16:44:13 +00:00
|
|
|
|
apply H,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply inv_pos
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem bdd_of_eq_var {s t : seq} (Hs : regular s) (Ht : regular t) (Heq : s ≡ t) :
|
|
|
|
|
∀ ε : ℚ, ε > 0 → ∃ Nj : ℕ+, ∀ n : ℕ+, Nj ≤ n → abs (s n - t n) ≤ ε :=
|
|
|
|
|
begin
|
|
|
|
|
intro ε Hε,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
cases pnat_bound Hε with [N, HN],
|
2015-05-26 03:22:37 +00:00
|
|
|
|
existsi 2 * N,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intro n Hn,
|
|
|
|
|
apply rat.le.trans,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
apply bdd_of_eq Heq N n Hn,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
assumption
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem equiv.trans (s t u : seq) (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
|
|
|
|
(H : s ≡ t) (H2 : t ≡ u) : s ≡ u :=
|
|
|
|
|
begin
|
2015-05-26 03:22:37 +00:00
|
|
|
|
apply eq_of_bdd Hs Hu,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
existsi 2 * (2 * j),
|
|
|
|
|
intro n Hn,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite [-rat.sub_add_cancel (s n) (t n), rat.add.assoc],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
have Hst : abs (s n - t n) ≤ (2 * j)⁻¹, from bdd_of_eq H _ _ Hn,
|
|
|
|
|
have Htu : abs (t n - u n) ≤ (2 * j)⁻¹, from bdd_of_eq H2 _ _ Hn,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite -(add_halves j),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.add_le_add,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
repeat assumption
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
-----------------------------------
|
|
|
|
|
-- define operations on cauchy sequences. show operations preserve regularity
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private definition K (s : seq) : ℕ+ := pnat.pos (ubound (abs (s pone)) + 1 + 1) dec_trivial
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of_pnat (K s) :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
calc
|
|
|
|
|
abs (s n) = abs (s n - s pone + s pone) : by rewrite rat.sub_add_cancel
|
|
|
|
|
... ≤ abs (s n - s pone) + abs (s pone) : abs_add_le_abs_add_abs
|
|
|
|
|
... ≤ n⁻¹ + pone⁻¹ + abs (s pone) : rat.add_le_add_right !Hs
|
|
|
|
|
... = n⁻¹ + (1 + abs (s pone)) : by rewrite [pone_inv, rat.add.assoc]
|
|
|
|
|
... ≤ 1 + (1 + abs (s pone)) : rat.add_le_add_right (inv_le_one n)
|
|
|
|
|
... = abs (s pone) + (1 + 1) :
|
|
|
|
|
by rewrite [add.comm 1 (abs (s pone)), rat.add.comm 1, rat.add.assoc]
|
2015-06-16 03:14:05 +00:00
|
|
|
|
... ≤ of_nat (ubound (abs (s pone))) + (1 + 1) : rat.add_le_add_right (!ubound_ge)
|
2015-07-24 15:56:18 +00:00
|
|
|
|
... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add
|
2015-09-01 02:56:05 +00:00
|
|
|
|
... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc
|
|
|
|
|
... = rat_of_pnat (K s) : by esimp
|
2015-05-26 03:22:37 +00:00
|
|
|
|
|
2015-07-29 19:44:11 +00:00
|
|
|
|
theorem bdd_of_regular {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : ℕ+, s n ≤ b :=
|
|
|
|
|
begin
|
|
|
|
|
existsi rat_of_pnat (K s),
|
|
|
|
|
intros,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply le_abs_self,
|
|
|
|
|
apply canon_bound H
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem bdd_of_regular_strict {s : seq} (H : regular s) : ∃ b : ℚ, ∀ n : ℕ+, s n < b :=
|
|
|
|
|
begin
|
|
|
|
|
cases bdd_of_regular H with [b, Hb],
|
|
|
|
|
existsi b + 1,
|
|
|
|
|
intro n,
|
|
|
|
|
apply rat.lt_of_le_of_lt,
|
|
|
|
|
apply Hb,
|
|
|
|
|
apply rat.lt_add_of_pos_right,
|
|
|
|
|
apply rat.zero_lt_one
|
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 02:05:53 +00:00
|
|
|
|
definition K₂ (s t : seq) := max (K s) (K t)
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
|
2015-05-26 03:22:37 +00:00
|
|
|
|
if H : K s < K t then
|
2015-07-24 17:07:16 +00:00
|
|
|
|
(assert H1 : K₂ s t = K t, from max_eq_right H,
|
|
|
|
|
assert H2 : K₂ t s = K t, from max_eq_left (not_lt_of_ge (le_of_lt H)),
|
|
|
|
|
by rewrite [H1, -H2])
|
2015-05-26 02:05:53 +00:00
|
|
|
|
else
|
2015-07-24 17:07:16 +00:00
|
|
|
|
(assert H1 : K₂ s t = K s, from max_eq_left H,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
if J : K t < K s then
|
2015-07-24 17:07:16 +00:00
|
|
|
|
(assert H2 : K₂ t s = K s, from max_eq_right J, by rewrite [H1, -H2])
|
2015-05-26 02:05:53 +00:00
|
|
|
|
else
|
2015-07-24 17:07:16 +00:00
|
|
|
|
(assert Heq : K t = K s, from
|
2015-06-16 04:55:02 +00:00
|
|
|
|
eq_of_le_of_ge (le_of_not_gt H) (le_of_not_gt J),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
by rewrite [↑K₂, Heq]))
|
|
|
|
|
|
|
|
|
|
theorem canon_2_bound_left (s t : seq) (Hs : regular s) (n : ℕ+) :
|
2015-06-16 04:55:02 +00:00
|
|
|
|
abs (s n) ≤ rat_of_pnat (K₂ s t) :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
calc
|
2015-06-16 04:55:02 +00:00
|
|
|
|
abs (s n) ≤ rat_of_pnat (K s) : canon_bound Hs n
|
|
|
|
|
... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!max_left)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem canon_2_bound_right (s t : seq) (Ht : regular t) (n : ℕ+) :
|
2015-06-16 04:55:02 +00:00
|
|
|
|
abs (t n) ≤ rat_of_pnat (K₂ s t) :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
calc
|
2015-06-16 04:55:02 +00:00
|
|
|
|
abs (t n) ≤ rat_of_pnat (K t) : canon_bound Ht n
|
|
|
|
|
... ≤ rat_of_pnat (K₂ s t) : rat_of_pnat_le_of_pnat_le (!max_right)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
definition sadd (s t : seq) : seq := λ n, (s (2 * n)) + (t (2 * n))
|
|
|
|
|
|
|
|
|
|
theorem reg_add_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (sadd s t) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑regular at *, ↑sadd],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite add_sub_comm,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
rewrite add_halves_double,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply Ht
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition smul (s t : seq) : seq := λ n : ℕ+, (s ((K₂ s t) * 2 * n)) * (t ((K₂ s t) * 2 * n))
|
|
|
|
|
|
|
|
|
|
theorem reg_mul_reg {s t : seq} (Hs : regular s) (Ht : regular t) : regular (smul s t) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑regular at *, ↑smul],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite rewrite_helper,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
rewrite abs_mul,
|
|
|
|
|
apply rat.mul_le_mul_of_nonneg_right,
|
|
|
|
|
apply canon_2_bound_left s t Hs,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
rewrite abs_mul,
|
|
|
|
|
apply rat.mul_le_mul_of_nonneg_left,
|
|
|
|
|
apply canon_2_bound_right s t Ht,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply ineq_helper,
|
|
|
|
|
apply Ht,
|
|
|
|
|
apply Hs
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
definition sneg (s : seq) : seq := λ n : ℕ+, - (s n)
|
|
|
|
|
|
|
|
|
|
theorem reg_neg_reg {s : seq} (Hs : regular s) : regular (sneg s) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑regular at *, ↑sneg],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [-abs_neg, neg_sub, sub_neg_eq_add, rat.add.comm],
|
|
|
|
|
apply Hs
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
-----------------------------------
|
|
|
|
|
-- show properties of +, *, -
|
|
|
|
|
|
|
|
|
|
definition zero : seq := λ n, 0
|
|
|
|
|
|
|
|
|
|
definition one : seq := λ n, 1
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem s_add_comm (s t : seq) : sadd s t ≡ sadd t s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
2015-05-26 03:22:37 +00:00
|
|
|
|
esimp [sadd],
|
|
|
|
|
intro n,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite [sub_add_eq_sub_sub, rat.add_sub_cancel, rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_add_assoc (s t u : seq) (Hs : regular s) (Hu : regular u) :
|
|
|
|
|
sadd (sadd s t) u ≡ sadd s (sadd t u) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑equiv, ↑regular at *],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite factor_lemma,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
rotate 1,
|
|
|
|
|
apply rat.add_le_add_right,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply inv_two_mul_le_inv,
|
|
|
|
|
rewrite [-(add_halves (2 * n)), -(add_halves n), factor_lemma_2],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply Hu
|
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem s_mul_comm (s t : seq) : smul s t ≡ smul t s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
rewrite ↑smul,
|
|
|
|
|
intros n,
|
|
|
|
|
rewrite [*(K₂_symm s t), rat.mul.comm, rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private definition DK (s t : seq) := (K₂ s t) * 2
|
|
|
|
|
private theorem DK_rewrite (s t : seq) : (K₂ s t) * 2 = DK s t := rfl
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private definition TK (s t u : seq) := (DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem TK_rewrite (s t u : seq) :
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(DK (λ (n : ℕ+), s (mul (DK s t) n) * t (mul (DK s t) n)) u) = TK s t u := rfl
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem s_mul_assoc_lemma (s t u : seq) (a b c d : ℕ+) :
|
2015-05-26 02:05:53 +00:00
|
|
|
|
abs (s a * t a * u b - s c * t d * u d) ≤ abs (t a) * abs (u b) * abs (s a - s c) +
|
|
|
|
|
abs (s c) * abs (t a) * abs (u b - u d) + abs (s c) * abs (u d) * abs (t a - t d) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite (rewrite_helper7 _ _ _ _ (s c)),
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
rewrite rat.add.assoc,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
rewrite 2 abs_mul,
|
|
|
|
|
apply rat.le.refl,
|
|
|
|
|
rewrite [*rat.mul.assoc, -rat.mul_sub_left_distrib, -rat.left_distrib, abs_mul],
|
|
|
|
|
apply rat.mul_le_mul_of_nonneg_left,
|
|
|
|
|
rewrite rewrite_helper,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
rewrite abs_mul, apply rat.le.refl,
|
|
|
|
|
rewrite [abs_mul, rat.mul.comm], apply rat.le.refl,
|
|
|
|
|
apply abs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private definition Kq (s : seq) := rat_of_pnat (K s) + 1
|
|
|
|
|
private theorem Kq_bound {s : seq} (H : regular s) : ∀ n, abs (s n) ≤ Kq s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply rat.lt_of_le_of_lt,
|
|
|
|
|
apply canon_bound H,
|
|
|
|
|
apply rat.lt_add_of_pos_right,
|
|
|
|
|
apply rat.zero_lt_one
|
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem Kq_bound_nonneg {s : seq} (H : regular s) : 0 ≤ Kq s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rat.le.trans !abs_nonneg (Kq_bound H 2)
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem Kq_bound_pos {s : seq} (H : regular s) : 0 < Kq s :=
|
2015-06-16 04:55:02 +00:00
|
|
|
|
have H1 : 0 ≤ rat_of_pnat (K s), from rat.le.trans (!abs_nonneg) (canon_bound H 2),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
add_pos_of_nonneg_of_pos H1 rat.zero_lt_one
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem s_mul_assoc_lemma_5 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(a b c : ℕ+) : abs (t a) * abs (u b) * abs (s a - s c) ≤ (Kq t) * (Kq u) * (a⁻¹ + c⁻¹) :=
|
|
|
|
|
begin
|
|
|
|
|
repeat apply rat.mul_le_mul,
|
|
|
|
|
apply Kq_bound Ht,
|
|
|
|
|
apply Kq_bound Hu,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply Kq_bound_nonneg Ht,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.mul_nonneg,
|
|
|
|
|
apply Kq_bound_nonneg Ht,
|
|
|
|
|
apply Kq_bound_nonneg Hu,
|
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem s_mul_assoc_lemma_2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 03:22:37 +00:00
|
|
|
|
(a b c d : ℕ+) :
|
2015-05-26 02:05:53 +00:00
|
|
|
|
abs (t a) * abs (u b) * abs (s a - s c) + abs (s c) * abs (t a) * abs (u b - u d)
|
|
|
|
|
+ abs (s c) * abs (u d) * abs (t a - t d) ≤
|
|
|
|
|
(Kq t) * (Kq u) * (a⁻¹ + c⁻¹) + (Kq s) * (Kq t) * (b⁻¹ + d⁻¹) + (Kq s) * (Kq u) * (a⁻¹ + d⁻¹) :=
|
|
|
|
|
begin
|
|
|
|
|
apply add_le_add_three,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
|
|
|
|
|
apply abs_nonneg),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply Hs,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.mul_nonneg,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
|
|
|
|
|
apply abs_nonneg),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply Hu,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.mul_nonneg,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (assumption | apply rat.mul_le_mul | apply Kq_bound | apply Kq_bound_nonneg |
|
|
|
|
|
apply abs_nonneg),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply Ht,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.mul_nonneg,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (apply Kq_bound_nonneg; assumption)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_mul_assoc {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) :
|
|
|
|
|
smul (smul s t) u ≡ smul s (smul t u) :=
|
|
|
|
|
begin
|
|
|
|
|
apply eq_of_bdd_var,
|
|
|
|
|
repeat apply reg_mul_reg,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply Ht,
|
|
|
|
|
apply Hu,
|
|
|
|
|
apply reg_mul_reg Hs,
|
|
|
|
|
apply reg_mul_reg Ht Hu,
|
|
|
|
|
intros,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
apply exists.intro,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [↑smul, *DK_rewrite, *TK_rewrite, -*pnat.mul.assoc, -*rat.mul.assoc],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply s_mul_assoc_lemma,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply s_mul_assoc_lemma_2,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply Ht,
|
|
|
|
|
apply Hu,
|
2015-06-16 06:55:06 +00:00
|
|
|
|
rewrite [*s_mul_assoc_lemma_3, -rat.distrib_three_right],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply s_mul_assoc_lemma_4,
|
|
|
|
|
apply a,
|
|
|
|
|
repeat apply rat.add_pos,
|
|
|
|
|
repeat apply rat.mul_pos,
|
|
|
|
|
apply Kq_bound_pos Ht,
|
|
|
|
|
apply Kq_bound_pos Hu,
|
|
|
|
|
apply rat.add_pos,
|
|
|
|
|
repeat apply inv_pos,
|
|
|
|
|
repeat apply rat.mul_pos,
|
|
|
|
|
apply Kq_bound_pos Hs,
|
|
|
|
|
apply Kq_bound_pos Ht,
|
|
|
|
|
apply rat.add_pos,
|
|
|
|
|
repeat apply inv_pos,
|
|
|
|
|
repeat apply rat.mul_pos,
|
|
|
|
|
apply Kq_bound_pos Hs,
|
|
|
|
|
apply Kq_bound_pos Hu,
|
|
|
|
|
apply rat.add_pos,
|
|
|
|
|
repeat apply inv_pos,
|
|
|
|
|
apply a_1
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem zero_is_reg : regular zero :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑regular, ↑zero],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.sub_zero, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_zero_add (s : seq) (H : regular s) : sadd zero s ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑zero, ↑equiv, ↑regular at H],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.zero_add],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply H,
|
|
|
|
|
apply rat.add_le_add,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply inv_two_mul_le_inv,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le.refl
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_add_zero (s : seq) (H : regular s) : sadd s zero ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑zero, ↑equiv, ↑regular at H],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.add_zero],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply H,
|
|
|
|
|
apply rat.add_le_add,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply inv_two_mul_le_inv,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le.refl
|
2015-05-26 03:22:37 +00:00
|
|
|
|
end
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
theorem s_neg_cancel (s : seq) (H : regular s) : sadd (sneg s) s ≡ zero :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑sneg, ↑regular at H, ↑zero, ↑equiv],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [neg_add_eq_sub, rat.sub_self, rat.sub_zero, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-05-29 04:11:00 +00:00
|
|
|
|
theorem neg_s_cancel (s : seq) (H : regular s) : sadd s (sneg s) ≡ zero :=
|
|
|
|
|
begin
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply s_add_comm,
|
|
|
|
|
apply s_neg_cancel s H,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (apply reg_add_reg | apply reg_neg_reg | assumption),
|
2015-05-29 04:11:00 +00:00
|
|
|
|
apply zero_is_reg
|
|
|
|
|
end
|
|
|
|
|
|
2015-06-10 02:46:30 +00:00
|
|
|
|
theorem add_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(Hv : regular v) (Esu : s ≡ u) (Etv : t ≡ v) : sadd s t ≡ sadd u v :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sadd, ↑equiv at *],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [add_sub_comm, add_halves_double],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply Esu,
|
|
|
|
|
apply Etv
|
|
|
|
|
end
|
|
|
|
|
|
2015-07-24 15:56:18 +00:00
|
|
|
|
set_option tactic.goal_names false
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem mul_bound_helper {s t : seq} (Hs : regular s) (Ht : regular t) (a b c : ℕ+) (j : ℕ+) :
|
2015-05-26 03:22:37 +00:00
|
|
|
|
∃ N : ℕ+, ∀ n : ℕ+, n ≥ N → abs (s (a * n) * t (b * n) - s (c * n) * t (c * n)) ≤ j⁻¹ :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
2015-06-16 04:55:02 +00:00
|
|
|
|
existsi pceil (((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) *
|
|
|
|
|
(rat_of_pnat (K t))) * (rat_of_pnat j)),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros n Hn,
|
|
|
|
|
rewrite rewrite_helper4,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
rotate 1,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
show n⁻¹ * ((rat_of_pnat (K s)) * (b⁻¹ + c⁻¹)) +
|
|
|
|
|
n⁻¹ * ((a⁻¹ + c⁻¹) * (rat_of_pnat (K t))) ≤ j⁻¹, begin
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite -rat.left_distrib,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.mul_le_mul_of_nonneg_right,
|
|
|
|
|
apply pceil_helper Hn,
|
2015-07-24 18:47:37 +00:00
|
|
|
|
repeat (apply rat.mul_pos | apply rat.add_pos | apply inv_pos | apply rat_of_pnat_is_pos),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply rat.add_pos,
|
|
|
|
|
apply rat.mul_pos,
|
|
|
|
|
apply rat_of_pnat_is_pos,
|
|
|
|
|
apply rat.add_pos,
|
|
|
|
|
repeat apply inv_pos,
|
|
|
|
|
apply rat.mul_pos,
|
|
|
|
|
apply rat.add_pos,
|
2015-07-24 18:47:37 +00:00
|
|
|
|
repeat apply inv_pos,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat_of_pnat_is_pos,
|
2015-06-16 06:55:06 +00:00
|
|
|
|
have H : (rat_of_pnat (K s) * (b⁻¹ + c⁻¹) + (a⁻¹ + c⁻¹) * rat_of_pnat (K t)) ≠ 0, begin
|
|
|
|
|
apply rat.ne_of_gt,
|
2015-07-24 15:56:18 +00:00
|
|
|
|
repeat (apply rat.mul_pos | apply rat.add_pos | apply rat_of_pnat_is_pos | apply inv_pos),
|
2015-06-16 06:55:06 +00:00
|
|
|
|
end,
|
2015-08-27 17:29:19 +00:00
|
|
|
|
rewrite (!rat.div_helper H),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le.refl
|
2015-07-24 15:56:18 +00:00
|
|
|
|
end,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
rewrite [-rat.mul_sub_left_distrib, abs_mul],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.mul_le_mul,
|
|
|
|
|
apply canon_bound,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply Ht,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply rat_of_pnat_is_pos,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, -rat.mul.assoc, rat.mul.comm],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.mul_le_mul_of_nonneg_left,
|
|
|
|
|
apply rat.le.refl,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos,
|
|
|
|
|
rewrite [-rat.mul_sub_right_distrib, abs_mul],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.mul_le_mul,
|
|
|
|
|
apply Hs,
|
|
|
|
|
apply canon_bound,
|
|
|
|
|
apply Ht,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply add_invs_nonneg,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [*inv_mul_eq_mul_inv, -rat.right_distrib, mul.comm _ n⁻¹, rat.mul.assoc],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.mul_le_mul,
|
2015-07-27 15:11:14 +00:00
|
|
|
|
repeat apply rat.le.refl,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply rat.mul_pos,
|
|
|
|
|
apply rat.add_pos,
|
2015-07-24 18:47:37 +00:00
|
|
|
|
repeat apply inv_pos,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat_of_pnat_is_pos,
|
|
|
|
|
apply rat.le_of_lt,
|
|
|
|
|
apply inv_pos
|
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem s_distrib {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u) :
|
2015-05-26 02:05:53 +00:00
|
|
|
|
smul s (sadd t u) ≡ sadd (smul s t) (smul s u) :=
|
|
|
|
|
begin
|
|
|
|
|
apply eq_of_bdd,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
repeat (assumption | apply reg_add_reg | apply reg_mul_reg),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros,
|
|
|
|
|
let exh1 := λ a b c, mul_bound_helper Hs Ht a b c (2 * j),
|
|
|
|
|
apply exists.elim,
|
|
|
|
|
apply exh1,
|
|
|
|
|
rotate 3,
|
|
|
|
|
intros N1 HN1,
|
|
|
|
|
let exh2 := λ d e f, mul_bound_helper Hs Hu d e f (2 * j),
|
|
|
|
|
apply exists.elim,
|
|
|
|
|
apply exh2,
|
|
|
|
|
rotate 3,
|
|
|
|
|
intros N2 HN2,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
existsi max N1 N2,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros n Hn,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [↑sadd at *, ↑smul, rewrite_helper3, -add_halves j, -*pnat.mul.assoc at *],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_le_abs_add_abs,
|
|
|
|
|
apply rat.add_le_add,
|
|
|
|
|
apply HN1,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply le.trans,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply max_left N1 N2,
|
|
|
|
|
apply Hn,
|
|
|
|
|
apply HN2,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply le.trans,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply max_right N1 N2,
|
|
|
|
|
apply Hn
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem mul_zero_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t) (Htz : t ≡ zero) :
|
|
|
|
|
smul s t ≡ zero :=
|
|
|
|
|
begin
|
|
|
|
|
apply eq_of_bdd_var,
|
|
|
|
|
apply reg_mul_reg Hs Ht,
|
|
|
|
|
apply zero_is_reg,
|
|
|
|
|
intro ε Hε,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
let Bd := bdd_of_eq_var Ht zero_is_reg Htz (ε / (Kq s))
|
2015-08-27 14:24:48 +00:00
|
|
|
|
(div_pos_of_pos_of_pos Hε (Kq_bound_pos Hs)),
|
2015-08-03 19:02:03 +00:00
|
|
|
|
cases Bd with [N, HN],
|
2015-05-26 03:22:37 +00:00
|
|
|
|
existsi N,
|
|
|
|
|
intro n Hn,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
rewrite [↑equiv at Htz, ↑zero at *, rat.sub_zero, ↑smul, abs_mul],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply rat.mul_le_mul,
|
|
|
|
|
apply Kq_bound Hs,
|
|
|
|
|
let HN' := λ n, (!rat.sub_zero ▸ HN n),
|
|
|
|
|
apply HN',
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply le.trans Hn,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply pnat.mul_le_mul_left,
|
|
|
|
|
apply abs_nonneg,
|
|
|
|
|
apply rat.le_of_lt (Kq_bound_pos Hs),
|
|
|
|
|
rewrite (rat.mul_div_cancel' (ne.symm (rat.ne_of_lt (Kq_bound_pos Hs)))),
|
|
|
|
|
apply rat.le.refl
|
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem neg_bound_eq_bound (s : seq) : K (sneg s) = K s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
by rewrite [↑K, ↑sneg, abs_neg]
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem neg_bound2_eq_bound2 (s t : seq) : K₂ s (sneg t) = K₂ s t :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
by rewrite [↑K₂, neg_bound_eq_bound]
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem sneg_def (s : seq) : (λ (n : ℕ+), -(s n)) = sneg s := rfl
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
theorem mul_neg_equiv_neg_mul {s t : seq} : smul s (sneg t) ≡ sneg (smul s t) :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑equiv, ↑smul],
|
|
|
|
|
intros,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
rewrite [↑sneg, *sub_neg_eq_add, -neg_mul_eq_mul_neg, rat.add.comm, *sneg_def,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
*neg_bound2_eq_bound2, rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem equiv_of_diff_equiv_zero {s t : seq} (Hs : regular s) (Ht : regular t)
|
|
|
|
|
(H : sadd s (sneg t) ≡ zero) : s ≡ t :=
|
|
|
|
|
begin
|
2015-07-24 15:56:18 +00:00
|
|
|
|
have hsimp : ∀ a b c d e : ℚ, a + b + c + (d + e) = b + d + a + e + c, from
|
|
|
|
|
λ a b c d e, calc
|
|
|
|
|
a + b + c + (d + e) = a + b + (d + e) + c : rat.add.right_comm
|
|
|
|
|
... = a + (b + d) + e + c : by rewrite[-*rat.add.assoc]
|
|
|
|
|
... = b + d + a + e + c : rat.add.comm,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply eq_of_bdd Hs Ht,
|
|
|
|
|
intros,
|
|
|
|
|
let He := bdd_of_eq H,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
existsi 2 * (2 * (2 * j)),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
intros n Hn,
|
|
|
|
|
rewrite (rewrite_helper5 _ _ (s (2 * n)) (t (2 * n))),
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply abs_add_three,
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply add_le_add_three,
|
|
|
|
|
apply Hs,
|
|
|
|
|
rewrite [↑sadd at He, ↑sneg at He, ↑zero at He],
|
|
|
|
|
let He' := λ a b c, !rat.sub_zero ▸ (He a b c),
|
|
|
|
|
apply (He' _ _ Hn),
|
|
|
|
|
apply Ht,
|
2015-07-14 13:54:53 +00:00
|
|
|
|
rewrite [hsimp, add_halves, -(add_halves j), -(add_halves (2 * j)), -*rat.add.assoc],
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply add_le_add_three,
|
2015-06-16 04:55:02 +00:00
|
|
|
|
repeat (apply rat.le.trans; apply inv_ge_of_le Hn; apply inv_two_mul_le_inv)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem s_sub_cancel (s : seq) : sadd s (sneg s) ≡ zero :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
rewrite [↑equiv, ↑sadd, ↑sneg, ↑zero],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.sub_zero, rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem diff_equiv_zero_of_equiv {s t : seq} (Hs : regular s) (Ht : regular t) (H : s ≡ t) :
|
|
|
|
|
sadd s (sneg t) ≡ zero :=
|
|
|
|
|
begin
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 4,
|
|
|
|
|
apply s_sub_cancel t,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply zero_is_reg,
|
|
|
|
|
apply add_well_defined,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (assumption | apply reg_neg_reg),
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply equiv.refl,
|
2015-08-03 19:02:03 +00:00
|
|
|
|
repeat (assumption | apply reg_add_reg | apply reg_neg_reg)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem mul_well_defined_half1 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(Etu : t ≡ u) : smul s t ≡ smul s u :=
|
|
|
|
|
begin
|
2015-06-16 06:55:06 +00:00
|
|
|
|
apply equiv_of_diff_equiv_zero,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply equiv.symm,
|
|
|
|
|
apply add_well_defined,
|
|
|
|
|
rotate 4,
|
|
|
|
|
apply equiv.refl,
|
|
|
|
|
apply mul_neg_equiv_neg_mul,
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply equiv.symm,
|
|
|
|
|
apply s_distrib,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply mul_zero_equiv_zero,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply diff_equiv_zero_of_equiv,
|
|
|
|
|
repeat (assumption | apply reg_mul_reg | apply reg_neg_reg | apply reg_add_reg |
|
|
|
|
|
apply zero_is_reg)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
private theorem mul_well_defined_half2 {s t u : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(Est : s ≡ t) : smul s u ≡ smul t u :=
|
|
|
|
|
begin
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply s_mul_comm,
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
rotate 3,
|
|
|
|
|
apply mul_well_defined_half1,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply Ht,
|
|
|
|
|
rotate 1,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
apply s_mul_comm,
|
2015-06-16 06:55:06 +00:00
|
|
|
|
repeat (assumption | apply reg_mul_reg)
|
2015-05-26 03:22:37 +00:00
|
|
|
|
end
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem mul_well_defined {s t u v : seq} (Hs : regular s) (Ht : regular t) (Hu : regular u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(Hv : regular v) (Esu : s ≡ u) (Etv : t ≡ v) : smul s t ≡ smul u v :=
|
|
|
|
|
begin
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
exact reg_mul_reg Hs Ht,
|
|
|
|
|
exact reg_mul_reg Hs Hv,
|
|
|
|
|
exact reg_mul_reg Hu Hv,
|
|
|
|
|
apply mul_well_defined_half1,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
repeat assumption,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply mul_well_defined_half2,
|
2015-05-26 03:22:37 +00:00
|
|
|
|
repeat assumption
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem neg_well_defined {s t : seq} (Est : s ≡ t) : sneg s ≡ sneg t :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑sneg, ↑equiv at *],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [-abs_neg, neg_sub, sub_neg_eq_add, rat.add.comm],
|
|
|
|
|
apply Est
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem one_is_reg : regular one :=
|
|
|
|
|
begin
|
|
|
|
|
rewrite [↑regular, ↑one],
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_one_mul {s : seq} (H : regular s) : smul one s ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [↑smul, ↑one, rat.one_mul],
|
|
|
|
|
apply rat.le.trans,
|
|
|
|
|
apply H,
|
|
|
|
|
apply rat.add_le_add_right,
|
|
|
|
|
apply inv_mul_le_inv
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem s_mul_one {s : seq} (H : regular s) : smul s one ≡ s :=
|
|
|
|
|
begin
|
|
|
|
|
apply equiv.trans,
|
|
|
|
|
apply reg_mul_reg H one_is_reg,
|
|
|
|
|
rotate 2,
|
|
|
|
|
apply s_mul_comm,
|
|
|
|
|
apply s_one_mul H,
|
|
|
|
|
apply reg_mul_reg one_is_reg H,
|
|
|
|
|
apply H
|
|
|
|
|
end
|
|
|
|
|
|
2015-05-29 04:11:00 +00:00
|
|
|
|
theorem zero_nequiv_one : ¬ zero ≡ one :=
|
|
|
|
|
begin
|
|
|
|
|
intro Hz,
|
|
|
|
|
rewrite [↑equiv at Hz, ↑zero at Hz, ↑one at Hz],
|
|
|
|
|
let H := Hz (2 * 2),
|
2015-06-16 04:55:02 +00:00
|
|
|
|
rewrite [rat.zero_sub at H, abs_neg at H, add_halves at H],
|
2015-05-29 04:11:00 +00:00
|
|
|
|
have H' : pone⁻¹ ≤ 2⁻¹, from calc
|
|
|
|
|
pone⁻¹ = 1 : by rewrite -pone_inv
|
|
|
|
|
... = abs 1 : abs_of_pos zero_lt_one
|
|
|
|
|
... ≤ 2⁻¹ : H,
|
2015-06-10 02:46:30 +00:00
|
|
|
|
let H'' := ge_of_inv_le H',
|
2015-06-16 04:55:02 +00:00
|
|
|
|
apply absurd (one_lt_two) (not_lt_of_ge H'')
|
2015-05-29 04:11:00 +00:00
|
|
|
|
end
|
|
|
|
|
|
2015-06-23 12:17:50 +00:00
|
|
|
|
---------------------------------------------
|
|
|
|
|
-- constant sequences
|
|
|
|
|
|
|
|
|
|
definition const (a : ℚ) : seq := λ n, a
|
|
|
|
|
|
|
|
|
|
theorem const_reg (a : ℚ) : regular (const a) :=
|
|
|
|
|
begin
|
|
|
|
|
intros,
|
|
|
|
|
rewrite [↑const, rat.sub_self, abs_zero],
|
|
|
|
|
apply add_invs_nonneg
|
|
|
|
|
end
|
|
|
|
|
|
|
|
|
|
theorem add_consts (a b : ℚ) : sadd (const a) (const b) ≡ const (a + b) :=
|
2015-07-16 17:18:35 +00:00
|
|
|
|
by apply equiv.refl
|
|
|
|
|
|
|
|
|
|
theorem mul_consts (a b : ℚ) : smul (const a) (const b) ≡ const (a * b) :=
|
|
|
|
|
by apply equiv.refl
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem neg_const (a : ℚ) : sneg (const a) ≡ const (-a) :=
|
|
|
|
|
by apply equiv.refl
|
|
|
|
|
|
2015-05-26 02:05:53 +00:00
|
|
|
|
---------------------------------------------
|
|
|
|
|
-- create the type of regular sequences and lift theorems
|
|
|
|
|
|
|
|
|
|
record reg_seq : Type :=
|
|
|
|
|
(sq : seq) (is_reg : regular sq)
|
|
|
|
|
|
|
|
|
|
definition requiv (s t : reg_seq) := (reg_seq.sq s) ≡ (reg_seq.sq t)
|
|
|
|
|
definition requiv.refl (s : reg_seq) : requiv s s := equiv.refl (reg_seq.sq s)
|
2015-05-26 03:22:37 +00:00
|
|
|
|
definition requiv.symm (s t : reg_seq) (H : requiv s t) : requiv t s :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
equiv.symm (reg_seq.sq s) (reg_seq.sq t) H
|
|
|
|
|
definition requiv.trans (s t u : reg_seq) (H : requiv s t) (H2 : requiv t u) : requiv s u :=
|
|
|
|
|
equiv.trans _ _ _ (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) H H2
|
|
|
|
|
|
|
|
|
|
definition radd (s t : reg_seq) : reg_seq :=
|
|
|
|
|
reg_seq.mk (sadd (reg_seq.sq s) (reg_seq.sq t))
|
|
|
|
|
(reg_add_reg (reg_seq.is_reg s) (reg_seq.is_reg t))
|
|
|
|
|
infix `+` := radd
|
|
|
|
|
|
|
|
|
|
definition rmul (s t : reg_seq) : reg_seq :=
|
|
|
|
|
reg_seq.mk (smul (reg_seq.sq s) (reg_seq.sq t))
|
|
|
|
|
(reg_mul_reg (reg_seq.is_reg s) (reg_seq.is_reg t))
|
|
|
|
|
infix `*` := rmul
|
|
|
|
|
|
|
|
|
|
definition rneg (s : reg_seq) : reg_seq :=
|
|
|
|
|
reg_seq.mk (sneg (reg_seq.sq s)) (reg_neg_reg (reg_seq.is_reg s))
|
|
|
|
|
prefix `-` := rneg
|
|
|
|
|
|
|
|
|
|
definition radd_well_defined {s t u v : reg_seq} (H : requiv s u) (H2 : requiv t v) :
|
|
|
|
|
requiv (s + t) (u + v) :=
|
|
|
|
|
add_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) (reg_seq.is_reg v) H H2
|
|
|
|
|
|
|
|
|
|
definition rmul_well_defined {s t u v : reg_seq} (H : requiv s u) (H2 : requiv t v) :
|
|
|
|
|
requiv (s * t) (u * v) :=
|
|
|
|
|
mul_well_defined (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u) (reg_seq.is_reg v) H H2
|
|
|
|
|
|
|
|
|
|
definition rneg_well_defined {s t : reg_seq} (H : requiv s t) : requiv (-s) (-t) :=
|
|
|
|
|
neg_well_defined H
|
|
|
|
|
|
|
|
|
|
theorem requiv_is_equiv : equivalence requiv :=
|
|
|
|
|
mk_equivalence requiv requiv.refl requiv.symm requiv.trans
|
|
|
|
|
|
|
|
|
|
definition reg_seq.to_setoid [instance] : setoid reg_seq :=
|
|
|
|
|
⦃setoid, r := requiv, iseqv := requiv_is_equiv⦄
|
|
|
|
|
|
|
|
|
|
definition r_zero : reg_seq :=
|
|
|
|
|
reg_seq.mk (zero) (zero_is_reg)
|
|
|
|
|
|
|
|
|
|
definition r_one : reg_seq :=
|
|
|
|
|
reg_seq.mk (one) (one_is_reg)
|
|
|
|
|
|
|
|
|
|
theorem r_add_comm (s t : reg_seq) : requiv (s + t) (t + s) :=
|
|
|
|
|
s_add_comm (reg_seq.sq s) (reg_seq.sq t)
|
|
|
|
|
|
|
|
|
|
theorem r_add_assoc (s t u : reg_seq) : requiv (s + t + u) (s + (t + u)) :=
|
|
|
|
|
s_add_assoc (reg_seq.sq s) (reg_seq.sq t) (reg_seq.sq u) (reg_seq.is_reg s) (reg_seq.is_reg u)
|
|
|
|
|
|
|
|
|
|
theorem r_zero_add (s : reg_seq) : requiv (r_zero + s) s :=
|
|
|
|
|
s_zero_add (reg_seq.sq s) (reg_seq.is_reg s)
|
|
|
|
|
|
|
|
|
|
theorem r_add_zero (s : reg_seq) : requiv (s + r_zero) s :=
|
|
|
|
|
s_add_zero (reg_seq.sq s) (reg_seq.is_reg s)
|
|
|
|
|
|
|
|
|
|
theorem r_neg_cancel (s : reg_seq) : requiv (-s + s) r_zero :=
|
|
|
|
|
s_neg_cancel (reg_seq.sq s) (reg_seq.is_reg s)
|
|
|
|
|
|
2015-05-26 03:22:37 +00:00
|
|
|
|
theorem r_mul_comm (s t : reg_seq) : requiv (s * t) (t * s) :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
s_mul_comm (reg_seq.sq s) (reg_seq.sq t)
|
|
|
|
|
|
|
|
|
|
theorem r_mul_assoc (s t u : reg_seq) : requiv (s * t * u) (s * (t * u)) :=
|
2015-05-26 03:22:37 +00:00
|
|
|
|
s_mul_assoc (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u)
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
theorem r_mul_one (s : reg_seq) : requiv (s * r_one) s :=
|
|
|
|
|
s_mul_one (reg_seq.is_reg s)
|
|
|
|
|
|
|
|
|
|
theorem r_one_mul (s : reg_seq) : requiv (r_one * s) s :=
|
|
|
|
|
s_one_mul (reg_seq.is_reg s)
|
|
|
|
|
|
|
|
|
|
theorem r_distrib (s t u : reg_seq) : requiv (s * (t + u)) (s * t + s * u) :=
|
|
|
|
|
s_distrib (reg_seq.is_reg s) (reg_seq.is_reg t) (reg_seq.is_reg u)
|
|
|
|
|
|
2015-05-29 04:11:00 +00:00
|
|
|
|
theorem r_zero_nequiv_one : ¬ requiv r_zero r_one :=
|
2015-06-10 02:46:30 +00:00
|
|
|
|
zero_nequiv_one
|
2015-05-29 04:11:00 +00:00
|
|
|
|
|
2015-06-23 12:17:50 +00:00
|
|
|
|
definition r_const (a : ℚ) : reg_seq := reg_seq.mk (const a) (const_reg a)
|
|
|
|
|
|
|
|
|
|
theorem r_add_consts (a b : ℚ) : requiv (r_const a + r_const b) (r_const (a + b)) := add_consts a b
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem r_mul_consts (a b : ℚ) : requiv (r_const a * r_const b) (r_const (a * b)) := mul_consts a b
|
|
|
|
|
|
2015-07-27 21:49:26 +00:00
|
|
|
|
theorem r_neg_const (a : ℚ) : requiv (-r_const a) (r_const (-a)) := neg_const a
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
end rat_seq
|
2015-05-26 02:05:53 +00:00
|
|
|
|
----------------------------------------------
|
|
|
|
|
-- take quotients to get ℝ and show it's a comm ring
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
open rat_seq
|
2015-05-26 02:05:53 +00:00
|
|
|
|
definition real := quot reg_seq.to_setoid
|
2015-07-24 18:59:46 +00:00
|
|
|
|
namespace real
|
2015-05-26 02:05:53 +00:00
|
|
|
|
notation `ℝ` := real
|
|
|
|
|
|
|
|
|
|
definition add (x y : ℝ) : ℝ :=
|
2015-05-26 03:22:37 +00:00
|
|
|
|
(quot.lift_on₂ x y (λ a b, quot.mk (a + b))
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d,
|
|
|
|
|
quot.sound (radd_well_defined Hab Hcd)))
|
2015-07-01 00:34:35 +00:00
|
|
|
|
protected definition prio := num.pred rat.prio
|
|
|
|
|
infix [priority real.prio] `+` := add
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
definition mul (x y : ℝ) : ℝ :=
|
2015-05-26 03:22:37 +00:00
|
|
|
|
(quot.lift_on₂ x y (λ a b, quot.mk (a * b))
|
2015-05-26 02:05:53 +00:00
|
|
|
|
(take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d,
|
|
|
|
|
quot.sound (rmul_well_defined Hab Hcd)))
|
2015-07-01 00:34:35 +00:00
|
|
|
|
infix [priority real.prio] `*` := mul
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
definition neg (x : ℝ) : ℝ :=
|
|
|
|
|
(quot.lift_on x (λ a, quot.mk (-a)) (take a b : reg_seq, take Hab : requiv a b,
|
|
|
|
|
quot.sound (rneg_well_defined Hab)))
|
2015-07-01 00:34:35 +00:00
|
|
|
|
prefix [priority real.prio] `-` := neg
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
open rat -- no coercions before
|
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
definition of_rat [coercion] (a : ℚ) : ℝ := quot.mk (r_const a)
|
2015-08-27 13:39:39 +00:00
|
|
|
|
definition of_num [coercion] [reducible] (n : num) : ℝ := of_rat (rat.of_num n)
|
|
|
|
|
|
|
|
|
|
--definition zero : ℝ := 0
|
|
|
|
|
--definition one : ℝ := 1
|
|
|
|
|
--definition zero : ℝ := quot.mk r_zero
|
2015-05-26 02:05:53 +00:00
|
|
|
|
--notation 0 := zero
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
--definition one : ℝ := quot.mk r_one
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
|
|
|
|
theorem add_comm (x y : ℝ) : x + y = y + x :=
|
|
|
|
|
quot.induction_on₂ x y (λ s t, quot.sound (r_add_comm s t))
|
|
|
|
|
|
|
|
|
|
theorem add_assoc (x y z : ℝ) : x + y + z = x + (y + z) :=
|
|
|
|
|
quot.induction_on₃ x y z (λ s t u, quot.sound (r_add_assoc s t u))
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem zero_add (x : ℝ) : 0 + x = x :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on x (λ s, quot.sound (r_zero_add s))
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem add_zero (x : ℝ) : x + 0 = x :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on x (λ s, quot.sound (r_add_zero s))
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem neg_cancel (x : ℝ) : -x + x = 0 :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on x (λ s, quot.sound (r_neg_cancel s))
|
|
|
|
|
|
|
|
|
|
theorem mul_assoc (x y z : ℝ) : x * y * z = x * (y * z) :=
|
|
|
|
|
quot.induction_on₃ x y z (λ s t u, quot.sound (r_mul_assoc s t u))
|
|
|
|
|
|
|
|
|
|
theorem mul_comm (x y : ℝ) : x * y = y * x :=
|
|
|
|
|
quot.induction_on₂ x y (λ s t, quot.sound (r_mul_comm s t))
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem one_mul (x : ℝ) : 1 * x = x :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on x (λ s, quot.sound (r_one_mul s))
|
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem mul_one (x : ℝ) : x * 1 = x :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on x (λ s, quot.sound (r_mul_one s))
|
|
|
|
|
|
2015-09-12 14:00:34 +00:00
|
|
|
|
theorem left_distrib (x y z : ℝ) : x * (y + z) = x * y + x * z :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
quot.induction_on₃ x y z (λ s t u, quot.sound (r_distrib s t u))
|
|
|
|
|
|
2015-09-12 14:00:34 +00:00
|
|
|
|
theorem right_distrib (x y z : ℝ) : (x + y) * z = x * z + y * z :=
|
|
|
|
|
by rewrite [mul_comm, left_distrib, {x * _}mul_comm, {y * _}mul_comm] -- this shouldn't be necessary
|
2015-05-26 02:05:53 +00:00
|
|
|
|
|
2015-08-27 13:39:39 +00:00
|
|
|
|
theorem zero_ne_one : ¬ (0 : ℝ) = 1 :=
|
|
|
|
|
take H : 0 = 1,
|
2015-05-29 04:11:00 +00:00
|
|
|
|
absurd (quot.exact H) (r_zero_nequiv_one)
|
|
|
|
|
|
2015-06-24 07:14:31 +00:00
|
|
|
|
protected definition comm_ring [reducible] : algebra.comm_ring ℝ :=
|
2015-05-26 02:05:53 +00:00
|
|
|
|
begin
|
|
|
|
|
fapply algebra.comm_ring.mk,
|
|
|
|
|
exact add,
|
|
|
|
|
exact add_assoc,
|
2015-08-27 13:39:39 +00:00
|
|
|
|
exact of_num 0,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
exact zero_add,
|
|
|
|
|
exact add_zero,
|
|
|
|
|
exact neg,
|
|
|
|
|
exact neg_cancel,
|
|
|
|
|
exact add_comm,
|
|
|
|
|
exact mul,
|
|
|
|
|
exact mul_assoc,
|
2015-08-27 13:39:39 +00:00
|
|
|
|
apply of_num 1,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply one_mul,
|
|
|
|
|
apply mul_one,
|
2015-09-12 14:00:34 +00:00
|
|
|
|
apply left_distrib,
|
|
|
|
|
apply right_distrib,
|
2015-05-26 02:05:53 +00:00
|
|
|
|
apply mul_comm
|
|
|
|
|
end
|
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem of_rat_add (a b : ℚ) : of_rat a + of_rat b = of_rat (a + b) :=
|
2015-09-11 03:00:18 +00:00
|
|
|
|
quot.sound (r_add_consts a b)
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-09-11 03:00:18 +00:00
|
|
|
|
theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := eq.symm (quot.sound (r_neg_const a))
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem of_rat_mul (a b : ℚ) : of_rat a * of_rat b = of_rat (a * b) :=
|
2015-09-11 03:00:18 +00:00
|
|
|
|
quot.sound (r_mul_consts a b)
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-07-16 17:18:35 +00:00
|
|
|
|
theorem add_half_of_rat (n : ℕ+) : of_rat (2 * n)⁻¹ + of_rat (2 * n)⁻¹ = of_rat (n⁻¹) :=
|
|
|
|
|
by rewrite [of_rat_add, pnat.add_halves]
|
2015-06-23 12:17:50 +00:00
|
|
|
|
|
2015-05-26 02:05:53 +00:00
|
|
|
|
end real
|