Ramanujan–Petersson conjecture

StructureFamily of local exponents#✓fully proved

A local-exponent family indexed by a type \(\iota\) is a function \(m : \iota \to \mathbb{R}\), the local Langlands exponents, with \(0 \le m(i) \le 1/2\) for every \(i \in \iota\).

The upper bound \(1/2\) is the Jacquet--Shalika range for genuine cuspidal data. The index type is part of the data, so the exponent of such a family is a construction attached to the family, not a definition of the fixed Ramanujan exponent \(\delta_2\) of \(\mathrm{GL}_2\).

structure LocalExponentFamily (ι : Type*) where
  exponent : ι → ℝ
  exponent_nonneg : ∀ i, 0 ≤ exponent i
  exponent_le_half : ∀ i, exponent i ≤ 1 / 2

Used by 16

Used byAdmissible exponents of a local-exponent family · Families dominating the Selberg exceptional spectrum · Local exponents are bounded by the Ramanujan exponent · Exponent set of a local-exponent family · Generalized Ramanujan conjecture for a family · Admissibility of an exponent for a local-exponent family · Admissibility is a bound by the Ramanujan exponent · The Ramanujan exponent is admissible · Ramanujan exponent of a local-exponent family · The Ramanujan exponent is the infimum of the admissible exponents · The Ramanujan exponent vanishes exactly in the tempered case · Admissible exponents bound the Ramanujan exponent · The Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Selberg family of archimedean exponents · Exceptional eigenvalues bound Selberg-dominating exponents from below

DefinitionExponent set of a local-exponent family#✓fully proved

For a local-exponent family \(F\) indexed by a type \(\iota\), with local exponents \(m(i)\) for \(i \in \iota\), the exponent set of \(F\) is the set of real numbers \(\{0\} \cup \{m(i) : i \in \iota\}\).

The adjoined \(0\) makes the supremum of this set the correct value when \(\iota\) is empty and in the tempered case, where every local exponent is \(0\).

def exponentSet {ι : Type*} (F : LocalExponentFamily ι) : Set ℝ :=
  {0} ∪ Set.range F.exponent

Uses 1 · Used by 6

Statement usesFamily of local exponents

Used byLocal exponents are bounded by the Ramanujan exponent · Ramanujan exponent of a local-exponent family · The Ramanujan exponent is the infimum of the admissible exponents · The Ramanujan exponent vanishes exactly in the tempered case · Admissible exponents bound the Ramanujan exponent · Selberg's constant is at most every dominating family's exponent

DefinitionRamanujan exponent of a local-exponent family#✓fully proved

The Ramanujan exponent of a local-exponent family \(F\) with local exponents \(m(i)\), \(i \in \iota\), is the supremum of the set \(\{0\} \cup \{m(i) : i \in \iota\}\). It is the supremum of the local exponents when \(\iota\) is nonempty, and \(0\) when \(\iota\) is empty.

For the eventual genuine family of cuspidal local components of \(\mathrm{GL}_2\) this will be the Ramanujan exponent \(\delta_2\); for other families it is only the supremum of the given exponents.

noncomputable def ramanujanExponentOf {ι : Type*}
    (F : LocalExponentFamily ι) : ℝ :=
  sSup (exponentSet F)

Uses 2 · Used by 9

Statement usesFamily of local exponents · Exponent set of a local-exponent family

Used byLocal exponents are bounded by the Ramanujan exponent · Admissibility is a bound by the Ramanujan exponent · The Ramanujan exponent is admissible · The Ramanujan exponent is the infimum of the admissible exponents · The Ramanujan exponent vanishes exactly in the tempered case · Admissible exponents bound the Ramanujan exponent · The Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Exceptional eigenvalues bound Selberg-dominating exponents from below

DefinitionAdmissibility of an exponent for a local-exponent family#✓fully proved

A local-exponent family \(F\) is admissible at a real number \(\delta\) (Hypothesis \(H_2(\delta)\) for \(F\)) when every local exponent \(m_i\) of \(F\) (\(i \in \iota\)) is at most \(\delta\).

def IsAdmissible {ι : Type*} (F : LocalExponentFamily ι) (δ : ℝ) : Prop :=
  ∀ i, F.exponent i ≤ δ

Uses 1 · Used by 5

Statement usesFamily of local exponents

