English
If f is convex on Ioi(0) and f(y+1) = f(y) + log y for y>0, then for n≥2 and x∈(0,1], f(n+x) ≤ f(n) + x log n.
Русский
Если f выпукла на Ioi(0) и удовлетворяет f(y+1)=f(y)+log y, то для n≥2 и x∈(0,1] имеет место неравенство f(n+x) ≤ f(n) + x log n.
LaTeX
$$$$ f(n+x) \le f(n) + x \log n. $$$$
Lean4
/-- Linear upper bound for `f (x + n)` on unit interval -/
theorem f_add_nat_le (hf_conv : ConvexOn ℝ (Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hn : n ≠ 0)
(hx : 0 < x) (hx' : x ≤ 1) : f (n + x) ≤ f n + x * log n :=
by
have hn' : 0 < (n : ℝ) := Nat.cast_pos.mpr (Nat.pos_of_ne_zero hn)
have : f n + x * log n = (1 - x) * f n + x * f (n + 1) := by rw [hf_feq hn']; ring
rw [this, (by ring : (n : ℝ) + x = (1 - x) * n + x * (n + 1))]
simpa only [smul_eq_mul] using
hf_conv.2 hn' (by linarith : 0 < (n + 1 : ℝ)) (by linarith : 0 ≤ 1 - x) hx.le (by linarith)
