Sphere Packing in R^8

3. Density of Packings🔗

Lemma3.1
AL∃∀Nused by 0

Finite density is squeezed between center counts in slightly smaller/larger balls.

Code for Lemma3.1●2 definitions, 2 incomplete
  • axiom 
    SpherePacking.finiteDensity_le : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    SpherePacking.finiteDensity_le : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    SpherePacking.finiteDensity_ge : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    SpherePacking.finiteDensity_ge : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Compare unions of radius-r/2 balls and use disjointness.

Lemma3.2
Group: Volume-count asymptotics for lattice and periodic center sets. (2)
Hover another entry in this group to preview it.
Preview
Lemma 3.3
Blueprint label
  • «lemma:periodic-points-bounds»
Group
  • Volume-count asymptotics for lattice and periodic center sets.
AL∃∀Nused by 0

The number of lattice points in a radius-R ball is controlled by ball-volume over fundamental-domain volume.

Code for Lemma3.2●2 definitions, 2 incomplete
  • axiom 
    PeriodicSpherePacking.aux2_ge' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    PeriodicSpherePacking.aux2_ge' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    PeriodicSpherePacking.aux2_le' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    PeriodicSpherePacking.aux2_le' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Use the lattice tiling by translates of a bounded fundamental domain.

Lemma3.3
Group: Volume-count asymptotics for lattice and periodic center sets. (2)
Hover another entry in this group to preview it.
Preview
Lemma 3.2
Blueprint label
  • «lemma:lattice-points-bound»
Group
  • Volume-count asymptotics for lattice and periodic center sets.
AL∃∀Nused by 0

Center counts for periodic sets are controlled by lattice counts times the quotient cardinality.

Code for Lemma3.3●2 definitions, 2 incomplete
  • axiom 
    PeriodicSpherePacking.aux_ge : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    PeriodicSpherePacking.aux_ge : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
  • axiom 
    PeriodicSpherePacking.aux_le : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    PeriodicSpherePacking.aux_le : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Intersect the fundamental-domain tilings with the periodic center set.

Lemma3.4
Group: Volume-count asymptotics for lattice and periodic center sets. (2)
Hover another entry in this group to preview it.
Preview
Lemma 3.2
Blueprint label
  • «lemma:lattice-points-bound»
Group
  • Volume-count asymptotics for lattice and periodic center sets.
AL∃∀Nused by 1

For fixed C > 0, we have \mathrm{Vol}(B_d(R)) / \mathrm{Vol}(B_d(R + C)) \to 1 as R \to \infty.

Code for Lemma3.4●1 definition, incomplete
  • axiom 
    volume_ball_ratio_tendsto_nhds_one'' : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    volume_ball_ratio_tendsto_nhds_one'' :
  PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Expand ball volumes and simplify to a rational power limit.

Theorem3.5
AL∃∀Nused by 1

For periodic packing centers X with lattice \Lambda and separation r, \Delta_{\mathcal{P}} = |X / \Lambda| \cdot \mathrm{Vol}(B_d(r/2)) / \mathrm{Vol}(\mathbb{R}^d / \Lambda).

Code for Theorem3.5●1 definition, incomplete
  • axiom 
    PeriodicSpherePacking.density_eq : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`. 
    PeriodicSpherePacking.density_eq : PropThe universe of propositions. `Prop ≡ Sort 0`.

Every proposition is propositionally equal to either `True` or `False`.
    axiom-like (no body)
Proof

Combine the counting bounds and apply the sandwich theorem with Lemma 3.4.