GammaAux — Mathlib

English

For s ∈ ℂ and n ∈ ℕ with -Re(s) < n, ΓAux(n,s) = ΓAux(n,(s+1)) / s.

Русский

Для комплексного s и натурального n с условием -Re(s) < n выполняется ΓAux(n,s) = ΓAux(n,(s+1)) / s.

LaTeX

$$$$ \GammaAux(n,s) = \dfrac{\GammaAux(n, s+1)}{s}, \quad -\operatorname{Re}(s) < n. $$$$

Lean4

/-- The `n`th function in this family is `Γ(s)` if `-n < s.re`, and junk otherwise. -/
noncomputable def GammaAux : ℕ → ℂ → ℂ
  | 0 => GammaIntegral
  | n + 1 => fun s : ℂ => GammaAux n (s + 1) / s

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