From d67e527adc99837b731799190fdc7cbeb596254f Mon Sep 17 00:00:00 2001 From: "Yury G. Kudryashov" Date: Tue, 19 Nov 2019 18:41:43 -0500 Subject: [PATCH] =?UTF-8?q?feat(algebra/group=5Fpower):=20prove=20Bernoull?= =?UTF-8?q?i's=20inequality=20for=20`a=20=E2=89=A5=20-2`=20(#1709)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit * feat(algebra/group_power): prove Bernoulli's inequality for `a ≥ -2` * Restate inequalities as suggested by @fpvandoorn * Fix docs --- src/algebra/archimedean.lean | 8 ++++-- src/algebra/group_power.lean | 46 +++++++++++++++++++++++-------- src/algebra/ordered_group.lean | 12 ++++++++ src/analysis/specific_limits.lean | 20 ++++---------- 4 files changed, 57 insertions(+), 29 deletions(-) diff --git a/src/algebra/archimedean.lean b/src/algebra/archimedean.lean index a1b55cd4d7c25..27d5bdbf8835f 100644 --- a/src/algebra/archimedean.lean +++ b/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. -/ diff --git a/src/algebra/group_power.lean b/src/algebra/group_power.lean index f3aad8be38081..8442c0c5639de 100644 --- a/src/algebra/group_power.lean +++ b/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 diff --git a/src/algebra/ordered_group.lean b/src/algebra/ordered_group.lean index 5682fa388ef54..a8a39058a5828 100644 --- a/src/algebra/ordered_group.lean +++ b/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] diff --git a/src/analysis/specific_limits.lean b/src/analysis/specific_limits.lean index a7f2943955258..b4d86c206f40c 100644 --- a/src/analysis/specific_limits.lean +++ b/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,