gammaFactor — Mathlib

English

The gamma factor gammaFactor(χ, s) is defined by gammaFactor(χ, s) = Γℝ(s) if χ is even, and Γℝ(s+1) otherwise.

Русский

Гамма-фактор gammaFactor(χ, s) равен Γℝ(s) при чётном χ и Γℝ(s+1) при нечётном χ.

LaTeX

$$$\gamma\text{Factor}(\chi,s) = \begin{cases} \Gamma_{\mathbb{R}}(s), & \chi\text{ чётный}, \\ \Gamma_{\mathbb{R}}(s+1), & \text{иначе}. \end{cases}$$$

Lean4

/-- The Archimedean Gamma factor: `Gammaℝ s` if `χ` is even, and `Gammaℝ (s + 1)` otherwise. -/
noncomputable def gammaFactor (χ : DirichletCharacter ℂ N) (s : ℂ) :=
  if χ.Even then Gammaℝ s else Gammaℝ (s + 1)

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