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.

source
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
    source
    theorem Complex.Gammaℝ_def (s : ℂ) :
    s.Gammaℝ = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2)
    source
    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
      source
      theorem Complex.Gammaℂ_def (s : ℂ) :
      s.Gammaℂ = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s
      source
      theorem Complex.Gammaℝ_add_two {s : ℂ} (hs : s ≠ 0) :
      (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑Real.pi
      source
      theorem Complex.Gammaℂ_add_one {s : ℂ} (hs : s ≠ 0) :
      (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑Real.pi
      source
      theorem Complex.Gammaℝ_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) :
      s.Gammaℝ ≠ 0
      source
      theorem Complex.Gammaℝ_eq_zero_iff {s : ℂ} :
      s.Gammaℝ = 0 ↔ ∃ (n : ℕ), s = -(2 * ↑n)
      source
      @[simp]
      theorem Complex.Gammaℝ_one :
      Complex.Gammaℝ 1 = 1
      source
      @[simp]
      theorem Complex.Gammaℂ_one :
      Complex.Gammaℂ 1 = 1 / ↑Real.pi
      source
      theorem Complex.differentiable_Gammaℝ_inv :
      Differentiable ℂ fun (s : ℂ) => s.Gammaℝ⁻¹
      source
      theorem Complex.Gammaℝ_residue_zero :
      Filter.Tendsto (fun (s : ℂ) => s * s.Gammaℝ) (nhdsWithin 0 {0}ᶜ) (nhds 2)
      source
      theorem Complex.Gammaℝ_mul_Gammaℝ_add_one (s : ℂ) :
      s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ

      Reformulation of the doubling formula in terms of Gammaℝ.

      source
      theorem Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add (s : ℂ) :
      (1 - s).Gammaℝ * (1 + s).Gammaℝ = (Complex.cos (↑Real.pi * s / 2))⁻¹

      Reformulation of the reflection formula in terms of Gammaℝ.

      source
      theorem Complex.Gammaℝ_div_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)) :
      s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * Complex.cos (↑Real.pi * s / 2)

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

      source
      theorem Complex.inv_Gammaℝ_one_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) :
      (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.cos (↑Real.pi * s / 2) * s.Gammaℝ⁻¹

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

      source
      theorem Complex.inv_Gammaℝ_two_sub {s : ℂ} (hs : ∀ (n : ℕ), s ≠ -↑n) :
      (2 - s).Gammaℝ⁻¹ = s.Gammaℂ * Complex.sin (↑Real.pi * s / 2) * (s + 1).Gammaℝ⁻¹

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