Sphere packing in four dimensions

AbbreviationFour-dimensional Euclidean space#✓fully proved

The ambient space is \(\mathbb{R}^4\), the space of real \(4\)-tuples with the standard Euclidean inner product and the distance it induces.

abbrev Space := EuclideanSpace ℝ (Fin 4)
Sources
  • CE2003, the ambient Euclidean space ℝ⁴.
Used by 16
Used byDensity of a packing at a fixed radius · The density at a fixed radius is at most one · A packing has countably many centers · Density of a packing in a ball · The density in a ball is at most one · Periodic packings · Balls of positive radius in \(\mathbb{R}^4\) have finite volume · Balls of positive radius in \(\mathbb{R}^4\) have nonzero volume · Packed ball · Packings of congruent balls in \(\mathbb{R}^4\) · Region covered by a packing · The region covered by a packing is measurable · Volume of the unit ball in \(\mathbb{R}^4\) · The unit ball in \(\mathbb{R}^4\) has volume \(\pi^2/2\) · The unit ball in \(\mathbb{R}^4\) has finite volume · The unit ball in \(\mathbb{R}^4\) has nonzero volume

AbbreviationPositive radii#✓fully proved

A positive radius is a real number \(R\) with \(R > 0\); the positive radii form the set \(\{R \in \mathbb{R} : R > 0\}\).

