Selberg's eigenvalue conjecture

DefinitionCongruence subgroup of the modular group#✓fully proved

A subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\) is a congruence subgroup if there is a positive integer \(N\) such that every \(\gamma \in \mathrm{SL}(2, \mathbb{Z})\) whose entries are congruent modulo \(N\) to those of the identity matrix lies in \(\Gamma\); that is, \(\Gamma\) contains the principal congruence subgroup of level \(N\).

def IsCongruenceSubgroup (Γ : Subgroup SL(2, ℤ)) : Prop :=
  ∃ N : ℕ, 0 < N ∧ ∀ γ : SL(2, ℤ),
    (∀ i j, γ.1 i j ≡ (1 : Matrix (Fin 2) (Fin 2) ℤ) i j [ZMOD (N : ℤ)]) →
      γ ∈ Γ
Used by 15
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Selberg family of archimedean exponents · Selberg gap of an exceptional eigenvalue · Exceptional Selberg eigenvalue witnesses · Exceptional eigenvalues bound Selberg-dominating exponents from below · Congruence gaps are bounded by Selberg's constant · The modular group is a congruence subgroup · Kim–Sarnak eigenvalue bound · Selberg's congruence spectral-gap constant · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half · Selberg's eigenvalue conjecture · Selberg's 3/16 theorem · Exceptional eigenvalues bound Selberg's constant

TheoremThe modular group is a congruence subgroup#✓fully proved

The full group \(\mathrm{SL}(2, \mathbb{Z})\), as a subgroup of itself, is a congruence subgroup.

It contains the principal congruence subgroup of level \(1\), which is the whole group.

theorem isCongruenceSubgroup_top : IsCongruenceSubgroup ⊤
Uses 1 · Used by 4
Statement usesCongruence subgroup of the modular group
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half

DefinitionZero extension from the upper half plane#✓fully proved

For a function \(f\) from the upper half plane to \(\mathbb{C}\), its zero extension is the function from \(\mathbb{C}\) to \(\mathbb{C}\) that takes the value \(f(z)\) at every \(z\) with \(\operatorname{Im} z > 0\) and the value \(0\) at every other point.

It is used to read coordinate derivatives of \(f\) in the interior.

def ext (f : UpperHalfPlane → ℂ) : ℂ → ℂ :=
  fun z => if hz : 0 < z.im then f ⟨z, hz⟩ else 0
Used by 4
Used byThe hyperbolic Laplacian kills constants · Hyperbolic Laplacian of the squared imaginary part · Partial derivative in the imaginary direction · Partial derivative in the real direction

DefinitionPartial derivative in the real direction#✓fully proved

For a function \(f \colon \mathbb{H} \to \mathbb{C}\) and a point \(z \in \mathbb{H}\), \(\partial_x f(z)\) is the real Fréchet derivative at \(z\) of the zero extension of \(f\) to \(\mathbb{C}\), applied to the vector \(1\). When the zero extension is real-differentiable at \(z\) this is the partial derivative of \(f\) with respect to \(x = \operatorname{Re} z\); otherwise the value is \(0\).

Real, not complex, differentiability is essential: with complex derivatives the two second derivatives in the hyperbolic Laplacian would cancel by the Cauchy–Riemann equations, and the Laplacian would vanish identically.

