feat(algebra/group_power): prove Bernoulli's inequality for a ≥ -2 (#…

…1709)

* feat(algebra/group_power): prove Bernoulli's inequality for `a ≥ -2`

* Restate inequalities as suggested by @fpvandoorn

* Fix docs

src/algebra/archimedean.lean

@@ -26,11 +26,13 @@ variables [linear_ordered_ring α] [archimedean α]
 
 lemma pow_unbounded_of_one_lt (x : α) {y : α}
     (hy1 : 1 < y) : ∃ n : ℕ, x < y ^ n :=
-have hy0 : 0 <  y - 1 := sub_pos_of_lt hy1,
+have hy0 : 0 < y - 1 := sub_pos_of_lt hy1,
+-- TODO `by linarith` fails to prove hy1'
+have hy1' : (-1:α) ≤ y, from le_trans (neg_le_self zero_le_one) (le_of_lt hy1),
 let ⟨n, h⟩ := archimedean.arch x hy0 in
 ⟨n, calc x ≤ n • (y - 1)     : h
-       ... < 1 + n • (y - 1) : by rw add_comm; exact lt_add_one _
-       ... ≤ y ^ n           : one_add_sub_mul_le_pow (le_of_lt hy1) _⟩
+       ... < 1 + n • (y - 1) : lt_one_add _
+       ... ≤ y ^ n           : one_add_sub_mul_le_pow hy1' n⟩
 
 /-- Every x greater than 1 is between two successive natural-number
 powers of another y greater than one. -/

src/algebra/group_power.lean

@@ -566,17 +566,16 @@ theorem one_le_pow_of_one_le {a : α} (H : 1 ≤ a) : ∀ (n : ℕ), 1 ≤ a ^ n
 | (n+1) := by simpa only [mul_one] using mul_le_mul H (one_le_pow_of_one_le n)
     zero_le_one (le_trans zero_le_one H)
 
-theorem one_add_mul_le_pow {a : α} (H : 0 ≤ a) :
+/-- Bernoulli's inequality. This version works for semirings but requires
+an additional hypothesis `0 ≤ a * a`. -/
+theorem one_add_mul_le_pow' {a : α} (Hsqr : 0 ≤ a * a) (H : 0 ≤ 1 + a) :
   ∀ (n : ℕ), 1 + n • a ≤ (1 + a) ^ n
 | 0     := le_of_eq $ add_zero _
