Gammaℝ — Mathlib

English

The Archimedean real-analytic gamma factor on complex arguments is defined by Γℝ(s) = π^{−s/2} Γ(s/2).

Русский

Архимедово‑аналитический фактор Гамма на комплексных аргументах определяется как Γℝ(s) = π^{−s/2} Γ(s/2).

LaTeX

$$$ \Gamma\mathbb{R}(s) = \pi^{-{s}/2} \; \Gamma\left(\dfrac{s}{2}\right) $$$

Lean4

/-- Deligne's archimedean Gamma factor for a real infinite place.

See "Valeurs de fonctions L et periodes d'integrales" § 5.3. Note that this is not the same as
`Real.Gamma`; in particular it is a function `ℂ → ℂ`. -/
noncomputable def Gammaℝ (s : ℂ) :=
  π ^ (-s / 2) * Gamma (s / 2)

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