abbrev PositiveRadius := {R : ℝ // 0 < R}
Sources
  • CE2003 Appendix A, positive observation radii tending to infinity.
Used by 8
Used byDensity of a packing at a fixed radius · The density at a fixed radius is at most one · Density of a packing in a ball · The density in a ball is at most one · Balls of positive radius in \(\mathbb{R}^4\) have finite volume · Balls of positive radius in \(\mathbb{R}^4\) have nonzero volume · Upper density of a packing · The upper density of a packing is at most one

StructurePackings of congruent balls in \(\mathbb{R}^4\)#✓fully proved

A packing in \(\mathbb{R}^4\) consists of a real radius \(r > 0\) and a set \(C \subseteq \mathbb{R}^4\) of centres such that for any two distinct centres \(c, c' \in C\) the open balls of radius \(r\) about \(c\) and \(c'\) are disjoint.

structure Packing where
  radius : ℝ
  radius_pos : 0 < radius
  centers : Set Space
  interior_disjoint : centers.PairwiseDisjoint (fun c => Metric.ball c radius)
Sources
  • CE2003 introduction, congruent positive-radius balls with disjoint interiors.
Uses 1 · Used by 14
Statement usesFour-dimensional Euclidean space
Used byDensity of a packing at a fixed radius · The density at a fixed radius is at most one · A packing has countably many centers · Density of a packing in a ball · The density in a ball is at most one · Periodic packings · Packed ball · Region covered by a packing · The region covered by a packing is measurable · Statement that periodic packings approach the optimal density in dimension four · Sphere-packing density of \(\mathbb{R}^4\) · The sphere-packing density of \(\mathbb{R}^4\) is at most one · Upper density of a packing · The upper density of a packing is at most one

DefinitionPacked ball#✓fully proved

For a packing \(P\) in \(\mathbb{R}^4\) with radius \(r\) and a point \(c \in \mathbb{R}^4\), the packed ball of \(P\) at \(c\) is the closed ball \(\{x \in \mathbb{R}^4 : \|x - c\| \le r\}\), boundary included.

def packedBall (P : Packing) (c : Space) : Set Space := Metric.closedBall c P.radius
Sources
  • CE2003, the packed closed ball at a center, including its boundary.
Uses 2 · Used by 2
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Four-dimensional Euclidean space
Used byRegion covered by a packing · The region covered by a packing is measurable

DefinitionRegion covered by a packing#✓fully proved

For a packing \(P\) in \(\mathbb{R}^4\) with radius \(r\) and set of centres \(C\), the region covered by \(P\) is the union, over all centres \(c \in C\), of the packed closed balls \(\{x \in \mathbb{R}^4 : \|x - c\| \le r\}\).

def packingRegion (P : Packing) : Set Space := ⋃ c ∈ P.centers, packedBall P c
Sources
  • CE2003 Appendix A, the union P of all packed balls.
Uses 3 · Used by 3
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Four-dimensional Euclidean space · Packed ball
Used byDensity of a packing in a ball · The density in a ball is at most one · The region covered by a packing is measurable

DefinitionDensity of a packing in a ball#✓fully proved

For a packing \(P\) of congruent balls in \(\mathbb{R}^4\), a point \(p \in \mathbb{R}^4\) and a radius \(R > 0\), the density of \(P\) in the open ball \(B(p, R)\) of radius \(R\) about \(p\) is \(\operatorname{vol}(U \cap B(p, R)) / \operatorname{vol}(B(p, R))\), where \(U\) is the union of the closed balls of \(P\) and \(\operatorname{vol}\) is Lebesgue measure; the quotient is taken in \([0, \infty]\).

def finiteRadiusDensity (P : Packing) (p : Space) (R : PositiveRadius) : ENNReal :=
  volume (packingRegion P ∩ Metric.ball p (R : ℝ)) / volume (Metric.ball p (R : ℝ))
Sources
  • CE2003 Appendix A, vol(P ∩ B(p,R)) / vol(B(p,R)).
Uses 4 · Used by 3
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Positive radii · Four-dimensional Euclidean space · Region covered by a packing
Used byDensity of a packing at a fixed radius · The density at a fixed radius is at most one · The density in a ball is at most one

DefinitionDensity of a packing at a fixed radius#✓fully proved

For a packing \(P\) of congruent balls in \(\mathbb{R}^4\) and a radius \(R > 0\), the density of \(P\) at radius \(R\) is the supremum, over all centers \(p \in \mathbb{R}^4\), of the density of \(P\) in the open ball of radius \(R\) about \(p\); it is a value in \([0, \infty]\).

def centeredRadiusDensity (P : Packing) (R : PositiveRadius) : ENNReal :=
  ⨆ p : Space, finiteRadiusDensity P p R
Sources
  • CE2003 Appendix A, supremum over all observation centers at fixed radius.
Uses 4 · Used by 3
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Positive radii · Four-dimensional Euclidean space · Density of a packing in a ball
Used byThe density at a fixed radius is at most one · Upper density of a packing · The upper density of a packing is at most one

DefinitionUpper density of a packing#✓fully proved

For a packing \(P\) of congruent balls in \(\mathbb{R}^4\), let \(U_P\) be the union of the closed balls of the packing, and for \(p \in \mathbb{R}^4\) and \(R > 0\) let \(B(p, R)\) be the open ball of radius \(R\) about \(p\). The upper density of \(P\) is the extended nonnegative real number

\[\limsup_{R \to \infty} \sup_{p \in \mathbb{R}^4} \frac{\operatorname{vol}(U_P \cap B(p, R))}{\operatorname{vol}(B(p, R))},\]

where \(\operatorname{vol}\) is Lebesgue measure and the limit superior is taken as the positive radius \(R\) tends to infinity.

def upperDensity (P : Packing) : ENNReal :=
  Filter.limsup (centeredRadiusDensity P) Filter.atTop
Sources
  • CE2003 Appendix A, limsup as positive radii tend to infinity.
Uses 3 · Used by 4
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Positive radii · Density of a packing at a fixed radius
Used byStatement that periodic packings approach the optimal density in dimension four · Sphere-packing density of \(\mathbb{R}^4\) · The sphere-packing density of \(\mathbb{R}^4\) is at most one · The upper density of a packing is at most one

DefinitionSphere-packing density of \(\mathbb{R}^4\)#✓fully proved

The sphere-packing density \(\Delta_4 \in [0, \infty]\) is the supremum, over all packings \(P\) of congruent balls in \(\mathbb{R}^4\), of the upper density of \(P\). Here the upper density of \(P\) is the limit superior, as the real radius \(R > 0\) tends to infinity, of the supremum over all points \(p \in \mathbb{R}^4\) of the ratio of the volume of the part of the open ball \(B(p, R)\) covered by \(P\) to the volume of \(B(p, R)\).

def spherePackingDensity4 : ENNReal := ⨆ P : Packing, upperDensity P
Sources
  • catalogue C36, supremum over all congruent-ball packings in ℝ⁴.
Uses 2 · Used by 10
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Upper density of a packing
Used byCenter-density upper bounds as packing-density upper bounds · Center density in four dimensions · Statement of the lower bound for sphere packing in dimension four · The trivial lower bound for the four-dimensional packing density · The four-dimensional packing density is nonnegative · Statement that periodic packings approach the optimal density in dimension four · Statement of the Cohn–Elkies upper bound in dimension four · Statement of the Rogers upper bound in dimension four · Statement of the de Laat–Oliveira–Vallentin upper bound in dimension four · Trivial upper bound for the sphere-packing density of \(\mathbb{R}^4\)

DefinitionVolume of the unit ball in \(\mathbb{R}^4\)#✓fully proved

The volume of the unit ball in \(\mathbb{R}^4\) is the Lebesgue measure, as an extended nonnegative real number, of the open ball of radius \(1\) about the origin in four-dimensional Euclidean space \(\mathbb{R}^4\).

def unitBallVolume4 : ENNReal := volume (Metric.ball (0 : Space) 1)
Sources
  • dLOV2014 Section 1.4, volume of a unit ball in ℝ⁴.
Uses 1 · Used by 5
Statement usesFour-dimensional Euclidean space
Used byCenter-density upper bounds as packing-density upper bounds · Center density in four dimensions · The unit ball in \(\mathbb{R}^4\) has volume \(\pi^2/2\) · The unit ball in \(\mathbb{R}^4\) has finite volume · The unit ball in \(\mathbb{R}^4\) has nonzero volume

DefinitionCenter density in four dimensions#✓fully proved

The center density of sphere packings in \(\mathbb{R}^4\) is \(\delta_4 = \Delta_4 / \operatorname{vol}(B)\), where \(\Delta_4\) is the sphere-packing density of \(\mathbb{R}^4\) and \(B\) is the open unit ball of \(\mathbb{R}^4\) centered at the origin; the quotient is taken in \([0, \infty]\).

def centerDensity4 : ENNReal := spherePackingDensity4 / unitBallVolume4
Sources
  • dLOV2014 Section 1.4, δ₄ = Δ₄ / vol(B) for unit spheres.
Uses 2 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\) · Volume of the unit ball in \(\mathbb{R}^4\)
Used byCenter-density upper bounds as packing-density upper bounds