-| (n+1) := begin
-  rw [pow_succ', succ_smul'],
-  refine le_trans _ (mul_le_mul_of_nonneg_right
-    (one_add_mul_le_pow n) (add_nonneg zero_le_one H)),
-  rw [mul_add, mul_one, ← add_assoc, add_le_add_iff_left],
-  simpa only [one_mul] using mul_le_mul_of_nonneg_right
-    ((le_add_iff_nonneg_right 1).2 (add_monoid.smul_nonneg H n)) H
-end
+| (n+1) :=
+calc 1 + (n + 1) • a ≤ (1 + a) * (1 + n • a) :
+  by simpa [succ_smul, mul_add, add_mul, add_monoid.mul_smul_left]
+    using add_monoid.smul_nonneg Hsqr n
+... ≤ (1 + a)^(n+1) : mul_le_mul_of_nonneg_left (one_add_mul_le_pow' n) H
 
 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
@@ -635,11 +634,34 @@ lemma pow_le_one {x : α} : ∀ (n : ℕ) (h0 : 0 ≤ x) (h1 : x ≤ 1), x ^ n 
 end linear_ordered_semiring
 
 theorem pow_two_nonneg [linear_ordered_ring α] (a : α) : 0 ≤ a ^ 2 :=
-by rw pow_two; exact mul_self_nonneg _
+by { rw pow_two, exact mul_self_nonneg _ }
 
+/-- Bernoulli's inequality for `n : ℕ`, `-2 ≤ a`. -/
+theorem one_add_mul_le_pow [linear_ordered_ring α] {a : α} (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 (add_monoid.smul_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_smul, add_monoid.smul_add,
+         add_monoid.mul_smul_assoc, (add_monoid.mul_smul_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]
+
+/-- Bernoulli's inequality reformulated to estimate `a^n`. -/
 theorem one_add_sub_mul_le_pow [linear_ordered_ring α]
-  {a : α} (H : 1 ≤ a) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
-by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow (sub_nonneg.2 H) n
+  {a : α} (H : -1 ≤ a) (n : ℕ) : 1 + n • (a - 1) ≤ a ^ n :=
+have -2 ≤ a - 1, by { rw [bit0, neg_add], exact sub_le_sub_right H 1 },
+by simpa only [add_sub_cancel'_right] using one_add_mul_le_pow this n
 
 namespace int
 

src/algebra/ordered_group.lean

@@ -510,6 +510,12 @@ lemma le_neg : a ≤ -b ↔ b ≤ -a :=
 have -(-a) ≤ -b ↔ b ≤ -a, from neg_le_neg_iff,
 by rwa neg_neg at this
 
+lemma neg_le_iff_add_nonneg : -a ≤ b ↔ 0 ≤ a + b :=
+(add_le_add_iff_left a).symm.trans $ by rw add_neg_self
+
+lemma le_neg_iff_add_nonpos : a ≤ -b ↔ a + b ≤ 0 :=
+(add_le_add_iff_right b).symm.trans $ by rw neg_add_self
+
 @[simp] lemma neg_nonpos : -a ≤ 0 ↔ 0 ≤ a :=
 have -a ≤ -0 ↔ 0 ≤ a, from neg_le_neg_iff,
 by rwa neg_zero at this
@@ -518,6 +524,12 @@ by rwa neg_zero at this
 have -0 ≤ -a ↔ a ≤ 0, from neg_le_neg_iff,
 by rwa neg_zero at this
 
+lemma neg_le_self (h : 0 ≤ a) : -a ≤ a :=
+le_trans (neg_nonpos.2 h) h
+
+lemma self_le_neg (h : a ≤ 0) : a ≤ -a :=
+le_trans h (neg_nonneg.2 h)
+
 @[simp] lemma neg_lt_neg_iff : -a < -b ↔ b < a :=
 have a + b + -a < a + b + -b ↔ -a < -b, from add_lt_add_iff_left _,
 by simp at this; simp [this]

src/analysis/specific_limits.lean

@@ -24,20 +24,12 @@ lemma summable_of_absolute_convergence_real {f : ℕ → ℝ} :
     simpa only using hr
   end
 
-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⟩ := 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_lt_add.mp $ by simp; assumption,
-  have p ≤ r ^ n,
-    from calc p = (p / (r - 1)) * (r - 1) : (div_mul_cancel _ $ ne_of_gt this).symm
-      ... ≤ n * (r - 1) : mul_le_mul (le_of_lt hn) (le_refl _) (le_of_lt this) hn_nn
-      ... ≤ 1 + n * (r - 1) : le_add_of_nonneg_of_le zero_le_one (le_refl _)
-      ... = 1 + add_monoid.smul n (r - 1) : by rw [add_monoid.smul_eq_mul]
-      ... ≤ (1 + (r - 1)) ^ n : one_add_mul_le_pow (le_of_lt this) _
-      ... ≤ r ^ n : by simp; exact le_refl _,
-  show {n | p ≤ r ^ n} ∈ at_top,
-    from mem_at_top_sets.mpr ⟨n, assume m hnm, le_trans this (pow_le_pow (le_of_lt h) hnm)⟩
+lemma tendsto_pow_at_top_at_top_of_gt_1 {r : ℝ} (h : r > 1) :
+  tendsto (λn:ℕ, r ^ n) at_top at_top :=
+(tendsto_at_top_at_top _).2 $ assume p,
+  let ⟨n, hn⟩ := pow_unbounded_of_one_lt p h in
+  ⟨n, λ m hnm, le_of_lt $
+    lt_of_lt_of_le hn (pow_le_pow (le_of_lt h) hnm)⟩
 
 lemma tendsto_inverse_at_top_nhds_0 : tendsto (λr:ℝ, r⁻¹) at_top (𝓝 0) :=
 tendsto_orderable_unbounded (no_top 0) (no_bot 0) $ assume l u hl hu,