one_add_mul_sub_le_pow — Mathlib

English

Bernoulli's inequality reformulated to estimate a^n: if -1 ≤ a, then for all n, 1 + n(a - 1) ≤ a^n.

Русский

Неравенство Бернулли в форме оценки a^n: если -1 ≤ a, то для всех n выполняется 1 + n(a - 1) ≤ a^n.

LaTeX

$$$-1 \\le a \\Rightarrow \\forall n \\in \\mathbb{N}, \\ 1 + n(a-1) \\le a^n$$$

Lean4

/-- **Bernoulli's inequality** reformulated to estimate `a^n`. -/
theorem one_add_mul_sub_le_pow (H : -1 ≤ a) (n : ℕ) : 1 + n * (a - 1) ≤ a ^ n :=
  by
  have : -2 ≤ a - 1 := by rwa [← one_add_one_eq_two, neg_add, ← sub_eq_add_neg, sub_le_sub_iff_right]
  simpa only [add_sub_cancel] using one_add_mul_le_pow this n

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