English
For s with -1 ≤ s, s ≠ 0 and p > 1, we have 1 + p s < (1 + s)^p.
Русский
Для s ∈ ℝ с -1 ≤ s, s ≠ 0 и p > 1 имеет место 1 + p s < (1 + s)^p.
LaTeX
$$$\forall s∈\mathbb{R},\ -1\le s,\ s\ne 0,\ \forall p∈\mathbb{R},\ p>1:\ 1+p s < (1+s)^p$$$
Lean4
/-- `Real.log` is strictly concave on `(0, +∞)`. -/
theorem strictConcaveOn_log_Ioi : StrictConcaveOn ℝ (Ioi 0) log :=
by
apply strictConcaveOn_of_slope_strict_anti_adjacent (convex_Ioi (0 : ℝ))
intro x y z (hx : 0 < x) (hz : 0 < z) hxy hyz
have hy : 0 < y := hx.trans hxy
trans y⁻¹
· have h : 0 < z - y := by linarith
rw [div_lt_iff₀ h]
have hyz' : 0 < z / y := by positivity
have hyz'' : z / y ≠ 1 := by
contrapose! h
rw [div_eq_one_iff_eq hy.ne'] at h
simp [h]
calc
log z - log y = log (z / y) := by rw [← log_div hz.ne' hy.ne']
_ < z / y - 1 := (log_lt_sub_one_of_pos hyz' hyz'')
_ = y⁻¹ * (z - y) := by field_simp
· have h : 0 < y - x := by linarith
rw [lt_div_iff₀ h]
have hxy' : 0 < x / y := by positivity
have hxy'' : x / y ≠ 1 := by
contrapose! h
rw [div_eq_one_iff_eq hy.ne'] at h
simp [h]
calc
y⁻¹ * (y - x) = 1 - x / y := by field_simp
_ < -log (x / y) := by linarith [log_lt_sub_one_of_pos hxy' hxy'']
_ = -(log x - log y) := by rw [log_div hx.ne' hy.ne']
_ = log y - log x := by ring
