Density of Sphere Packings

Let X ⊆ ℝ^d be a set of points such that distinct points are at least distance r apart. Putting a ball of radius r / 2 around each point, we have a configuration of sphere packing. We call X the sphere packing centers.

We also define the density of the configuration.

structure SpherePacking (d : ℕ) : Type

• centers : Set (EuclideanSpace ℝ (Fin d))
• separation : ℝ
• separation_pos : 0 < self.separation
• centers_dist : Pairwise fun (x1 x2 : ↑self.centers) => self.separation ≤ dist x1 x2

structure PeriodicSpherePacking (d : ℕ) extends SpherePacking d : Type

• centers : Set (EuclideanSpace ℝ (Fin d))
• separation : ℝ
• separation_pos : 0 < self.separation
• centers_dist : Pairwise fun (x1 x2 : ↑self.centers) => self.separation ≤ dist x1 x2
• 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

theorem SpherePacking.centers_dist' {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

instance PeriodicSpherePacking.instLatticeDiscrete {d : ℕ} (S : PeriodicSpherePacking d) : DiscreteTopology ↥S.lattice

instance PeriodicSpherePacking.instIsZLattice {d : ℕ} (S : PeriodicSpherePacking d) : IsZLattice ℝ S.lattice

instance SpherePacking.instCentersDiscrete {d : ℕ} (S : SpherePacking d) : DiscreteTopology ↑S.centers

noncomputable instance PeriodicSpherePacking.addAction {d : ℕ} (S : PeriodicSpherePacking d) : AddAction ↥S.lattice ↑S.centers

Equations

• S.addAction = { vadd := fun (x : ↥S.lattice) (y : ↑S.centers) => ⟨↑x + ↑y, ⋯⟩, zero_vadd := ⋯, add_vadd := ⋯ }

def PeriodicSpherePacking.instAddAction {d : ℕ} (S : PeriodicSpherePacking d) : AddAction ↥S.lattice ↑S.centers

Alias of PeriodicSpherePacking.addAction.

Equations

• @PeriodicSpherePacking.instAddAction = @PeriodicSpherePacking.addAction

theorem PeriodicSpherePacking.addAction_vadd {d : ℕ} (S : PeriodicSpherePacking d) {x : ↥S.lattice} {y : ↑S.centers} : x +ᵥ y = ⟨↑x + ↑y, ⋯⟩

@[reducible, inline]

abbrev SpherePacking.balls {d : ℕ} (S : SpherePacking d) : Set (EuclideanSpace ℝ (Fin d))

Equations

• S.balls = ⋃ (x : ↑S.centers), Metric.ball (↑x) (S.separation / 2)

noncomputable def SpherePacking.finiteDensity {d : ℕ} (S : SpherePacking d) (R : ℝ) : ENNReal

Equations

• S.finiteDensity R = MeasureTheory.volume (S.balls ∩ Metric.ball 0 R) / MeasureTheory.volume (Metric.ball 0 R)

noncomputable def SpherePacking.density {d : ℕ} (S : SpherePacking d) : ENNReal

Equations

• S.density = Filter.limsup S.finiteDensity Filter.atTop

theorem PeriodicSpherePacking.basis_Z_span {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) : Submodule.span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ S.lattice b)) = S.lattice

theorem PeriodicSpherePacking.mem_basis_Z_span {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) (v : EuclideanSpace ℝ (Fin d)) : v ∈ Submodule.span ℤ (Set.range ⇑(Basis.ofZLatticeBasis ℝ S.lattice b)) ↔ v ∈ S.lattice

theorem PeriodicSpherePacking.basis_R_span {d : ℕ} (S : PeriodicSpherePacking d) {ι : Type u_1} [Fintype ι] (b : Basis ι ℤ ↥S.lattice) : Submodule.span ℝ (Set.range ⇑(Basis.ofZLatticeBasis ℝ S.lattice b)) = ⊤

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

Equations

• S.scale hc = { centers := c • S.centers, separation := c * S.separation, separation_pos := ⋯, centers_dist := ⋯ }

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

Equations

• S.scale hc = { toSpherePacking := S.scale hc, lattice := c • S.lattice, lattice_action := ⋯, lattice_discrete := ⋯, lattice_isZLattice := ⋯ }

theorem PeriodicSpherePacking.scale_toSpherePacking {d : ℕ} {S : PeriodicSpherePacking d} {c : ℝ} (hc : 0 < c) : (S.scale hc).toSpherePacking = S.scale hc

