English
Let f be convex on (0, ∞) and satisfy f(y+1) = f(y) + log y for y > 0, with 0 < x ≤ 1. Then logGammaSeq(x) converges to f(x) − f(1) as n → ∞.
Русский
Пусть f выпукла на (0, ∞) и удовлетворяет f(y+1) = f(y) + log y для y > 0, при этом 0 < x ≤ 1. Тогда logGammaSeq(x) сходится к f(x) − f(1) при n → ∞.
LaTeX
$$$ \operatorname{Tendsto} \logGammaSeq(x)_{n \to \infty} = f(x) - f(1). $$$
Lean4
theorem tendsto_logGammaSeq_of_le_one (hf_conv : ConvexOn ℝ (Ioi 0) f)
(hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y) (hx : 0 < x) (hx' : x ≤ 1) :
Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1) :=
by
refine
tendsto_of_tendsto_of_tendsto_of_le_of_le' (f := logGammaSeq x) (g := fun n ↦ f x - f 1 - x * (log (n + 1) - log n))
?_ tendsto_const_nhds ?_ ?_
· have : f x - f 1 = f x - f 1 - x * 0 := by ring
nth_rw 2 [this]
exact Tendsto.sub tendsto_const_nhds (tendsto_log_nat_add_one_sub_log.const_mul _)
· filter_upwards with n
rw [sub_le_iff_le_add', sub_le_iff_le_add']
convert le_logGammaSeq hf_conv (@hf_feq) hx hx' n using 1
ring
· change ∀ᶠ n : ℕ in atTop, logGammaSeq x n ≤ f x - f 1
filter_upwards [eventually_ne_atTop 0] with n hn using le_sub_iff_add_le'.mpr (ge_logGammaSeq hf_conv hf_feq hx hn)
