Bernoulli's inequality

theorem one_add_mul_le_pow' {R : Type u_1} [OrderedSemiring 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 one_add_mul_le_pow {R : Type u_1} [LinearOrderedRing 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} [LinearOrderedRing R] {a : R} (H : -1 ≤ a) (n : ℕ) : 1 + ↑n * (a - 1) ≤ a ^ n

Bernoulli's inequality reformulated to estimate a^n.