half finished decimal expansions

Author: kbuzzard

src/algebra/archimedean.lean

@@ -37,6 +37,9 @@ lt_iff_lt_of_le_iff_le le_floor
 theorem floor_le (x : α) : (⌊x⌋ : α) ≤ x :=
 le_floor.1 (le_refl _)
 
+theorem sub_floor_nonneg (x : α) : 0 ≤ x - ⌊x⌋ :=
+sub_nonneg.2 $ floor_le _
+
 theorem floor_nonneg {x : α} : 0 ≤ ⌊x⌋ ↔ 0 ≤ x :=
 by rw [le_floor]; refl
 
@@ -49,6 +52,9 @@ by simpa only [int.succ, int.cast_add, int.cast_one] using lt_succ_floor x
 theorem sub_one_lt_floor (x : α) : x - 1 < ⌊x⌋ :=
 sub_lt_iff_lt_add.2 (lt_floor_add_one x)
 
+theorem sub_floor_lt_one (x : α) : x - ⌊x⌋ < 1 :=
+sub_lt.1 $ sub_one_lt_floor _
+
 @[simp] theorem floor_coe (z : ℤ) : ⌊(z:α)⌋ = z :=
 eq_of_forall_le_iff $ λ a, by rw [le_floor, int.cast_le]
 
@@ -67,6 +73,11 @@ eq_of_forall_le_iff $ λ a, by rw [le_floor,
 theorem floor_sub_int (x : α) (z : ℤ) : ⌊x - z⌋ = ⌊x⌋ - z :=
 eq.trans (by rw [int.cast_neg]; refl) (floor_add_int _ _)
 
+lemma floor_of_bounds (r : α) (z : ℤ) :
+  ↑z ≤ r ∧ r < (z + 1) ↔ ⌊ r ⌋ = z :=
+by rw [←le_floor, ←int.cast_one, ←int.cast_add, ←floor_lt,
+int.lt_add_one_iff, le_antisymm_iff, and.comm]
+
 /-- `ceil x` is the smallest integer `z` such that `x ≤ z` -/
 def ceil (x : α) : ℤ := -⌊-x⌋
 

src/algebra/expansion.lean

@@ -0,0 +1,62 @@
+/-
+Copyright (c) 2019 Kevin Buzzard. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Kevin Buzzard
+-/
+
+import algebra.archimedean tactic.linarith
+
+/-
+
+This file provides decimal (and more generally base b>=2) expansions of "floor rings",
+that is, ordered rings equipped with a floor function to the integers, such as
+the rational or real numbers.
+
+If r is an element of such a ring, then expansion.digit b r n is the (n+1)'st digit
+after the decimal point in the base b expansion of r, so 0 <= expansion.digit b r n < b.
+In other words, if aₙ = expansion.digit b r n then for a real number r, we have
+r = (floor r) + 0.a₀a₁a₂... in base b. We have 0 ≤ aₙ < b (digit_lt_base).
+
+-/
+
+namespace expansion
+
+variables {α : Type*} [linear_ordered_ring α] [floor_ring α]
+
+def digit_aux (b : ℕ) (r : α) : ℕ → α
+| 0 := (r - ⌊r⌋) * b
+| (n + 1) := (digit_aux n - ⌊digit_aux n⌋) * b
+
+lemma digit_aux_nonneg (b : ℕ) (r : α) (n : ℕ) : 0 ≤ digit_aux b r n :=
+nat.cases_on n (mul_nonneg (sub_floor_nonneg _) (nat.cast_nonneg _))
+  (λ _,(mul_nonneg (sub_floor_nonneg _) (nat.cast_nonneg _)))
+
+lemma digit_aux_lt_base {b : ℕ} (hb : 0 < b) (r : α) (n : ℕ) : digit_aux b r n < b :=
+nat.cases_on n
+  ((mul_lt_iff_lt_one_left (show (0 : α) < b, by simp [hb])).2 (sub_floor_lt_one _))
+  (λ n, (mul_lt_iff_lt_one_left (show (0 : α) < b, by simp [hb])).2 (sub_floor_lt_one _))
+
+definition digit (b : ℕ) (r : α) (n : ℕ) := int.to_nat (⌊digit_aux b r n⌋)
+
+lemma digit_lt_base {b : ℕ} (hb : 0 < b) (r : α) (n : ℕ) : digit b r n < b :=
+begin
+  have h : (⌊digit_aux b r n⌋ : α) < b,
+    exact lt_of_le_of_lt (floor_le _) (digit_aux_lt_base hb r n),
+  have h2 : ⌊digit_aux b r n⌋ = digit b r n,
+    exact (int.to_nat_of_nonneg (floor_nonneg.2 $ digit_aux_nonneg b r n)).symm,
+  have h3 : ((digit b r n : ℤ) : α) < b,
+     rwa ←h2,
+  simpa using h3,
+end
+
+theorem approx {b : ℕ} (hb : 0 < b) (r : α) (n : ℕ) :
+⌊((r - ⌊r⌋) * b ^ n)⌋ = finset.sum (finset.range n) (λ i, digit b r i) :=
+begin
+  induction n with m hm,
+  { rw [pow_zero,mul_one,finset.range_zero,finset.sum_empty,←floor_of_bounds],
+    exact ⟨sub_floor_nonneg _,by convert (sub_floor_lt_one _);simp⟩
+  },
+  sorry
+end
+
+end expansion