The Cohn–Elkies exponent and sign uncertainty

2.1. Periodic packings🔗

Definition2.1.1
uses 1
Used by 4
Reverse dependency previews
Preview
Definition 2.1.2
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

A sphere packing with set of centers X and separation s (Definition 1.1.1) is periodic if X is invariant under translation by a lattice \Lambda \subseteq \mathbb{R}^d, that is, a discrete subgroup of rank d: \Lambda + X \subseteq X.

Lean code for Definition2.1.1●1 definition
  • structure(extends 1, 8 fields)defined in CohnElkies/SpherePacking/Basic.lean
    complete
    structure PeriodicSpherePacking (d : ℕ) : Type
    structure PeriodicSpherePacking (d : ℕ) : Type
    A periodic sphere packing: a sphere packing whose set of centers is invariant under
translation by a full-rank lattice.

    Extends

    • SpherePacking d

    Fields

    centers : Set (EuclideanSpace ℝ (Fin d))
    Inherited from
    1. SpherePacking
    separation : ℝ
    Inherited from
    1. SpherePacking
    separation_pos : 0 < self.separation
    Inherited from
    1. SpherePacking
    centers_dist : Pairwise fun x1 x2 ↦ self.separation ≤ dist x1 x2
    Inherited from
    1. SpherePacking
    lattice : Submodule ℤ (EuclideanSpace ℝ (Fin d))
    The lattice of periods. 
    lattice_action : ∀ ⦃x y : EuclideanSpace ℝ (Fin d)⦄, x ∈ self.lattice → y ∈ self.centers → x + y ∈ self.centers
    The set of centers is invariant under translation by the lattice. 
    lattice_discrete : DiscreteTopology ↥self.lattice
    The lattice is discrete. 
    lattice_isZLattice : IsZLattice ℝ self.lattice
    The lattice has full rank.
Definition2.1.2
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 2.1.7
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The periodic packing constant is the supremum of the upper densities of all periodic packings (Definition 2.1.1).

Lean code for Definition2.1.2●1 definition
  • defdefined in CohnElkies/SpherePacking/Basic.lean
    complete
    def PeriodicSpherePackingConstant (d : ℕ) : ENNReal
    def PeriodicSpherePackingConstant (d : ℕ) :
  ENNReal
    The periodic packing constant of `ℝ ^ d`: the supremum of the densities of all periodic
sphere packings.
Definition2.1.3
uses 1
Used by 2
Reverse dependency previews
Preview
Lemma 2.1.4
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a periodic packing (Definition 2.1.1) the number N of \Lambda-orbits of centers.

Lean code for Definition2.1.3●1 definition
  • defdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    def PeriodicSpherePacking.centerOrbitCardinality {d : ℕ}
  (S : PeriodicSpherePacking d) : ℕ
    def PeriodicSpherePacking.centerOrbitCardinality
  {d : ℕ} (S : PeriodicSpherePacking d) :
  ℕ
    The number of orbits of the lattice of `S` acting on the centers of `S`.
Lemma2.1.4
uses 1used by 1✓L∃∀N

For a periodic packing the \Lambda-orbits of centers are finite in number, and their number N (Definition 2.1.3) equals the number of centers in any bounded region D whose \Lambda-translates tile \mathbb{R}^d.

Lean code for Lemma2.1.4●2 theorems
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem PeriodicSpherePacking.finiteCenterTranslationQuotient {d : ℕ}
  (S : PeriodicSpherePacking d) :
  Finite (Quotient (AddAction.orbitRel ↥S.lattice ↑S.centers))
    theorem PeriodicSpherePacking.finiteCenterTranslationQuotient
  {d : ℕ} (S : PeriodicSpherePacking d) :
  Finite
    (Quotient
      (AddAction.orbitRel ↥S.lattice
        ↑S.centers))
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem PeriodicSpherePacking.encard_centers_in_fundamental_region {d : ℕ}
  (S : PeriodicSpherePacking d) (D : Set (EuclideanSpace ℝ (Fin d)))
  (hD_isBounded : Bornology.IsBounded D)
  (hD_unique_covers :
    ∀ (x : EuclideanSpace ℝ (Fin d)), ∃! g, g +ᵥ x ∈ D)
  (hd : 0 < d) : (S.centers ∩ D).encard = ↑S.centerOrbitCardinality
    theorem PeriodicSpherePacking.encard_centers_in_fundamental_region
  {d : ℕ} (S : PeriodicSpherePacking d)
  (D : Set (EuclideanSpace ℝ (Fin d)))
  (hD_isBounded : Bornology.IsBounded D)
  (hD_unique_covers :
    ∀ (x : EuclideanSpace ℝ (Fin d)),
      ∃! g, g +ᵥ x ∈ D)
  (hd : 0 < d) :
  (S.centers ∩ D).encard =
    ↑S.centerOrbitCardinality
