feat: add a version of Bernoulli's inequality (#31502)

Motivated by #31492

Author: urkud

Mathlib/Algebra/Order/Archimedean/Basic.lean

@@ -183,7 +183,7 @@ theorem add_one_pow_unbounded_of_pos (x : R) (hy : 0 < y) : ∃ n : ℕ, x < (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)
+        one_add_mul_le_pow_of_sq_nonneg (pow_nonneg hy.le _) (pow_nonneg this _)
           (add_nonneg zero_le_two hy.le) _
       _ = (y + 1) ^ n := by rw [add_comm]
 

Mathlib/Algebra/Order/Ring/Pow.lean

@@ -5,43 +5,104 @@ Authors: Yury Kudryashov
 -/
 import Mathlib.Data.Nat.Cast.Commute
 import Mathlib.Data.Nat.Cast.Order.Ring
+import Mathlib.Tactic.Abel
 
-/-! # Bernoulli's inequality -/
+/-! # Bernoulli's inequality
+
+In this file we prove several versions of Bernoulli's inequality.
+Besides the standard version `1 + n * a ≤ (1 + a) ^ n`,
+we also prove `a ^ n + n * a ^ (n - 1) * b ≤ (a + b) ^ n`,
+which can be regarded as Bernoulli's inequality for `b / a` multiplied by `a ^ n`.
+
+Also, we prove versions for different typeclass assumptions on the (semi)ring.
+-/
 
 variable {R : Type*}
 
 section OrderedSemiring
-variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {a : R}
+variable [Semiring R] [PartialOrder R] [IsOrderedRing R] {a b : R}
 
