one_add_mul_self_le_rpow_one_add — Mathlib

English

Let s be a real number with -1 ≤ s and p a real number with 1 ≤ p. Then 1 + p s ≤ (1 + s)^p.

Русский

Пусть s ∈ ℝ удовлетворяет -1 ≤ s, и p ∈ ℝ удовлетворяет 1 ≤ p. Тогда 1 + p s ≤ (1 + s)^p.

LaTeX

$$$(-1 \le s) \land (1 \le p) \implies 1 + p s \le (1 + s)^p$$$

Lean4

/-- **Bernoulli's inequality** for real exponents, non-strict version: for `1 ≤ p` and `-1 ≤ s`
we have `1 + p * s ≤ (1 + s) ^ p`. -/
theorem one_add_mul_self_le_rpow_one_add {s : ℝ} (hs : -1 ≤ s) {p : ℝ} (hp : 1 ≤ p) : 1 + p * s ≤ (1 + s) ^ p :=
  by
  rcases eq_or_lt_of_le hp with (rfl | hp)
  · simp
  by_cases hs' : s = 0
  · simp [hs']
  exact (one_add_mul_self_lt_rpow_one_add hs hs' hp).le

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