English
For every s ∈ ℂ, GammaSeq(s,n) tends to Γ(s) as n → ∞.
Русский
Пусть s ∈ ℂ. GammaSeq(s,n) сходится к Γ(s) при n → ∞.
LaTeX
$$$$ \lim_{n\to\infty} \GammaSeq(s,n) = \Gamma(s). $$$$
Lean4
/-- Euler's limit formula for the complex Gamma function. -/
theorem GammaSeq_tendsto_Gamma (s : ℂ) : Tendsto (GammaSeq s) atTop (𝓝 <| Gamma s) :=
by
suffices ∀ m : ℕ, -↑m < re s → Tendsto (GammaSeq s) atTop (𝓝 <| GammaAux m s)
by
rw [Gamma]
apply this
rw [neg_lt]
rcases lt_or_ge 0 (re s) with (hs | hs)
· exact (neg_neg_of_pos hs).trans_le (Nat.cast_nonneg _)
· refine (Nat.lt_floor_add_one _).trans_le ?_
rw [sub_eq_neg_add, Nat.floor_add_one (neg_nonneg.mpr hs), Nat.cast_add_one]
intro m
induction m generalizing s with intro hs
| zero => -- Base case: `0 < re s`, so Gamma is given by the integral formula
rw [Nat.cast_zero, neg_zero] at hs
rw [← Gamma_eq_GammaAux]
· refine Tendsto.congr' ?_ (approx_Gamma_integral_tendsto_Gamma_integral hs)
refine (eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_)
exact (GammaSeq_eq_approx_Gamma_integral hs hn).symm
· rwa [Nat.cast_zero, neg_lt_zero]
| succ m IH => -- Induction step: use recurrence formulae in `s` for Gamma and GammaSeq
rw [Nat.cast_succ, neg_add, ← sub_eq_add_neg, sub_lt_iff_lt_add, ← one_re, ← add_re] at hs
rw [GammaAux]
have :=
@Tendsto.congr' _ _ _ ?_ _ _ ((eventually_ne_atTop 0).mp (Eventually.of_forall fun n hn => ?_))
((IH _ hs).div_const s)
pick_goal 3; · exact GammaSeq_add_one_left s hn
conv at this => arg 1; intro n; rw [mul_comm]
rwa [← mul_one (GammaAux m (s + 1) / s), tendsto_mul_iff_of_ne_zero _ (one_ne_zero' ℂ)] at this
simp_rw [add_assoc]
exact tendsto_natCast_div_add_atTop (1 + s)
