PackingBound

Periodic sphere packings, Poisson summation, and the linear-programming bound.

instance CohnElkies.numeralTwoAtLeast : Nat.AtLeastTwo 2

instance CohnElkies.euclideanFiniteDimensional (d : ℕ) : FiniteDimensional ℝ (EuclideanSpace ℝ (Fin d))

Euclidean coordinate space in a finite dimension is finite-dimensional.

instance CohnElkies.euclideanBorelSpace (d : ℕ) : BorelSpace (EuclideanSpace ℝ (Fin d))

Euclidean coordinate space carries its standard Borel structure.

structure SpherePacking (d : ℕ) : Type

A sphere-packing configuration in Euclidean dimension d.

• centers : Set (EuclideanSpace ℝ (Fin d))

  The set of packing centers.

• separation : ℝ

  The minimum prescribed distance between distinct centers.

• separation_pos : 0 < self.separation

  The prescribed separation is positive.

• centers_dist : Pairwise fun (x1 x2 : ↑self.centers) => self.separation ≤ dist x1 x2

  Distinct centers are separated by at least separation.

theorem SpherePacking.distinct_centers_separation_bound {d : ℕ} (S : SpherePacking d) (x y : EuclideanSpace ℝ (Fin d)) (hx : x ∈ S.centers) (hy : y ∈ S.centers) (hxy : x ≠ y) : S.separation ≤ dist x y

Distinct centers of a packing obey its separation bound.

noncomputable def SpherePacking.rescaleConfiguration {d : ℕ} (S : SpherePacking d) {c : ℝ} (hc : 0 < c) : SpherePacking d

Scale every center and the separation of a packing by a positive factor.

Equations

• S.rescaleConfiguration hc = { centers := (fun (x : EuclideanSpace ℝ (Fin d)) => c • x) '' S.centers, separation := c * S.separation, separation_pos := ⋯, centers_dist := ⋯ }

noncomputable def SpherePackingConstant (d : ℕ) : ENNReal

The supremal upper density among sphere packings in dimension d.

Equations

• SpherePackingConstant d = ⨆ (S : SpherePacking d), SpherePacking.upperPackingDensity✝ S