-/-- **Bernoulli's inequality**. This version works for semirings but requires
-additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
-lemma one_add_mul_le_pow' (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) :
-    ∀ n : ℕ, 1 + n * a ≤ (1 + a) ^ n
+/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators. -/
+lemma Commute.pow_add_mul_le_add_pow_of_sq_nonneg (Hcomm : Commute a b) (ha : 0 ≤ a)
+    (Hsq : 0 ≤ b ^ 2) (Hsq' : 0 ≤ (a + b) ^ 2) (H : 0 ≤ 2 * a + b) :
+    ∀ n : ℕ, a ^ n + n * a ^ (n - 1) * b ≤ (a + b) ^ n
   | 0 => by simp
   | 1 => by simp
-  | n + 2 =>
-    have : 0 ≤ n * (a * a * (2 + a)) + a * a :=
-      add_nonneg (mul_nonneg n.cast_nonneg (mul_nonneg Hsq H)) Hsq
+  | 2 =>
     calc
-      _ ≤ 1 + ↑(n + 2) * a + (n * (a * a * (2 + a)) + a * a) := le_add_of_nonneg_right this
-      _ = (1 + a) * (1 + a) * (1 + n * a) := by
-          simp only [Nat.cast_add, add_mul, mul_add, one_mul, mul_one, ← one_add_one_eq_two,
-            Nat.cast_one, add_assoc]
-          simp only [← add_assoc, add_comm _ (↑n * a)]
-          simp only [add_assoc, (n.cast_commute (_ : R)).left_comm]
-          simp only [add_comm, add_left_comm]
-      _ ≤ (1 + a) * (1 + a) * (1 + a) ^ n :=
-        mul_le_mul_of_nonneg_left (one_add_mul_le_pow' Hsq Hsq' H _) Hsq'
-      _ = (1 + a) ^ (n + 2) := by simp only [pow_succ', mul_assoc]
+      a ^ 2 + (2 : ℕ) * a ^ 1 * b ≤ a ^ 2 + (2 : ℕ) * a ^ 1 * b + b ^ 2 :=
+        le_add_of_nonneg_right Hsq
+      _ = (a + b) ^ 2 := by simp [sq, add_mul, mul_add, two_mul, Hcomm.eq, add_assoc]
+  | n + 3 => by
+    calc
+      _ ≤ a ^ (n + 3) + ↑(n + 3) * a ^ (n + 2) * b +
+            ((n + 1) * (b ^ 2 * (2 * a + b) * a ^ n) + a ^ (n + 1) * b ^ 2) :=
+        le_add_of_nonneg_right <| by
+          apply_rules [add_nonneg, mul_nonneg, Nat.cast_nonneg, pow_nonneg, zero_le_one]
+      _ = (a + b) ^ 2 * (a ^ (n + 1) + ↑(n + 1) * a ^ n * b) := by
+        simp only [Nat.cast_add, Nat.cast_one, Nat.cast_ofNat, pow_succ', add_mul, mul_add,
+          two_mul, pow_zero, mul_one,
+          Hcomm.eq, (n.cast_commute (_ : R)).symm.left_comm, mul_assoc, (Hcomm.pow_left _).eq,
+          (Hcomm.pow_left _).left_comm, Hcomm.left_comm, ← @two_add_one_eq_three R, one_mul]
+        abel
+      _ ≤ (a + b) ^ 2 * (a + b) ^ (n + 1) := by
+        gcongr
+        · assumption
+        · apply Commute.pow_add_mul_le_add_pow_of_sq_nonneg <;> assumption
+      _ = (a + b) ^ (n + 3) := by simp [pow_succ', mul_assoc]
+
+/-- **Bernoulli's inequality**. This version works for semirings but requires
+additional hypotheses `0 ≤ a ^ 2` and `0 ≤ (1 + a) ^ 2`. -/
+lemma one_add_mul_le_pow_of_sq_nonneg (Hsq : 0 ≤ a ^ 2) (Hsq' : 0 ≤ (1 + a) ^ 2) (H : 0 ≤ 2 + a)
+    (n : ℕ) : 1 + n * a ≤ (1 + a) ^ n := by
+  simpa using (Commute.one_left a).pow_add_mul_le_add_pow_of_sq_nonneg zero_le_one Hsq Hsq'
+    (by simpa using H) n
+
+/-- **Bernoulli's inequality**. This version works for semirings but requires
+additional hypotheses `0 ≤ a * a` and `0 ≤ (1 + a) * (1 + a)`. -/
+@[deprecated one_add_mul_le_pow_of_sq_nonneg (since := "2025-11-11")]
+lemma one_add_mul_le_pow' (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) (n : ℕ) :
+    1 + n * a ≤ (1 + a) ^ n :=
+  one_add_mul_le_pow_of_sq_nonneg (by rwa [sq]) (by rwa [sq]) H n
 
 end OrderedSemiring
 
+/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.
+
+This version works for partially ordered commutative semirings,
+but explicitly assumes that `b ^ 2` and `(a + b) ^ 2` are nonnegative. -/
+lemma pow_add_mul_le_add_pow_of_sq_nonneg [CommSemiring R] [PartialOrder R] [IsOrderedRing R]
+    {a b : R} (ha : 0 ≤ a) (Hsq : 0 ≤ b ^ 2) (Hsq' : 0 ≤ (a + b) ^ 2) (H : 0 ≤ 2 * a + b)
+    (n : ℕ) : a ^ n + n * a ^ (n - 1) * b ≤ (a + b) ^ n :=
+  (Commute.all a b).pow_add_mul_le_add_pow_of_sq_nonneg ha Hsq Hsq' H n
+
+/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.
+
+This is a version for a linear ordered semiring. -/
+lemma Commute.pow_add_mul_le_add_pow [Semiring R] [LinearOrder R] [IsOrderedRing R]
+    [ExistsAddOfLE R] {a b : R} (Hcomm : Commute a b) (ha : 0 ≤ a) (H : 0 ≤ 2 * a + b)
+    (n : ℕ) : a ^ n + n * a ^ (n - 1) * b ≤ (a + b) ^ n :=
+  Hcomm.pow_add_mul_le_add_pow_of_sq_nonneg ha (sq_nonneg _) (sq_nonneg _) H n
+
+/-- Bernoulli's inequality for `b / a`, written after multiplication by the denominators.
+
+This is a version for a linear ordered semiring. -/
+lemma pow_add_mul_le_add_pow [CommSemiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R]
+    {a b : R} (ha : 0 ≤ a) (H : 0 ≤ 2 * a + b) (n : ℕ) :
+    a ^ n + n * a ^ (n - 1) * b ≤ (a + b) ^ n :=
+  (Commute.all a b).pow_add_mul_le_add_pow ha H n
+
+/-- Bernoulli's inequality for linear ordered semirings. -/
+lemma one_add_le_pow_of_two_add_nonneg [Semiring R] [LinearOrder R] [IsOrderedRing R]
+    [ExistsAddOfLE R] {a : R} (H : 0 ≤ 2 + a) (n : ℕ) : 1 + n * a ≤ (1 + a) ^ n :=
+  one_add_mul_le_pow_of_sq_nonneg (sq_nonneg _) (sq_nonneg _) H _
+
 section LinearOrderedRing
 variable [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} {n : ℕ}
 
 /-- **Bernoulli's inequality** for `n : ℕ`, `-2 ≤ a`. -/
 lemma one_add_mul_le_pow (H : -2 ≤ a) (n : ℕ) : 1 + n * a ≤ (1 + a) ^ n :=
-  one_add_mul_le_pow' (mul_self_nonneg _) (mul_self_nonneg _) (neg_le_iff_add_nonneg'.1 H) _
+  one_add_le_pow_of_two_add_nonneg (neg_le_iff_add_nonneg'.mp H) n
 
 /-- **Bernoulli's inequality** reformulated to estimate `a^n`. -/
 lemma one_add_mul_sub_le_pow (H : -1 ≤ a) (n : ℕ) : 1 + n * (a - 1) ≤ a ^ n := by