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 : ℂ) :
    Complex.Gammaℝ s = ↑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 : ℂ) :
      Complex.Gammaℂ s = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s
      source
      theorem Complex.Gammaℝ_add_two {s : ℂ} (hs : s ≠ 0) :
      Complex.Gammaℝ (s + 2) = Complex.Gammaℝ s * s / 2 / ↑Real.pi
      source
      theorem Complex.Gammaℂ_add_one {s : ℂ} (hs : s ≠ 0) :
      Complex.Gammaℂ (s + 1) = Complex.Gammaℂ s * s / 2 / ↑Real.pi
      source
      theorem Complex.Gammaℝ_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) :
      Complex.Gammaℝ s ≠ 0
      source
      theorem Complex.Gammaℝ_eq_zero_iff {s : ℂ} :
      Complex.Gammaℝ s = 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 : ℂ) => (Complex.Gammaℝ s)⁻¹
      source
      theorem Complex.Gammaℝ_residue_zero :
      Filter.Tendsto (fun (s : ℂ) => s * Complex.Gammaℝ s) (nhdsWithin 0 {0}ᶜ) (nhds 2)
      source
      theorem Complex.Gammaℝ_mul_Gammaℝ_add_one (s : ℂ) :
      Complex.Gammaℝ s * Complex.Gammaℝ (s + 1) = Complex.Gammaℂ s

      Reformulation of the doubling formula in terms of Gammaℝ.

      source
      theorem Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add (s : ℂ) :
      Complex.Gammaℝ (1 - s) * Complex.Gammaℝ (1 + s) = (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)) :
      Complex.Gammaℝ s / Complex.Gammaℝ (1 - s) = Complex.Gammaℂ s * 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) :
      (Complex.Gammaℝ (1 - s))⁻¹ = Complex.Gammaℂ s * Complex.cos (↑Real.pi * s / 2) * (Complex.Gammaℝ s)⁻¹

      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) :
      (Complex.Gammaℝ (2 - s))⁻¹ = Complex.Gammaℂ s * Complex.sin (↑Real.pi * s / 2) * (Complex.Gammaℝ (s + 1))⁻¹

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