Used byAdmissible exponents of a local-exponent family · Admissibility is a bound by the Ramanujan exponent · The Ramanujan exponent is admissible · The Ramanujan exponent is the infimum of the admissible exponents · Admissible exponents bound the Ramanujan exponent

DefinitionGeneralized Ramanujan conjecture for a family#✓fully proved

A local-exponent family \(F\) satisfies the Generalized Ramanujan conclusion when every local exponent \(m_i\) of \(F\) (\(i \in \iota\)) is zero.

def GeneralizedRamanujanFor {ι : Type*}
    (F : LocalExponentFamily ι) : Prop :=
  ∀ i, F.exponent i = 0

Uses 1 · Used by 1

Statement usesFamily of local exponents

Used byThe Ramanujan exponent vanishes exactly in the tempered case

TheoremLocal exponents are bounded by the Ramanujan exponent#✓fully proved

For every local-exponent family \(F\) and every index \(i\), the local exponent \(m_i\) of \(F\) at \(i\) is at most the Ramanujan exponent of \(F\).

theorem exponent_le_ramanujanExponentOf {ι : Type*}
    (F : LocalExponentFamily ι) (i : ι) :
    F.exponent i ≤ ramanujanExponentOf F

Uses 3 · Used by 4

Statement usesFamily of local exponents · Ramanujan exponent of a local-exponent family

Proof usesExponent set of a local-exponent family

Used byAdmissibility is a bound by the Ramanujan exponent · The Ramanujan exponent is admissible · The Ramanujan exponent vanishes exactly in the tempered case · Exceptional eigenvalues bound Selberg-dominating exponents from below

TheoremThe Ramanujan exponent is admissible#✓fully proved

For every local-exponent family \(F\), \(F\) is admissible at its Ramanujan exponent: every local exponent of \(F\) is at most the Ramanujan exponent of \(F\).

theorem isAdmissible_ramanujanExponentOf {ι : Type*}
    (F : LocalExponentFamily ι) :
    IsAdmissible F (ramanujanExponentOf F)

Uses 4 · Used by 1

Statement usesAdmissibility of an exponent for a local-exponent family · Family of local exponents · Ramanujan exponent of a local-exponent family

Proof usesLocal exponents are bounded by the Ramanujan exponent

Used byThe Ramanujan exponent is the infimum of the admissible exponents

TheoremAdmissible exponents bound the Ramanujan exponent#✓fully proved

Let \(F\) be a local-exponent family and let \(\delta \ge 0\) be a real number. If \(\delta\) is admissible for \(F\), that is, every local exponent of \(F\) is at most \(\delta\), then the Ramanujan exponent of \(F\) is at most \(\delta\).

theorem ramanujanExponentOf_le_of_isAdmissible {ι : Type*}
    (F : LocalExponentFamily ι) {δ : ℝ} (hδ : 0 ≤ δ)
    (h : IsAdmissible F δ) : ramanujanExponentOf F ≤ δ

Uses 4 · Used by 4

Statement usesAdmissibility of an exponent for a local-exponent family · Family of local exponents · Ramanujan exponent of a local-exponent family

Proof usesExponent set of a local-exponent family

Used byAdmissibility is a bound by the Ramanujan exponent · The Ramanujan exponent is the infimum of the admissible exponents · The Ramanujan exponent vanishes exactly in the tempered case · The Selberg family's exponent is Selberg's constant

TheoremAdmissibility is a bound by the Ramanujan exponent#✓fully proved

For every local-exponent family \(F\) and every real \(\delta \ge 0\), \(F\) is admissible at \(\delta\) if and only if the Ramanujan exponent of \(F\) is at most \(\delta\).

theorem isAdmissible_iff_ramanujanExponentOf_le {ι : Type*}
    (F : LocalExponentFamily ι) {δ : ℝ} (hδ : 0 ≤ δ) :
    IsAdmissible F δ ↔ ramanujanExponentOf F ≤ δ

Uses 5

Statement usesAdmissibility of an exponent for a local-exponent family · Family of local exponents · Ramanujan exponent of a local-exponent family

Proof usesLocal exponents are bounded by the Ramanujan exponent · Admissible exponents bound the Ramanujan exponent

TheoremThe Ramanujan exponent vanishes exactly in the tempered case#✓fully proved

For every local-exponent family \(F\), the Ramanujan exponent of \(F\) is \(0\) if and only if \(F\) satisfies the generalized Ramanujan conclusion, that is, every local exponent of \(F\) is \(0\).