DefinitionPeriodic packings#✓fully proved

A packing \(P\) of congruent balls in \(\mathbb{R}^4\) is periodic if there are a basis \(b_1, b_2, b_3, b_4\) of \(\mathbb{R}^4\) and a finite set \(F \subseteq \mathbb{R}^4\) such that the set of centers of \(P\) equals \(\{c + w : c \in F, w \in \Lambda\}\), where \(\Lambda\) is the set of integer linear combinations of \(b_1, b_2, b_3, b_4\).

def Packing.IsPeriodic (P : Packing) : Prop :=
  ∃ (b : Module.Basis (Fin 4) ℝ Space) (offsets : Finset Space),
    P.centers = ⋃ c ∈ offsets,
      (fun w : Space => c + w) '' (Submodule.span ℤ (Set.range b) : Set Space)
Sources
  • CE2003 introduction, finite union of translates of a full-rank lattice. The lattice is the integer span of a real basis, not an arbitrary periodicity oracle.
Uses 2 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Four-dimensional Euclidean space
Used byStatement that periodic packings approach the optimal density in dimension four

DefinitionTrivial upper bound for the sphere-packing density of \(\mathbb{R}^4\)#✓fully proved

The trivial upper bound is the statement that the sphere-packing density of \(\mathbb{R}^4\) is at most \(1\).

