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.
Definition2.1
Group: Definitions of sphere packings, density, and the optimization target. (3)
Preview
Definition 2.3
Associated Lean declarations
-
SpherePacking.balls[complete]
Used by 2
Preview
Definition 2.3
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]
Associated Lean declarations
-
SpherePacking.balls[complete]
-
abbrev SpherePacking.balls {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`. Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets and predicates.(EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ))abbrev SpherePacking.balls {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) : SetSet.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`. Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets and predicates.(EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ))
We now define a notion of density for bounded regions of space by considering the density inside balls of finite radius.
Definition2.3
Group: Definitions of sphere packings, density, and the optimization target. (3)
Preview
Definition 2.1
Associated Lean declarations
-
SpherePacking.finiteDensity[complete]
Used by 3
Preview
Definition 2.4
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.
Uses Lemma 0 and Definition 2.1.
Lean code for Definition2.3●1 definition
Associated Lean declarations
-
SpherePacking.finiteDensity[complete]
Associated Lean declarations
-
SpherePacking.finiteDensity[complete]
-
def SpherePacking.finiteDensity {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) (Rℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.def SpherePacking.finiteDensity {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) (Rℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
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.
Definition2.4
Group: Definitions of sphere packings, density, and the optimization target. (3)
Preview
Definition 2.1
Associated Lean declarations
-
SpherePacking.density[complete]
Used by 7
Preview
Definition 2.5
We define the density of a packing \Pa as the limit superior
\Delta_{\mathcal{P}}:=\limsup\limits_{R\to\infty}\Delta_{\mathcal{P}}(R).
Uses Lemma 0 and Definition 2.3.
Lean code for Definition2.4●1 definition
Associated Lean declarations
-
SpherePacking.density[complete]
Associated Lean declarations
-
SpherePacking.density[complete]
-
def SpherePacking.density {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.def SpherePacking.density {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.
We may now define the sphere packing constant, the quantity that the sphere packing problem requires us to compute.
Definition2.5
Group: Definitions of sphere packings, density, and the optimization target. (3)
Preview
Definition 2.1
Associated Lean declarations
-
SpherePackingConstant[complete]
Used by 2
Preview
Lemma 2.9
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}}.
Uses Definition 2.1 and Definition 2.4.
Lean code for Definition2.5●1 definition
Associated Lean declarations
-
SpherePackingConstant[complete]
Associated Lean declarations
-
SpherePackingConstant[complete]
-
def SpherePackingConstant (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.def SpherePackingConstant (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.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.
Definition2.6
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.
Uses Lemma 0.
Lean code for Definition2.6●1 definition
Associated Lean declarations
-
SpherePacking.scale[complete]
Associated Lean declarations
-
SpherePacking.scale[complete]
-
def SpherePacking.scale {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) : SpherePackingSpherePacking (d : ℕ) : Typedℕdef SpherePacking.scale {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) : SpherePackingSpherePacking (d : ℕ) : Typedℕ
Lemma2.7
Group: Scaling invariance of finite density and asymptotic density. (3)
Preview
Definition 2.6
Associated Lean declarations
-
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).
Uses Definition 2.3 and Definition 2.6.
Lean code for Lemma2.7●1 theorem
Associated Lean declarations
-
SpherePacking.scale_finiteDensity[complete]
Associated Lean declarations
-
SpherePacking.scale_finiteDensity[complete]
-
theorem SpherePacking.scale_finiteDensity {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ→ ∀ (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) (Rℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.), (SSpherePacking d.scaleSpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking dhc0 < c).finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal(HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.cℝ*HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.Rℝ)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SSpherePacking d.finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNRealRℝtheorem SpherePacking.scale_finiteDensity {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} : 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ→ ∀ (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) (Rℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.), (SSpherePacking d.scaleSpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking dhc0 < c).finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal(HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.cℝ*HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.Rℝ)HMul.hMul.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HMul α β γ] : α → β → γ`a * b` computes the product of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `*` in identifiers is `mul`.=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SSpherePacking d.finiteDensitySpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNRealRℝFinite density of a scaled packing.
Proof
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)).
Lemma2.8
Group: Scaling invariance of finite density and asymptotic density. (3)
Preview
Definition 2.6
Associated Lean declarations
-
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).
Uses Definition 2.6.
Lean code for Lemma2.8●1 theorem
Associated Lean declarations
-
SpherePacking.scale_density[complete]
Associated Lean declarations
-
SpherePacking.scale_density[complete]
-
theorem SpherePacking.scale_density {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) : (SSpherePacking d.scaleSpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking dhc0 < c).densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNRealtheorem SpherePacking.scale_density {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) (SSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) {cℝ: ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.} (hc0 < c: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.cℝ) : (SSpherePacking d.scaleSpherePacking.scale {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking dhc0 < c).densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNRealDensity of a scaled packing.
Proof
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.7 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}.
Lemma2.9
Group: Scaling invariance of finite density and asymptotic density. (3)
Preview
Definition 2.6
Associated Lean declarations
\Delta_d = \sup\limits_{\substack{\Pa \subset \R^d \\ \text{sphere packing} \\ \text{sep.~rad.} = 1}} \Delta_{\Pa}
Uses Definition 2.5 and Definition 2.4.
Lean code for Lemma2.9●1 theorem
Associated Lean declarations
Associated Lean declarations
-
theorem SpherePacking.constant_eq_constant_normalized {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) : SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.dℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.⨆ SSpherePacking d, ⨆ (_ : SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1), SSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNRealtheorem SpherePacking.constant_eq_constant_normalized {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) : SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.dℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.⨆ SSpherePacking d, ⨆ (_ : SSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.1), SSpherePacking d.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal
Proof
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.8, 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.
Definition2.10
Group: Periodic and lattice packings as a reduced optimization class. (4)
Preview
Definition 2.11
Associated Lean declarations
-
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.10●1 definition
Associated Lean declarations
-
IsZLattice[complete]
Associated Lean declarations
-
IsZLattice[complete]
-
class IsZLattice.{u_1, u_2} (K
Type u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.) [NormedFieldNormedField.{u_5} (α : Type u_5) : Type u_5A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.KType u_1] {EType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [NormedAddCommGroupNormedAddCommGroup.{u_8} (E : Type u_8) : Type u_8A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines a metric space structure.EType u_2] [NormedSpaceNormedSpace.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] : Type (max u_6 u_7)A normed space over a normed field is a vector space endowed with a norm which satisfies the equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove `‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`. Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this typeclass can be used for "seminormed spaces" too, just as `Module` can be used for "semimodules".KType u_1EType u_2] (LSubmodule ℤ E: SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).EType u_2) [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.↥LSubmodule ℤ E] : PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.class IsZLattice.{u_1, u_2} (K
Type u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.) [NormedFieldNormedField.{u_5} (α : Type u_5) : Type u_5A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.KType u_1] {EType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [NormedAddCommGroupNormedAddCommGroup.{u_8} (E : Type u_8) : Type u_8A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines a metric space structure.EType u_2] [NormedSpaceNormedSpace.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] : Type (max u_6 u_7)A normed space over a normed field is a vector space endowed with a norm which satisfies the equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove `‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`. Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this typeclass can be used for "seminormed spaces" too, just as `Module` can be used for "semimodules".KType u_1EType u_2] (LSubmodule ℤ E: SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).EType u_2) [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.↥LSubmodule ℤ E] : PropThe universe of propositions. `Prop ≡ Sort 0`. Every proposition is propositionally equal to either `True` or `False`.`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`.
Instance Constructor
IsZLattice.mk.{u_1, u_2} {K
Type u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [NormedFieldNormedField.{u_5} (α : Type u_5) : Type u_5A normed field is a field with a norm satisfying ‖x y‖ = ‖x‖ ‖y‖.KType u_1] {EType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [NormedAddCommGroupNormedAddCommGroup.{u_8} (E : Type u_8) : Type u_8A normed group is an additive group endowed with a norm for which `dist x y = ‖-x + y‖` defines a metric space structure.EType u_2] [NormedSpaceNormedSpace.{u_6, u_7} (𝕜 : Type u_6) (E : Type u_7) [NormedField 𝕜] [SeminormedAddCommGroup E] : Type (max u_6 u_7)A normed space over a normed field is a vector space endowed with a norm which satisfies the equality `‖c • x‖ = ‖c‖ ‖x‖`. We require only `‖c • x‖ ≤ ‖c‖ ‖x‖` in the definition, then prove `‖c • x‖ = ‖c‖ ‖x‖` in `norm_smul`. Note that since this requires `SeminormedAddCommGroup` and not `NormedAddCommGroup`, this typeclass can be used for "seminormed spaces" too, just as `Module` can be used for "semimodules".KType u_1EType u_2] {LSubmodule ℤ E: SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).EType u_2} [DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.↥LSubmodule ℤ E] (span_topSubmodule.span K ↑L = ⊤: Submodule.spanSubmodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.KType u_1↑LSubmodule ℤ E=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element Conventions for notations in identifiers: * The recommended spelling of `⊤` in identifiers is `top`.) : IsZLatticeIsZLattice.{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`.KType u_1LSubmodule ℤ EMethods
span_top
Submodule.span K ↑L = ⊤`L` spans the full space `E` over `K`.: Submodule.spanSubmodule.span.{u_1, u_4} (R : Type u_1) {M : Type u_4} [Semiring R] [AddCommMonoid M] [Module R M] (s : Set M) : Submodule R MThe span of a set `s ⊆ M` is the smallest submodule of M that contains `s`.KType u_1↑LSubmodule ℤ E=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.⊤Top.top.{u_1} {α : Type u_1} [self : Top α] : αThe top (`⊤`, `\top`) element Conventions for notations in identifiers: * The recommended spelling of `⊤` in identifiers is `top`.`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.
Definition2.11
Group: Periodic and lattice packings as a reduced optimization class. (4)
Preview
Definition 2.10
Associated Lean declarations
-
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.11●1 definition
Associated Lean declarations
-
LinearMap.BilinForm.dualSubmodule[complete]
Associated Lean declarations
-
LinearMap.BilinForm.dualSubmodule[complete]
-
def LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} {R
Type u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} {SType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} {MType u_3: Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.RType u_1] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements. An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`. Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself). See also note [forgetful inheritance]. If the field has positive characteristic `p`, our division by zero convention forces `ratCast (1 / p) = 1 / 0 = 0`.SType u_2] [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.MType u_3] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`. See the implementation notes in this file for discussion of the details of this definition.RType u_1SType u_2] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`, connected by a "scalar multiplication" operation `r • x : M` (where `r : R` and `x : M`) with some natural associativity and distributivity axioms similar to those on a ring.RType u_1MType u_3] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`, connected by a "scalar multiplication" operation `r • x : M` (where `r : R` and `x : M`) with some natural associativity and distributivity axioms similar to those on a ring.SType u_2MType u_3] [IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative action of `M` on `α` is determined by the multiplicative actions of `M` on `N` and `N` on `α`.RType u_1SType u_2MType u_3] (BLinearMap.BilinForm S M: LinearMap.BilinFormLinearMap.BilinForm.{u_1, u_6} (R : Type u_1) [CommSemiring R] (M : Type u_6) [AddCommMonoid M] [Module R M] : Type (max u_1 u_6)For convenience, a shorthand for the type of bilinear forms from `M` to `R`.SType u_2MType u_3) (NSubmodule R M: SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.RType u_1MType u_3) : SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.RType u_1MType u_3def LinearMap.BilinForm.dualSubmodule.{u_1, u_2, u_3} {R
Type u_1: Type u_1A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} {SType u_2: Type u_2A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} {MType u_3: Type u_3A type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.} [CommRingCommRing.{u} (α : Type u) : Type uA commutative ring is a ring with commutative multiplication.RType u_1] [FieldField.{u} (K : Type u) : Type uA `Field` is a `CommRing` with multiplicative inverses for nonzero elements. An instance of `Field K` includes maps `ratCast : ℚ → K` and `qsmul : ℚ → K → K`. Those two fields are needed to implement the `DivisionRing K → Algebra ℚ K` instance since we need to control the specific definitions for some special cases of `K` (in particular `K = ℚ` itself). See also note [forgetful inheritance]. If the field has positive characteristic `p`, our division by zero convention forces `ratCast (1 / p) = 1 / 0 = 0`.SType u_2] [AddCommGroupAddCommGroup.{u} (G : Type u) : Type uAn additive commutative group is an additive group with commutative `(+)`.MType u_3] [AlgebraAlgebra.{u, v} (R : Type u) (A : Type v) [CommSemiring R] [Semiring A] : Type (max u v)An associative unital `R`-algebra is a semiring `A` equipped with a map into its center `R → A`. See the implementation notes in this file for discussion of the details of this definition.RType u_1SType u_2] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`, connected by a "scalar multiplication" operation `r • x : M` (where `r : R` and `x : M`) with some natural associativity and distributivity axioms similar to those on a ring.RType u_1MType u_3] [ModuleModule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] : Type (max u v)A module is a generalization of vector spaces to a scalar semiring. It consists of a scalar semiring `R` and an additive monoid of "vectors" `M`, connected by a "scalar multiplication" operation `r • x : M` (where `r : R` and `x : M`) with some natural associativity and distributivity axioms similar to those on a ring.SType u_2MType u_3] [IsScalarTowerIsScalarTower.{u_9, u_10, u_11} (M : Type u_9) (N : Type u_10) (α : Type u_11) [SMul M N] [SMul N α] [SMul M α] : PropAn instance of `IsScalarTower M N α` states that the multiplicative action of `M` on `α` is determined by the multiplicative actions of `M` on `N` and `N` on `α`.RType u_1SType u_2MType u_3] (BLinearMap.BilinForm S M: LinearMap.BilinFormLinearMap.BilinForm.{u_1, u_6} (R : Type u_1) [CommSemiring R] (M : Type u_6) [AddCommMonoid M] [Module R M] : Type (max u_1 u_6)For convenience, a shorthand for the type of bilinear forms from `M` to `R`.SType u_2MType u_3) (NSubmodule R M: SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.RType u_1MType u_3) : SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.RType u_1MType u_3The dual submodule of a submodule with respect to a bilinear form.
We can now define periodic sphere packings.
Definition2.12
Group: Periodic and lattice packings as a reduced optimization class. (4)
Preview
Definition 2.10
Associated Lean declarations
-
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.
Uses Lemma 0 and Definition 2.10.
Lean code for Definition2.12●1 definition
Associated Lean declarations
-
PeriodicSpherePacking[complete]
Associated Lean declarations
-
PeriodicSpherePacking[complete]
-
structure PeriodicSpherePacking (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.structure PeriodicSpherePacking (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : TypeA type universe. `Type ≡ Type 0`, `Type u ≡ Sort (u + 1)`.Constructor
PeriodicSpherePacking.mk {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (toSpherePackingSpherePacking d: SpherePackingSpherePacking (d : ℕ) : Typedℕ) (latticeSubmodule ℤ (EuclideanSpace ℝ (Fin d)): SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).(EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ))) (lattice_action∀ ⦃x y : EuclideanSpace ℝ (Fin d)⦄, x ∈ lattice → y ∈ toSpherePacking.centers → x + y ∈ toSpherePacking.centers: ∀ ⦃xEuclideanSpace ℝ (Fin d)yEuclideanSpace ℝ (Fin d): EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ)⦄, xEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.latticeSubmodule ℤ (EuclideanSpace ℝ (Fin d))→ yEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.toSpherePackingSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))→ xEuclideanSpace ℝ (Fin d)+HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `+` in identifiers is `add`.yEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.toSpherePackingSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))) (lattice_discreteautoParam (DiscreteTopology ↥lattice) PeriodicSpherePacking.lattice_discrete._autoParam: DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.↥latticeSubmodule ℤ (EuclideanSpace ℝ (Fin d)):= by infer_instance) (lattice_isZLatticeautoParam (IsZLattice ℝ lattice) PeriodicSpherePacking.lattice_isZLattice._autoParam: IsZLatticeIsZLattice.{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`.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.latticeSubmodule ℤ (EuclideanSpace ℝ (Fin d)):= by infer_instance) : PeriodicSpherePackingPeriodicSpherePacking (d : ℕ) : TypedℕExtends
-
SpherePackingSpherePacking (d : ℕ) : Typedℕ
Fields
centers : Set
Set.{u} (α : Type u) : Type uA set is a collection of elements of some type `α`. Although `Set` is defined as `α → Prop`, this is an implementation detail which should not be relied on. Instead, `setOf` and membership of a set (`∈`) should be used to convert between sets and predicates.(EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ))Inherited from-
SpherePacking
separation : ℝ
Real : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.Inherited from-
SpherePacking
separation_pos : 0 <
LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.selfPeriodicSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝInherited from-
SpherePacking
centers_dist : Pairwise
Pairwise.{u_1} {α : Type u_1} (r : α → α → Prop) : PropA relation `r` holds pairwise if `r i j` for all `i ≠ j`.fun x1↑self.centersx2↑self.centers↦ selfPeriodicSpherePacking d.separationSpherePacking.separation {d : ℕ} (self : SpherePacking d) : ℝ≤LE.le.{u} {α : Type u} [self : LE α] : α → α → PropThe less-equal relation: `x ≤ y` Conventions for notations in identifiers: * The recommended spelling of `≤` in identifiers is `le`. * The recommended spelling of `<=` in identifiers is `le` (prefer `≤` over `<=`).distDist.dist.{u_3} {α : Type u_3} [self : Dist α] : α → α → ℝDistance between two pointsx1↑self.centersx2↑self.centersInherited from-
SpherePacking
lattice
Submodule ℤ (EuclideanSpace ℝ (Fin d)): SubmoduleSubmodule.{u, v} (R : Type u) (M : Type v) [Semiring R] [AddCommMonoid M] [Module R M] : Type vA submodule of a module is one which is closed under vector operations. This is a sufficient condition for the subset of vectors in the submodule to themselves form a module.ℤInt : TypeThe integers. This type is special-cased by the compiler and overridden with an efficient implementation. The runtime has a special representation for `Int` that stores “small” signed numbers directly, while larger numbers use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)). A “small number” is an integer that can be encoded with one fewer bits than the platform's pointer size (i.e. 63 bits on 64-bit architectures and 31 bits on 32-bit architectures).(EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ))lattice_action
∀ ⦃x y : EuclideanSpace ℝ (Fin d)⦄, x ∈ self.lattice → y ∈ self.centers → x + y ∈ self.centers: ∀ ⦃xEuclideanSpace ℝ (Fin d)yEuclideanSpace ℝ (Fin d): EuclideanSpaceEuclideanSpace.{u_7, u_8} (𝕜 : Type u_7) (n : Type u_8) : Type (max u_7 u_8)The standard real/complex Euclidean space, functions on a finite type. For an `n`-dimensional space use `EuclideanSpace 𝕜 (Fin n)`. For the case when `n = Fin _`, there is `!₂[x, y, ...]` notation for building elements of this type, analogous to `![x, y, ...]` notation.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.(FinFin (n : ℕ) : TypeNatural numbers less than some upper bound. In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the canonical type with `n` elements.dℕ)⦄, xEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.selfPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d))→ yEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.selfPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))→ xEuclideanSpace ℝ (Fin d)+HAdd.hAdd.{u, v, w} {α : Type u} {β : Type v} {γ : outParam (Type w)} [self : HAdd α β γ] : α → β → γ`a + b` computes the sum of `a` and `b`. The meaning of this notation is type-dependent. Conventions for notations in identifiers: * The recommended spelling of `+` in identifiers is `add`.yEuclideanSpace ℝ (Fin d)∈Membership.mem.{u, v} {α : outParam (Type u)} {γ : Type v} [self : Membership α γ] : γ → α → PropThe membership relation `a ∈ s : Prop` where `a : α`, `s : γ`. Conventions for notations in identifiers: * The recommended spelling of `∈` in identifiers is `mem`.selfPeriodicSpherePacking d.centersSpherePacking.centers {d : ℕ} (self : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))lattice_discrete
DiscreteTopology ↥self.lattice: DiscreteTopologyDiscreteTopology.{u_2} (α : Type u_2) [t : TopologicalSpace α] : PropA topological space is discrete if every set is open, that is, its topology equals the discrete topology `⊥`.↥selfPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d))lattice_isZLattice
IsZLattice ℝ self.lattice: IsZLatticeIsZLattice.{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`.ℝReal : TypeThe type `ℝ` of real numbers constructed as equivalence classes of Cauchy sequences of rational numbers.selfPeriodicSpherePacking d.latticePeriodicSpherePacking.lattice {d : ℕ} (self : PeriodicSpherePacking d) : Submodule ℤ (EuclideanSpace ℝ (Fin d)) -
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 the periodic-density theorem below, 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.
Definition2.13
Group: Periodic and lattice packings as a reduced optimization class. (4)
Preview
Definition 2.10
Associated Lean declarations
-
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.
Uses Definition 2.4 and Definition 2.12.
Lean code for Definition2.13●1 definition
Associated Lean declarations
-
PeriodicSpherePackingConstant[complete]
Associated Lean declarations
-
PeriodicSpherePackingConstant[complete]
-
def PeriodicSpherePackingConstant (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.def PeriodicSpherePackingConstant (d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.) : ENNRealENNReal : TypeThe extended nonnegative real numbers. This is usually denoted [0, ∞], and is relevant as the codomain of a measure.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.
Theorem2.14
Group: Periodic and lattice packings as a reduced optimization class. (4)
Preview
Definition 2.10
Associated Lean declarations
-
periodic_constant_eq_constant[sorry in proof]
Used by 2
Preview
Corollary 2.16
For all d, the periodic sphere packing constant in \R^d is equal to
the sphere packing constant in \R^d.
Uses Definition 2.4 and Definition 2.13.
Lean code for Theorem2.14●1 theorem, incomplete
Associated Lean declarations
-
periodic_constant_eq_constant[sorry in proof]
Associated Lean declarations
-
periodic_constant_eq_constant[sorry in proof]
-
theorem periodic_constant_eq_constant {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) : PeriodicSpherePackingConstantPeriodicSpherePackingConstant (d : ℕ) : ENNRealThe `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.dℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.dℕtheorem periodic_constant_eq_constant {d
ℕ: ℕNat : TypeThe natural numbers, starting at zero. This type is special-cased by both the kernel and the compiler, and overridden with an efficient implementation. Both use a fast arbitrary-precision arithmetic library (usually [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed.} (hd0 < d: 0 <LT.lt.{u} {α : Type u} [self : LT α] : α → α → PropThe less-than relation: `x < y` Conventions for notations in identifiers: * The recommended spelling of `<` in identifiers is `lt`.dℕ) : PeriodicSpherePackingConstantPeriodicSpherePackingConstant (d : ℕ) : ENNRealThe `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.dℕ=Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.SpherePackingConstantSpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.dℕ
Proof
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.
Theorem2.15
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Preview
Corollary 2.16
Lean status
- 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 E8Packing.
Uses Lemma 4.5, Definition 2.5, Definition 2.4, Theorem 4.11, Theorem 6.3, and Theorem 6.2.
Proof
Directly follows from the Cohn-Elkies general theorem
Theorem 6.2 applied to the function
f(x)=g(x/\sqrt{2}) of the theorem Theorem 6.3.
Corollary2.16
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Preview
Theorem 2.15
Lean status
- No associated Lean code or declarations.
All packing \mathcal{P} \subseteq \R^8 has density satisfying
\Delta_{\mathcal{P}} \leq \Delta_{E_8}.
Uses Theorem 2.14 and Theorem 2.15.
Proof
This is a direct consequence of Theorem Theorem 2.14 on periodic-packing optimality and the CE main theorem Theorem 2.15.
Corollary2.17
Group: Reduction from Cohn-Elkies bounds to the final dimension-8 theorem. (2)
Preview
Theorem 2.15
Associated Lean declarations
-
SpherePacking.MainTheorem[sorry in proof]
\Delta_8 = \Delta_{E_8}.
Uses Corollary 2.16.
Lean code for Corollary2.17●1 theorem, incomplete
Associated Lean declarations
-
SpherePacking.MainTheorem[sorry in proof]
Associated Lean declarations
-
SpherePacking.MainTheorem[sorry in proof]
-
theorem SpherePacking.MainTheorem : SpherePackingConstant
SpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.8 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.E8PackingE8Packing : PeriodicSpherePacking 8.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNRealtheorem SpherePacking.MainTheorem : SpherePackingConstant
SpherePackingConstant (d : ℕ) : ENNRealThe `SpherePackingConstant` in dimension d is the supremum of the density of all packings. See also `<TODO>` for specifying the separation radius of the packings.8 =Eq.{u_1} {α : Sort u_1} : α → α → PropThe equality relation. It has one introduction rule, `Eq.refl`. We use `a = b` as notation for `Eq a b`. A fundamental property of equality is that it is an equivalence relation. ``` variable (α : Type) (a b c d : α) variable (hab : a = b) (hcb : c = b) (hcd : c = d) example : a = d := Eq.trans (Eq.trans hab (Eq.symm hcb)) hcd ``` Equality is much more than an equivalence relation, however. It has the important property that every assertion respects the equivalence, in the sense that we can substitute equal expressions without changing the truth value. That is, given `h1 : a = b` and `h2 : p a`, we can construct a proof for `p b` using substitution: `Eq.subst h1 h2`. Example: ``` example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := Eq.subst h1 h2 example (α : Type) (a b : α) (p : α → Prop) (h1 : a = b) (h2 : p a) : p b := h1 ▸ h2 ``` The triangle in the second presentation is a macro built on top of `Eq.subst` and `Eq.symm`, and you can enter it by typing `\t`. For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality) Conventions for notations in identifiers: * The recommended spelling of `=` in identifiers is `eq`.E8PackingE8Packing : PeriodicSpherePacking 8.densitySpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal
Proof
By definition, \Delta_{E_8} \leq \Delta_8, while the upper-bound-E8
corollary Corollary 2.16 shows that
\Delta_8 = \sup_{\mathrm{packing} \, \mathcal{P}} \leq \Delta_{E_8}, and
the result follows.