Equiangular lines

StructureEquiangular systems of unit vectors#✓fully proved

For a real number \(\alpha\) and a natural number \(d\), an equiangular system with inner product \(\pm\alpha\) in \(\mathbb{R}^d\) is a set of unit vectors in \(d\)-dimensional Euclidean space such that any two distinct vectors \(x\) and \(y\) in it satisfy \(|\langle x, y \rangle| = \alpha\).

structure EquiangularLines (α : ℝ) (d : ℕ) where
  /-- The set of unit vectors in `d`-dimensional Euclidean space. -/
  carrier : Set (EuclideanSpace ℝ (Fin d))
  norm : ∀ x ∈ carrier, ‖x‖ = 1
  angle : carrier.Pairwise fun x y ↦ |⟪x, y⟫| = α

Sources

• Z. Jiang, J. Tidor, Y. Yao, S. Zhang, and Y. Zhao, Equiangular lines with a fixed angle, Annals of Math, 194 (3) 2021, third paragraph of the introduction.

Used by 1

Used byMaximum number of equiangular lines

DefinitionMaximum number of equiangular lines#✓fully proved

For a real number \(\alpha\) and a natural number \(d\), \(N_\alpha(d)\) is the supremum, taken in \(\mathbb{N}\), of the cardinalities of the equiangular systems of unit vectors in \(\mathbb{R}^d\) with inner product \(\pm\alpha\). Here an infinite set counts as having cardinality \(0\), and a set of natural numbers that is not bounded above has supremum \(0\).

For \(0 \le \alpha < 1\) these cardinalities are at most \(\binom{d+1}{2}\) by Gerzon's bound, and a system contains at most one of \(x\) and \(-x\), so \(N_\alpha(d)\) is the maximum number of lines through the origin in \(\mathbb{R}^d\) with pairwise angle \(\arccos \alpha\).

noncomputable def N (α : ℝ) (d : ℕ) : ℕ := ⨆ E : EquiangularLines α d, E.carrier.ncard

Sources

• Z. Jiang, J. Tidor, Y. Yao, S. Zhang, and Y. Zhao, Equiangular lines with a fixed angle, Annals of Math, 194 (3) 2021, third paragraph of the introduction.

Uses 1 · Used by 1

Statement usesEquiangular systems of unit vectors

Used byEquiangular lines with a fixed angle

DefinitionSpectral radius order#✓fully proved

For a real number \(\lambda\), the spectral radius order \(k(\lambda) \in \mathbb{N} \cup \{\infty\}\) is the least natural number \(k\) such that some simple graph on \(k\) vertices has an adjacency matrix with spectral radius \(\max(\lambda, 0)\), and \(k(\lambda) = \infty\) if there is no such graph.

The source defines \(k(\lambda)\) only for \(\lambda > 0\), where \(\max(\lambda, 0) = \lambda\).

noncomputable def spectralRadiusOrder (lambda : ℝ) : ℕ∞ :=
  ⨅ k ∈ {k : ℕ | ∃ G : SimpleGraph (Fin k), spectralRadius ℝ (G.adjMatrix ℝ) = .ofReal lambda}, k

Sources

• Z. Jiang, J. Tidor, Y. Yao, S. Zhang, and Y. Zhao, Equiangular lines with a fixed angle, Annals of Math, 194 (3) 2021, Definition 1.1.

Used by 1

Used byEquiangular lines with a fixed angle

TheoremEquiangular lines with a fixed angle#●ready to prove

Fix a real number \(\alpha\) with \(0 < \alpha < 1\), let \(\lambda = (1 - \alpha)/(2\alpha)\) and let \(k = k(\lambda)\) be the spectral radius order of \(\lambda\). Let \(N_\alpha(d)\) be the maximum number of equiangular lines in \(\mathbb{R}^d\) with common angle \(\arccos \alpha\). Then: (a) if \(k < \infty\), then \(N_\alpha(d) = \lfloor k(d - 1)/(k - 1) \rfloor\) for all sufficiently large \(d\); (b) if \(k = \infty\), then \(N_\alpha(d) = d + o(d)\) as \(d \to \infty\).

public theorem_wanted theorem_1_2 (α : ℝ) (hα : α ∈ Set.Ioo 0 1) :
    let k := spectralRadiusOrder ((1 - α) / (2 * α))
    (k < ⊤ → ∀ᶠ d in atTop, N α d = ⌊(k.toNat * (d - 1) : ℝ) / (k.toNat - 1 : ℝ)⌋₊) ∧
    (k = ⊤ → ∃ e : ℕ → ℝ, e =o[atTop] (Nat.cast : ℕ → ℝ) ∧ ∀ d, N α d = d + e d)

Sources

• Z. Jiang, J. Tidor, Y. Yao, S. Zhang, and Y. Zhao, Equiangular lines with a fixed angle, Annals of Math, 194 (3) 2021. Statement taken from https://github.com/ImperialCollegeLondon/AnnalsChallenge. Problem annals_equiangular_lines_fixed_angle of the lean-eval benchmark.

Uses 2

Statement usesMaximum number of equiangular lines · Spectral radius order

3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.