chore(algebra/group_power): generalize semiring version of Bernoull…

…i's inequality (#5831)

Now `one_add_mul_le_pow'` assumes `0 ≤ a * a`, `0 ≤ (1 + a) * (1 +
a)`, and `0 ≤ 2 + a`.

Also add a couple of convenience lemmas.

src/algebra/archimedean.lean

@@ -62,11 +62,13 @@ end
 lemma add_one_pow_unbounded_of_pos [ordered_semiring α] [nontrivial α] [archimedean α]
   (x : α) {y : α} (hy : 0 < y) :
   ∃ n : ℕ, x < (y + 1) ^ n :=
+have 0 ≤ 1 + y, from add_nonneg zero_le_one hy.le,
 let ⟨n, h⟩ := archimedean.arch x hy in
 ⟨n, calc x ≤ n •ℕ y : h
-       ... < 1 + n •ℕ y : lt_one_add _
-       ... ≤ (1 + y) ^ n : one_add_mul_le_pow' (mul_nonneg (le_of_lt hy) (le_of_lt hy))
-                             (le_of_lt $ lt_trans hy (lt_one_add y)) _
+       ... = n * y : nsmul_eq_mul _ _
+       ... < 1 + n * y : lt_one_add _
+       ... ≤ (1 + y) ^ n : one_add_mul_le_pow' (mul_nonneg hy.le hy.le) (mul_nonneg this this)
+                             (add_nonneg zero_le_two hy.le) _
        ... = (y + 1) ^ n : by rw [add_comm]⟩
 
 section linear_ordered_ring

src/algebra/group_power/lemmas.lean

@@ -287,15 +287,23 @@ section ordered_semiring
 variable [ordered_semiring R]
 
 /-- Bernoulli's inequality. This version works for semirings but requires
-an additional hypothesis `0 ≤ a * a`. -/
-theorem one_add_mul_le_pow' {a : R} (Hsqr : 0 ≤ a * a) (H : 0 ≤ 1 + a) :
-  ∀ (n : ℕ), 1 + n •ℕ a ≤ (1 + a) ^ n
-| 0     := le_of_eq $ add_zero _
-| (n+1) :=
-calc 1 + (n + 1) •ℕ a ≤ (1 + a) * (1 + n •ℕ a) :
-  by simpa [succ_nsmul, mul_add, add_mul, mul_nsmul_left, add_comm, add_left_comm]
-    using nsmul_nonneg Hsqr n
-... ≤ (1 + a)^(n+1) : mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) H
+additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
+theorem one_add_mul_le_pow' {a : R} (Hsqr : 0 ≤ a * a) (Hsqr' : 0 ≤ (1 + a) * (1 + a))
+  (H : 0 ≤ 2 + a) :
+  ∀ (n : ℕ), 1 + (n : R) * a ≤ (1 + a) ^ n
+| 0     := by simp
+| 1     := by simp
+| (n+2) :=
+have 0 ≤ (n : R) * (a * a * (2 + a)) + a * a,
+  from add_nonneg (mul_nonneg n.cast_nonneg (mul_nonneg Hsqr H)) Hsqr,
+calc 1 + (↑(n + 2) : R) * a ≤ 1 + ↑(n + 2) * a + (n * (a * a * (2 + a)) + a * a) :
+  (le_add_iff_nonneg_right _).2 this
+... = (1 + a) * (1 + a) * (1 + n * a) :
+  by { simp [add_mul, mul_add, bit0, mul_assoc, (n.cast_commute (_ : R)).left_comm],
+       ac_refl }
+... ≤ (1 + a) * (1 + a) * (1 + a)^n :
+  mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) Hsqr'
+... = (1 + a)^(n + 2) : by simp only [pow_succ, mul_assoc]
 
 private lemma pow_lt_pow_of_lt_one_aux {a : R} (h : 0 < a) (ha : a < 1) (i : ℕ) :
   ∀ k : ℕ, a ^ (i + k + 1) < a ^ i
@@ -388,32 +396,29 @@ begin
 end
 
 /-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
-theorem one_add_mul_le_pow {a : R} (H : -2 ≤ a) : ∀ (n : ℕ), 1 + n •ℕ a ≤ (1 + a) ^ n
-| 0     := le_of_eq $ add_zero _
-| 1     := by simp
-| (n+2) :=
-have H' : 0 ≤ 2 + a,
-  from neg_le_iff_add_nonneg'.1 H,
-have 0 ≤ n •ℕ (a * a * (2 + a)) + a * a,
-  from add_nonneg (nsmul_nonneg (mul_nonneg (mul_self_nonneg a) H') n)
-    (mul_self_nonneg a),
-calc 1 + (n + 2) •ℕ a ≤ 1 + (n + 2) •ℕ a + (n •ℕ (a * a * (2 + a)) + a * a) :
-  (le_add_iff_nonneg_right _).2 this
-... = (1 + a) * (1 + a) * (1 + n •ℕ a) :
-  by { simp only [add_mul, mul_add, mul_two, mul_one, one_mul, succ_nsmul, nsmul_add,
-         mul_nsmul_assoc, (mul_nsmul_left _ _ _).symm],
-       ac_refl }
-... ≤ (1 + a) * (1 + a) * (1 + a)^n :
-  mul_le_mul_of_nonneg_left (one_add_mul_le_pow n) (mul_self_nonneg (1 + a))
-... = (1 + a)^(n + 2) : by simp only [pow_succ, mul_assoc]
+theorem one_add_mul_le_pow {a : R} (H : -2 ≤ a) (n : ℕ) : 1 + (n : R) * a ≤ (1 + a) ^ n :=
+one_add_mul_le_pow' (mul_self_nonneg _) (mul_self_nonneg _) (neg_le_iff_add_nonneg'.1 H) _
 
 /-- Bernoulli's inequality reformulated to estimate `a^n`. -/
-theorem one_add_sub_mul_le_pow {a : R} (H : -1 ≤ a) (n : ℕ) : 1 + n •ℕ (a - 1) ≤ a ^ n :=
+theorem one_add_mul_sub_le_pow {a : R} (H : -1 ≤ a) (n : ℕ) : 1 + (n : R) * (a - 1) ≤ a ^ n :=
 have -2 ≤ a - 1, by rwa [bit0, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right],
 by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
 
 end linear_ordered_ring
 
+/-- Bernoulli's inequality reformulated to estimate `(n : K)`. -/
+theorem nat.cast_le_pow_sub_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ℕ) :
+  (n : K) ≤ (a ^ n - 1) / (a - 1) :=
+(le_div_iff (sub_pos.2 H)).2 $ le_sub_left_of_add_le $
+  one_add_mul_sub_le_pow ((neg_le_self $ @zero_le_one K _).trans H.le) _
+
+/-- For any `a > 1` and a natural `n` we have `n ≤ a ^ n / (a - 1)`. See also
+`nat.cast_le_pow_sub_div_sub` for a stronger inequality with `a ^ n - 1` in the numerator. -/
+theorem nat.cast_le_pow_div_sub {K : Type*} [linear_ordered_field K] {a : K} (H : 1 < a) (n : ℕ) :
+  (n : K) ≤ a ^ n / (a - 1) :=
+(n.cast_le_pow_sub_div_sub H).trans $ div_le_div_of_le (sub_nonneg.2 H.le)
+  (sub_le_self _ zero_le_one)
+
 namespace int
 
 lemma units_pow_two (u : units ℤ) : u ^ 2 = 1 :=