def partialRe (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℂ :=
  fderiv ℝ (ext f) z (1 : ℂ)
Uses 1 · Used by 3
Statement usesZero extension from the upper half plane
Used byHyperbolic Laplacian · The hyperbolic Laplacian kills constants · Hyperbolic Laplacian of the squared imaginary part

DefinitionPartial derivative in the imaginary direction#✓fully proved

For a function \(f \colon \mathbb{H} \to \mathbb{C}\) and a point \(z \in \mathbb{H}\), \(\partial_y f(z)\) is the real Fréchet derivative at \(z\) of the zero extension of \(f\) to \(\mathbb{C}\), applied to the vector \(i\). When the zero extension is real-differentiable at \(z\) this is the partial derivative of \(f\) with respect to \(y = \operatorname{Im} z\); otherwise the value is \(0\).

def partialIm (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℂ :=
  fderiv ℝ (ext f) z Complex.I
Uses 1 · Used by 3
Statement usesZero extension from the upper half plane
Used byHyperbolic Laplacian · The hyperbolic Laplacian kills constants · Hyperbolic Laplacian of the squared imaginary part

DefinitionHyperbolic Laplacian#✓fully proved

For a function \(f\) from the upper half plane to \(\mathbb{C}\) and a point \(z = x + iy\) of the upper half plane, the hyperbolic Laplacian of \(f\) at \(z\) is

\[\Delta f(z) = -y^2 \left(\partial_x \partial_x f(z) + \partial_y \partial_y f(z)\right),\]

where, for a function \(g\) from the upper half plane to \(\mathbb{C}\), \(\partial_x g(z)\) and \(\partial_y g(z)\) are the real Fréchet derivatives at \(z\) of the zero extension of \(g\) to \(\mathbb{C}\), applied to the vectors \(1\) and \(i\) respectively (taken to be \(0\) where that extension is not real differentiable).

On smooth functions this agrees with the coordinate formula \(-y^2 (\partial^2 f / \partial x^2 + \partial^2 f / \partial y^2)\) at every interior point.

def hyperbolicLaplacian (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane) : ℂ :=
  -((z.im : ℂ) ^ 2) * (partialRe (partialRe f) z + partialIm (partialIm f) z)
Uses 2 · Used by 3
Statement usesPartial derivative in the imaginary direction · Partial derivative in the real direction
Used byThe hyperbolic Laplacian kills constants · Hyperbolic Laplacian of the squared imaginary part · Eigenvalues of the hyperbolic Laplacian on a modular quotient

TheoremThe hyperbolic Laplacian kills constants#✓fully proved

For every complex number \(c\) and every point \(z\) of the upper half plane, the hyperbolic Laplacian of the constant function with value \(c\) at \(z\) is \(0\).

theorem hyperbolicLaplacian_const (c : ℂ) (z : UpperHalfPlane) :
    hyperbolicLaplacian (fun _ => c) z = 0
Uses 4
Statement usesHyperbolic Laplacian
Proof usesZero extension from the upper half plane · Partial derivative in the imaginary direction · Partial derivative in the real direction

TheoremHyperbolic Laplacian of the squared imaginary part#✓fully proved

Let \(f\) be the function on the upper half plane given by \(f(u) = (\operatorname{Im} u)^2\), viewed as a complex number. Then for every point \(z\) of the upper half plane the hyperbolic Laplacian of \(f\) at \(z\) equals \(-2 (\operatorname{Im} z)^2\).

This is a non-holomorphic check: the value is not zero, whereas with complex derivatives the computation would collapse by Cauchy--Riemann.

theorem hyperbolicLaplacian_im_sq (z : UpperHalfPlane) :
    hyperbolicLaplacian (fun u : UpperHalfPlane => (((u : ℂ).im ^ 2 : ℝ) : ℂ)) z =
      -2 * (((z : ℂ).im ^ 2 : ℝ) : ℂ)
Uses 4
Statement usesHyperbolic Laplacian
Proof usesZero extension from the upper half plane · Partial derivative in the imaginary direction · Partial derivative in the real direction

DefinitionTwice continuously differentiable functions on the upper half-plane#✓fully proved

A function \(f \colon \mathbb{H} \to \mathbb{C}\) is smooth (of order two) when it is the restriction of a function \(F \colon \mathbb{C} \to \mathbb{C}\) that is twice continuously differentiable, in the real sense, on the open set \(\{z \in \mathbb{C} : \operatorname{Im} z > 0\}\).

Differentiability is real, not complex: eigenfunctions of the Laplacian need not be holomorphic.

def IsSmooth (f : UpperHalfPlane → ℂ) : Prop :=
  ∃ F : ℂ → ℂ, ContDiffOn ℝ 2 F {z | 0 < z.im} ∧ ∀ z : UpperHalfPlane, f z = F z
Used by 1
Used byEigenvalues of the hyperbolic Laplacian on a modular quotient

DefinitionStandard fundamental domain of the modular group#✓fully proved

The standard fundamental domain for \(\mathrm{SL}(2, \mathbb{Z})\) is the set of points \(z\) of the upper half plane with \(|\operatorname{Re} z| \le 1/2\) and \(|z| \ge 1\).

def fundamentalDomain : Set UpperHalfPlane :=
  {z | |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖(z : ℂ)‖}
Used by 1
Used bySquare-integrable functions on a modular quotient

DefinitionFinite coset covers of the modular group#✓fully proved

A finite set \(s \subseteq \mathrm{SL}(2, \mathbb{Z})\) covers \(\mathrm{SL}(2, \mathbb{Z})\) by cosets of a subgroup \(\Gamma\) when every \(g \in \mathrm{SL}(2, \mathbb{Z})\) can be written as \(g = \gamma a\) with \(\gamma \in \Gamma\) and \(a \in s\), that is, when the cosets \(\Gamma a\) with \(a \in s\) cover \(\mathrm{SL}(2, \mathbb{Z})\). The elements of \(s\) need not lie in distinct cosets.

def IsCosetCover (Γ : Subgroup SL(2, ℤ)) (s : Finset SL(2, ℤ)) : Prop :=
  ∀ g : SL(2, ℤ), ∃ a ∈ s, ∃ γ ∈ Γ, g = γ * a
Used by 1
Used bySquare-integrable functions on a modular quotient

DefinitionSquare-integrable functions on a modular quotient#✓fully proved

For a subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\), a function \(f \colon \mathbb{H} \to \mathbb{C}\) is square-integrable on \(\Gamma \backslash \mathbb{H}\) when there is a finite set \(s \subseteq \mathrm{SL}(2, \mathbb{Z})\) whose cosets \(\Gamma a\), \(a \in s\), cover \(\mathrm{SL}(2, \mathbb{Z})\), such that

\[\int_{U} |f(z)|^2 \, d\mu(z) < \infty, \qquad U = \bigcup_{a \in s} a \cdot \mathcal{F},\]

where \(\mathcal{F} = \{z \in \mathbb{H} : |\operatorname{Re} z| \le 1/2,\ |z| \ge 1\}\) is the standard fundamental domain of \(\mathrm{SL}(2, \mathbb{Z})\), \(a \cdot \mathcal{F}\) is its image under the Möbius action of \(a\), and \(\mu\) is the hyperbolic area measure \(dx \, dy / y^2\) on \(\mathbb{H}\).

def IsL2Quotient (Γ : Subgroup SL(2, ℤ)) (f : UpperHalfPlane → ℂ) : Prop :=
  ∃ s : Finset SL(2, ℤ), IsCosetCover Γ s ∧
    (∫⁻ z in ⋃ a ∈ (s : Set SL(2, ℤ)), (fun z => a • z) '' fundamentalDomain,
      ‖f z‖ₑ ^ 2) < ∞
Uses 2 · Used by 1
Statement usesFinite coset covers of the modular group · Standard fundamental domain of the modular group
Used byEigenvalues of the hyperbolic Laplacian on a modular quotient

DefinitionEigenvalues of the hyperbolic Laplacian on a modular quotient#✓fully proved

Let \(\Gamma\) be a subgroup of \(\mathrm{SL}(2, \mathbb{Z})\). A real number \(\lambda\) is an eigenvalue of the hyperbolic Laplacian \(\Delta\) for \(\Gamma\) when there is a function \(f \colon \mathbb{H} \to \mathbb{C}\) on the upper half plane \(\mathbb{H}\) such that \(f\) is not identically zero, \(f\) is the restriction of a function on \(\mathbb{C}\) that is twice continuously differentiable in the real sense on the upper half plane, \(f(\gamma z) = f(z)\) for every \(\gamma \in \Gamma\) and every \(z \in \mathbb{H}\) (Möbius action), \(f\) is square-integrable on \(\Gamma \backslash \mathbb{H}\), and \(\Delta f(z) = \lambda f(z)\) for every \(z \in \mathbb{H}\).

def IsEigenvalue (Γ : Subgroup SL(2, ℤ)) (lam : ℝ) : Prop :=
  ∃ f : UpperHalfPlane → ℂ, f ≠ 0 ∧ IsSmooth f ∧
    (∀ γ : SL(2, ℤ), γ ∈ Γ → ∀ z : UpperHalfPlane, f (γ • z) = f z) ∧
    IsL2Quotient Γ f ∧
    ∀ z : UpperHalfPlane, hyperbolicLaplacian f z = (lam : ℂ) * f z
Uses 3 · Used by 15
Statement usesSquare-integrable functions on a modular quotient · Twice continuously differentiable functions on the upper half-plane · Hyperbolic Laplacian
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Selberg family of archimedean exponents · Selberg gap of an exceptional eigenvalue · Exceptional Selberg eigenvalue witnesses · Exceptional eigenvalues bound Selberg-dominating exponents from below · Congruence gaps are bounded by Selberg's constant · Gap contributions of a subgroup of the modular group · Kim–Sarnak eigenvalue bound · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half · Selberg's eigenvalue conjecture · Selberg's 3/16 theorem · Exceptional eigenvalues bound the gap parameter · Exceptional eigenvalues bound Selberg's constant

DefinitionGap contributions of a subgroup of the modular group#✓fully proved

For a subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\), the set of gap contributions of \(\Gamma\) is the set of real numbers consisting of \(0\) together with \(\sqrt{1/4 - \lambda}\) for every real eigenvalue \(\lambda\) of the hyperbolic Laplacian for \(\Gamma\) with \(0 < \lambda < 1/4\) (an exceptional eigenvalue).