theorem ramanujanExponentOf_eq_zero_iff {ι : Type*}
    (F : LocalExponentFamily ι) :
    ramanujanExponentOf F = 0 ↔ GeneralizedRamanujanFor F

Uses 6

Statement usesGeneralized Ramanujan conjecture for a family · Family of local exponents · Ramanujan exponent of a local-exponent family

Proof usesExponent set of a local-exponent family · Local exponents are bounded by the Ramanujan exponent · Admissible exponents bound the Ramanujan exponent

DefinitionAdmissible exponents of a local-exponent family#✓fully proved

For a local-exponent family \(F\) with local exponents \(m_i\) (\(i \in \iota\)), the set of admissible exponents of \(F\) is the set of real numbers \(\delta \ge 0\) such that \(F\) is admissible at \(\delta\), that is, \(m_i \le \delta\) for every index \(i\).

def admissibleExponents {ι : Type*} (F : LocalExponentFamily ι) : Set ℝ :=
  {δ | 0 ≤ δ ∧ IsAdmissible F δ}

Uses 2 · Used by 1

Statement usesAdmissibility of an exponent for a local-exponent family · Family of local exponents

Used byThe Ramanujan exponent is the infimum of the admissible exponents

TheoremThe Ramanujan exponent is the infimum of the admissible exponents#✓fully proved

For every local-exponent family \(F\), the Ramanujan exponent of \(F\) equals the infimum of the admissible exponents of \(F\), that is, of the set of real numbers \(\delta \ge 0\) such that every local exponent of \(F\) is at most \(\delta\).

theorem ramanujanExponentOf_eq_sInf_admissibleExponents {ι : Type*}
    (F : LocalExponentFamily ι) :
    ramanujanExponentOf F = sInf (admissibleExponents F)

Uses 7

Statement usesFamily of local exponents · Admissible exponents of a local-exponent family · Ramanujan exponent of a local-exponent family

Proof usesAdmissibility of an exponent for a local-exponent family · Exponent set of a local-exponent family · The Ramanujan exponent is admissible · Admissible exponents bound the Ramanujan exponent

DefinitionSatake pairs with a given local exponent#✓fully proved

For real numbers \(N\) and \(t\), a pair \((\alpha, \beta)\) of complex numbers is in arithmetic Satake normalization with local exponent \(t\) at residue cardinality \(N\) when \(|\alpha\beta| = 1\), \(|\alpha| = N^t\) and \(|\beta| = N^{-t}\).

def IsSatakePair (N t : ℝ) (α β : ℂ) : Prop :=
  ‖α * β‖ = 1 ∧ ‖α‖ = N ^ t ∧ ‖β‖ = N ^ (-t)

Used by 2

Used byHecke bound from a Satake pair at a finite place · Hecke bound from a Satake pair

TheoremHecke bound from a Satake pair#✓fully proved

Let \(N \ge 1\) and \(t, \delta\) be real numbers with \(0 \le t \le \delta\). If complex numbers \(\alpha, \beta\) form a Satake pair with local exponent \(t\) at residue cardinality \(N\), then \(|\alpha + \beta| \le 2 N^\delta\).

The catalogue also records the sharper expression \(N^\delta + N^{-\delta}\); the bound proved here is its displayed consequence \(2N^\delta\).

theorem hecke_norm_le_two_mul_rpow_of_isSatakePair {N t δ : ℝ}
    {α β : ℂ} (hN : 1 ≤ N) (ht0 : 0 ≤ t) (ht : t ≤ δ)
    (h : IsSatakePair N t α β) : ‖α + β‖ ≤ 2 * N ^ δ

Uses 1 · Used by 1

Statement usesSatake pairs with a given local exponent

Used byHecke bound from a Satake pair at a finite place

TheoremHecke bound from a Satake pair at a finite place#✓fully proved

Let \(K\) be a number field, \(v\) a finite place of \(K\) with residue norm \(N(v)\), and \(t, \delta\) real numbers with \(0 \le t \le \delta\). If complex numbers \(\alpha, \beta\) form a Satake pair with local exponent \(t\) at residue cardinality \(N(v)\), then \(|\alpha + \beta| \le 2 N(v)^\delta\).

