Pólya's conjecture on Laplacian eigenvalues

StructureNonnegative discrete spectrum#✓fully proved

A nonnegative discrete spectrum is a sequence of real numbers \(E_0, E_1, E_2, \ldots\), the eigenvalues listed with multiplicity, such that \(E_j \ge 0\) for every \(j\), \(E_i \le E_j\) whenever \(i \le j\), and \(E_j \to +\infty\) as \(j \to \infty\).

The sequence is not required to be the spectrum of any particular operator, such as a Dirichlet or Neumann Laplacian.

structure NonnegativeDiscreteSpectrum where
  eigenvalue : ℕ → ℝ
  nonnegative_eigenvalue : ∀ j, 0 ≤ eigenvalue j
  monotone_eigenvalue : Monotone eigenvalue
  tendsto_eigenvalue_atTop :
    Filter.Tendsto eigenvalue Filter.atTop Filter.atTop

Used by 9

Used byEigenvalue counting function · A nonnegative discrete spectrum is determined by its eigenvalues · Dirichlet spectrum of an open set · Membership in the finite strict sublevel set · Riesz mean · The Riesz mean of order zero is the counting function · Finite strict sublevel set · Strict sublevel set · Strict sublevel sets are finite

TheoremA nonnegative discrete spectrum is determined by its eigenvalues#✓fully proved

If two nonnegative discrete spectra \(S\) and \(T\) have the same \(j\)-th eigenvalue for every index \(j \in \mathbb{N}\), then \(S = T\).

@[ext] theorem ext {S T : NonnegativeDiscreteSpectrum} (h : ∀ j, S j = T j) :
    S = T

Uses 1

Statement usesNonnegative discrete spectrum

DefinitionStrict sublevel set#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and a real number \(\Lambda\), the strict sublevel set at \(\Lambda\) is the set of indices \(\{j \in \mathbb{N} : E_j < \Lambda\}\).

The strict inequality matches the convention that \((\Lambda - E_j)_+^0\) equals \(1\) only when \(E_j < \Lambda\), avoiding \(0^0 = 1\) at the cutoff.

def sublevelSet (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) : Set ℕ :=
  {j | S j < Λ}

Uses 1 · Used by 3

Statement usesNonnegative discrete spectrum

Used byMembership in the finite strict sublevel set · Finite strict sublevel set · Strict sublevel sets are finite

TheoremStrict sublevel sets are finite#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and every real number \(\Lambda\), the strict sublevel set \(\{j \in \mathbb{N} : E_j < \Lambda\}\) is finite.

Since \(E_j \to +\infty\), there is \(N\) with \(E_j \ge \Lambda\) for all \(j \ge N\), so the set is contained in \(\{0, 1, \ldots, N - 1\}\).

theorem sublevelSet_finite
    (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) :
    (S.sublevelSet Λ).Finite

Uses 2 · Used by 2

Statement usesNonnegative discrete spectrum · Strict sublevel set

Used byMembership in the finite strict sublevel set · Finite strict sublevel set

DefinitionFinite strict sublevel set#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and a real number \(\Lambda\), the finite strict sublevel set at \(\Lambda\) is the strict sublevel set \(\{j \in \mathbb{N} : E_j < \Lambda\}\), regarded as a finite set of indices; it is finite because \(E_j \to +\infty\).

noncomputable def sublevelFinset
    (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) : Finset ℕ :=
  (S.sublevelSet_finite Λ).toFinset

Uses 3 · Used by 4

Statement usesNonnegative discrete spectrum · Strict sublevel set · Strict sublevel sets are finite

Used byEigenvalue counting function · Membership in the finite strict sublevel set · Riesz mean · The Riesz mean of order zero is the counting function

TheoremMembership in the finite strict sublevel set#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\), a real number \(\Lambda\) and an index \(j \in \mathbb{N}\), the index \(j\) lies in the finite strict sublevel set at \(\Lambda\) if and only if \(E_j < \Lambda\).

@[simp] theorem mem_sublevelFinset
    (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) (j : ℕ) :
    j ∈ S.sublevelFinset Λ ↔ S j < Λ

Uses 4

Statement usesNonnegative discrete spectrum · Finite strict sublevel set

Proof usesStrict sublevel set · Strict sublevel sets are finite

DefinitionEigenvalue counting function#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and a real number \(\Lambda\), the counting function \(N(\Lambda)\) is the number of indices \(j \in \mathbb{N}\) with \(E_j < \Lambda\), so eigenvalues are counted with multiplicity.

noncomputable def countingFunction
    (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) : ℕ :=
  (S.sublevelFinset Λ).card

Uses 2 · Used by 1

Statement usesNonnegative discrete spectrum · Finite strict sublevel set

Used byThe Riesz mean of order zero is the counting function

DefinitionRiesz mean#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and real numbers \(\sigma\) and \(\Lambda\), the Riesz mean of order \(\sigma\) at \(\Lambda\) is the finite sum \(R_\sigma(\Lambda) = \sum_{j \in \mathbb{N},\, E_j < \Lambda} (\Lambda - E_j)^\sigma\) over indices, where \(x^\sigma\) is the real power.