def exceptionalGaps (Γ : Subgroup SL(2, ℤ)) : Set ℝ :=
  {0} ∪ {y | ∃ lam : ℝ, IsEigenvalue Γ lam ∧ 0 < lam ∧ lam < 1 / 4 ∧
    y = Real.sqrt (1 / 4 - lam)}
Uses 1 · Used by 8
Statement usesEigenvalues of the hyperbolic Laplacian on a modular quotient
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Selberg family of archimedean exponents · Gap parameter of a subgroup of the modular group · Congruence gaps are bounded by Selberg's constant · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half · Exceptional eigenvalues bound the gap parameter

DefinitionGap parameter of a subgroup of the modular group#✓fully proved

For a subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\), the gap parameter \(\theta(\Gamma)\) is the supremum of the set of gap contributions of \(\Gamma\): the number \(0\) together with \(\sqrt{1/4 - \lambda}\) for every real eigenvalue \(\lambda\) of the hyperbolic Laplacian for \(\Gamma\) with \(0 < \lambda < 1/4\).

noncomputable def exceptionalGap (Γ : Subgroup SL(2, ℤ)) : ℝ :=
  sSup (exceptionalGaps Γ)
Uses 1 · Used by 8
Statement usesGap contributions of a subgroup of the modular group
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Congruence gaps are bounded by Selberg's constant · Selberg's congruence spectral-gap constant · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half · Exceptional eigenvalues bound the gap parameter · Exceptional eigenvalues bound Selberg's constant