theorem hecke_norm_le_two_mul_residueNorm_rpow_of_isSatakePair
    {K : Type*} [Field K] [NumberField K]
    (v : NumberField.FinitePlace K) {t δ : ℝ}
    {α β : ℂ} (ht0 : 0 ≤ t) (ht : t ≤ δ)
    (h : IsSatakePair v.residueNorm t α β) :
    ‖α + β‖ ≤ 2 * v.residueNorm ^ δ

Uses 3

Statement usesSatake pairs with a given local exponent · Residue norm of a finite place

Proof usesHecke bound from a Satake pair

DefinitionExceptional Selberg eigenvalue witnesses#✓fully proved

The type of pairs \((\Gamma, \lambda)\) where \(\Gamma\) is a congruence subgroup of \(\mathrm{SL}_2(\mathbb{Z})\) and \(\lambda\) is a real eigenvalue of the hyperbolic Laplacian on \(L^2(\Gamma \backslash \mathbb{H})\) with \(0 < \lambda < 1/4\).

Morally, these pairs index archimedean local components over \(\mathbb{Q}\); their identification with genuine cuspidal automorphic local components is a modelling assumption.

def SelbergWitness : Type :=
  {x : Subgroup SL(2, ℤ) × ℝ // IsCongruenceSubgroup x.1 ∧
    IsEigenvalue x.1 x.2 ∧ 0 < x.2 ∧ x.2 < 1 / 4}

Uses 2 · Used by 4

Statement usesCongruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient

Used byFamilies dominating the Selberg exceptional spectrum · The Selberg family's exponent is Selberg's constant · Selberg family of archimedean exponents · Selberg gap of an exceptional eigenvalue

DefinitionSelberg gap of an exceptional eigenvalue#✓fully proved

For an exceptional-eigenvalue witness, a congruence subgroup \(\Gamma\) of \(\mathrm{SL}_2(\mathbb{Z})\) with a Laplace eigenvalue \(\lambda \in (0, 1/4)\), the Selberg gap is \(\sqrt{1/4 - \lambda}\): the archimedean local exponent \(\theta\) forced by \(\lambda\), written as \(\lambda = 1/4 - \theta^2\).

noncomputable def selbergGap (w : SelbergWitness) : ℝ :=
  Real.sqrt (1 / 4 - w.1.2)

Uses 3 · Used by 4

Statement usesExceptional Selberg eigenvalue witnesses · Congruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient

Used byFamilies dominating the Selberg exceptional spectrum · The Selberg family's exponent is Selberg's constant · Selberg family of archimedean exponents · Exceptional eigenvalues bound Selberg-dominating exponents from below

DefinitionSelberg family of archimedean exponents#✓fully proved

The Selberg family is the local-exponent family indexed by the exceptional-eigenvalue witnesses, the pairs \((\Gamma, \lambda)\) of a congruence subgroup \(\Gamma\) of \(\mathrm{SL}_2(\mathbb{Z})\) and a Laplace eigenvalue \(\lambda \in (0, 1/4)\) of \(\Gamma\), whose local exponent at \((\Gamma, \lambda)\) is \(\sqrt{1/4 - \lambda}\).

noncomputable def selbergFamily : LocalExponentFamily SelbergWitness where
  exponent := selbergGap
  exponent_nonneg := fun w => Real.sqrt_nonneg _
  exponent_le_half := by
    intro w
    apply le_half_of_mem_exceptionalGaps
    exact Or.inr ⟨w.1.2, w.2.2.1, w.2.2.2.1, w.2.2.2.2, rfl⟩

Uses 6 · Used by 1

Statement usesFamily of local exponents · Exceptional Selberg eigenvalue witnesses · Selberg gap of an exceptional eigenvalue · Congruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient · Gap contributions of a subgroup of the modular group

Used byThe Selberg family's exponent is Selberg's constant

DefinitionFamilies dominating the Selberg exceptional spectrum#✓fully proved

A local-exponent family \(F\) with local exponents \(m_i\) (\(i \in \iota\)) dominates the Selberg archimedean slice when, for every congruence subgroup \(\Gamma\) of \(\mathrm{SL}_2(\mathbb{Z})\) and every eigenvalue \(\lambda\) of the hyperbolic Laplacian on \(L^2(\Gamma \backslash \mathbb{H})\) with \(0 < \lambda < 1/4\), there is an index \(i\) with \(m_i = \sqrt{1/4 - \lambda}\).

This is the precise anchor needed for the comparison with Selberg's constant; it is a hypothesis on a proposed genuine family, not a definition of one.

