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, f(n) + x log(n-1) ≤ f(n+x).
Русский
Если f выпукла на Ioi(0) и f(y+1)=f(y)+log y, то для n≥2 и x>0 верно f(n) + x log(n−1) ≤ f(n+x).
LaTeX
$$$$ f(n) + x \log(n-1) \le f(n+x). $$$$
Lean4
/-- Linear lower bound for `f (x + n)` on unit interval -/
theorem f_add_nat_ge (hf_conv : ConvexOn ℝ (Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hn : 2 ≤ n)
(hx : 0 < x) : f n + x * log (n - 1) ≤ f (n + x) :=
by
have npos : 0 < (n : ℝ) - 1 := by rw [← Nat.cast_one, sub_pos, Nat.cast_lt]; omega
have c :=
(convexOn_iff_slope_mono_adjacent.mp <| hf_conv).2 npos (by linarith : 0 < (n : ℝ) + x)
(by linarith : (n : ℝ) - 1 < (n : ℝ)) (by linarith)
rw [add_sub_cancel_left, sub_sub_cancel, div_one] at c
have : f (↑n - 1) = f n - log (↑n - 1) := by rw [eq_sub_iff_add_eq, ← hf_feq npos, sub_add_cancel]
rwa [this, le_div_iff₀ hx, sub_sub_cancel, le_sub_iff_add_le, mul_comm _ x, add_comm] at c