DefinitionSelberg's congruence spectral-gap constant#✓fully proved

Selberg's constant \(C_{61}\) is the supremum of the gap parameters \(\theta(\Gamma)\) over all congruence subgroups \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\), where \(\theta(\Gamma)\) is the supremum of \(0\) and of the numbers \(\sqrt{1/4 - \lambda}\) for the eigenvalues \(\lambda\) of \(\Gamma\) with \(0 < \lambda < 1/4\).

noncomputable def selbergConstant : ℝ :=
  sSup {y | ∃ Γ : Subgroup SL(2, ℤ), IsCongruenceSubgroup Γ ∧
    y = exceptionalGap Γ}
Uses 2 · Used by 8
Statement usesCongruence subgroup of the modular group · Gap parameter of a subgroup of the modular group
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant is at most every dominating family's exponent · Congruence gaps are bounded by Selberg's constant · Kim–Sarnak bound on the spectral-gap constant · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Selberg's constant is at most one half · Selberg's bound on the spectral-gap constant · Exceptional eigenvalues bound Selberg's constant

DefinitionSelberg's eigenvalue conjecture#✓fully proved

No congruence subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\) has an eigenvalue \(\lambda\) with \(0 < \lambda < 1/4\): for every congruence subgroup \(\Gamma\) and every eigenvalue \(\lambda\) of \(\Gamma\), either \(\lambda \le 0\) or \(\lambda \ge 1/4\).

