English
Let f: R → R be convex on the positive reals and satisfy f(y+1) = f(y) + log y for all y > 0. If 0 < x ≤ 1, then for every natural number n, f(x) ≤ f(1) + x log(n+1) − x log n + logGammaSeq(x, n).
Русский
Пусть f: ℝ → ℝ выпукла на множествах положительных вещественных, и выполняется f(y+1) = f(y) + log y для всех y > 0. Если 0 < x ≤ 1, то для каждого натурального n выполняется неравенство f(x) ≤ f(1) + x log(n+1) − x log n + logGammaSeq(x, n).
LaTeX
$$$ f(x) \le f(1) + x \log(n+1) - x \log n + \log\GammaSeq(x,n) $$$
Lean4
theorem le_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y)
(hx : 0 < x) (hx' : x ≤ 1) (n : ℕ) : f x ≤ f 1 + x * log (n + 1) - x * log n + logGammaSeq x n :=
by
rw [logGammaSeq, ← add_sub_assoc, le_sub_iff_add_le, ← f_add_nat_eq (@hf_feq) hx, add_comm x]
refine (f_add_nat_le hf_conv (@hf_feq) (Nat.add_one_ne_zero n) hx hx').trans (le_of_eq ?_)
rw [f_nat_eq @hf_feq (by cutsat : n + 1 ≠ 0), Nat.add_sub_cancel, Nat.cast_add_one]
ring