Proof for Lemma 2.1.4
uses 0

Each orbit meets D exactly once, and D is bounded while the centers are 1-separated, so X \cap D is finite.

Definition2.1.5
uses 0
Used by 3
Reverse dependency previews
Preview
Lemma 2.1.6
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

For a lattice \Lambda \subseteq \mathbb{R}^d write \operatorname{covol}(\Lambda) for the volume of a fundamental domain of \Lambda (Mathlib's ZLattice.covolume) and \Lambda^* = \{ y \in \mathbb{R}^d : \langle x, y\rangle \in \mathbb{Z} \text{ for all } x \in \Lambda\} for the polar lattice.

Lean code for Definition2.1.5●1 definition
  • abbrevdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean
    complete
    abbrev SchwartzMap.polarIntegerLattice {d : ℕ}
  (L : Submodule ℤ (EuclideanSpace ℝ (Fin d))) :
  Submodule ℤ (EuclideanSpace ℝ (Fin d))
    abbrev SchwartzMap.polarIntegerLattice {d : ℕ}
  (L :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d))) :
  Submodule ℤ (EuclideanSpace ℝ (Fin d))
    The polar (dual) lattice `{y | ∀ x ∈ L, ⟪x, y⟫ ∈ ℤ}` of a lattice `L ⊆ ℝ^d`.
Lemma2.1.6
uses 1used by 1✓L∃∀N

The standard lattice \mathbb{Z}^d is its own polar lattice (Definition 2.1.5), and if A is the linear automorphism of \mathbb{R}^d sending the standard basis to a \mathbb{Z}-basis of \Lambda, then A\mathbb{Z}^d = \Lambda, |\det A| = \operatorname{covol}(\Lambda) and (A^{-1})^{*}\mathbb{Z}^d = \Lambda^*, where (A^{-1})^* is the adjoint of A^{-1}; moreover \langle A^{-1}v, n\rangle = \langle v, (A^{-1})^*n\rangle.

Lean code for Lemma2.1.6●4 declarations
  • defdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean
    complete
    def SchwartzMap.latticeCoordinateEquiv {d : ℕ}
  (L : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥L]
  [IsZLattice ℝ L] :
  EuclideanSpace ℝ (Fin d) ≃ₗ[ℝ] EuclideanSpace ℝ (Fin d)
    def SchwartzMap.latticeCoordinateEquiv {d : ℕ}
  (L :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d)))
  [DiscreteTopology ↥L] [IsZLattice ℝ L] :
  EuclideanSpace ℝ (Fin d) ≃ₗ[ℝ]
    EuclideanSpace ℝ (Fin d)
    The linear automorphism of `ℝ^d` sending the standard basis to a basis of `L`; it maps the
standard lattice `ℤ^d` onto `L`.
  • theoremdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean
    complete
    theorem SchwartzMap.lattice_covolume_eq_coordinate_determinant {d : ℕ}
  (L : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥L]
  [IsZLattice ℝ L] :
  ZLattice.covolume L MeasureTheory.volume =
    |LinearMap.det ↑(SchwartzMap.latticeCoordinateEquiv L)|
    theorem SchwartzMap.lattice_covolume_eq_coordinate_determinant
  {d : ℕ}
  (L :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d)))
  [DiscreteTopology ↥L] [IsZLattice ℝ L] :
  ZLattice.covolume L
      MeasureTheory.volume =
    |LinearMap.det
        ↑(SchwartzMap.latticeCoordinateEquiv
            L)|
    The covolume of `L` is the absolute value of the determinant of `latticeCoordinateEquiv L`.
  • defdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean
    complete
    def SchwartzMap.integerVectorPolarEquiv {d : ℕ}
  (L : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥L]
  [IsZLattice ℝ L] : (Fin d → ℤ) ≃ ↥(SchwartzMap.polarIntegerLattice L)
    def SchwartzMap.integerVectorPolarEquiv
  {d : ℕ}
  (L :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d)))
  [DiscreteTopology ↥L] [IsZLattice ℝ L] :
  (Fin d → ℤ) ≃
    ↥(SchwartzMap.polarIntegerLattice L)
    Integer vectors parametrise the polar lattice of `L`.
  • theoremdefined in CohnElkiesForMathlib/Analysis/Fourier/PoissonSummation.lean
    complete
    theorem SchwartzMap.wInner_latticeCoordinateEquiv_symm {d : ℕ}
  (L : Submodule ℤ (EuclideanSpace ℝ (Fin d))) [DiscreteTopology ↥L]
  [IsZLattice ℝ L] (v w : EuclideanSpace ℝ (Fin d)) :
  ⟪((SchwartzMap.latticeCoordinateEquiv L).symm v).ofLp, w.ofLp⟫_[ℝ] =
    ⟪v.ofLp, ((SchwartzMap.dualCoordinateTransport L) w).ofLp⟫_[ℝ]
    theorem SchwartzMap.wInner_latticeCoordinateEquiv_symm
  {d : ℕ}
  (L :
    Submodule ℤ
      (EuclideanSpace ℝ (Fin d)))
  [DiscreteTopology ↥L] [IsZLattice ℝ L]
  (v w : EuclideanSpace ℝ (Fin d)) :
  ⟪((SchwartzMap.latticeCoordinateEquiv
              L).symm
          v).ofLp,
      w.ofLp⟫_[ℝ] =
    ⟪v.ofLp,
      ((SchwartzMap.dualCoordinateTransport
            L)
          w).ofLp⟫_[ℝ]