def DominatesSelberg {ι : Type*} (F : LocalExponentFamily ι) : Prop :=
  ∀ w : SelbergWitness, ∃ i, selbergGap w = F.exponent i

Uses 3 · Used by 3

Statement usesFamily of local exponents · Exceptional Selberg eigenvalue witnesses · Selberg gap of an exceptional eigenvalue

Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Exceptional eigenvalues bound Selberg-dominating exponents from below

TheoremExceptional eigenvalues bound Selberg-dominating exponents from below#✓fully proved

Let \(F\) be a local-exponent family that dominates the Selberg archimedean slice. If \(\Gamma\) is a congruence subgroup of \(\mathrm{SL}_2(\mathbb{Z})\) and \(\lambda\) is a real eigenvalue of the hyperbolic Laplacian on \(L^2(\Gamma \backslash \mathbb{H})\) with \(0 < \lambda < 1/4\), then \(\sqrt{1/4 - \lambda}\) is at most the Ramanujan exponent of \(F\).

theorem sqrt_le_ramanujanExponentOf_of_dominatesSelberg {ι : Type*}
    (F : LocalExponentFamily ι) (hdom : DominatesSelberg F)
    {Γ : Subgroup SL(2, ℤ)} (hΓ : IsCongruenceSubgroup Γ) {lam : ℝ}
    (hlam : IsEigenvalue Γ lam) (hpos : 0 < lam) (hlt : lam < 1 / 4) :
    Real.sqrt (1 / 4 - lam) ≤ ramanujanExponentOf F

Uses 7 · Used by 1

Statement usesFamilies dominating the Selberg exceptional spectrum · Family of local exponents · Ramanujan exponent of a local-exponent family · Congruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient

Proof usesLocal exponents are bounded by the Ramanujan exponent · Selberg gap of an exceptional eigenvalue

Used bySelberg's constant is at most every dominating family's exponent

TheoremSelberg's constant is at most every dominating family's exponent#✓fully proved

Let \(F\) be a local-exponent family that dominates the Selberg archimedean slice, that is, for every congruence subgroup \(\Gamma\) of \(\mathrm{SL}_2(\mathbb{Z})\) and every Laplace eigenvalue \(\lambda \in (0, 1/4)\) of \(\Gamma\), the gap \(\sqrt{1/4 - \lambda}\) is one of the local exponents of \(F\). Then Selberg's constant is at most the Ramanujan exponent of \(F\).

For the genuine cuspidal family this is the archimedean comparison of Selberg's constant with the Ramanujan exponent \(\delta_2\); it is not an equality of constants.

theorem selbergConstant_le_of_dominatesSelberg {ι : Type*}
    (F : LocalExponentFamily ι) (hdom : DominatesSelberg F) :
    selbergConstant ≤ ramanujanExponentOf F

Uses 11 · Used by 1

Statement usesFamilies dominating the Selberg exceptional spectrum · Family of local exponents · Ramanujan exponent of a local-exponent family · Selberg's congruence spectral-gap constant

Proof usesExponent set of a local-exponent family · Exceptional eigenvalues bound Selberg-dominating exponents from below · Congruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient · Gap parameter of a subgroup of the modular group · Gap contributions of a subgroup of the modular group · The modular group is a congruence subgroup

Used byThe Selberg family's exponent is Selberg's constant

TheoremThe Selberg family's exponent is Selberg's constant#✓fully proved

The Ramanujan exponent of the canonical Selberg family of archimedean exponents is exactly Selberg's congruence spectral-gap constant.

This identifies the currently anchored archimedean slice; it does not identify that slice with the full Ramanujan exponent.

theorem ramanujanExponentOf_selbergFamily :
    ramanujanExponentOf selbergFamily = selbergConstant

Uses 16

Statement usesExceptional Selberg eigenvalue witnesses · Ramanujan exponent of a local-exponent family · Selberg family of archimedean exponents · Selberg's congruence spectral-gap constant

Proof usesFamilies dominating the Selberg exceptional spectrum · Family of local exponents · Admissible exponents bound the Ramanujan exponent · Selberg's constant is at most every dominating family's exponent · Selberg gap of an exceptional eigenvalue · Congruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient · Gap parameter of a subgroup of the modular group · Congruence gaps are bounded by Selberg's constant · Gap contributions of a subgroup of the modular group · The modular group is a congruence subgroup · Exceptional eigenvalues bound Selberg's constant

22 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.