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)