Proof for Lemma 2.1.6
uses 0

\langle Am, y\rangle = \langle m, A^*y\rangle, so y \in \Lambda^* iff A^*y \in \mathbb{Z}^d, i.e. y \in (A^*)^{-1}\mathbb{Z}^d = (A^{-1})^*\mathbb{Z}^d; the covolume of A\mathbb{Z}^d is |\det A| (Mathlib's ZLattice.covolume_eq_measure_fundamentalDomain).

Lemma2.1.7
Statement uses 2
Statement dependency previews
Preview
Definition 1.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.4.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

The constant \Delta_d of Definition 1.1.1 is the supremum of the upper densities of the sphere packings of separation exactly 1; likewise the periodic packing constant of Definition 2.1.2 is the supremum over periodic packings of separation 1.

Lean code for Lemma2.1.7●2 theorems
  • theoremdefined in CohnElkies/SpherePacking/Basic.lean
    complete
    theorem SpherePacking.packing_supremum_eq_unit_separation {d : ℕ} :
  SpherePackingConstant d =
    ⨆ S, ⨆ (_ : S.separation = 1), S.upperPackingDensity
    theorem SpherePacking.packing_supremum_eq_unit_separation
  {d : ℕ} :
  SpherePackingConstant d =
    ⨆ S,
      ⨆ (_ : S.separation = 1),
        S.upperPackingDensity
    Rescaling reduces the packing constant to packings of separation `1`.
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem periodic_packing_supremum_eq_unit_separation {d : ℕ} :
  PeriodicSpherePackingConstant d =
    ⨆ S, ⨆ (_ : S.separation = 1), S.upperPackingDensity
    theorem periodic_packing_supremum_eq_unit_separation
  {d : ℕ} :
  PeriodicSpherePackingConstant d =
    ⨆ S,
      ⨆ (_ : S.separation = 1),
        S.upperPackingDensity
    Rescaling reduces the periodic packing constant to packings of separation `1`.
Proof for Lemma 2.1.7
uses 0

For c > 0 the rescaled packing cX (SpherePacking.rescaleConfiguration) has separation cs and its balls are the images of the original balls under x \mapsto cx. Hence the proportion of B(0,r) covered by cX equals the proportion of B(0,r/c) covered by X (SpherePacking.rescale_densityInsideRadius), and the limit superior as r \to \infty is the same for both (SpherePacking.rescale_upper_packing_density). Taking c = 1/s normalizes the separation to 1 without changing the upper density; for a periodic packing the lattice is rescaled as well (PeriodicSpherePacking.rescaleConfiguration).

Lemma2.1.8
Statement uses 3
Statement dependency previews
Preview
Definition 2.1.1
Loading preview
Statement dependency preview content is loaded from the rendered-fragment cache.
Used by 2
Reverse dependency previews
Preview
Theorem 2.3.1
Loading preview
Reverse dependency preview content is loaded from the rendered-fragment cache.
✓L∃∀N

Let P be a periodic packing (Definition 2.1.1) with lattice \Lambda, separation s and N orbits of centers (Definition 2.1.3), and let F be the fundamental domain of a \mathbb{Z}-basis of \Lambda (a bounded half-open parallelotope). Then the upper density of P is a limit, namely \dfrac{N\operatorname{vol}(B(0,s/2))}{\operatorname{vol}(F)} = \dfrac{N\operatorname{vol}(B(0,s/2))}{\operatorname{covol}(\Lambda)}, with the covolume of Definition 2.1.5; a periodic packing without centers has density 0.

Lean code for Lemma2.1.8●3 theorems
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem PeriodicSpherePacking.upperPackingDensity_eq_div_volume_fundamentalDomain.{u_1}
  {d : ℕ} {S : PeriodicSpherePacking d} {ι : Type u_1} [Finite ι]
  (b : Module.Basis ι ℤ ↥S.lattice) {L : ℝ}
  (hL :
    ∀
      x ∈
        ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ S.lattice b),
      ‖x‖ ≤ L)
  (hd : 0 < d) :
  S.upperPackingDensity =
    ↑S.centerOrbitCardinality *
        MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) /
      MeasureTheory.volume
        (ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ S.lattice b))
    theorem PeriodicSpherePacking.upperPackingDensity_eq_div_volume_fundamentalDomain.{u_1}
  {d : ℕ} {S : PeriodicSpherePacking d}
  {ι : Type u_1} [Finite ι]
  (b : Module.Basis ι ℤ ↥S.lattice)
  {L : ℝ}
  (hL :
    ∀
      x ∈
        ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ
            S.lattice b),
      ‖x‖ ≤ L)
  (hd : 0 < d) :
  S.upperPackingDensity =
    ↑S.centerOrbitCardinality *
        MeasureTheory.volume
          (Metric.ball 0
            (S.separation / 2)) /
      MeasureTheory.volume
        (ZSpan.fundamentalDomain
          (Module.Basis.ofZLatticeBasis ℝ
            S.lattice b))
    The density of a periodic packing equals the number of centers in a fundamental domain times