def upperBound_trivial : Prop := spherePackingDensity4 ≤ 1
Sources
  • catalogue C36, trivial upper-bound row.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byThe sphere-packing density of \(\mathbb{R}^4\) is at most one

DefinitionThe trivial lower bound for the four-dimensional packing density#✓fully proved

This is the statement that the sphere-packing density \(\Delta_4\) of \(\mathbb{R}^4\) satisfies \(0 \le \Delta_4\).

def lowerBound_trivial : Prop := 0 ≤ spherePackingDensity4
Sources
  • catalogue C36, trivial nonnegative lower-bound row.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byThe four-dimensional packing density is nonnegative

TheoremA packing has countably many centers#✓fully proved

For every packing of congruent balls in \(\mathbb{R}^4\), the set of centers of its balls is countable.

theorem centers_countable (P : Packing) : P.centers.Countable
Sources
  • packing admission conditions; disjoint nonempty open balls have countably many centers.
Uses 2 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Four-dimensional Euclidean space
Used byThe region covered by a packing is measurable

TheoremThe region covered by a packing is measurable#✓fully proved

For every packing \(P\) in \(\mathbb{R}^4\), the region covered by \(P\), the union of its packed closed balls, is a Borel set; in particular it is Lebesgue measurable.

theorem packingRegion_measurable (P : Packing) : MeasurableSet (packingRegion P)
Sources
  • the covered region is Lebesgue measurable, without an extra packing restriction.
Uses 5
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Four-dimensional Euclidean space · Region covered by a packing
Proof usesA packing has countably many centers · Packed ball

TheoremBalls of positive radius in \(\mathbb{R}^4\) have nonzero volume#✓fully proved

For every point \(p \in \mathbb{R}^4\) and every real \(R > 0\), the open ball of radius \(R\) centred at \(p\) has nonzero Lebesgue measure.

theorem observationVolume_ne_zero (p : Space) (R : PositiveRadius) :
    volume (Metric.ball p (R : ℝ)) ≠ 0
Sources
  • positive observation radii give nonzero volume denominators.
Uses 2 · Used by 1
Statement usesPositive radii · Four-dimensional Euclidean space
Used byThe density in a ball is at most one

TheoremBalls of positive radius in \(\mathbb{R}^4\) have finite volume#✓fully proved

For every point \(p \in \mathbb{R}^4\) and every real \(R > 0\), the open ball of radius \(R\) centred at \(p\) has finite Lebesgue measure.

theorem observationVolume_ne_top (p : Space) (R : PositiveRadius) :
    volume (Metric.ball p (R : ℝ)) ≠ ⊤
Sources
  • every finite-radius observation ball has finite volume.
Uses 2 · Used by 1
Statement usesPositive radii · Four-dimensional Euclidean space
Used byThe density in a ball is at most one

TheoremThe density in a ball is at most one#✓fully proved

For every packing \(P\) of congruent balls in \(\mathbb{R}^4\), every point \(p \in \mathbb{R}^4\) and every radius \(R > 0\), the density of \(P\) in the open ball of radius \(R\) about \(p\) is at most \(1\).

theorem finiteRadiusDensity_le_one (P : Packing) (p : Space) (R : PositiveRadius) :
    finiteRadiusDensity P p R ≤ 1
Sources
  • a covered-volume fraction cannot exceed one.
Uses 7 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Positive radii · Four-dimensional Euclidean space · Density of a packing in a ball
Proof usesBalls of positive radius in \(\mathbb{R}^4\) have finite volume · Balls of positive radius in \(\mathbb{R}^4\) have nonzero volume · Region covered by a packing
Used byThe density at a fixed radius is at most one

TheoremThe density at a fixed radius is at most one#✓fully proved

For every packing \(P\) of congruent balls in \(\mathbb{R}^4\) and every radius \(R > 0\), the density of \(P\) at radius \(R\) (the supremum over all centers \(p \in \mathbb{R}^4\) of the density of \(P\) in the open ball of radius \(R\) about \(p\)) is at most \(1\).

