lean_workbook_plus_32441

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Bernoulli's Inequality: For $x > -1$ and $i \geq 1$ , prove that $(1+x)^i \geq 1 + ix$ with equality occurring when $x = 0$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32441 (x : ℝ) (i : ℕ) (hx : x > -1) (hi : 1 ≤ i) :
  (1 + x) ^ i ≥ 1 + i * x   :=  by sorry

Source