2. Sphere Packings
The sphere packing problem is a classic optimisation problem with widespread applications that go well beyond mathematics. The task is to determine the densest possible arrangement of spheres in a given space. It remains unsolved in all but finitely many dimensions.
It was famously determined, in Viazovska (2017), that the optimal arrangement
in \R^8 is given by the E_8 lattice. The result is strongly dependent on
the Cohn-Elkies linear programming bound, Theorem 3.1 in Cohn and Elkies (2003),
which, if a \R^d \to \R function satisfying certain conditions exists,
bounds the optimal density of sphere packings in \R^d in terms of it. The
proof in Viazovska (2017) uses the theory of modular forms to construct a
function that can be used to bound the density of all sphere packings in
\R^8 above by the density of the E_8 lattice packing. This then allows us
to conclude that no packing in \R^8 can be denser than the E_8 lattice
packing.
This subsection gives an overview of the setup of the problem, both
informally and in Lean. Throughout this blueprint, \R^d denotes the
Euclidean vector space equipped with distance \|\cdot\| and Lebesgue
measure \mathrm{Vol}(\cdot). For any x \in \R^d and
r \in \R_{>0}, we denote by B_d(x,r) the open ball in \R^d with
center x and radius r. While we will give a more formal definition of
a sphere packing below, the underlying idea is that it is a union of balls of
equal radius centered at points that are far enough from each other that the
balls do not overlap.
Arguably the most important definition in this subsection is that of packing
density, which measures which portion of d-dimensional Euclidean space is
covered by a given sphere packing. Taking the supremum over all packings gives
the sphere packing constant, which is the quantity we are interested in
optimising.
-
SpherePacking.balls[complete]
Given a set X \subset \R^d and a real number r > 0 such that
\|x-y\| \ge r for all distinct x,y \in X, we define the sphere packing
\Pa(X) with centres at X to be the union of all open balls of radius
r centred at points in X:
\Pa(X) := \bigcup_{x \in X} B_d(x,r)
Lean code for Definition2.1●1 definition
Associated Lean declarations
-
SpherePacking.balls[complete]
-
SpherePacking.balls[complete]
-
abbrevdefined in SpherePacking/Basic/SpherePacking.leancomplete
abbrev SpherePacking.balls {d : ℕ} (S : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))
abbrev SpherePacking.balls {d : ℕ} (S : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))
We now define a notion of density for bounded regions of space by considering the density inside balls of finite radius.
- Definition 2.1
- SpherePacking
-
SpherePacking.finiteDensity[complete]
The finite density of a packing \Pa is defined as
\Delta_{\mathcal{P}}(R):=\frac{\Vol{\mathcal{P}\cap B_d(0,R)}}{\Vol{B_d(0,R)}},\quad R>0.
Lean code for Definition2.2●1 definition
Associated Lean declarations
-
SpherePacking.finiteDensity[complete]
-
SpherePacking.finiteDensity[complete]
-
defdefined in SpherePacking/Basic/SpherePacking.leancomplete
def SpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal
def SpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal
As intuitive as it seems to take the density of a packing to be the limit of the finite densities as the radius of the ball goes to infinity, it is not immediately clear that this limit exists. Therefore, we define the density of a sphere packing as a limit superior instead.
- Definition 2.2
- SpherePacking
-
SpherePacking.density[complete]
We define the density of a packing \Pa as the limit superior
\Delta_{\mathcal{P}}:=\limsup\limits_{R\to\infty}\Delta_{\mathcal{P}}(R).
Lean code for Definition2.3●1 definition
Associated Lean declarations
-
SpherePacking.density[complete]
-
SpherePacking.density[complete]
-
defdefined in SpherePacking/Basic/SpherePacking.leancomplete
def SpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal
def SpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal
We may now define the sphere packing constant, the quantity that the sphere packing problem requires us to compute.
-
SpherePackingConstant[complete]
The sphere packing constant is defined as the supremum of packing densities
over all possible packings:
\Delta_d:=\sup\limits_{\substack{\mathcal{P}\subset\R^d\\ \scriptscriptstyle\mathrm{sphere}\;\mathrm{packing}}}\Delta_{\mathcal{P}}.
Lean code for Definition2.4●1 definition
Associated Lean declarations
-
SpherePackingConstant[complete]
-
SpherePackingConstant[complete]
-
defdefined in SpherePacking/Basic/SpherePacking.leancomplete
def SpherePackingConstant (d : ℕ) : ENNReal
def SpherePackingConstant (d : ℕ) : ENNReal
The `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.
Given a sphere packing \Pa(X) with separation radius r, we define the
scaled packing with respect to a real number c > 0 to be the packing
\Pa(cX), where cX = \setof{cx \in V}{x \in X} has separation radius
cr.
Lean code for Definition2.5●1 definition
Associated Lean declarations
-
SpherePacking.scale[complete]
-
SpherePacking.scale[complete]
-
defdefined in SpherePacking/Basic/SpherePacking.leancomplete
def SpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking d
def SpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking d
-
SpherePacking.scale_finiteDensity[complete]
Let \Pa(X) be a sphere packing and c a positive real number. Then, for
all R > 0,
\Delta_{\Pa(cX)}(cR) = \Delta_{\Pa(X)}(R).
Lean code for Lemma2.6●1 theorem
Associated Lean declarations
-
SpherePacking.scale_finiteDensity[complete]
-
SpherePacking.scale_finiteDensity[complete]
-
theoremdefined in SpherePacking/Basic/SpherePacking.leancomplete
theorem SpherePacking.scale_finiteDensity {d : ℕ} : 0 < d → ∀ (S : SpherePacking d) {c : ℝ} (hc : 0 < c) (R : ℝ), (S.scale hc).finiteDensity (c * R) = S.finiteDensity R
theorem SpherePacking.scale_finiteDensity {d : ℕ} : 0 < d → ∀ (S : SpherePacking d) {c : ℝ} (hc : 0 < c) (R : ℝ), (S.scale hc).finiteDensity (c * R) = S.finiteDensity R
Finite density of a scaled packing.
The proof follows by direct computation:
\Delta_{\Pa(cX)}(cR) = \frac{\Vol{\Pa(cX) \cap B_d(0, cR)}}{\Vol{B_d(0, cR)}} = \frac{c^d \cdot \Vol{\Pa(X) \cap B_d(0, R)}}{c^d \cdot \Vol{B_d(0, R)}} = \Delta_{\Pa(X)}(R).
The second equality follows from the fact that scaling a measurable set by a
factor of c scales its volume by a factor of c^d, together with
\Pa(cX) \cap B_d(0, cR) = c \cdot (\Pa(X) \cap B_d(0, R)).
-
SpherePacking.scale_density[complete]
Let \Pa(X) be a sphere packing and c a positive real number. Then the
density of the scaled packing \Pa(cX) is equal to the density of the
original packing \Pa(X).
Lean code for Lemma2.7●1 theorem
Associated Lean declarations
-
SpherePacking.scale_density[complete]
-
SpherePacking.scale_density[complete]
-
theoremdefined in SpherePacking/Basic/SpherePacking.leancomplete
theorem SpherePacking.scale_density {d : ℕ} (hd : 0 < d) (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : (S.scale hc).density = S.density
theorem SpherePacking.scale_density {d : ℕ} (hd : 0 < d) (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : (S.scale hc).density = S.density
Density of a scaled packing.
One can show, using relatively unsophisticated real analysis, that
\limsup_{R \to \infty} \Delta_{\Pa(cX)}(R) = \limsup_{cR \to \infty} \Delta_{\Pa(cX)}(cR).
Lemma Lemma 2.6 tells us that
\Delta_{\Pa(cX)}(cR) = \Delta_{\Pa(X)}(R) for every R > 0. Therefore,
\limsup_{cR \to \infty} \Delta_{\Pa(cX)}(cR) = \limsup_{cR \to \infty} \Delta_{\Pa(X)}(R) = \limsup_{R \to \infty} \Delta_{\Pa(X)}(R),
where the second equality is the result of a similar change of variables.
Therefore, as expected, we do not need to worry about the separation radius
when constructing sphere packings. This will be useful when we attempt to
construct the optimal sphere packing in \R^8, and even more so when
attempting to formalise this construction, because the underlying structure of
the packing is given by the E_8 lattice, which has separation radius
\sqrt{2}.
\Delta_d = \sup\limits_{\substack{\Pa \subset \R^d \\ \text{sphere packing} \\ \text{sep.~rad.} = 1}} \Delta_{\Pa}
Lean code for Lemma2.8●1 theorem
Associated Lean declarations
-
theoremdefined in SpherePacking/Basic/SpherePacking.leancomplete
theorem SpherePacking.constant_eq_constant_normalized {d : ℕ} (hd : 0 < d) : SpherePackingConstant d = ⨆ S, ⨆ (_ : S.separation = 1), S.density
theorem SpherePacking.constant_eq_constant_normalized {d : ℕ} (hd : 0 < d) : SpherePackingConstant d = ⨆ S, ⨆ (_ : S.separation = 1), S.density
That the supremum over packings of unit density is at most the sphere packing
constant is obvious. For the reverse inequality, let \Pa(X) be any sphere
packing with separation radius r. By
Lemma 2.7, the density of \Pa(X) is equal to
that of the scaled packing \Pa\!\left(\frac{X}{r}\right). Since the scaled
packing has separation radius 1, its density is at most the supremum over
all packings of unit density, and therefore the same is true of \Pa(X).
We begin by defining what a lattice is in Euclidean space.
-
IsZLattice[complete]
We say that an additive subgroup \Lambda \le \R^d is a lattice if it is
discrete and its \R-span contains all the elements of \R^d.
Lean code for Definition2.9●1 definition
Associated Lean declarations
-
IsZLattice[complete]
-
IsZLattice[complete]
-
classdefined in Mathlib/Algebra/Module/ZLattice/Basic.leancomplete
class IsZLattice.{u_1, u_2} (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Prop
class IsZLattice.{u_1, u_2} (K : Type u_1) [NormedField K] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace K E] (L : Submodule ℤ E) [DiscreteTopology ↥L] : Prop
`L : Submodule ℤ E` where `E` is a vector space over a normed field `K` is a `ℤ`-lattice if it is discrete and spans `E` over `K`.
Methods
span_top : Submodule.span K ↑L = ⊤
`L` spans the full space `E` over `K`.
There is also a corresponding dual notion, which becomes relevant when we start doing Fourier analysis on functions over lattices.
-
LinearMap.BilinForm.dualSubmodule[complete]
The dual lattice of a lattice \Lambda is the set
\Lambda^* := \setof{v \in \R^d}{\forall l \in \Lambda, \left\langle v,l \right\rangle \in \Z}.
Lean code for Definition2.10●1 definition
Associated Lean declarations
-
LinearMap.BilinForm.dualSubmodule[complete]
-
LinearMap.BilinForm.dualSubmodule[complete]
-
defdefined in Mathlib/LinearAlgebra/BilinearForm/DualLattice.leancomplete
def LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (N : Submodule R M) : Submodule R M
def LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} {R : Type u_1} {S : Type u_2} {M : Type u_3} [CommRing R] [Field S] [AddCommGroup M] [Algebra R S] [Module R M] [Module S M] [IsScalarTower R S M] (B : LinearMap.BilinForm S M) (N : Submodule R M) : Submodule R M
The dual submodule of a submodule with respect to a bilinear form.
We can now define periodic sphere packings.
- Definition 2.9
- SpherePacking
-
PeriodicSpherePacking[complete]
We say that a sphere packing \Pa(X) is \Lambda-periodic if there exists
a lattice \Lambda \subset \R^d such that for all x \in X and
y \in \Lambda, we have x+y \in X.
Lean code for Definition2.11●1 definition
Associated Lean declarations
-
PeriodicSpherePacking[complete]
-
PeriodicSpherePacking[complete]
-
structuredefined in SpherePacking/Basic/SpherePacking.leancomplete
structure PeriodicSpherePacking (d : ℕ) : Type
structure PeriodicSpherePacking (d : ℕ) : Type
Extends
-
SpherePacking d
Fields
centers : Set (EuclideanSpace ℝ (Fin d))
Inherited from-
SpherePacking
separation : ℝ
Inherited from-
SpherePacking
separation_pos : 0 < self.separation
Inherited from-
SpherePacking
centers_dist : Pairwise fun x1 x2 ↦ self.separation ≤ dist x1 x2
Inherited from-
SpherePacking
lattice : Submodule ℤ (EuclideanSpace ℝ (Fin d))
lattice_action : ∀ ⦃x y : EuclideanSpace ℝ (Fin d)⦄, x ∈ self.lattice → y ∈ self.centers → x + y ∈ self.centers
lattice_discrete : DiscreteTopology ↥self.lattice
lattice_isZLattice : IsZLattice ℝ self.lattice
-
There is a natural definition of density for periodic sphere packings, namely the local density of balls in a fundamental domain. However, a priori the density of sphere packing above need not to coincide with this alternative definition. In Theorem 3.5, we will prove that this is the case.
Now that we have simplified the process of computing the packing densities of specific packings, we can simplify the computation of the sphere packing constant. It turns out that once again, periodicity is key.
-
PeriodicSpherePackingConstant[complete]
The periodic sphere packing constant is defined to be
\Delta_{d}^{\text{periodic}} := \sup_{\substack{P \subset \R^d \\ \text{periodic packing}}} \Delta_P.
Lean code for Definition2.12●1 definition
Associated Lean declarations
-
PeriodicSpherePackingConstant[complete]
-
PeriodicSpherePackingConstant[complete]
-
defdefined in SpherePacking/Basic/SpherePacking.leancomplete
def PeriodicSpherePackingConstant (d : ℕ) : ENNReal
def PeriodicSpherePackingConstant (d : ℕ) : ENNReal
The `PeriodicSpherePackingConstant` in dimension d is the supremum of the density of all periodic packings. See also `<TODO>` for specifying the separation radius of the packings.
-
periodic_constant_eq_constant[sorry in proof]
For all d, the periodic sphere packing constant in \R^d is equal to
the sphere packing constant in \R^d.
Lean code for Theorem2.13●1 theorem, incomplete
Associated Lean declarations
-
periodic_constant_eq_constant[sorry in proof]
-
periodic_constant_eq_constant[sorry in proof]
-
theoremdefined in SpherePacking/Basic/PeriodicPacking.leancontains sorry
theorem periodic_constant_eq_constant {d : ℕ} (hd : 0 < d) : PeriodicSpherePackingConstant d = SpherePackingConstant d
theorem periodic_constant_eq_constant {d : ℕ} (hd : 0 < d) : PeriodicSpherePackingConstant d = SpherePackingConstant d
State this in Lean (ready). Fill in proof here (see ElkiesCohn, Appendix A).
Thus, one can show a sphere packing to be optimal by showing its density to be equal to the periodic sphere packing constant instead of the regular sphere packing constant. Determining the periodic constant is easier than determining the general constant, as we shall see when investigating the linear programming bounds derived by Cohn and Elkies in Cohn and Elkies (2003).
With the terminologies above, we can state the main theorem of this project.
- No associated Lean code or declarations.
All periodic packing \mathcal{P} \subseteq \R^8 has density satisfying
\Delta_{\mathcal{P}} \leq \Delta_{E_8} = \frac{\pi^4}{384}, the density of
the E_8 sphere packing; see Definition 4.9.
Directly follows from Theorem 6.2 applied to the
function f(x)=g(x/\sqrt{2}) of Theorem 6.3.
- No associated Lean code or declarations.
All packing \mathcal{P} \subseteq \R^8 has density satisfying
\Delta_{\mathcal{P}} \leq \Delta_{E_8}.
This is a direct consequence of Theorem 2.13 and Theorem 2.14.
-
SpherePacking.MainTheorem[sorry in proof]
\Delta_8 = \Delta_{E_8}.
Lean code for Corollary2.16●1 theorem, incomplete
Associated Lean declarations
-
SpherePacking.MainTheorem[sorry in proof]
-
SpherePacking.MainTheorem[sorry in proof]
-
theoremdefined in SpherePacking/MainTheorem.leancontains sorry
theorem SpherePacking.MainTheorem : SpherePackingConstant 8 = E8Packing.density
theorem SpherePacking.MainTheorem : SpherePackingConstant 8 = E8Packing.density
By definition, \Delta_{E_8} \leq \Delta_8, while the upper-bound-E8
corollary Corollary 2.15 shows that
\Delta_8 = \sup_{\mathrm{packing} \, \mathcal{P}} \leq \Delta_{E_8}, and
the result follows.