theorem Equiangular.exists_exp_many_approx_equiangular (α : ℝ) (hα_pos : 0 < α) (hα_lt : α < 1) (ε : ℝ) (hε : 0 < ε) : ∃ (c : ℝ), 0 < c ∧ ∀ (n : ℕ), ∃ (N : ℕ) (v : Fin N → EuclideanSpace ℝ (Fin n)), (∀ (i : Fin N), ‖v i‖ = 1) ∧ (∀ (i j : Fin N), i ≠ j → |inner ℝ (v i) (v j) - α| ≤ ε) ∧ ↑N ≥ 2 ^ (c * ↑n)

Exponentially many approximately equiangular vectors (Theorem 5.2.1). For any target inner product $\alpha \in (0, 1)$ and tolerance $\varepsilon > 0$, there is a constant $c > 0$ such that for every $n$ there exist $N \geq 2^{cn}$ unit vectors $v_1, \dots, v_N \in \mathbb{R}^n$ with $|\langle v_i, v_j \rangle - \alpha| \leq \varepsilon$ for all $i \neq j$.

theorem Equiangular.exists_exp_many_approx_orthogonal (ε : ℝ) (hε : 0 < ε) : ∃ (c : ℝ), 0 < c ∧ ∀ (d : ℕ), ∃ (N : ℕ) (v : Fin N → EuclideanSpace ℝ (Fin d)), (∀ (i : Fin N), ‖v i‖ = 1) ∧ (∀ (i j : Fin N), i ≠ j → |inner ℝ (v i) (v j)| ≤ ε) ∧ ↑N ≥ Real.exp (c * ε ^ 2 * ↑d)

Exponentially many approximately orthogonal vectors. For any tolerance $\varepsilon > 0$ there is a constant $c > 0$ such that for every dimension $d$ there exist $N \geq \exp(c \varepsilon^2 d)$ unit vectors $v_1, \dots, v_N \in \mathbb{R}^d$ with $|\langle v_i, v_j \rangle| \leq \varepsilon$ for all $i \neq j$.