one_add_mul_le_pow — Mathlib

English

Bernoulli's inequality for natural exponent n: if a ≤ 0 or appropriate conditions hold in a ring, then 1 + n a ≤ (1 + a)^n.

Русский

Неравенство Бернулли для целого n: при соблюдении условий a и т.д. выполняется 1 + n a ≤ (1 + a)^n.

LaTeX

$$∀ n ∈ ℕ, 1 + n a ≤ (1 + a)^n$$

Lean4

/-- **Bernoulli's inequality** for `n : ℕ`, `-2 ≤ a`. -/
theorem 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) _

Похожие утверждения