theorem SpherePacking.scale_balls {d : ℕ} {S : SpherePacking d} {c : ℝ} (hc : 0 < c) : (S.scale hc).balls = c • S.balls

theorem PeriodicSpherePacking.scale_balls {d : ℕ} {S : PeriodicSpherePacking d} {c : ℝ} (hc : 0 < c) : (S.scale hc).balls = c • S.balls

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.

Equations

• PeriodicSpherePackingConstant d = ⨆ (S : PeriodicSpherePacking d), S.density

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.

Equations

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

theorem SpherePacking.finiteDensity_le_one {d : ℕ} (S : SpherePacking d) (R : ℝ) : S.finiteDensity R ≤ 1

theorem SpherePacking.density_le_one {d : ℕ} (S : SpherePacking d) : S.density ≤ 1

@[simp]

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.

@[simp]

theorem SpherePacking.scale_finiteDensity' {d : ℕ} (hd : 0 < d) (S : SpherePacking d) {c : ℝ} (hc : 0 < c) (R : ℝ) : (S.scale hc).finiteDensity R = S.finiteDensity (R / c)

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.

theorem SpherePacking.constant_eq_constant_normalized {d : ℕ} (hd : 0 < d) : SpherePackingConstant d = ⨆ (S : SpherePacking d), ⨆ (_ : S.separation = 1), S.density

theorem biUnion_inter_balls_subset_biUnion_balls_inter {d : ℕ} (X : Set (EuclideanSpace ℝ (Fin d))) (r R : ℝ) : ⋃ x ∈ X ∩ Metric.ball 0 R, Metric.ball x r ⊆ (⋃ x ∈ X, Metric.ball x r) ∩ Metric.ball 0 (R + r)

theorem biUnion_balls_inter_subset_biUnion_inter_balls {d : ℕ} (X : Set (EuclideanSpace ℝ (Fin d))) (r R : ℝ) : (⋃ x ∈ X, Metric.ball x r) ∩ Metric.ball 0 (R - r) ⊆ ⋃ x ∈ X ∩ Metric.ball 0 R, Metric.ball x r

theorem SpherePacking.volume_iUnion_balls_eq_tsum {d : ℕ} (S : SpherePacking d) (R : ℝ) {r' : ℝ} (hr' : r' ≤ S.separation / 2) : MeasureTheory.volume (⋃ (x : ↑(S.centers ∩ Metric.ball 0 R)), Metric.ball (↑x) r') = ∑' (x : ↑(S.centers ∩ Metric.ball 0 R)), MeasureTheory.volume (Metric.ball (↑x) r')

theorem SpherePacking.inter_ball_encard_le {d : ℕ} (S : SpherePacking d) (hd : 0 < d) (R : ℝ) : ↑(S.centers ∩ Metric.ball 0 R).encard ≤ MeasureTheory.volume (S.balls ∩ Metric.ball 0 (R + S.separation / 2)) / MeasureTheory.volume (Metric.ball 0 (S.separation / 2))

This gives an upper bound on the number of points in the sphere packing X with norm less than R.

theorem SpherePacking.inter_ball_encard_ge {d : ℕ} (S : SpherePacking d) (hd : 0 < d) (R : ℝ) : ↑(S.centers ∩ Metric.ball 0 R).encard ≥ MeasureTheory.volume (S.balls ∩ Metric.ball 0 (R - S.separation / 2)) / MeasureTheory.volume (Metric.ball 0 (S.separation / 2))

This gives an upper bound on the number of points in the sphere packing X with norm less than R.

theorem aux6 {d : ℕ} (S : SpherePacking d) (R : ℝ) : Finite ↑(S.centers ∩ Metric.ball 0 R)

theorem SpherePacking.finiteDensity_ge {d : ℕ} (S : SpherePacking d) (hd : 0 < d) (R : ℝ) : S.finiteDensity R ≥ ↑(S.centers ∩ Metric.ball 0 (R - S.separation / 2)).encard * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / MeasureTheory.volume (Metric.ball 0 R)

theorem SpherePacking.finiteDensity_le {d : ℕ} (S : SpherePacking d) (hd : 0 < d) (R : ℝ) : S.finiteDensity R ≤ ↑(S.centers ∩ Metric.ball 0 (R + S.separation / 2)).encard * MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) / MeasureTheory.volume (Metric.ball 0 R)