noncomputable def rieszMean
    (S : NonnegativeDiscreteSpectrum) (σ Λ : ℝ) : ℝ :=
  ∑ j ∈ S.sublevelFinset Λ, Real.rpow (Λ - S j) σ

Uses 2 · Used by 1

Statement usesNonnegative discrete spectrum · Finite strict sublevel set

Used byThe Riesz mean of order zero is the counting function

TheoremThe Riesz mean of order zero is the counting function#✓fully proved

For a nonnegative discrete spectrum with eigenvalues \(E_0 \le E_1 \le \cdots\) and every real number \(\Lambda\), the Riesz mean of order \(0\) at \(\Lambda\) equals the counting function at \(\Lambda\), viewed as a real number: \(R_0(\Lambda) = N(\Lambda)\).

Every summand \((\Lambda - E_j)^0\) has strictly positive base \(\Lambda - E_j\), so it equals \(1\).

@[simp] theorem rieszMean_zero
    (S : NonnegativeDiscreteSpectrum) (Λ : ℝ) :
    S.rieszMean 0 Λ = S.countingFunction Λ

Uses 4

Statement usesNonnegative discrete spectrum · Eigenvalue counting function · Riesz mean

Proof usesFinite strict sublevel set

AbbreviationSmooth test functions#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\), the space of smooth test functions on \(\Omega\) is the real vector space of infinitely differentiable functions \(f : \mathbb{R}^n \to \mathbb{R}\) whose support is compact and contained in \(\Omega\).

These functions form the core of the Dirichlet form.

abbrev SmoothTestSpace {n : ℕ} (Ω : Opens (EuclideanSpace ℝ (Fin n))) :=
  TestFunction Ω ℝ ⊤

Used by 2

Used byRayleigh quotient · Variational eigenvalue

DefinitionRayleigh quotient#✓fully proved

For a smooth test function \(f\) on an open set \(\Omega \subseteq \mathbb{R}^n\), the Rayleigh quotient of \(f\) is

\[R(f) = \frac{\int_{\mathbb{R}^n} \|Df(x)\|^2 \, dx}{\int_{\mathbb{R}^n} |f(x)|^2 \, dx},\]

where \(\|Df(x)\|\) is the operator norm of the derivative of \(f\) at \(x\) (equal to \(|\nabla f(x)|\)) and both integrals are against Lebesgue measure. For \(f = 0\) the quotient \(0/0\) is read as \(0\).

noncomputable def rayleighQuotient {n : ℕ} {Ω : Opens (EuclideanSpace ℝ (Fin n))}
    (f : SmoothTestSpace Ω) : ℝ :=
  (∫ x, ‖fderiv ℝ (f : EuclideanSpace ℝ (Fin n) → ℝ) x‖ ^ 2 ∂volume) /
    (∫ x, |f x| ^ 2 ∂volume)

Uses 1 · Used by 1

Statement usesSmooth test functions

Used byVariational eigenvalue

DefinitionVariational eigenvalue#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\) and an index \(j \ge 0\), the variational eigenvalue of \(\Omega\) at index \(j\) is the Courant–Fischer min–max value

\[\lambda_j(\Omega) = \inf_V \, \sup_{f \in V,\ f \ne 0} R(f),\]

where \(V\) ranges over the \((j+1)\)-dimensional subspaces of the space of smooth test functions on \(\Omega\) and \(R(f)\) is the Rayleigh quotient of \(f\). Infima and suprema are taken in \(\mathbb{R}\), where an empty set, or a set unbounded in the relevant direction, has value \(0\).

This is a definition only: it does not claim that the values are attained, nonnegative, monotone in \(j\), divergent, or eigenvalues of an operator.

noncomputable def variationalEigenvalue {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) (j : ℕ) : ℝ :=
  sInf {a : ℝ | ∃ V : Submodule ℝ (SmoothTestSpace Ω),
    Module.finrank ℝ ↥V = j + 1 ∧
      a = sSup {q : ℝ | ∃ f : ↥V,
        (f : SmoothTestSpace Ω) ≠ 0 ∧
          rayleighQuotient (f : SmoothTestSpace Ω) = q}}

Uses 2 · Used by 1

Statement usesSmooth test functions · Rayleigh quotient

Used byDirichlet spectrum of an open set

DefinitionDirichlet spectrum of an open set#✓fully proved

A nonnegative discrete spectrum \(S = (S_j)_{j \ge 0}\) is the Dirichlet spectrum of an open set \(\Omega \subseteq \mathbb{R}^n\) when \(S_j = \lambda_j(\Omega)\) for every \(j \ge 0\), where \(\lambda_j(\Omega)\) is the variational eigenvalue of \(\Omega\) at index \(j\).

def NonnegativeDiscreteSpectrum.IsDirichletSpectrum {n : ℕ}
    (S : NonnegativeDiscreteSpectrum)
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) : Prop :=
  ∀ j, S j = DirichletLaplacian.variationalEigenvalue Ω j

Uses 2

