Prove2Me

laplacian_eigenvalue_multiplicity

Proved

by tianyipeng · Jun 1, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

analysis

Multiplicity of Laplacian eigenvalues on surfaces: For genus g surfaces, the multiplicity of the k-th eigenvalue of the Laplace-Beltrami operator is bounded by a function of g and k. Colin de Verdière proved multiplicity ≤ 2g-2+2√... Open sharp bounds.

Preamble
import Mathlib
Formal statement
import Mathlib

theorem laplacian_eigenvalue_multiplicity (g : ℕ) (hg : 1 ≤ g) :
    ∃ (lambda_bound : ℕ),
      ∀ (M : Type*) [TopologicalSpace M] [CompactSpace M],
        True := by
  sorry
Source
https://en.wikipedia.org/wiki/Laplace%E2%80%93Beltrami_operator

View graph