English
Let s be a real number with -1 ≤ s and s ≠ 0, and 0 < p < 1. Then (1 + s)^p < 1 + p s.
Русский
Пусть s ∈ ℝ удовлетворяет -1 ≤ s и s ≠ 0, и 0 < p < 1. Тогда (1 + s)^p < 1 + p s.
LaTeX
$$$(-1 \le s) \land (s \neq 0) \land (0 < p) \land (p < 1) \implies (1 + s)^p < 1 + p s$$$
Lean4
/-- **Bernoulli's inequality** for real exponents, strict version: for `0 < p < 1` and `-1 ≤ s`,
with `s ≠ 0`, we have `(1 + s) ^ p < 1 + p * s`. -/
theorem rpow_one_add_lt_one_add_mul_self {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp1 : 0 < p) (hp2 : p < 1) :
(1 + s) ^ p < 1 + p * s := by
rcases eq_or_lt_of_le hs with rfl | hs
· rwa [add_neg_cancel, zero_rpow hp1.ne', mul_neg_one, lt_add_neg_iff_add_lt, zero_add]
have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
have hs2 : 0 < 1 + p * s := by
rw [← neg_lt_iff_pos_add']
rcases lt_or_gt_of_ne hs' with h | h
· exact hs.trans (lt_mul_of_lt_one_left h hp2)
· exact neg_one_lt_zero.trans (mul_pos hp1 h)
have hs3 : 1 + s ≠ 1 := hs' ∘ add_eq_left.mp
have hs4 : 1 + p * s ≠ 1 := by contrapose! hs';
rwa [add_eq_left, mul_eq_zero, eq_false_intro hp1.ne', false_or] at hs'
rw [rpow_def_of_pos hs1, ← exp_log hs2]
apply exp_strictMono
rcases lt_or_gt_of_ne hs' with hs' | hs'
· rw [← lt_div_iff₀ hp1, ← div_lt_div_right_of_neg hs']
convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs1 hs2 hs3 hs4 _ using 1
· rw [add_sub_cancel_left, div_div, log_one, sub_zero]
· rw [add_sub_cancel_left, log_one, sub_zero]
· apply add_lt_add_left (lt_mul_of_lt_one_left hs' hp2)
· rw [← lt_div_iff₀ hp1, ← div_lt_div_iff_of_pos_right hs']
convert strictConcaveOn_log_Ioi.secant_strict_mono (zero_lt_one' ℝ) hs2 hs1 hs4 hs3 _ using 1
· rw [add_sub_cancel_left, log_one, sub_zero]
· rw [add_sub_cancel_left, div_div, log_one, sub_zero]
· apply add_lt_add_left (mul_lt_of_lt_one_left hs' hp2)
