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:

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

and

$${\mathrm{\Gamma }}_{\mathbb{C}}(s)=2(2\pi {)}^{-s}\mathrm{\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

• s.Gammaℝ = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2)

theorem Complex.Gammaℝ_def (s : ℂ) : s.Gammaℝ = ↑Real.pi ^ (-s / 2) * Complex.Gamma (s / 2)

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

• s.Gammaℂ = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s

theorem Complex.Gammaℂ_def (s : ℂ) : s.Gammaℂ = 2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s

theorem Complex.Gammaℝ_add_two {s : ℂ} (hs : s ≠ 0) : (s + 2).Gammaℝ = s.Gammaℝ * s / 2 / ↑Real.pi

theorem Complex.Gammaℂ_add_one {s : ℂ} (hs : s ≠ 0) : (s + 1).Gammaℂ = s.Gammaℂ * s / 2 / ↑Real.pi

theorem Complex.Gammaℝ_ne_zero_of_re_pos {s : ℂ} (hs : 0 < s.re) : s.Gammaℝ ≠ 0

theorem Complex.Gammaℝ_eq_zero_iff {s : ℂ} : s.Gammaℝ = 0 ↔ ∃ (n : ℕ), s = -(2 * ↑n)

@[simp]

theorem Complex.Gammaℝ_one : Complex.Gammaℝ 1 = 1

@[simp]

theorem Complex.Gammaℂ_one : Complex.Gammaℂ 1 = 1 / ↑Real.pi

theorem Complex.differentiable_Gammaℝ_inv : Differentiable ℂ fun (s : ℂ) => s.Gammaℝ⁻¹

theorem Complex.Gammaℝ_residue_zero : Filter.Tendsto (fun (s : ℂ) => s * s.Gammaℝ) (nhdsWithin 0 {0}ᶜ) (nhds 2)

theorem Complex.Gammaℝ_mul_Gammaℝ_add_one (s : ℂ) : s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ

Reformulation of the doubling formula in terms of Gammaℝ.

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ℝ.

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ℝ.

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).

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.