theorem centeredRadiusDensity_le_one (P : Packing) (R : PositiveRadius) :
    centeredRadiusDensity P R ≤ 1
Sources
  • taking the observation-center supremum preserves the bound by one.
Uses 6 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Positive radii · Density of a packing at a fixed radius
Proof usesFour-dimensional Euclidean space · Density of a packing in a ball · The density in a ball is at most one
Used byThe upper density of a packing is at most one

TheoremThe upper density of a packing is at most one#✓fully proved

For every packing \(P\) of congruent balls in \(\mathbb{R}^4\), the upper density of \(P\) is at most \(1\).

theorem upperDensity_le_one (P : Packing) : upperDensity P ≤ 1
Sources
  • taking the radius limsup preserves the bound by one.
Uses 5 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Upper density of a packing
Proof usesPositive radii · Density of a packing at a fixed radius · The density at a fixed radius is at most one
Used byThe sphere-packing density of \(\mathbb{R}^4\) is at most one

TheoremThe sphere-packing density of \(\mathbb{R}^4\) is at most one#✓fully proved

The trivial upper bound holds: the sphere-packing density of \(\mathbb{R}^4\) is at most \(1\).

theorem upperBound_trivial_proved : upperBound_trivial
Sources
  • catalogue C36 trivial upper bound, proved for the actual optimized constant.
Uses 4
Statement usesTrivial upper bound for the sphere-packing density of \(\mathbb{R}^4\)
Proof usesPackings of congruent balls in \(\mathbb{R}^4\) · Upper density of a packing · The upper density of a packing is at most one

TheoremThe four-dimensional packing density is nonnegative#✓fully proved

The trivial lower bound holds: the sphere-packing density \(\Delta_4\) of \(\mathbb{R}^4\) satisfies \(0 \le \Delta_4\).

theorem lowerBound_trivial_proved : lowerBound_trivial
Sources
  • catalogue C36 trivial lower bound, proved in the measure codomain.
Uses 2
Statement usesThe trivial lower bound for the four-dimensional packing density
Proof usesSphere-packing density of \(\mathbb{R}^4\)

TheoremThe unit ball in \(\mathbb{R}^4\) has volume \(\pi^2/2\)#✓fully proved

The Lebesgue measure of the open unit ball centred at the origin of \(\mathbb{R}^4\) equals \(\pi^2/2\).

theorem unitBallVolume4_eq : unitBallVolume4 = ENNReal.ofReal (Real.pi ^ 2 / 2)
Sources
  • the standard four-dimensional unit-ball volume π²/2.
Uses 2 · Used by 1
Statement usesVolume of the unit ball in \(\mathbb{R}^4\)
Proof usesFour-dimensional Euclidean space
Used byCenter-density upper bounds as packing-density upper bounds

TheoremThe unit ball in \(\mathbb{R}^4\) has nonzero volume#✓fully proved

The Lebesgue volume of the open unit ball of radius \(1\) about the origin in \(\mathbb{R}^4\) is not \(0\).

theorem unitBallVolume4_ne_zero : unitBallVolume4 ≠ 0
Sources
  • the center-density divisor is nonzero.
Uses 2 · Used by 1
Statement usesVolume of the unit ball in \(\mathbb{R}^4\)
Proof usesFour-dimensional Euclidean space
Used byCenter-density upper bounds as packing-density upper bounds

TheoremThe unit ball in \(\mathbb{R}^4\) has finite volume#✓fully proved

The Lebesgue volume of the open unit ball of radius \(1\) about the origin in \(\mathbb{R}^4\) is not \(\infty\).

theorem unitBallVolume4_ne_top : unitBallVolume4 ≠ ⊤
Sources
  • the center-density divisor is finite.
Uses 2 · Used by 1
Statement usesVolume of the unit ball in \(\mathbb{R}^4\)
Proof usesFour-dimensional Euclidean space
Used byCenter-density upper bounds as packing-density upper bounds

TheoremCenter-density upper bounds as packing-density upper bounds#✓fully proved

