Hermite's inequality for the minimum of a positive definite lattice

Let L be a positive definite integral lattice of rank n. Hermite's inequality bounds its minimum min L, the least norm B(x, x) of a nonzero lattice vector, by its determinant:

min L ≤ (4 / 3) ^ ((n - 1) / 2) · (det L) ^ (1 / n).

It is the specialization to the integral form of L of LinearMap.BilinForm.exists_ne_zero_three_pow_mul_pow_le_four_pow_mul_det, and it is stated twice: once as the inequality of integers 3 ^ (n choose 2) · (min L)ⁿ ≤ 4 ^ (n choose 2) · det L, and once in the root form displayed above. Neither needs a rank hypothesis: in rank zero the minimum is 0, the determinant is 1, and both statements hold trivially.

The constant is sharp in rank 2: the root lattice A₂ has minimum 2 and determinant 3, and 2 = (4 / 3) ^ (1 / 2) · 3 ^ (1 / 2); this is recorded in TauCeti.LinearAlgebra.IntegralLattice.RootLattice.TypeA.Hermite.

Main results

• TauCeti.IntegralLattice.IsPosDef.three_pow_mul_minimum_pow_le: 3 ^ (n choose 2) · (min L)ⁿ ≤ 4 ^ (n choose 2) · det L.
• TauCeti.IntegralLattice.IsPosDef.minimum_le_rpow_mul_determinant_rpow: min L ≤ (4 / 3) ^ ((n - 1) / 2) · (det L) ^ (1 / n).

References

• C. Hermite, Extraits de lettres de M. Ch. Hermite à M. Jacobi sur différents objets de la théorie des nombres, J. Reine Angew. Math. 40 (1850), 261–315.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 1, §1.5.

theorem TauCeti.IntegralLattice.IsPosDef.three_pow_mul_minimum_pow_le {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : 3 ^ (Module.finrank ℤ ↥L.carrier).choose 2 * ↑L.minimum ^ Module.finrank ℤ ↥L.carrier ≤ 4 ^ (Module.finrank ℤ ↥L.carrier).choose 2 * L.determinant

Hermite's inequality for the minimum, without roots. A positive definite integral lattice of rank n satisfies 3 ^ (n choose 2) · (min L)ⁿ ≤ 4 ^ (n choose 2) · det L.

theorem TauCeti.IntegralLattice.IsPosDef.minimum_le_rpow_mul_determinant_rpow {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : ↑L.minimum ≤ (4 / 3) ^ ((↑(Module.finrank ℤ ↥L.carrier) - 1) / 2) * ↑L.determinant ^ (1 / ↑(Module.finrank ℤ ↥L.carrier))

Hermite's inequality for the minimum. A positive definite integral lattice of rank n satisfies min L ≤ (4 / 3) ^ ((n - 1) / 2) · (det L) ^ (1 / n).