Here eigenvalues are realized by smooth square-integrable eigenfunctions, which captures the discrete spectrum of the hyperbolic Laplacian.

def SelbergEigenvalueConjecture : Prop :=
  ∀ Γ : Subgroup SL(2, ℤ), IsCongruenceSubgroup Γ → ∀ lam : ℝ,
    IsEigenvalue Γ lam → ¬ (0 < lam ∧ lam < 1 / 4)
Uses 2 · Used by 1
Statement usesCongruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient
Used bySelberg's constant vanishes exactly under Selberg's eigenvalue conjecture

TheoremExceptional eigenvalues bound the gap parameter#✓fully proved

Let \(\Gamma\) be a subgroup of \(\mathrm{SL}(2, \mathbb{Z})\) and let \(\lambda\) be 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 gap parameter \(\theta(\Gamma)\) of \(\Gamma\).

theorem sqrt_le_exceptionalGap {Γ : Subgroup SL(2, ℤ)} {lam : ℝ}
    (hlam : IsEigenvalue Γ lam) (hpos : 0 < lam) (hlt : lam < 1 / 4) :
    Real.sqrt (1 / 4 - lam) ≤ exceptionalGap Γ
Uses 3 · Used by 1
Statement usesEigenvalues of the hyperbolic Laplacian on a modular quotient · Gap parameter of a subgroup of the modular group
Proof usesGap contributions of a subgroup of the modular group
Used byExceptional eigenvalues bound Selberg's constant

TheoremCongruence gaps are bounded by Selberg's constant#✓fully proved

For every congruence subgroup \(\Gamma\) of \(\mathrm{SL}(2, \mathbb{Z})\), the gap parameter \(\theta(\Gamma)\) is at most the Selberg constant \(C_{61}\).

theorem exceptionalGap_le_selbergConstant {Γ : Subgroup SL(2, ℤ)}
    (hΓ : IsCongruenceSubgroup Γ) : exceptionalGap Γ ≤ selbergConstant
Uses 5 · Used by 3
Statement usesCongruence subgroup of the modular group · Gap parameter of a subgroup of the modular group · Selberg's congruence spectral-gap constant
Proof usesEigenvalues 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 · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture · Exceptional eigenvalues bound Selberg's constant

TheoremSelberg's constant is at most one half#✓fully proved

Selberg's constant \(C_{61}\) satisfies \(C_{61} \le 1/2\).

This elementary bound follows directly from the definition.

theorem selbergConstant_le_half : selbergConstant ≤ 1 / 2
Uses 6
Statement usesSelberg's congruence spectral-gap constant
Proof usesCongruence 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

TheoremExceptional eigenvalues bound Selberg's constant#✓fully proved

Let \(\Gamma\) be a congruence subgroup of \(\mathrm{SL}(2, \mathbb{Z})\) and let \(\lambda\) be 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 Selberg's constant \(C_{61}\).

theorem sqrt_le_selbergConstant {Γ : Subgroup SL(2, ℤ)}
    (hΓ : IsCongruenceSubgroup Γ) {lam : ℝ} (hlam : IsEigenvalue Γ lam)
    (hpos : 0 < lam) (hlt : lam < 1 / 4) :
    Real.sqrt (1 / 4 - lam) ≤ selbergConstant
Uses 6 · Used by 2
Statement usesCongruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient · Selberg's congruence spectral-gap constant
Proof usesGap parameter of a subgroup of the modular group · Congruence gaps are bounded by Selberg's constant · Exceptional eigenvalues bound the gap parameter
Used byThe Selberg family's exponent is Selberg's constant · Selberg's constant vanishes exactly under Selberg's eigenvalue conjecture

TheoremSelberg's constant vanishes exactly under Selberg's eigenvalue conjecture#✓fully proved

