From cb4f71b16c1a8ba8d7e90ae56f8c68c5504a4793 Mon Sep 17 00:00:00 2001 From: Rob Lewis Date: Thu, 28 Jan 2016 17:23:02 -0500 Subject: [PATCH] feat(library/data/real): add more theorems concerning rationals embedded in reals --- library/data/real/basic.lean | 4 +++ library/data/real/complete.lean | 50 +++++++++++++++++++++++++++++++++ library/data/real/division.lean | 4 --- library/data/real/order.lean | 15 ++++++++++ 4 files changed, 69 insertions(+), 4 deletions(-) diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean index 5e2b5b114..472a7c118 100644 --- a/library/data/real/basic.lean +++ b/library/data/real/basic.lean @@ -1206,6 +1206,10 @@ theorem of_rat_neg (a : ℚ) : of_rat (-a) = -of_rat a := theorem of_rat_mul (a b : ℚ) : of_rat (a * b) = of_rat a * of_rat b := quot.sound (r_mul_consts a b) +theorem of_rat_zero : of_rat 0 = 0 := rfl + +theorem of_rat_one : of_rat 1 = 1 := rfl + open int theorem of_int_add (a b : ℤ) : of_int (a + b) = of_int a + of_int b := diff --git a/library/data/real/complete.lean b/library/data/real/complete.lean index 05597ccff..094e556c9 100644 --- a/library/data/real/complete.lean +++ b/library/data/real/complete.lean @@ -213,6 +213,56 @@ theorem approx_spec (x : ℝ) (n : ℕ+) : abs (x - (of_rat (approx x n))) ≤ o theorem approx_spec' (x : ℝ) (n : ℕ+) : abs ((of_rat (approx x n)) - x) ≤ of_rat n⁻¹ := by rewrite abs_sub; apply approx_spec +theorem ex_rat_pos_lower_bound_of_pos {x : ℝ} (H : x > 0) : ∃ q : ℚ, q > 0 ∧ of_rat q ≤ x := + if Hgeo : x ≥ 1 then + exists.intro 1 (and.intro zero_lt_one Hgeo) + else + have Hdp : 1 / x > 0, from one_div_pos_of_pos H, + begin + cases rat_approx (1 / x) 2 with q Hq, + have Hqp : q > 0, begin + apply lt_of_not_ge, + intro Hq2, + note Hx' := one_div_lt_one_div_of_lt H (lt_of_not_ge Hgeo), + rewrite div_one at Hx', + have Horqn : of_rat q ≤ 0, begin + krewrite -of_rat_zero, + apply of_rat_le_of_rat_of_le Hq2 + end, + have Hgt1 : 1 / x - of_rat q > 1, from calc + 1 / x - of_rat q = 1 / x + -of_rat q : sub_eq_add_neg + ... ≥ 1 / x : le_add_of_nonneg_right (neg_nonneg_of_nonpos Horqn) + ... > 1 : Hx', + have Hpos : 1 / x - of_rat q > 0, from gt.trans Hgt1 zero_lt_one, + rewrite [abs_of_pos Hpos at Hq], + apply not_le_of_gt Hgt1, + apply le.trans, + apply Hq, + krewrite -of_rat_one, + apply of_rat_le_of_rat_of_le, + apply inv_le_one + end, + existsi 1 / (2⁻¹ + q), + split, + apply div_pos_of_pos_of_pos, + exact zero_lt_one, + apply add_pos, + apply pnat.inv_pos, + exact Hqp, + note Hle2 := sub_le_of_abs_sub_le_right Hq, + note Hle3 := le_add_of_sub_left_le Hle2, + note Hle4 := one_div_le_of_one_div_le_of_pos H Hle3, + rewrite [of_rat_divide, of_rat_add], + exact Hle4 + end + +theorem ex_rat_neg_upper_bound_of_neg {x : ℝ} (H : x < 0) : ∃ q : ℚ, q < 0 ∧ x ≤ of_rat q := + have H' : -x > 0, from neg_pos_of_neg H, + obtain q [Hq1 Hq2], from ex_rat_pos_lower_bound_of_pos H', + exists.intro (-q) (and.intro + (neg_neg_of_pos Hq1) + (le_neg_of_le_neg Hq2)) + notation `r_seq` := ℕ+ → ℝ noncomputable definition converges_to_with_rate (X : r_seq) (a : ℝ) (N : ℕ+ → ℕ+) := diff --git a/library/data/real/division.lean b/library/data/real/division.lean index 0766ccf65..87f9af41f 100644 --- a/library/data/real/division.lean +++ b/library/data/real/division.lean @@ -649,10 +649,6 @@ protected noncomputable definition discrete_linear_ordered_field [reducible] [tr decidable_lt := dec_lt ⦄ -theorem of_rat_zero : of_rat (0:rat) = (0:real) := rfl - -theorem of_rat_one : of_rat (1:rat) = (1:real) := rfl - theorem of_rat_divide (x y : ℚ) : of_rat (x / y) = of_rat x / of_rat y := by_cases (assume yz : y = 0, by krewrite [yz, div_zero, +of_rat_zero, div_zero]) diff --git a/library/data/real/order.lean b/library/data/real/order.lean index a32d4f2a7..837f0ff6b 100644 --- a/library/data/real/order.lean +++ b/library/data/real/order.lean @@ -1165,9 +1165,24 @@ theorem of_nat_lt_of_nat_of_lt {a b : ℕ} : (a < b) → of_nat a < of_nat b := theorem lt_of_of_nat_lt_of_nat {a b : ℕ} : of_nat a < of_nat b → (a < b) := iff.mp !of_nat_lt_of_nat_iff +theorem of_rat_pos_of_pos {q : ℚ} (Hq : q > 0) : of_rat q > 0 := + of_rat_lt_of_rat_of_lt Hq + +theorem of_rat_nonneg_of_nonneg {q : ℚ} (Hq : q ≥ 0) : of_rat q ≥ 0 := + of_rat_le_of_rat_of_le Hq + +theorem of_rat_neg_of_neg {q : ℚ} (Hq : q < 0) : of_rat q < 0 := + of_rat_lt_of_rat_of_lt Hq + +theorem of_rat_nonpos_of_nonpos {q : ℚ} (Hq : q ≤ 0) : of_rat q ≤ 0 := + of_rat_le_of_rat_of_le Hq + theorem of_nat_nonneg (a : ℕ) : of_nat a ≥ 0 := of_rat_le_of_rat_of_le !rat.of_nat_nonneg +theorem of_nat_succ_pos (k : ℕ) : 0 < of_nat k + 1 := + add_pos_of_nonneg_of_pos (of_nat_nonneg k) real.zero_lt_one + theorem of_rat_pow (a : ℚ) (n : ℕ) : of_rat (a^n) = (of_rat a)^n := begin induction n with n ih,