For every real number \(a \ge 0\), the center density \(\delta_4\) of sphere packings in \(\mathbb{R}^4\) is at most \(a\) if and only if the sphere-packing density \(\Delta_4\) of \(\mathbb{R}^4\) is at most \(\pi^2 a / 2\).

theorem centerDensity_upper_iff (a : ℝ) (ha : 0 ≤ a) :
    centerDensity4 ≤ ENNReal.ofReal a ↔
      spherePackingDensity4 ≤ ENNReal.ofReal ((Real.pi ^ 2 / 2) * a)
Sources
  • exact conversion between a nonnegative center-density upper bound and its π²/2-scaled volume-density bound.
Uses 6
Statement usesCenter density in four dimensions · Sphere-packing density of \(\mathbb{R}^4\)
Proof usesVolume of the unit ball in \(\mathbb{R}^4\) · The unit ball in \(\mathbb{R}^4\) has volume \(\pi^2/2\) · The unit ball in \(\mathbb{R}^4\) has finite volume · The unit ball in \(\mathbb{R}^4\) has nonzero volume

DefinitionStatement that periodic packings approach the optimal density in dimension four#✓fully proved

For a packing \(Q\) of congruent balls in \(\mathbb{R}^4\), let its upper density \(\overline{\delta}(Q)\) be the limit superior, as \(R \to \infty\), of the supremum over all points \(p\) of the fraction of the volume of the open ball \(B(p, R)\) covered by the closed balls of \(Q\), and let the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\) be the supremum of \(\overline{\delta}(Q)\) over all such packings \(Q\). This is the proposition that for every real \(\varepsilon > 0\) there is a periodic packing \(P\) of congruent balls in \(\mathbb{R}^4\), meaning that its set of centers is a finite union of translates of the lattice \(\mathbb{Z}b_1 + \mathbb{Z}b_2 + \mathbb{Z}b_3 + \mathbb{Z}b_4\) for some basis \(b_1, \dots, b_4\) of \(\mathbb{R}^4\), such that \(\Delta_4 \le \overline{\delta}(P) + \varepsilon\).

def periodicApproximation : Prop :=
  ∀ ε : ℝ, 0 < ε → ∃ P : Packing,
    P.IsPeriodic ∧ spherePackingDensity4 ≤ upperDensity P + ENNReal.ofReal ε
Sources
  • CE2003 introduction and Appendix A, periodic packings come arbitrarily close to the greatest density. Positive error does not assert attainment.
Uses 4 · Used by 1
Statement usesPackings of congruent balls in \(\mathbb{R}^4\) · Periodic packings · Sphere-packing density of \(\mathbb{R}^4\) · Upper density of a packing
Used byPeriodic packings approach the optimal density in dimension four

DefinitionStatement of the Rogers upper bound in dimension four#✓fully proved

The proposition that the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{13127}{100000}\).

def upperBound_CE2003_Rogers : Prop :=
  spherePackingDensity4 ≤ ENNReal.ofReal ((Real.pi ^ 2 / 2) * ((13127 : ℝ) / 100000))
Sources
  • CE2003 Table 3, Rogers center-density upper bound 0.13127, converted exactly; displayed 0.647791… is only an approximation.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byRogers upper bound for sphere packing in dimension four

DefinitionStatement of the Cohn–Elkies upper bound in dimension four#✓fully proved

The proposition that the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{13126}{100000}\).

def upperBound_CE2003_new : Prop :=
  spherePackingDensity4 ≤ ENNReal.ofReal ((Real.pi ^ 2 / 2) * ((13126 : ℝ) / 100000))
Sources
  • CE2003 Table 3, new center-density upper bound 0.13126, converted exactly; displayed 0.647742… is only an approximation.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byCohn–Elkies upper bound for sphere packing in dimension four

DefinitionStatement of the de Laat–Oliveira–Vallentin upper bound in dimension four#✓fully proved

The proposition that the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{130587}{1000000}\).

def upperBound_dLOV2014 : Prop :=
  spherePackingDensity4 ≤ ENNReal.ofReal ((Real.pi ^ 2 / 2) * ((130587 : ℝ) / 1000000))
