Documentation

SpherePacking.Basic.E8

Basic properties of the E₈ lattice #

We define the E₈ lattice in two ways, as the ℤ-span of a chosen basis (E8Matrix), and as the set of vectors in ℝ^8 with sum of coordinates an even integer and coordinates either all integers or half-integers (E8_Set). We prove these two definitions are equivalent, and prove various properties about the E₈ lattice.

See also earlier work which inspired this one, by Gareth Ma: https://github.com/thefundamentaltheor3m/Sphere-Packing-Lean/blob/42c839d1002f5bcc1f8d2eb73190d97cd9c52852/SpherePacking/Basic/E8.lean

Main declarations #

Submodule.E8: The E₈ lattice as a submodule of Fin 8 → R for a field R in which 2 is nonzero. We define it to be the set of vectors in Fin 8 → R such that the sum of coordinates is even, and either all coordinates are integers, or all coordinates are half of an odd integer.
Submodule.E8_eq_sup: The E₈ lattice can be seen as the smallest submodule containing both: the even lattice (the lattice of all integer points whose sum of coordinates is even); and the submodule spanned by the vector which is 2⁻¹ in each coordinate.
E8Matrix: An explicit matrix whose rows form a basis for the E₈ lattice over ℤ.
E8Matrix_unimodular: A proof that E8Matrix has determinant 1.
span_E8Matrix_eq_top: The ℝ-span of E8Matrix is the whole of ℝ⁸.
span_E8Matrix: The ℤ-span of E8Matrix is the E₈ lattice. This is the third characterisation of the E₈ lattice given in this file.
E8_integral: The E₈ lattice is integral, i.e., the dot product of any two vectors in E₈ is an integer.
E8_integral_self: The E₈ lattice is even, i.e., the norm-squared of any vector in E₈ is an even integer.
E8Lattice: The E₈ lattice as a submodule of eight-dimensional Euclidean space. This additional definition is valuable, since it now puts the correct metric space structure on the lattice.
E8Packing: The E₈ packing as a periodic sphere packing.
E8Packing_density: The density of the E₈ packing is π ^ 4 / 384.

theorem AddCommGroup.ModEq.zsmul' {α : Type u_2} [AddCommGroup α] {p a b : α} {n : ℤ} (h : a ≡ b [PMOD p]) :

n • a ≡ n • b [PMOD p]

def LinearMap.intCast {ι : Type u_2} (R : Type u_3) [Ring R] :

(ι → ℤ) →ₗ[ℤ ] ι → R

Equations

LinearMap.intCast R = { toFun := fun (f : ι → ℤ) (i : ι) => ↑(f i), map_add' := ⋯, map_smul' := ⋯ }

Instances For

@[simp]

theorem LinearMap.intCast_apply {ι : Type u_2} (R : Type u_3) [Ring R] (f : ι → ℤ) (i : ι) :

(intCast R) f i = ↑(f i)

def Submodule.evenLatticeInt (n : ℕ) :

Submodule ℤ (Fin n → ℤ)

Equations

