feat(algebra/archimedean): generalize real thms to archimedean fields

algebra/archimedean.lean

@@ -0,0 +1,226 @@
+/-
+Copyright (c) 2018 Mario Carneiro. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Mario Carneiro
+
+Archimedean groups and fields.
+-/
+import algebra.group_power data.rat data.int.order
+
+local infix ` • `:73 := add_monoid.smul
+
+variables {α : Type*}
+
+class floor_ring (α) extends linear_ordered_ring α :=
+(floor : α → ℤ)
+(le_floor : ∀ (z : ℤ) (x : α), z ≤ floor x ↔ (z : α) ≤ x)
+
+instance : floor_ring ℤ :=
+{ floor := id, le_floor := by simp,
+  ..linear_ordered_comm_ring.to_linear_ordered_ring ℤ }
+
+instance : floor_ring ℚ :=
+{ floor := rat.floor, le_floor := @rat.le_floor,
+  ..linear_ordered_comm_ring.to_linear_ordered_ring ℚ }
+
+section
+variable [floor_ring α]
+
+def floor : α → ℤ := floor_ring.floor
+
+notation `⌊` x `⌋` := floor x
+
+theorem le_floor : ∀ {z : ℤ} {x : α}, z ≤ ⌊x⌋ ↔ (z : α) ≤ x :=
+floor_ring.le_floor
+
+theorem floor_lt {x : α} {z : ℤ} : ⌊x⌋ < z ↔ x < z :=
+le_iff_le_iff_lt_iff_lt.1 le_floor
+
+theorem floor_le (x : α) : (⌊x⌋ : α) ≤ x :=
+le_floor.1 (le_refl _)
+
+theorem floor_nonneg {x : α} : 0 ≤ ⌊x⌋ ↔ 0 ≤ x :=
+by simpa using @le_floor _ _ 0 x
+
+theorem lt_succ_floor (x : α) : x < ⌊x⌋.succ :=
+floor_lt.1 $ int.lt_succ_self _
+
+theorem lt_floor_add_one (x : α) : x < ⌊x⌋ + 1 :=
+by simpa [int.succ] 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)
+
+@[simp] theorem floor_coe (z : ℤ) : ⌊(z:α)⌋ = z :=
+eq_of_forall_le_iff $ λ a, by rw [le_floor, int.cast_le]
+
+theorem floor_mono {a b : α} (h : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋ :=
+le_floor.2 (le_trans (floor_le _) h)
+
+@[simp] theorem floor_add_int (x : α) (z : ℤ) : ⌊x + z⌋ = ⌊x⌋ + z :=
+eq_of_forall_le_iff $ λ a, by rw [le_floor,
+  ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, int.cast_sub]
+
+theorem floor_sub_int (x : α) (z : ℤ) : ⌊x - z⌋ = ⌊x⌋ - z :=
+eq.trans (by rw [int.cast_neg]; refl) (floor_add_int _ _)
+
+/-- `ceil x` is the smallest integer `z` such that `x ≤ z` -/
+def ceil (x : α) : ℤ := -⌊-x⌋
+
+notation `⌈` x `⌉` := ceil x
+
+theorem ceil_le {z : ℤ} {x : α} : ⌈x⌉ ≤ z ↔ x ≤ z :=
+by rw [ceil, neg_le, le_floor, int.cast_neg, neg_le_neg_iff]
+
+theorem lt_ceil {x : α} {z : ℤ} : z < ⌈x⌉ ↔ (z:α) < x :=
+le_iff_le_iff_lt_iff_lt.1 ceil_le
+
+theorem le_ceil (x : α) : x ≤ ⌈x⌉ :=
+ceil_le.1 (le_refl _)
+
+@[simp] theorem ceil_coe (z : ℤ) : ⌈(z:α)⌉ = z :=
+by rw [ceil, ← int.cast_neg, floor_coe, neg_neg]
+
+theorem ceil_mono {a b : α} (h : a ≤ b) : ⌈a⌉ ≤ ⌈b⌉ :=
+ceil_le.2 (le_trans h (le_ceil _))
+
+@[simp] theorem ceil_add_int (x : α) (z : ℤ) : ⌈x + z⌉ = ⌈x⌉ + z :=
+by rw [ceil, neg_add', floor_sub_int, neg_sub, sub_eq_neg_add]; refl
+
+theorem ceil_sub_int (x : α) (z : ℤ) : ⌈x - z⌉ = ⌈x⌉ - z :=
+eq.trans (by rw [int.cast_neg]; refl) (ceil_add_int _ _)
+
+theorem ceil_lt_add_one (x : α) : (⌈x⌉ : α) < x + 1 :=
+by rw [← lt_ceil, ← int.cast_one, ceil_add_int]; apply lt_add_one
+
+end
+
+class archimedean (α) [ordered_comm_monoid α] : Prop :=
+(arch : ∀ (x : α) {y}, 0 < y → ∃ n, x ≤ y • n)
+
+theorem exists_nat_gt [linear_ordered_semiring α] [archimedean α]
+  (x : α) : ∃ n : ℕ, x < n :=
+let ⟨n, h⟩ := archimedean.arch x zero_lt_one in
+⟨n+1, lt_of_le_of_lt (by simpa using h)
+  (nat.cast_lt.2 (nat.lt_succ_self _))⟩
+
+section linear_ordered_ring
+variables [linear_ordered_ring α] [archimedean α]
+
+theorem exists_int_gt (x : α) : ∃ n : ℤ, x < n :=
+let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by simp [h]⟩
+
+theorem exists_int_lt (x : α) : ∃ n : ℤ, (n : α) < x :=
+let ⟨n, h⟩ := exists_int_gt (-x) in ⟨-n, by simp [neg_lt.1 h]⟩
+
+theorem exists_floor (x : α) :
+  ∃ (fl : ℤ), ∀ (z : ℤ), z ≤ fl ↔ (z : α) ≤ x :=
+begin
+  have := classical.prop_decidable,
+  have : ∃ (ub : ℤ), (ub:α) ≤ x ∧ ∀ (z : ℤ), (z:α) ≤ x → z ≤ ub :=
+  int.exists_greatest_of_bdd
+    (let ⟨n, hn⟩ := exists_int_gt x in ⟨n, λ z h',
+      int.cast_le.1 $ le_trans h' $ le_of_lt hn⟩)
+    (let ⟨n, hn⟩ := exists_int_lt x in ⟨n, le_of_lt hn⟩),
+  refine this.imp (λ fl h z, _),
+  cases h with h₁ h₂,
+  exact ⟨λ h, le_trans (int.cast_le.2 h) h₁, h₂ z⟩,
+end
+
+end linear_ordered_ring
+
+instance : archimedean ℕ :=
+⟨λ n m m0, ⟨n, by simpa using nat.mul_le_mul_right n m0⟩⟩
+
+instance : archimedean ℤ :=
+⟨λ n m m0, ⟨n.to_nat, begin
+  simp [add_monoid.smul_eq_mul],
+  refine le_trans (int.le_to_nat _) _,
+  simpa using mul_le_mul_of_nonneg_right
+    (int.add_one_le_iff.2 m0) (int.coe_zero_le n.to_nat),
+end⟩⟩
+
+noncomputable def archimedean.floor_ring (α)
+  [R : linear_ordered_ring α] [archimedean α] : floor_ring α :=
+{ floor := λ x, classical.some (exists_floor x),
+  le_floor := λ z x, classical.some_spec (exists_floor x) z,
+  ..R }
+
+section linear_ordered_field
+variables [linear_ordered_field α]
+
+theorem archimedean_iff_nat_lt :
+  archimedean α ↔ ∀ x : α, ∃ n : ℕ, x < n :=
+⟨@exists_nat_gt α _, λ H, ⟨λ x y y0,
+  (H (x / y)).imp $ λ n h, le_of_lt $
+  by rwa [div_lt_iff y0, ← add_monoid.smul_eq_mul'] at h⟩⟩
+
+theorem archimedean_iff_nat_le :
+  archimedean α ↔ ∀ x : α, ∃ n : ℕ, x ≤ n :=
+archimedean_iff_nat_lt.trans
+⟨λ H x, (H x).imp $ λ _, le_of_lt,
+ λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
+   lt_of_le_of_lt h (nat.cast_lt.2 (lt_add_one _))⟩⟩
+
+theorem exists_rat_gt [archimedean α] (x : α) : ∃ q : ℚ, x < q :=
+let ⟨n, h⟩ := exists_nat_gt x in ⟨n, by simp [h]⟩
+
+theorem archimedean_iff_rat_lt :
+  archimedean α ↔ ∀ x : α, ∃ q : ℚ, x < q :=
+⟨@exists_rat_gt α _,
+  λ H, archimedean_iff_nat_lt.2 $ λ x,
+  let ⟨q, h⟩ := H x in
+  ⟨rat.nat_ceil q, lt_of_lt_of_le h $ 
+    by simpa using (@rat.cast_le α _ _ _).2 (rat.le_nat_ceil _)⟩⟩
+
+theorem archimedean_iff_rat_le :
+  archimedean α ↔ ∀ x : α, ∃ q : ℚ, x ≤ q :=
+archimedean_iff_rat_lt.trans
+⟨λ H x, (H x).imp $ λ _, le_of_lt,
+ λ H x, let ⟨n, h⟩ := H x in ⟨n+1,
+   lt_of_le_of_lt h (rat.cast_lt.2 (lt_add_one _))⟩⟩
+
+variable [archimedean α]
+
+theorem exists_rat_lt (x : α) : ∃ q : ℚ, (q : α) < x :=
+let ⟨n, h⟩ := exists_int_lt x in ⟨n, by simp [h]⟩
+
+theorem exists_pos_rat_lt {x : α} (x0 : 0 < x) : ∃ q : ℚ, 0 < q ∧ (q : α) < x :=
+let ⟨n, h⟩ := exists_nat_gt x⁻¹ in begin
+  have n0 := nat.cast_pos.1 (lt_trans (inv_pos x0) h),
+  refine ⟨n⁻¹, inv_pos (nat.cast_pos.2 n0), _⟩,
+  simpa [rat.cast_inv_of_ne_zero, ne_of_gt n0] using
+    (inv_lt x0 (nat.cast_pos.2 n0)).1 h
+end
+
+theorem exists_rat_btwn {x y : α} (h : x < y) : ∃ q : ℚ, x < q ∧ (q:α) < y :=
+begin
+  cases exists_nat_gt (y - x)⁻¹ with n nh,
+  cases exists_floor (x * n) with z zh,
+  refine ⟨(z + 1 : ℤ) / n, _⟩,
+  have n0 := nat.cast_pos.1 (lt_trans (inv_pos (sub_pos.2 h)) nh),
+  simp [rat.cast_div_of_ne_zero, -int.cast_add, ne_of_gt n0],
+  have n0' := (@nat.cast_pos α _ _).2 n0,
+  refine ⟨(lt_div_iff n0').2 $
+    (le_iff_le_iff_lt_iff_lt.1 (zh _)).1 (lt_add_one _), _⟩,
+  simp [div_lt_iff n0', -add_comm],
+  refine lt_of_le_of_lt (add_le_add_right ((zh _).1 (le_refl _)) _) _,
+  rwa [← lt_sub_iff_add_lt', ← sub_mul,
+       ← div_lt_iff' (sub_pos.2 h), one_div_eq_inv]
+end
+
+end linear_ordered_field
+
+section
+variables [discrete_linear_ordered_field α] [archimedean α]
+
+theorem exists_rat_near (x : α) {ε : α} (ε0 : ε > 0) :
+  ∃ q : ℚ, abs (x - q) < ε :=
+let ⟨q, h₁, h₂⟩ := exists_rat_btwn $
+  lt_trans ((sub_lt_self_iff x).2 ε0) ((lt_add_iff_pos_left x).2 ε0) in
+⟨q, abs_sub_lt_iff.2 ⟨sub_lt.1 h₁, sub_lt_iff_lt_add.2 h₂⟩⟩
+
+end
+
+instance : archimedean ℚ :=
+archimedean_iff_rat_le.2 $ λ q, ⟨q, by simp⟩

algebra/group_power.lean

@@ -11,7 +11,7 @@ a^n is used for the first, but users can locally redefine it to gpow when needed
 
 Note: power adopts the convention that 0^0=1.
 -/
-import data.nat.basic data.int.basic algebra.group algebra.field data.list.basic
+import algebra.char_zero data.int.basic algebra.group algebra.ordered_field data.list.basic
 
 universe u
 variable {α : Type u}
@@ -80,6 +80,9 @@ theorem add_monoid.smul_mul (a : β) (m : ℕ) : ∀ n, a•(m * n) = (a•m)•
 | (n+1) := by rw [nat.mul_succ, add_monoid.smul_add, smul_succ', add_monoid.smul_mul]
 attribute [to_additive add_monoid.smul_mul] pow_mul
 
+@[simp] theorem add_monoid.one_smul [has_one β] : ∀ n, (1 : β) • n = n :=
+nat.eq_cast _ (add_monoid.smul_zero _) (add_monoid.smul_one _) (add_monoid.smul_add _)
+
 @[to_additive smul_bit0]
 theorem pow_bit0 (a : α) (n : ℕ) : a ^ bit0 n = a^n * a^n := pow_add _ _ _
 
@@ -257,6 +260,32 @@ attribute [to_additive gsmul_bit1] gpow_bit1
 
 end group
 
+theorem add_monoid.smul_eq_mul [semiring α] (a : α) : ∀ n, a • n = a * n
+| 0 := by simp
+| (n+1) := by simp [add_monoid.smul_eq_mul n, mul_add, smul_succ']
+
+theorem add_monoid.smul_eq_mul' [semiring α] (a : α) (n) : a • n = n * a :=
+by rw [add_monoid.smul_eq_mul, nat.mul_cast_comm]
+
+theorem add_monoid.mul_smul_assoc [semiring α] (a b : α) (n) : (a * b) • n = a * b • n :=
+by rw [add_monoid.smul_eq_mul, add_monoid.smul_eq_mul, mul_assoc]
+
+theorem add_monoid.mul_smul_right [semiring α] (a b : α) (n) : (a * b) • n = a • n * b :=
+by rw [add_monoid.smul_eq_mul', add_monoid.smul_eq_mul', mul_assoc]
+
+theorem gsmul_eq_mul [ring α] (a : α) : ∀ n, gsmul a n = a * n
+| (n : ℕ) := by simp [add_monoid.smul_eq_mul]
+| -[1+ n] := by simp [add_monoid.smul_eq_mul, -add_comm, mul_add]
+
+theorem gsmul_eq_mul' [ring α] (a : α) (n) : gsmul a n = n * a :=
+by rw [gsmul_eq_mul, int.mul_cast_comm]
+
+theorem mul_gsmul_assoc [ring α] (a b : α) (n) : gsmul (a * b) n = a * gsmul b n :=
+by rw [gsmul_eq_mul, gsmul_eq_mul, mul_assoc]
+
+theorem mul_gsmul_right [ring α] (a b : α) (n) : gsmul (a * b) n = gsmul a n * b :=
+by rw [gsmul_eq_mul', gsmul_eq_mul', mul_assoc]
+
 theorem pow_ne_zero [domain α] {a : α} (n : ℕ) (h : a ≠ 0) : a ^ n ≠ 0 :=
 by induction n with n ih; simp [pow_succ, mul_eq_zero, *]
 
@@ -271,35 +300,55 @@ by simp [inv_eq_one_div, -one_div_eq_inv, ha]
 @[simp] theorem div_pow [field α] (a : α) {b : α} (hb : b ≠ 0) (n) : (a / b) ^ n = a ^ n / b ^ n :=
 by rw [div_eq_mul_one_div, mul_pow, one_div_pow hb, ← div_eq_mul_one_div]
 
-section ordered_ring
-variable [linear_ordered_ring α]
+theorem add_monoid.smul_nonneg [ordered_comm_monoid α] {a : α} (H : 0 ≤ a) : ∀ n, 0 ≤ a • n
+| 0     := le_refl _
+| (n+1) := add_nonneg' H (add_monoid.smul_nonneg n)
+
+section linear_ordered_semiring
+variable [linear_ordered_semiring α]
 
-theorem pow_pos {a : α} (H : a > 0) : ∀ (n : ℕ), a ^ n > 0
-| 0     := by simp; apply zero_lt_one
-| (n+1) := begin simp [_root_.pow_succ], apply mul_pos, assumption, apply pow_pos end
+theorem pow_pos {a : α} (H : 0 < a) : ∀ (n : ℕ), 0 < a ^ n
+| 0     := by simp [zero_lt_one]
+| (n+1) := by simpa [pow_succ] using mul_pos H (pow_pos _)
 
-theorem pow_nonneg {a : α} (H : a ≥ 0) : ∀ (n : ℕ), a ^ n ≥ 0
-| 0     := by simp; apply zero_le_one
-| (n+1) := begin simp [_root_.pow_succ], apply mul_nonneg, assumption, apply pow_nonneg end
+theorem pow_nonneg {a : α} (H : 0 ≤ a) : ∀ (n : ℕ), 0 ≤ a ^ n
+| 0     := by simp [zero_le_one]
+| (n+1) := by simpa [pow_succ] using mul_nonneg H (pow_nonneg _)
 
-theorem pow_ge_one_of_ge_one {a : α} (H : a ≥ 1) : ∀ (n : ℕ), a ^ n ≥ 1
+theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | 0     := by simp; apply le_refl
 | (n+1) :=
   begin
-   simp [_root_.pow_succ], rw ←(one_mul (1 : α)),
+   simp [pow_succ], rw ← one_mul (1 : α),
    apply mul_le_mul,
    assumption,
-   apply pow_ge_one_of_ge_one,
+   apply one_le_pow_of_one_le,
    apply zero_le_one,
    transitivity, apply zero_le_one, assumption
   end
 
+theorem pow_ge_one_add_mul {a : α} (H : a ≥ 0) :
+  ∀ (n : ℕ), 1 + a • n ≤ (1 + a) ^ n
+| 0     := by simp
+| (n+1) := begin
+  rw [pow_succ', smul_succ'],
+  refine le_trans _ (mul_le_mul_of_nonneg_right
+    (pow_ge_one_add_mul n) (add_nonneg zero_le_one H)),
+  rw [mul_add, mul_one, ← add_assoc, add_le_add_iff_left],
+  simpa using mul_le_mul_of_nonneg_right
+    ((le_add_iff_nonneg_right 1).2 (add_monoid.smul_nonneg H n)) H
+end
+
 theorem pow_le_pow {a : α} {n m : ℕ} (ha : 1 ≤ a) (h : n ≤ m) : a ^ n ≤ a ^ m :=
 let ⟨k, hk⟩ := nat.le.dest h in
 calc a ^ n = a ^ n * 1 : by simp
   ... ≤ a ^ n * a ^ k : mul_le_mul_of_nonneg_left
-    (pow_ge_one_of_ge_one ha _)
+    (one_le_pow_of_one_le ha _)
     (pow_nonneg (le_trans zero_le_one ha) _)
   ... = a ^ m : by rw [←hk, pow_add]
 
-end ordered_ring
+end linear_ordered_semiring
+
+theorem pow_ge_one_add_sub_mul [linear_ordered_ring α]
+  {a : α} (H : a ≥ 1) (n : ℕ) : 1 + (a - 1) • n ≤ a ^ n :=
+by simpa using pow_ge_one_add_mul (sub_nonneg.2 H) n

analysis/complex.lean

@@ -5,7 +5,7 @@ Author: Mario Carneiro
 
 Topology of the complex numbers.
 -/
-import data.complex analysis.metric_space
+import data.complex.basic analysis.metric_space
 
 noncomputable theory
 open filter

analysis/ennreal.lean

@@ -405,7 +405,7 @@ protected lemma lt_iff_exists_rat_btwn :
   rcases lt_iff_exists_of_real.1 h with ⟨p, p0, rfl, _⟩;
   rcases dense h with ⟨c, pc, cb⟩;
   rcases lt_iff_exists_of_real.1 cb with ⟨r, r0, rfl, _⟩;
-  rcases real.exists_rat_btwn ((of_real_lt_of_real_iff p0 r0).1 pc) with ⟨q, pq, qr⟩;
+  rcases exists_rat_btwn ((of_real_lt_of_real_iff p0 r0).1 pc) with ⟨q, pq, qr⟩;
   have q0 := le_trans p0 (le_of_lt pq); exact
   ⟨q, rat.cast_nonneg.1 q0, (of_real_lt_of_real_iff p0 q0).2 pq,
     lt_trans ((of_real_lt_of_real_iff q0 r0).2 qr) cb⟩,

analysis/limits.lean

@@ -82,7 +82,7 @@ lemma mul_add_one_le_pow {r : ℝ} (hr : 0 ≤ r) : ∀{n:ℕ}, (n:ℝ) * r + 1
 
 lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : r > 1) : tendsto (λn:ℕ, r ^ n) at_top at_top :=
 tendsto_infi.2 $ assume p, tendsto_principal.2 $
-  let ⟨n, hn⟩ := real.exists_nat_gt (p / (r - 1)) in
+  let ⟨n, hn⟩ := exists_nat_gt (p / (r - 1)) in
   have hn_nn : (0:ℝ) ≤ n, from nat.cast_nonneg n,
   have r - 1 > 0, from sub_lt_iff.mp $ by simp; assumption,
   have p ≤ r ^ n,

analysis/measure_theory/borel_space.lean

@@ -220,13 +220,13 @@ have ∀a b : ℚ, a < b → g.is_measurable (Ioo a b),
     from assume q, g.is_measurable_compl _ $ hg q,
   have (⋃c>a, - Iio (c:ℝ)) ∩ Iio b = Ioo a b,
     from set.ext $ assume x,
-    have h₁ : x < b → ∀p:ℚ, (p:ℝ) ≤ x → p > a → (a:ℝ) < x,
-      from assume hxb p hpx hpa, lt_of_lt_of_le (rat.cast_lt.2 hpa) hpx,
-    have h₂ : x < b → (a:ℝ) < x → (∃ (i : ℚ), (i:ℝ) ≤ x ∧ i > a),
-      from assume hxb hax,
+    have h₁ : ∀p:ℚ, p > a → (p:ℝ) ≤ x → x < b → (a:ℝ) < x,
+      from assume p hpa hpx hxb, lt_of_lt_of_le (rat.cast_lt.2 hpa) hpx,
+    have h₂ : (a:ℝ) < x → x < b → (∃ (i : ℚ), i > a ∧ (i:ℝ) ≤ x),
+      from assume hax hxb,
       let ⟨c, hac, hcx⟩ := exists_rat_btwn hax in
-      ⟨c, le_of_lt hcx, rat.cast_lt.1 hac⟩,
-    by simp [iff_def, Iio, Ioo, and_comm] {contextual := tt}; exact ⟨h₁, h₂⟩,
+      ⟨c, rat.cast_lt.1 hac, le_of_lt hcx⟩,
+    by simp [iff_def, Iio, Ioo] {contextual := tt}; exact ⟨h₁, h₂⟩,
   this ▸ @is_measurable_inter _ g _ _
     (@is_measurable_bUnion _ _ g _ _ countable_encodable $ assume b hb, hgc b)
     (hg b),