Hermite's inequality for positive definite integral forms

Let B be a symmetric positive definite ℤ-valued bilinear form on a free ℤ-module M of rank n ≥ 1, and let det B be its Gram determinant, which does not depend on the basis. Hermite's inequality says that some nonzero vector satisfies

B(x, x) ≤ (4 / 3) ^ ((n - 1) / 2) · (det B) ^ (1 / n).

This file proves it with the powers cleared, as the inequality of integers

3 ^ (n choose 2) · B(x, x) ^ n ≤ 4 ^ (n choose 2) · det B.

The proof is Hermite's induction on the rank. Let v be a nonzero vector of least norm μ = B(v, v). It is primitive, so M = ℤ v ⊕ K with K the kernel of a functional taking the value 1 on v. On K the integral form

S(y, z) = μ · B(y, z) - B(y, v) · B(v, z)

is μ times the form induced on the projection of K orthogonal to v; it is again positive definite (LinearMap.BilinForm.apply_mul_apply_lt_of_mem_ker), and Chiò's condensation for Gram matrices (LinearMap.BilinForm.mul_det_toMatrix_eq_pow_mul_det_toMatrix) gives μ · det S = μⁿ · det B in a basis of M extending v. Writing a vector of M as y + t v and choosing t to be a nearest integer to -B(v, y) / μ, the minimality of μ gives 3 μ² ≤ 4 S(y, y) for every y outside ℤ v, in particular for every nonzero y ∈ K. The inductive hypothesis applied to S then bounds μ.

The forms and the determinant argument stay integral; the nearest-integer step is Int.exists_two_mul_abs_sub_mul_le. The least norm exists because norms of nonzero vectors are positive integers.

Main results

• LinearMap.BilinForm.exists_isPrimitive_forall_apply_self_le: a positive definite integral form attains its minimum at a primitive vector.
• LinearMap.BilinForm.three_mul_sq_le_four_mul_sub_of_forall_le: the minimality step, which bounds the condensed form along a vector of least norm from below.
• LinearMap.BilinForm.exists_ne_zero_three_pow_mul_pow_le_four_pow_mul_det: Hermite's inequality 3 ^ (n choose 2) · B(x, x) ^ n ≤ 4 ^ (n choose 2) · det B for some nonzero x.

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 LinearMap.BilinForm.exists_isPrimitive_forall_apply_self_le {M : Type u_1} [AddCommGroup M] [Module.Free ℤ M] [Nontrivial M] (B : LinearMap.BilinForm ℤ M) (hpos : (BilinMap.toQuadraticMap B).PosDef) : ∃ (v : M), TauCeti.IsPrimitive v ∧ ∀ (x : M), x ≠ 0 → (B v) v ≤ (B x) x

A positive definite integral form attains its minimum at a primitive vector. On a nontrivial free ℤ-module, a bilinear form whose values B(x, x) on nonzero vectors are positive integers has a nonzero vector of least norm, and every such vector is primitive: a proper multiple d • w, d ≥ 2, has norm d² B(w, w) > B(w, w).

theorem LinearMap.BilinForm.three_mul_sq_le_four_mul_sub_of_forall_le {M : Type u_1} [AddCommGroup M] {B : LinearMap.BilinForm ℤ M} (hB : B.IsSymm) {v y : M} (hμ : 0 < (B v) v) (hmin : ∀ (x : M), x ≠ 0 → (B v) v ≤ (B x) x) (hy : y ∉ ℤ ∙ v) : 3 * (B v) v ^ 2 ≤ 4 * ((B v) v * (B y) y - (B y) v * (B v) y)

The minimality step of Hermite's inequality. Let v be a vector of least norm μ = B(v, v) > 0 among the nonzero vectors, for a symmetric integral form B. Every y outside ℤ v satisfies 3 μ² ≤ 4 (μ B(y, y) - B(y, v) B(v, y)). Indeed, adding to y a multiple t v with t nearest to -B(v, y) / μ gives a nonzero vector with 4 B(v, y + t v)² ≤ μ², and completing the square along v (LinearMap.BilinForm.mul_apply_add_smul_add_smul) compares its norm, which is at least μ, with the condensed form.

theorem LinearMap.BilinForm.exists_ne_zero_three_pow_mul_pow_le_four_pow_mul_det {M : Type u_1} [AddCommGroup M] [Nontrivial M] {ι : Type u_2} [Fintype ι] [DecidableEq ι] (B : LinearMap.BilinForm ℤ M) (hB : B.IsSymm) (hpos : (BilinMap.toQuadraticMap B).PosDef) (b : Module.Basis ι ℤ M) : ∃ (x : M), x ≠ 0 ∧ 3 ^ (Fintype.card ι).choose 2 * (B x) x ^ Fintype.card ι ≤ 4 ^ (Fintype.card ι).choose 2 * ((toMatrix b) B).det

Hermite's inequality. A symmetric positive definite integral bilinear form B on a free ℤ-module of rank n ≥ 1 takes on some nonzero vector x a value with 3 ^ (n choose 2) · B(x, x) ^ n ≤ 4 ^ (n choose 2) · det B, where det B is the Gram determinant of B in any basis. Equivalently B(x, x) ≤ (4 / 3) ^ ((n - 1) / 2) · (det B) ^ (1 / n).