English
For Re(s) > 0, the complex gamma equals the Euler integral: Γ(s) = ΓIntegral(s).
Русский
При Re(s) > 0 комплексная гамма равна эйлеровому интегралу: Γ(s) = ΓIntegral(s).
LaTeX
$$$$ \Gamma(s) = \GammaIntegral(s), \quad \operatorname{Re}(s) > 0. $$$$
Lean4
theorem Gamma_eq_GammaAux (s : ℂ) (n : ℕ) (h1 : -s.re < ↑n) : Gamma s = GammaAux n s :=
by
have u : ∀ k : ℕ, GammaAux (⌊1 - s.re⌋₊ + k) s = Gamma s := fun k ↦ by
induction k with
| zero => simp [Gamma]
| succ k hk =>
rw [← hk, ← add_assoc]
refine (GammaAux_recurrence2 s (⌊1 - s.re⌋₊ + k) ?_).symm
rw [Nat.cast_add]
have i0 := Nat.sub_one_lt_floor (1 - s.re)
simp only [sub_sub_cancel_left] at i0
refine lt_add_of_lt_of_nonneg i0 ?_
rw [← Nat.cast_zero, Nat.cast_le]; exact Nat.zero_le k
convert (u <| n - ⌊1 - s.re⌋₊).symm; rw [Nat.add_sub_of_le]
by_cases h : 0 ≤ 1 - s.re
· apply Nat.le_of_lt_succ
exact_mod_cast lt_of_le_of_lt (Nat.floor_le h) (by linarith : 1 - s.re < n + 1)
· rw [Nat.floor_of_nonpos]
· cutsat
· linarith