Sources
  • dLOV2014 Table 1, center-density upper bound 0.130587, converted exactly; displayed 0.644421… is only an approximation.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byde Laat–Oliveira–Vallentin upper bound for sphere packing in dimension four

DefinitionStatement of the lower bound for sphere packing in dimension four#✓fully proved

The proposition that the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\frac{\pi^2}{16} \le \Delta_4\).

def lowerBound_dLOV2014 : Prop :=
  ENNReal.ofReal (Real.pi ^ 2 / 16) ≤ spherePackingDensity4
Sources
  • dLOV2014 Table 1, center-density lower bound 0.12500 = 1/8, converted exactly to π²/16; 0.616850 is only an approximation.
Uses 1 · Used by 1
Statement usesSphere-packing density of \(\mathbb{R}^4\)
Used byLower bound for sphere packing in dimension four

TheoremRogers upper bound for sphere packing in dimension four#●ready to prove

The sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{13127}{100000}\).

theorem_wanted upperBound_CE2003_Rogers_wanted : upperBound_CE2003_Rogers
Sources
  • CE2003 Table 3. Known literature bound; no Lean proof supplied.
Uses 1
Statement usesStatement of the Rogers upper bound in dimension four

TheoremCohn–Elkies upper bound for sphere packing in dimension four#●ready to prove

The sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{13126}{100000}\).

theorem_wanted upperBound_CE2003_new_wanted : upperBound_CE2003_new
Sources
  • CE2003 Table 3. Known literature bound; no Lean proof supplied.
Uses 1
Statement usesStatement of the Cohn–Elkies upper bound in dimension four

Theoremde Laat–Oliveira–Vallentin upper bound for sphere packing in dimension four#●ready to prove

The sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\Delta_4 \le \frac{\pi^2}{2} \cdot \frac{130587}{1000000}\).

theorem_wanted upperBound_dLOV2014_wanted : upperBound_dLOV2014
Sources
  • dLOV2014 Table 1. Known literature bound; no Lean proof supplied.
Uses 1
Statement usesStatement of the de Laat–Oliveira–Vallentin upper bound in dimension four

TheoremLower bound for sphere packing in dimension four#●ready to prove

The sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\), the supremum of the upper densities of all packings of congruent balls in \(\mathbb{R}^4\), satisfies \(\frac{\pi^2}{16} \le \Delta_4\).

theorem_wanted lowerBound_dLOV2014_wanted : lowerBound_dLOV2014
Sources
  • dLOV2014 Table 1. Known literature bound; no Lean proof supplied.
Uses 1
Statement usesStatement of the lower bound for sphere packing in dimension four

TheoremPeriodic packings approach the optimal density in dimension four#●ready to prove

For a packing \(Q\) of congruent balls in \(\mathbb{R}^4\), let its upper density \(\overline{\delta}(Q)\) be the limit superior, as \(R \to \infty\), of the supremum over all points \(p\) of the fraction of the volume of the open ball \(B(p, R)\) covered by the closed balls of \(Q\), and let the sphere packing density \(\Delta_4\) of \(\mathbb{R}^4\) be the supremum of \(\overline{\delta}(Q)\) over all such packings \(Q\). Then for every real \(\varepsilon > 0\) there is a periodic packing \(P\) of congruent balls in \(\mathbb{R}^4\), meaning that its set of centers is a finite union of translates of the lattice \(\mathbb{Z}b_1 + \mathbb{Z}b_2 + \mathbb{Z}b_3 + \mathbb{Z}b_4\) for some basis \(b_1, \dots, b_4\) of \(\mathbb{R}^4\), such that \(\Delta_4 \le \overline{\delta}(P) + \varepsilon\).

theorem_wanted periodicApproximation_wanted : periodicApproximation
Sources
  • CE2003 introduction and Appendix A. Known periodic approximation; no Lean proof supplied and no exact optimum-attainment claim.
Uses 1
Statement usesStatement that periodic packings approach the optimal density in dimension four
32 fully proved5 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.