English
For the same hypotheses as above, the inequality holds: 1 + p s < (1 + s)^p.
Русский
При тех же предположениях выполняется неравенство 1 + p s < (1 + s)^p.
LaTeX
$$$\forall s\in\mathbb{R},\ -1\le s,\ s\ne 0,\ \forall p>1:\ 1+p s < (1+s)^p$$$
Lean4
/-- **Bernoulli's inequality** for real exponents, strict version: for `1 < p` and `-1 ≤ s`, with
`s ≠ 0`, we have `1 + p * s < (1 + s) ^ p`. -/
theorem one_add_mul_self_lt_rpow_one_add {s : ℝ} (hs : -1 ≤ s) (hs' : s ≠ 0) {p : ℝ} (hp : 1 < p) :
1 + p * s < (1 + s) ^ p := by
have hp' : 0 < p := zero_lt_one.trans hp
rcases eq_or_lt_of_le hs with rfl | hs
· rwa [add_neg_cancel, zero_rpow hp'.ne', mul_neg_one, add_neg_lt_iff_lt_add, zero_add]
have hs1 : 0 < 1 + s := neg_lt_iff_pos_add'.mp hs
rcases le_or_gt (1 + p * s) 0 with hs2 | hs2
· exact hs2.trans_lt (rpow_pos_of_pos hs1 _)
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 hp'.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 [← div_lt_iff₀ hp', ← div_lt_div_right_of_neg 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_one_lt_left hs' hp)
· rw [← div_lt_iff₀ hp', ← div_lt_div_iff_of_pos_right 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_one_lt_left hs' hp)
