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 (E8_Matrix), 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.

Main theorems #

E8_Matrix: a fixed ℤ-basis for the E₈ lattice
E8_is_basis: E8_Matrix forms a ℝ-basis of ℝ⁸
E8_Set: the set of vectors in E₈, characterised by relations of their coordinates
E8_Set_eq_span: the ℤ-span of E8_Matrix coincides with E8_Set
E8_norm_eq_sqrt_even: E₈ is even

TODO #

Prove E₈ is unimodular
Prove E₈ is positive-definite
Documentation and naming

def E8.E8_Set :

Set (EuclideanSpace ℝ (Fin 8))

E₈ is characterised as the set of vectors with (1) coordinates summing to an even integer, and (2) all its coordinates either an integer or a half-integer.

Equations

E8.E8_Set = {v : EuclideanSpace ℝ (Fin 8) | ((∀ (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]}

Instances For

theorem E8.mem_E8_Set {v : EuclideanSpace ℝ (Fin 8)} :

v ∈ E8_Set ↔ ((∀ (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 E8.mem_E8_Set' {v : EuclideanSpace ℝ (Fin 8)} :

v ∈ E8_Set ↔ ((∀ (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]

def E8.E8' :

Matrix (Fin 8) (Fin 8) ℚ

E₈ is also characterised as the ℤ-span of the following vectors.

Equations

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

Instances For

def E8.F8' :

Matrix (Fin 8) (Fin 8) ℚ

F8 is the inverse matrix of E₈, used to assist computation below.

Equations

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

Instances For

@[simp]

theorem E8.E8_mul_F8_eq_id_Q :

E8' * F8' = !![1, 0, 0, 0, 0, 0, 0, 0; 0, 1, 0, 0, 0, 0, 0, 0; 0, 0, 1, 0, 0, 0, 0, 0; 0, 0, 0, 1, 0, 0, 0, 0; 0, 0, 0, 0, 1, 0, 0, 0; 0, 0, 0, 0, 0, 1, 0, 0; 0, 0, 0, 0, 0, 0, 1, 0; 0, 0, 0, 0, 0, 0, 0, 1]

@[simp]

theorem E8.E8_mul_F8_eq_one_Q :

@[simp]

theorem E8.F8_mul_E8_eq_one_Q :

theorem E8.E8'_updateRow₆₇ :

(E8'.updateRow 6 (∑ k : Fin 8, E8.c₆✝ k • E8' k)).updateRow 7 (∑ k : Fin 8, E8.c₇✝ k • E8'.updateRow 6 (∑ k : Fin 8, E8.c₆✝ k • E8' k) k) = !![1, -1, 0, 0, 0, 0, 0, 0; 0, 1, -1, 0, 0, 0, 0, 0; 0, 0, 1, -1, 0, 0, 0, 0; 0, 0, 0, 1, -1, 0, 0, 0; 0, 0, 0, 0, 1, -1, 0, 0; 0, 0, 0, 0, 0, 1, 1, 0; 0, 0, 0, 0, 0, 0, 5 / 2, -1 / 2; 0, 0, 0, 0, 0, 0, 0, -2 / 5]

theorem E8.E8'_det_aux_4 :

!![1, -1, 0, 0, 0, 0, 0, 0; 0, 1, -1, 0, 0, 0, 0, 0; 0, 0, 1, -1, 0, 0, 0, 0; 0, 0, 0, 1, -1, 0, 0, 0; 0, 0, 0, 0, 1, -1, 0, 0; 0, 0, 0, 0, 0, 1, 1, 0; 0, 0, 0, 0, 0, 0, 5 / 2, -1 / 2; 0, 0, 0, 0, 0, 0, 0, -2 / 5].det = -1

theorem E8.E8_det_eq_one :

def E8.E8_Matrix :

Matrix (Fin 8) (Fin 8) ℝ

Equations

E8.E8_Matrix = (algebraMap ℚ ℝ).mapMatrix E8.E8'

Instances For

def E8.F8_Matrix :

Matrix (Fin 8) (Fin 8) ℝ

Equations

E8.F8_Matrix = (algebraMap ℚ ℝ).mapMatrix E8.F8'

Instances For

theorem E8.E8_Matrix_apply {i j : Fin 8} :

E8_Matrix i j = ↑(E8' i j)

theorem E8.E8_Matrix_apply_row {i : Fin 8} :

E8_Matrix i = fun (j : Fin 8) => ↑(E8' i j)

@[simp]

theorem E8.E8_mul_F8_eq_one_R :

E8_Matrix * F8_Matrix = 1

@[simp]

theorem E8.F8_mul_E8_eq_one_R :

F8_Matrix * E8_Matrix = 1

theorem E8.E8_is_basis :

LinearIndependent ℝ E8_Matrix ∧ Submodule.span ℝ (Set.range E8_Matrix) = ⊤

theorem E8.E8_sum_apply_0 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 0 = y 0 • 1 - y 6 • (1 / 2)

theorem E8.E8_sum_apply_1 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 1 = y 0 • -1 + y 1 • 1 - y 6 • (1 / 2)

theorem E8.E8_sum_apply_2 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 2 = y 1 • -1 + y 2 • 1 - y 6 • (1 / 2)

theorem E8.E8_sum_apply_3 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 3 = y 2 • -1 + y 3 • 1 - y 6 • (1 / 2)

theorem E8.E8_sum_apply_4 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 4 = y 3 • -1 + y 4 • 1 - y 6 • (1 / 2)

theorem E8.E8_sum_apply_5 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 5 = y 4 • -1 + y 5 • 1 - y 6 • (1 / 2) + y 7 • 1

theorem E8.E8_sum_apply_6 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 6 = y 5 • 1 - y 6 • (1 / 2) - y 7 • 1

theorem E8.E8_sum_apply_7 {α : Type u_1} [Semiring α] [Module α ℝ] (y : Fin 8 → α) :

(∑ j : Fin 8, y j • E8_Matrix j) 7 = y 6 • (-1 / 2)

def E8.tacticSimp_E8_sum_apply :

Lean.ParserDescr

Equations

E8.tacticSimp_E8_sum_apply = Lean.ParserDescr.node `E8.tacticSimp_E8_sum_apply 1024 (Lean.ParserDescr.nonReservedSymbol "simp_E8_sum_apply" false)

Instances For

theorem E8.E8_Set_eq_span :

E8_Set = ↑(Submodule.span ℤ (Set.range E8_Matrix))

theorem E8.E8_add_mem {a b : EuclideanSpace ℝ (Fin 8)} (ha : a ∈ E8_Set) (hb : b ∈ E8_Set) :

a + b ∈ E8_Set

theorem E8.E8_neg_mem {a : EuclideanSpace ℝ (Fin 8)} (ha : a ∈ E8_Set) :

def E8.E8_AddSubgroup :

AddSubgroup (EuclideanSpace ℝ (Fin 8))

Equations

E8.E8_AddSubgroup = { carrier := E8.E8_Set, add_mem' := ⋯, zero_mem' := E8.E8_AddSubgroup._proof_2, neg_mem' := ⋯ }

Instances For

def E8.E8_Lattice :

Submodule ℤ (EuclideanSpace ℝ (Fin 8))

Equations

E8.E8_Lattice = { carrier := E8.E8_Set, add_mem' := ⋯, zero_mem' := E8.E8_Lattice._proof_1, smul_mem' := E8.E8_Lattice._proof_2 }

Instances For

theorem E8.E8_Matrix_inner {i j : Fin 8} :

inner ℝ (E8_Matrix i) (E8_Matrix j) = ↑(∑ k : Fin 8, E8' i k * E8' j k)

theorem E8.E8_norm_eq_sqrt_even (v : ↥E8_Lattice) :

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

All vectors in E₈ have norm √(2n)

theorem E8.E8_norm_lower_bound (v : ↥E8_Lattice) :

v = 0 ∨ √2 ≤ ‖v‖

instance E8.instDiscreteE8Lattice :

DiscreteTopology ↥E8_Lattice

instance E8.instDiscreteTopologyElemEuclideanSpaceRealFinOfNatNatE8_Set :

DiscreteTopology ↑E8_Set

theorem E8.E8_Set_span_eq_top :

Submodule.span ℝ E8_Set = ⊤

instance E8.instIsZLatticeE8Lattice :

IsZLattice ℝ E8_Lattice

noncomputable def E8.E8Packing :

PeriodicSpherePacking 8

Equations

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

Instances For

theorem E8.E8Packing_numReps :

E8Packing.numReps = 1

theorem E8.E8_Matrix_mem (i : Fin 8) :

E8_Matrix i ∈ E8_Lattice

noncomputable def E8.E8_Basis :

Basis (Fin 8) ℤ ↥E8_Lattice

Equations

E8.E8_Basis = Basis.mk ⋯ E8.E8_Basis._proof_3

Instances For

theorem E8.E8_Basis_apply_norm (i : Fin 8) :

‖E8_Basis i‖ = √2

theorem E8.E8_Basis_volume :

MeasureTheory.volume (ZSpan.fundamentalDomain (Basis.ofZLatticeBasis ℝ E8_Lattice E8_Basis)) = 1

theorem E8.E8Packing_density :

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

theorem E8.Main :

PeriodicSpherePackingConstant 8 = E8Packing.density

theorem E8.Main' :

SpherePackingConstant 8 = E8Packing.density