Documentation

Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Deligne's archimedean Gamma-factors #

In the theory of L-series one frequently encounters the following functions (of a complex variable s) introduced in Deligne's landmark paper Valeurs de fonctions L et periodes d'integrales:

$$ \Gamma_{\mathbb{R}}(s) = \pi ^ {-s / 2} \Gamma (s / 2) $$

and

$$ \Gamma_{\mathbb{C}}(s) = 2 (2 \pi) ^ {-s} \Gamma (s). $$

These are the factors that need to be included in the Dedekind zeta function of a number field for each real, resp. complex, infinite place.

(Note that these are not the same as Mathlib's Real.Gamma vs. Complex.Gamma; Deligne's functions both take a complex variable as input.)

This file defines these functions, and proves some elementary properties, including a reflection formula which is an important input in functional equations of (un-completed) Dirichlet L-functions.

noncomputable def Complex.Gammaℝ (s : ) :

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 ℂ → ℂ.

Equations
Instances For
    noncomputable def Complex.Gammaℂ (s : ) :

    Deligne's archimedean Gamma factor for a complex infinite place.

    See "Valeurs de fonctions L et periodes d'integrales" § 5.3. (Some authors omit the factor of 2). Note that this is not the same as Complex.Gamma.

    Equations
    Instances For

      Reformulation of the doubling formula in terms of Gammaℝ.

      Reformulation of the reflection formula in terms of Gammaℝ.

      Another formulation of the reflection formula in terms of Gammaℝ.

      Formulation of reflection formula tailored to functional equations of L-functions of even Dirichlet characters (including Riemann zeta).

      Formulation of reflection formula tailored to functional equations of L-functions of odd Dirichlet characters.