The root lattice A₂ attains equality in Hermite's inequality

Hermite's inequality min L ≤ (4 / 3) ^ ((n - 1) / 2) · (det L) ^ (1 / n) (TauCeti.IntegralLattice.IsPosDef.minimum_le_rpow_mul_determinant_rpow) is sharp in rank 2: the root lattice A₂ has minimum 2 and determinant 3, and 2 = (4 / 3) ^ (1 / 2) · 3 ^ (1 / 2).

Main results

• TauCeti.IntegralLattice.minimum_typeARootLattice_two_eq_rpow_mul_determinant_rpow: A₂ attains equality in Hermite's inequality.

References

• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 1, §1.5.

theorem TauCeti.IntegralLattice.minimum_typeARootLattice_two_eq_rpow_mul_determinant_rpow : ↑(typeARootLattice 2).minimum = (4 / 3) ^ ((↑(Module.finrank ℤ ↥(typeARootLattice 2).carrier) - 1) / 2) * ↑(typeARootLattice 2).determinant ^ (1 / ↑(Module.finrank ℤ ↥(typeARootLattice 2).carrier))

A₂ attains equality in Hermite's inequality. The root lattice of type A₂ has rank 2, minimum 2 and determinant 3, and 2 = (4 / 3) ^ (1 / 2) · 3 ^ (1 / 2).