English
Recurrence for the Gamma integral: ΓIntegral(s+1) = s ΓIntegral(s).
Русский
Рекуррентность для интеграла Гамма: ΓIntegral(s+1) = s ΓIntegral(s).
LaTeX
$$$$ \GammaIntegral(s+1) = s \cdot \GammaIntegral(s). $$$$
Lean4
/-- The recurrence relation for the `Γ` integral. -/
theorem GammaIntegral_add_one {s : ℂ} (hs : 0 < s.re) : GammaIntegral (s + 1) = s * GammaIntegral s :=
by
suffices Tendsto (s + 1).partialGamma atTop (𝓝 <| s * GammaIntegral s)
by
refine tendsto_nhds_unique ?_ this
apply tendsto_partialGamma; rw [add_re, one_re]; linarith
have : (fun X : ℝ => s * partialGamma s X - X ^ s * (-X).exp) =ᶠ[atTop] (s + 1).partialGamma :=
by
apply eventuallyEq_of_mem (Ici_mem_atTop (0 : ℝ))
intro X hX
rw [partialGamma_add_one hs (mem_Ici.mp hX)]
ring_nf
refine Tendsto.congr' this ?_
suffices Tendsto (fun X => -X ^ s * (-X).exp : ℝ → ℂ) atTop (𝓝 0) by
simpa using Tendsto.add (Tendsto.const_mul s (tendsto_partialGamma hs)) this
rw [tendsto_zero_iff_norm_tendsto_zero]
have : (fun e : ℝ => ‖-(e : ℂ) ^ s * (-e).exp‖) =ᶠ[atTop] fun e : ℝ => e ^ s.re * (-1 * e).exp :=
by
refine eventuallyEq_of_mem (Ioi_mem_atTop 0) ?_
intro x hx; dsimp only
rw [norm_mul, norm_neg, norm_cpow_eq_rpow_re_of_pos hx, Complex.norm_of_nonneg (exp_pos (-x)).le, neg_mul, one_mul]
exact (tendsto_congr' this).mpr (tendsto_rpow_mul_exp_neg_mul_atTop_nhds_zero _ _ zero_lt_one)
