From 954e30b59a2a6f9d91295dc1eb55d13eaa2fc0ee Mon Sep 17 00:00:00 2001
From: Rob Lewis <rlewis1@andrew.cmu.edu>
Date: Wed, 29 Jul 2015 15:44:11 -0400
Subject: [PATCH] feat(library/data/real): add more theorems to reals

---
 library/data/real/basic.lean | 20 ++++++++++++++++++++
 library/data/real/order.lean | 13 +++++++++++++
 2 files changed, 33 insertions(+)

diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index fa551eaac..e9bea89d9 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -292,6 +292,26 @@ theorem canon_bound {s : seq} (Hs : regular s) (n : ℕ+) : abs (s n) ≤ rat_of
     ... = of_nat (ubound (abs (s pone)) + (1 + 1)) : of_nat_add
     ... = of_nat (ubound (abs (s pone)) + 1 + 1) : nat.add.assoc
 
+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
+
 definition K₂ (s t : seq) := max (K s) (K t)
 
 theorem K₂_symm (s t : seq) : K₂ s t = K₂ t s :=
diff --git a/library/data/real/order.lean b/library/data/real/order.lean
index cc43862fa..0dcc00ced 100644
--- a/library/data/real/order.lean
+++ b/library/data/real/order.lean
@@ -990,6 +990,19 @@ theorem lt_of_const_lt_const {a b : ℚ} (H : s_lt (const a) (const b)) : a < b
     apply pnat.inv_pos
   end
 
+theorem s_le_of_le_pointwise {s t : seq} (Hs : regular s) (Ht : s.regular t)
+        (H : ∀ n : ℕ+, s n ≤ t n) : s_le s t :=
+  begin
+    rewrite [↑s_le, ↑nonneg, ↑sadd, ↑sneg],
+    intros,
+    apply rat.le.trans,
+    apply iff.mpr !neg_nonpos_iff_nonneg,
+    apply le_of_lt,
+    apply inv_pos,
+    apply iff.mpr !sub_nonneg_iff_le,
+    apply H
+  end
+
 -------- lift to reg_seqs
 definition r_lt (s t : reg_seq) := s_lt (reg_seq.sq s) (reg_seq.sq t)
 definition r_le (s t : reg_seq) := s_le (reg_seq.sq s) (reg_seq.sq t)