English
Let f be convex on (0, ∞) and satisfy f(y+1) = f(y) + log y for y > 0. Then logGammaSeq x tends to f(x) − f(1) as n → ∞ for all x > 0.
Русский
Пусть f выпукла на (0, ∞) и удовлетворяет f(y+1) = f(y) + log y для y > 0. Тогда logGammaSeq x стремится к f(x) − f(1) при n → ∞ для всех x > 0.
LaTeX
$$$ \operatorname{Tendsto} \logGammaSeq(x)_{n \to \infty} = f(x) - f(1) $$$
Lean4
theorem tendsto_logGammaSeq (hf_conv : ConvexOn ℝ (Ioi 0) f) (hf_feq : ∀ {y : ℝ}, 0 < y → f (y + 1) = f y + log y)
(hx : 0 < x) : Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1) :=
by
suffices ∀ m : ℕ, ↑m < x → x ≤ m + 1 → Tendsto (logGammaSeq x) atTop (𝓝 <| f x - f 1)
by
refine this ⌈x - 1⌉₊ ?_ ?_
· rcases lt_or_ge x 1 with ⟨⟩
· rwa [Nat.ceil_eq_zero.mpr (by linarith : x - 1 ≤ 0), Nat.cast_zero]
· convert Nat.ceil_lt_add_one (by linarith : 0 ≤ x - 1)
abel
· rw [← sub_le_iff_le_add]; exact Nat.le_ceil _
intro m
induction m generalizing x with
| zero =>
rw [Nat.cast_zero, zero_add]
exact fun _ hx' => tendsto_logGammaSeq_of_le_one hf_conv (@hf_feq) hx hx'
| succ m hm =>
intro hy hy'
rw [Nat.cast_succ, ← sub_le_iff_le_add] at hy'
rw [Nat.cast_succ, ← lt_sub_iff_add_lt] at hy
specialize hm ((Nat.cast_nonneg _).trans_lt hy) hy hy'
have :
∀ᶠ n : ℕ in atTop,
logGammaSeq (x - 1) n = logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1) :=
by
refine Eventually.mp (eventually_ge_atTop 1) (Eventually.of_forall fun n hn => ?_)
have := logGammaSeq_add_one (x - 1) (n - 1)
rw [sub_add_cancel, Nat.sub_add_cancel hn] at this
rw [this]
ring
replace hm :=
((Tendsto.congr' this hm).add (tendsto_const_nhds : Tendsto (fun _ => log (x - 1)) _ _)).comp
(tendsto_add_atTop_nat 1)
have :
((fun x_1 : ℕ =>
(fun n : ℕ => logGammaSeq x (n - 1) + x * (log (↑(n - 1) + 1) - log ↑(n - 1)) - log (x - 1)) x_1 +
(fun b : ℕ => log (x - 1)) x_1) ∘
fun a : ℕ => a + 1) =
fun n => logGammaSeq x n + x * (log (↑n + 1) - log ↑n) :=
by
ext1 n
dsimp only [Function.comp_apply]
rw [sub_add_cancel, Nat.add_sub_cancel]
rw [this] at hm
convert hm.sub (tendsto_log_nat_add_one_sub_log.const_mul x) using 2
· ring
· have := hf_feq ((Nat.cast_nonneg m).trans_lt hy)
rw [sub_add_cancel] at this
rw [this]
ring
