rpow_one_add_le_one_add_mul_self — Mathlib

English

Let s ∈ ℝ with -1 ≤ s and 0 ≤ p ≤ 1. Then (1 + s)^p ≤ 1 + p s.

Русский

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

LaTeX

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

Lean4

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

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