English
Bernoulli's inequality for semirings: if a ∈ R with nonnegativity conditions 0 ≤ a^2, 0 ≤ (1+a)^2 and 0 ≤ 2+a, then for all n ∈ ℕ, 1 + n a ≤ (1 + a)^n.
Русский
Неравенство Бернулли для полусколь: если a ∈ R удовлетворяет неотрицательности 0 ≤ a^2, 0 ≤ (1+a)^2 и 0 ≤ 2+a, то для всех n ∈ ℕ выполняется 1 + n a ≤ (1 + a)^n.
LaTeX
$$$0 \\le a^2 \\;\\land\\; 0 \\le (1+a)^2 \\;\\land\\; 0 \\le 2+a \\Rightarrow \\forall n \\in \\mathbb{N}, \\; 1 + n a \\le (1+a)^n$$$
Lean4
/-- **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' (Hsq : 0 ≤ a * a) (Hsq' : 0 ≤ (1 + a) * (1 + a)) (H : 0 ≤ 2 + a) :
∀ n : ℕ, 1 + n * a ≤ (1 + a) ^ 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
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]
