A multiplicative Bernoulli inequality

For p ≤ 1 and n : ℕ, (1 - p) ^ n * (1 + n * p) ≤ 1 (Real.one_sub_pow_mul_one_add_mul_le_one). By induction on n, each factor 1 - p ≥ 0 decreases (1 + (n + 1) * p) below (1 + n * p) / (1 - p) because (n + 1) * p ^ 2 ≥ 0. For 0 ≤ p ≤ 1 this bounds (1 - p) ^ n from above by 1 / (1 + n * p).

Main results

• Real.one_sub_pow_mul_one_add_mul_le_one: (1 - p) ^ n * (1 + n * p) ≤ 1 for p ≤ 1.

theorem Real.one_sub_pow_mul_one_add_mul_le_one {p : ℝ} (hp : p ≤ 1) (n : ℕ) : (1 - p) ^ n * (1 + ↑n * p) ≤ 1

A multiplicative form of Bernoulli's inequality: (1 - p) ^ n (1 + n p) ≤ 1 for p ≤ 1.