the volume of a ball of radius `separation / 2`, divided by the covolume of the lattice.
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem PeriodicSpherePacking.density_eq_numReps_mul_volume_ball_div_covolume
  {d : ℕ} (S : PeriodicSpherePacking d) (hd : 0 < d) :
  S.upperPackingDensity =
    ↑↑S.centerOrbitCardinality *
        MeasureTheory.volume (Metric.ball 0 (S.separation / 2)) /
      ↑(ZLattice.covolume S.lattice MeasureTheory.volume).toNNReal
    theorem PeriodicSpherePacking.density_eq_numReps_mul_volume_ball_div_covolume
  {d : ℕ} (S : PeriodicSpherePacking d)
  (hd : 0 < d) :
  S.upperPackingDensity =
    ↑↑S.centerOrbitCardinality *
        MeasureTheory.volume
          (Metric.ball 0
            (S.separation / 2)) /
      ↑(ZLattice.covolume S.lattice
            MeasureTheory.volume).toNNReal
  • theoremdefined in CohnElkies/SpherePacking/Periodic.lean
    complete
    theorem PeriodicSpherePacking.packing_density_zero_of_empty_centers {d : ℕ}
  (S : PeriodicSpherePacking d) (hd : 0 < d)
  [instEmpty : IsEmpty ↑S.centers] : S.upperPackingDensity = 0
    theorem PeriodicSpherePacking.packing_density_zero_of_empty_centers
  {d : ℕ} (S : PeriodicSpherePacking d)
  (hd : 0 < d)
  [instEmpty : IsEmpty ↑S.centers] :
  S.upperPackingDensity = 0
    A periodic packing without centers has density zero.
Proof for Lemma 2.1.8
uses 1

Let L bound the norm of the points of F. The translates F + \lambda, \lambda \in \Lambda, tile \mathbb{R}^d (PeriodicSpherePacking.exists_unique_vadd_mem_fundamentalDomain), each containing exactly N centers (Lemma 2.1.4, PeriodicSpherePacking.encard_centers_in_translated_region). Counting the translates that meet B(0,R) gives N\,|\Lambda \cap B(0,R-L)| \le |X \cap B(0,R)| \le N\,|\Lambda \cap B(0,R+L)| (PeriodicSpherePacking.nsmul_encard_lattice_le_encard_centers and PeriodicSpherePacking.encard_centers_le_nsmul_encard_lattice), while comparing the union of the translates F + \lambda with balls gives \operatorname{vol}(B(0,R-L))/\operatorname{vol}(F) \le |\Lambda \cap B(0,R)| \le \operatorname{vol}(B(0,R+L))/\operatorname{vol}(F) (PeriodicSpherePacking.volume_div_le_encard_lattice and PeriodicSpherePacking.encard_lattice_le_volume_div). Since the balls of radius s/2 around the centers are disjoint, the covered proportion of B(0,R) is sandwiched between N\operatorname{vol}(B(0,s/2))/\operatorname{vol}(F) times the ratios \operatorname{vol}(B(0,R \mp s/2 \mp 2L))/\operatorname{vol}(B(0,R)) (densityInsideRadius_le_mul_ratio, densityInsideRadius_ge_mul_ratio), and these ratios tend to 1 (volume_ball_add_div_volume_ball_add_tendsto_one). Hence the covered proportion converges (PeriodicSpherePacking.tendsto_densityInsideRadius) and its limit superior is the stated value. The identification of \operatorname{vol}(F) with \operatorname{covol}(\Lambda) is Mathlib's ZLattice.covolume_eq_measure_fundamentalDomain.