Submodule.evenLatticeInt n = { carrier := {v : Fin n → ℤ | ∑ i : Fin n, v i ≡ 0 [PMOD 2]}, add_mem' := ⋯, zero_mem' := ⋯, smul_mem' := ⋯ }

Instances For

def Submodule.evenLattice (R : Type u_2) (n : ℕ) [Ring R] :

Submodule ℤ (Fin n → R)

Equations

Submodule.evenLattice R n = Submodule.map (LinearMap.intCast R) (Submodule.evenLatticeInt n)

Instances For

theorem Submodule.coe_evenLattice (R : Type u_2) (n : ℕ) [Ring R] [CharZero R] :

↑(evenLattice R n) = {v : Fin n → R | (∀ (i : Fin n), ∃ (n : ℤ), ↑n = v i) ∧ ∑ i : Fin n, v i ≡ 0 [PMOD 2]}

theorem Submodule.mem_evenLattice {R : Type u_2} [Ring R] [CharZero R] (n : ℕ) {v : Fin n → R} :

v ∈ evenLattice R n ↔ (∀ (i : Fin n), ∃ (n : ℤ), ↑n = v i) ∧ ∑ i : Fin n, v i ≡ 0 [PMOD 2]

noncomputable def Submodule.E8 (R : Type u_2) [Field R] [NeZero 2] :

Submodule ℤ (Fin 8 → R)

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem Submodule.mem_E8 {R : Type u_2} [Field R] [NeZero 2] {v : Fin 8 → R} :

v ∈ E8 R ↔ ((∀ (i : Fin 8), ∃ (n : ℤ), ↑n = v i) ∨ ∀ (i : Fin 8), ∃ (n : ℤ), Odd n ∧ ↑n = 2 • v i) ∧ ∑ i : Fin 8, v i ≡ 0 [PMOD 2]

theorem Submodule.mem_E8' {R : Type u_2} [Field R] [NeZero 2] {v : Fin 8 → R} :

v ∈ E8 R ↔ ((∀ (i : Fin 8), ∃ (n : ℤ), Even n ∧ ↑n = 2 • v i) ∨ ∀ (i : Fin 8), ∃ (n : ℤ), Odd n ∧ ↑n = 2 • v i) ∧ ∑ i : Fin 8, v i ≡ 0 [PMOD 2]

theorem Submodule.mem_E8'' {R : Type u_2} [Field R] [NeZero 2] {v : Fin 8 → R} :

v ∈ E8 R ↔ ((∀ (i : Fin 8), ∃ (n : ℤ), ↑n = v i) ∨ ∀ (i : Fin 8), ∃ (n : ℤ), ↑n + 2⁻¹ = v i) ∧ ∑ i : Fin 8, v i ≡ 0 [PMOD 2]

theorem Submodule.E8_eq_sup (R : Type u_2) [Field R] [CharZero R] :

E8 R = evenLattice R 8 ⊔ span ℤ {fun (x : Fin 8) => 2⁻¹}

def E8Matrix (R : Type u_2) [Field R] :

Matrix (Fin 8) (Fin 8) R

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem E8Matrix_row_mem_E8 {R : Type u_1} [Field R] [CharZero R] (i : Fin 8) :

(E8Matrix R).row i ∈ Submodule.E8 R

theorem E8Matrix_eq_cast (R : Type u_2) [Field R] [CharZero R] :

E8Matrix R = (E8Matrix ℚ).map ⇑(Rat.castHom R)

theorem lowerTriangular_E8Matrix {R : Type u_2} [Field R] :

(E8Matrix R).BlockTriangular ⇑OrderDual.toDual

theorem E8Matrix_unimodular (R : Type u_2) [Field R] [NeZero 2] :

(E8Matrix R).det = 1

theorem linearIndependent_E8Matrix (R : Type u_2) [Field R] [NeZero 2] :

LinearIndependent R (E8Matrix R).row

theorem span_E8Matrix_eq_top (R : Type u_2) [Field R] [NeZero 2] :

Submodule.span R (Set.range (E8Matrix R).row) = ⊤

noncomputable def E8Basis (R : Type u_2) [Field R] [NeZero 2] :

Module.Basis (Fin 8) R (Fin 8 → R)

Equations

E8Basis R = Module.Basis.mk ⋯ ⋯

Instances For

theorem E8Basis_apply {R : Type u_1} [Field R] [NeZero 2] (i : Fin 8) :

(E8Basis R) i = (E8Matrix R).row i

theorem of_basis_eq_matrix {R : Type u_1} [Field R] [CharZero R] :

Matrix.of ⇑(E8Basis R) = E8Matrix R

theorem range_E8Matrix_row_subset (R : Type u_2) [Field R] [CharZero R] :

Set.range (E8Matrix R).row ⊆ ↑(Submodule.E8 R)

theorem span_E8Matrix (R : Type u_2) [Field R] [CharZero R] :

Submodule.span ℤ (Set.range (E8Matrix R).row) = Submodule.E8 R

def E8.inn :

Matrix (Fin 8) (Fin 8) ℤ

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem E8Matrix_mul_E8Matrix_transpose_rat :

E8Matrix ℚ * (E8Matrix ℚ).transpose = E8.inn.map Int.cast

theorem E8Matrix_mul_E8Matrix_transpose {R : Type u_1} [Field R] [CharZero R] :

E8Matrix R * (E8Matrix R).transpose = E8.inn.map Int.cast

theorem dotProduct_eq_inn {R : Type u_2} [Field R] [CharZero R] (i j : Fin 8) :

(E8Matrix R).row i ⬝ᵥ (E8Matrix R).row j = ↑(E8.inn i j)

theorem dotProduct_is_integer {R : Type u_2} [Field R] [CharZero R] (i j : Fin 8) :

∃ (z : ℤ), ↑z = (E8Matrix R).row i ⬝ᵥ (E8Matrix R).row j

theorem E8_integral {R : Type u_2} [Field R] [CharZero R] (v w : Fin 8 → R) (hv : v ∈ Submodule.E8 R) (hw : w ∈ Submodule.E8 R) :

∃ (z : ℤ), ↑z = v ⬝ᵥ w

theorem E8_integral_self {R : Type u_2} [Field R] [CharZero R] (v : Fin 8 → R) (hv : v ∈ Submodule.E8 R) :

∃ (z : ℤ), Even z ∧ ↑z = v ⬝ᵥ v

theorem E8_norm_eq_sqrt_even (v : Fin 8 → ℝ) (hv : v ∈ Submodule.E8 ℝ) :

∃ (n : ℤ), Even n ∧ ↑n = ‖WithLp.toLp 2 v‖ ^ 2

theorem E8_norm_lower_bound (v : Fin 8 → ℝ) (hv : v ∈ Submodule.E8 ℝ) :

v = 0 ∨ √2 ≤ ‖WithLp.toLp 2 v‖

@[reducible, inline]

noncomputable abbrev E8Lattice :

Submodule ℤ (EuclideanSpace ℝ (Fin 8))

Equations

E8Lattice = Submodule.map (WithLp.linearEquiv 2 ℤ (Fin 8 → ℝ)).symm (Submodule.E8 ℝ)

Instances For

instance instDiscreteE8Lattice :

DiscreteTopology ↥E8Lattice

theorem span_E8_eq_top :

Submodule.span ℝ ↑(Submodule.E8 ℝ) = ⊤

theorem span_E8_eq_top' :

Submodule.span ℝ ↑E8Lattice = ⊤

theorem span_E8Matrix_eq_E8Lattice :

Submodule.span ℤ (Set.range fun (i : Fin 8) => (WithLp.linearEquiv 2 ℤ (Fin 8 → ℝ)).symm ((E8Matrix ℝ).row i)) = E8Lattice

instance instIsZLatticeE8Lattice :

IsZLattice ℝ E8Lattice

theorem Submodule.span_restrict {ι : Type u_2} {M : Type u_3} [AddCommMonoid M] [Module ℤ M] (p : Submodule ℤ M) (f : ι → M) (h : ∀ (i : ι), f i ∈ p) :

(span ℤ (Set.range f)).submoduleOf p = span ℤ (Set.range fun (i : ι) => ⟨f i, ⋯⟩)

noncomputable def E8_ℤBasis :

Module.Basis (Fin 8) ℤ ↥E8Lattice

Equations

E8_ℤBasis = Module.Basis.mk E8_ℤBasis._proof_2 E8_ℤBasis._proof_3

Instances For

theorem coe_E8_ℤBasis_apply (i : Fin 8) :

↑(E8_ℤBasis i) = (WithLp.linearEquiv 2 ℤ (Fin 8 → ℝ)).symm ((E8Matrix ℝ).row i)

theorem E8_ℤBasis_ofZLatticeBasis_apply (i : Fin 8) :

(Module.Basis.ofZLatticeBasis ℝ E8Lattice E8_ℤBasis) i = WithLp.toLp 2 ((E8Matrix ℝ).row i)

noncomputable def E8Packing :

PeriodicSpherePacking 8

Equations

One or more equations did not get rendered due to their size.

Instances For

theorem E8Packing_separation :

E8Packing.separation = √2

theorem E8Packing_lattice :

E8Packing.lattice = E8Lattice

theorem E8Packing_numReps :

E8Packing.numReps = 1

theorem E8Basis_apply_norm (i : Fin 8) :

‖WithLp.toLp 2 ((E8Basis ℝ) i)‖ ≤ 2

theorem E8_ℤBasis_apply_norm (i : Fin 8) :

‖E8_ℤBasis i‖ ≤ 2

def Matrix.myDet {n : Type u_2} [DecidableEq n] [Fintype n] {R : Type u_3} [CommRing R] (M : Matrix n n R) :

R

Equations

M.myDet = M.det

Instances For

theorem E8Matrix_myDet_eq_one (R : Type u_2) [Field R] [NeZero 2] :

(E8Matrix R).myDet = 1

theorem ZSpan.volume_fundamentalDomain' {ι : Type u_2} [Fintype ι] [DecidableEq ι] (b : Module.Basis ι ℝ (ι → ℝ)) :

MeasureTheory.volume (fundamentalDomain b) = ENNReal.ofReal |(Matrix.of ⇑b).myDet|

theorem E8Basis_volume :

MeasureTheory.volume (ZSpan.fundamentalDomain (E8Basis ℝ)) = 1

theorem test'' {ι : Type u_2} [Fintype ι] (s : Set (EuclideanSpace ℝ ι)) :

MeasureTheory.volume (⇑(WithLp.equiv 2 ((i : ι) → (fun (x : ι) => ℝ) i)).symm ⁻¹' s) = MeasureTheory.volume s

theorem same_domain :

⇑(WithLp.linearEquiv 2 ℝ ((i : Fin 8) → (fun (x : Fin 8) => ℝ) i)).symm ⁻¹' ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ E8Lattice E8_ℤBasis) = ZSpan.fundamentalDomain (E8Basis ℝ)

theorem E8_Basis_volume :

MeasureTheory.volume (ZSpan.fundamentalDomain (Module.Basis.ofZLatticeBasis ℝ E8Lattice E8_ℤBasis)) = 1

theorem E8Packing_density :

E8Packing.density = ENNReal.ofReal Real.pi ^ 4 / 384