feat(library/algebra/ring_power): add properties of power in ring structures

library/algebra/algebra.md

@@ -13,7 +13,9 @@ Algebraic structures.
 * [ring](ring.lean)
 * [ordered_group](ordered_group.lean)
 * [ordered_ring](ordered_ring.lean)
+* [ring_power](ring_power.lean) : power in ring structures
 * [field](field.lean)
 * [ordered_field](ordered_field.lean)
+
 * [category](category/category.md) : category theory
 

library/algebra/ring_power.lean

@@ -0,0 +1,63 @@
+/-
+Copyright (c) 2015 Jeremy Avigad. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Author: Jeremy Avigad
+
+Properties of the power operation in an ordered ring.
+
+(Right now, this file is just a stub. More soon.)
+-/
+import .group_power
+open nat
+
+namespace algebra
+
+variable {A : Type}
+
+section linear_ordered_semiring
+variable [s : linear_ordered_semiring A]
+include s
+
+theorem pow_pos_of_pos {x : A} (i : ℕ) (H : x > 0) : x^i > 0 :=
+begin
+  induction i with [j, ih],
+    {show (1 : A) > 0, from zero_lt_one},
+    {show x^(succ j) > 0, from mul_pos ih H}
+end
+
+theorem pow_nonneg_of_nonneg {x : A} (i : ℕ) (H : x ≥ 0) : x^i ≥ 0 :=
+begin
+  induction i with [j, ih],
+    {show (1 : A) ≥ 0, from le_of_lt zero_lt_one},
+    {show x^(succ j) ≥ 0, from mul_nonneg ih H}
+end
+
+theorem pow_le_pow_of_le {x y : A} (i : ℕ) (H₁ : 0 ≤ x) (H₂ : x ≤ y) : x^i ≤ y^i :=
+begin
+  induction i with [i, ih],
+    {rewrite *pow_zero, apply le.refl},
+  rewrite *pow_succ,
+  have H : 0 ≤ y^i, from pow_nonneg_of_nonneg i (le.trans H₁ H₂),
+  apply mul_le_mul ih H₂ H₁ H
+end
+
+theorem pow_ge_one {x : A} (i : ℕ) (xge1 : x ≥ 1) : x^i ≥ 1 :=
+assert H : x^i ≥ 1^i, from pow_le_pow_of_le i (le_of_lt zero_lt_one) xge1,
+by rewrite one_pow at H; exact H
+
+set_option formatter.hide_full_terms false
+
+theorem pow_gt_one {x : A} {i : ℕ} (xgt1 : x > 1) (ipos : i > 0) : x^i > 1 :=
+assert xpos : x > 0, from lt.trans zero_lt_one xgt1,
+begin
+  induction i with [i, ih],
+    {exfalso, exact !nat.lt.irrefl ipos},
+  have xige1 : x^i ≥ 1, from pow_ge_one _ (le_of_lt xgt1),
+  rewrite [pow_succ', -mul_one 1, ↑has_lt.gt],
+  apply mul_lt_mul xgt1 xige1 zero_lt_one,
+  apply le_of_lt xpos
+end
+
+end linear_ordered_semiring
+
+end algebra

library/data/nat/power.lean

@@ -5,7 +5,7 @@ Authors: Leonardo de Moura, Jeremy Avigad
 
 The power function on the natural numbers.
 -/
-import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.group_power
+import data.nat.basic data.nat.order data.nat.div data.nat.gcd algebra.ring_power
 
 namespace nat
 
@@ -17,14 +17,33 @@ section migrate_algebra
   definition pow (a : ℕ) (n : ℕ) : ℕ := algebra.pow a n
   infix ^ := pow
 
+  theorem pow_le_pow_of_le {x y : ℕ} (i : ℕ) (H : x ≤ y) : x^i ≤ y^i :=
+  algebra.pow_le_pow_of_le i !zero_le H
+
   migrate from algebra with nat
     replacing dvd → dvd, has_le.ge → ge, has_lt.gt → gt, pow → pow
     hiding add_pos_of_pos_of_nonneg,  add_pos_of_nonneg_of_pos,
       add_eq_zero_iff_eq_zero_and_eq_zero_of_nonneg_of_nonneg, le_add_of_nonneg_of_le,
       le_add_of_le_of_nonneg, lt_add_of_nonneg_of_lt, lt_add_of_lt_of_nonneg,
-      lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right
+      lt_of_mul_lt_mul_left, lt_of_mul_lt_mul_right, pos_of_mul_pos_left, pos_of_mul_pos_right,
+      pow_nonneg_of_nonneg
 end migrate_algebra
 
+-- generalize to semirings?
+theorem le_pow_self {x : ℕ} (H : x > 1) : ∀ i, i ≤ x^i
+| 0        := !zero_le
+| (succ j) := have xpos : x > 0, from lt.trans zero_lt_one H,
+              have xjge1 : x^j ≥ 1, from succ_le_of_lt (pow_pos_of_pos _ xpos),
+              have xge2 : x ≥ 2, from succ_le_of_lt H,
+              calc
+                succ j = j + 1         : rfl
+                   ... ≤ x^j + 1       : add_le_add_right (le_pow_self j)
+                   ... ≤ x^j + x^j     : add_le_add_left xjge1
+                   ... = x^j * (1 + 1) : by rewrite [mul.left_distrib, *mul_one]
+                   ... = x^j * 2       : rfl
+                   ... ≤ x^j * x       : mul_le_mul_left _ xge2
+                   ... = x^(succ j)    : rfl
+
 -- TODO: eventually this will be subsumed under the algebraic theorems
 
 theorem mul_self_eq_pow_2 (a : nat) : a * a = pow a 2 :=