Selberg's constant \(C_{61}\) equals \(0\) if and only if Selberg's eigenvalue conjecture holds, that is, if and only if no congruence subgroup of \(\mathrm{SL}(2, \mathbb{Z})\) has an eigenvalue \(\lambda\) with \(0 < \lambda < 1/4\).

theorem selbergConstant_eq_zero_iff :
    selbergConstant = 0 ↔ SelbergEigenvalueConjecture
Uses 9
Statement usesSelberg's eigenvalue conjecture · Selberg's congruence spectral-gap constant
Proof usesCongruence 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

TheoremSelberg's 3/16 theorem#●ready to prove

Let \(\Gamma\) be a congruence subgroup of \(\mathrm{SL}(2, \mathbb{Z})\) and let \(\lambda\) be a real eigenvalue of the hyperbolic Laplacian \(\Delta\) for \(\Gamma\), that is, \(\Delta f = \lambda f\) for some nonzero, twice continuously differentiable, \(\Gamma\)-invariant function \(f\) on the upper half plane that is square-integrable on \(\Gamma \backslash \mathbb{H}\). Then \(\lambda\) does not lie in the open interval \((0, 3/16)\): either \(\lambda \le 0\) or \(\lambda \ge 3/16\).

theorem_wanted selberg_threeSixteenths_wanted
    (Γ : Subgroup SL(2, ℤ)) (hΓ : IsCongruenceSubgroup Γ) (lam : ℝ)
    (hlam : IsEigenvalue Γ lam) :
    ¬ (0 < lam ∧ lam < 3 / 16)
Sources
  • Selberg, as recorded in Luo--Rudnick--Sarnak (1995): every eigenvalue of a congruence subgroup in the model is either 0-side excluded or at least 3/16; stated here as the absence of eigenvalues in (0, 3/16).
Uses 2
Statement usesCongruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient

TheoremSelberg's bound on the spectral-gap constant#●ready to prove

Selberg's congruence spectral-gap constant \(C_{61}\) is at most \(1/4\).

theorem_wanted selbergUpperBound_wanted :
    selbergConstant ≤ 1 / 4
Sources
  • Selberg's theorem λ₁(Γ) ≥ 3/16, catalogue upper row C₆₁ ≤ 1/4.
Uses 1
Statement usesSelberg's congruence spectral-gap constant

TheoremKim–Sarnak eigenvalue bound#●ready to prove

Let \(\Gamma\) be a congruence subgroup of \(\mathrm{SL}(2, \mathbb{Z})\) and let \(\lambda\) be a real eigenvalue of the hyperbolic Laplacian \(\Delta\) for \(\Gamma\), that is, \(\Delta f = \lambda f\) for some nonzero, twice continuously differentiable, \(\Gamma\)-invariant function \(f\) on the upper half plane that is square-integrable on \(\Gamma \backslash \mathbb{H}\). Then \(\lambda\) does not lie in the open interval \((0, 975/4096)\): either \(\lambda \le 0\) or \(\lambda \ge 975/4096\).

theorem_wanted kimSarnak975_wanted
    (Γ : Subgroup SL(2, ℤ)) (hΓ : IsCongruenceSubgroup Γ) (lam : ℝ)
    (hlam : IsEigenvalue Γ lam) :
    ¬ (0 < lam ∧ lam < 975 / 4096)
Sources
  • Kim--Sarnak (2003), as recorded in Kim--Ramakrishnan (2003): no eigenvalue of a congruence subgroup lies in (0, 975/4096).
Uses 2
Statement usesCongruence subgroup of the modular group · Eigenvalues of the hyperbolic Laplacian on a modular quotient

TheoremKim–Sarnak bound on the spectral-gap constant#●ready to prove

Selberg's congruence spectral-gap constant \(C_{61}\) is at most \(7/64\).

theorem_wanted kimSarnakUpperBound_wanted :
    selbergConstant ≤ 7 / 64
Sources
  • Kim--Sarnak bound λ₁(Γ) ≥ 975/4096 = 1/4 - (7/64)^2, catalogue best upper row C₆₁ ≤ 7/64.
Uses 1
Statement usesSelberg's congruence spectral-gap constant
22 fully proved4 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.