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.

theorem Commute.pow_add_mul_le_add_pow_of_sq_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {a b : R} (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

Bernoulli's inequality for b / a, written after multiplication by the denominators.

theorem one_add_mul_le_pow_of_sq_nonneg {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {a : R} (Hsq : 0 ≤ a ^ 2) (Hsq' : 0 ≤ (1 + a) ^ 2) (H : 0 ≤ 2 + a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires additional hypotheses 0 ≤ a ^ 2 and 0 ≤ (1 + a) ^ 2.

@[deprecated one_add_mul_le_pow_of_sq_nonneg (since := "2025-11-11")]

theorem one_add_mul_le_pow' {R : Type u_1} [Semiring R] [PartialOrder R] [IsOrderedRing R] {a : R} (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n

Bernoulli's inequality. This version works for semirings but requires additional hypotheses 0 ≤ a * a and 0 ≤ (1 + a) * (1 + a).

theorem pow_add_mul_le_add_pow_of_sq_nonneg {R : Type u_1} [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

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.

theorem Commute.pow_add_mul_le_add_pow {R : Type u_1} [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

Bernoulli's inequality for b / a, written after multiplication by the denominators.

This is a version for a linear ordered semiring.

theorem pow_add_mul_le_add_pow {R : Type u_1} [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

Bernoulli's inequality for b / a, written after multiplication by the denominators.

This is a version for a linear ordered semiring.

theorem one_add_le_pow_of_two_add_nonneg {R : Type u_1} [Semiring R] [LinearOrder R] [IsOrderedRing R] [ExistsAddOfLE R] {a : R} (H : 0 ≤ 2 + a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n

Bernoulli's inequality for linear ordered semirings.

theorem one_add_mul_le_pow {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} (H : -2 ≤ a) (n : ℕ) : 1 + ↑n * a ≤ (1 + a) ^ n

Bernoulli's inequality for n : ℕ, -2 ≤ a.

theorem one_add_mul_sub_le_pow {R : Type u_1} [Ring R] [LinearOrder R] [IsStrictOrderedRing R] {a : R} (H : -1 ≤ a) (n : ℕ) : 1 + ↑n * (a - 1) ≤ a ^ n

Bernoulli's inequality reformulated to estimate a^n.