tendsto_log_gamma — Mathlib

English

For x > 0, the sequence logGammaSeq x converges to log(Gamma x).

Русский

Для x > 0 последовательность logGammaSeq x сходится к log(Γ(x)).

LaTeX

$$$ \operatorname{Tendsto} (\logGammaSeq\, x)_{n \to \infty} \;\;\;\; (\log(\Gamma x)) $$$

Lean4

theorem tendsto_log_gamma {x : ℝ} (hx : 0 < x) : Tendsto (logGammaSeq x) atTop (𝓝 <| log (Gamma x)) :=
  by
  have : log (Gamma x) = (log ∘ Gamma) x - (log ∘ Gamma) 1 := by
    simp_rw [Function.comp_apply, Gamma_one, log_one, sub_zero]
  rw [this]
  refine BohrMollerup.tendsto_logGammaSeq convexOn_log_Gamma (fun {y} hy => ?_) hx
  rw [Function.comp_apply, Gamma_add_one hy.ne', log_mul hy.ne' (Gamma_pos_of_pos hy).ne', add_comm,
    Function.comp_apply]

Похожие утверждения