Statement usesVariational eigenvalue · Nonnegative discrete spectrum

DefinitionVolume of the unit ball#✓fully proved

For \(n \ge 0\), \(\omega_n\) is the Lebesgue measure of the open unit ball \(\{x \in \mathbb{R}^n : |x| < 1\}\) of Euclidean space \(\mathbb{R}^n\), as a real number.

noncomputable def unitBallVolume (n : ℕ) : ℝ :=
  (volume : Measure (EuclideanSpace ℝ (Fin n))).real
    (Metric.ball (0 : EuclideanSpace ℝ (Fin n)) 1)

Used by 3

Used byNeumann Pólya benchmark · Pólya eigenvalue benchmark · Semiclassical counting coefficient

DefinitionVolume of a domain#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\), the volume \(|\Omega|\) is the Lebesgue measure of \(\Omega\) taken as a real number, with \(|\Omega| = 0\) when the Lebesgue measure of \(\Omega\) is infinite.

noncomputable def domainVolume {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) : ℝ :=
  (volume : Measure (EuclideanSpace ℝ (Fin n))).real (Ω : Set _)

Used by 3

Used byNeumann Pólya benchmark · Pólya eigenvalue benchmark · Semiclassical counting coefficient

DefinitionSemiclassical counting coefficient#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\), the semiclassical counting coefficient is \(\omega_n |\Omega| / (2\pi)^n\), where \(\omega_n\) is the volume of the unit ball in \(\mathbb{R}^n\) and \(|\Omega|\) is the Lebesgue measure of \(\Omega\) taken as a real number, with \(|\Omega| = 0\) when that measure is infinite.

noncomputable def semiclassicalCountingCoefficient {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) : ℝ :=
  unitBallVolume n * domainVolume Ω / (2 * Real.pi) ^ n

Uses 2

Statement usesVolume of a domain · Volume of the unit ball

DefinitionPólya eigenvalue benchmark#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\) and an index \(j \ge 0\), the Pólya benchmark at index \(j\) is

\[(2\pi)^2 \left(\frac{j+1}{\omega_n |\Omega|}\right)^{2/n},\]

where \(\omega_n\) is the volume of the unit ball in \(\mathbb{R}^n\) and \(|\Omega|\) is the volume of \(\Omega\). Indices start at \(0\), so index \(j\) belongs to the \((j+1)\)-st eigenvalue.

Division by zero is read as \(0\): the exponent is \(0\) when \(n = 0\), and the base is \(0\) when \(\omega_n |\Omega| = 0\).

noncomputable def polyaEigenvalueBenchmark {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) (j : ℕ) : ℝ :=
  (2 * Real.pi) ^ 2 *
    ((((j + 1 : ℕ) : ℝ) /
      (unitBallVolume n * domainVolume Ω)) ^ (2 / (n : ℝ)))

Uses 2 · Used by 1

Statement usesVolume of a domain · Volume of the unit ball

Used byNeumann and Dirichlet Pólya benchmarks agree after an index shift

DefinitionNeumann Pólya benchmark#✓fully proved

For an open set \(\Omega \subseteq \mathbb{R}^n\) and a natural number \(j\), the Neumann Pólya benchmark of \(\Omega\) at index \(j\) is the real number \((2\pi)^2 \left(j / (\omega_n |\Omega|)\right)^{2/n}\), where \(\omega_n\) is the volume of the unit ball of \(\mathbb{R}^n\), \(|\Omega|\) is the volume of \(\Omega\), the power is the real power with exponent \(2/n\), and a quotient by \(0\) is read as \(0\).

The index is zero-based: \(j\) is the source's one-based eigenvalue number minus one, so index zero records the constant Neumann mode in positive dimension.

noncomputable def neumannPolyaEigenvalueBenchmark {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) (j : ℕ) : ℝ :=
  (2 * Real.pi) ^ 2 *
    ((((j : ℕ) : ℝ) /
      (unitBallVolume n * domainVolume Ω)) ^ (2 / (n : ℝ)))

Uses 2 · Used by 1

Statement usesVolume of a domain · Volume of the unit ball

Used byNeumann and Dirichlet Pólya benchmarks agree after an index shift

TheoremNeumann and Dirichlet Pólya benchmarks agree after an index shift#✓fully proved

For every open set \(\Omega \subseteq \mathbb{R}^n\) and every natural number \(j\), the Neumann Pólya benchmark of \(\Omega\) at index \(j + 1\) equals the Pólya eigenvalue benchmark of \(\Omega\) at index \(j\).

In the source's one-based numbering, the Neumann index \(j + 2\) has the same Weyl benchmark as the Dirichlet index \(j + 1\).

@[simp] theorem neumannPolyaEigenvalueBenchmark_succ {n : ℕ}
    (Ω : Opens (EuclideanSpace ℝ (Fin n))) (j : ℕ) :
    neumannPolyaEigenvalueBenchmark Ω (j + 1) =
      polyaEigenvalueBenchmark Ω j

Uses 2

Statement usesNeumann Pólya benchmark · Pólya eigenvalue benchmark

19 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.