Minkowski's theorems on the minima of a positive definite lattice

Let L be a positive definite integral lattice of rank n, with successive minima λ₀ ≤ ⋯ ≤ λ_{n-1} measured as norms B(x, x), so that λ₀ = min L. Minkowski's convex body theorem, applied to a realization of L in ℝⁿ, bounds their product by the determinant:

λ₀ ⋯ λ_{n-1} ≤ cₙⁿ · det L,   cₙ = (4 / π) · Γ(n / 2 + 1) ^ (2 / n).

This is Minkowski's second theorem, with the explicit constant cₙ of the convex body theorem for the Euclidean ball; cₙ is an upper bound for the Hermite constant γₙ. Since every λᵢ is at least min L, it contains Minkowski's bound for the minimum (his first theorem),

min L ≤ (4 / π) · Γ(n / 2 + 1) ^ (2 / n) · (det L) ^ (1 / n).

For the proof, let x₀, …, x_{n-1} be independent lattice vectors with B(xᵢ, xᵢ) = λᵢ, let φ : L → ℝⁿ be a realization, and let e₀, …, e_{n-1} be the Gram–Schmidt orthonormalization of φ x₀, …, φ x_{n-1}. If the last nonzero coordinate of φ y in the basis e is the k-th, then y is independent of x₀, …, x_{k-1}, so B(y, y) ≥ λₖ and hence ∑ⱼ ⟪eⱼ, φ y⟫² / λⱼ ≥ 1. The open ellipsoid ∑ⱼ ⟪eⱼ, v⟫² / λⱼ < 1 thus contains no nonzero vector of φ(L), and by the convex body theorem its volume √(λ₀ ⋯ λ_{n-1}) · π^(n/2) / Γ(n/2 + 1) is at most 2ⁿ times the covolume √(det L).

The bounds are stated without real powers, as (∏ᵢ λᵢ) · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L and (min L)ⁿ · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L, and the bound for the minimum also in the root form displayed above. None needs a rank hypothesis: in rank zero the product is empty, the minimum is 0, and all statements hold trivially.

Main results

• TauCeti.IntegralLattice.exists_ne_zero_mem_of_two_pow_mul_sqrt_determinant_lt: the convex body theorem for a realization of a nondegenerate lattice: a symmetric convex set of volume greater than 2ⁿ √(det L) contains a nonzero lattice vector.
• TauCeti.IntegralLattice.IsPosDef.prod_successiveMinimum_mul_pi_pow_le: Minkowski's second theorem, (∏ᵢ λᵢ) · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L.
• TauCeti.IntegralLattice.IsPosDef.minimum_pow_mul_pi_pow_le: (min L)ⁿ · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L.
• TauCeti.IntegralLattice.IsPosDef.minimum_le_mul_determinant_rpow: min L ≤ (4 / π) · Γ(n/2 + 1) ^ (2/n) · (det L) ^ (1/n).

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Chapter III, §2, Chapter VIII, and Chapter X.
• J. H. Conway and N. J. A. Sloane, Sphere Packings, Lattices and Groups, Chapter 1, §1.5.

theorem TauCeti.IntegralLattice.exists_ne_zero_mem_of_two_pow_mul_sqrt_determinant_lt {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [L.IsNondegenerate] {φ : ↥L.carrier →ₗ[ℤ] E} (hφ : ∀ (x y : ↥L.carrier), inner ℝ (φ x) (φ y) = ↑((L.integralForm x) y)) (hspan : Submodule.span ℝ (Set.range ⇑φ) = ⊤) {K : Set E} (hsymm : ∀ v ∈ K, -v ∈ K) (hconv : Convex ℝ K) (hK : ENNReal.ofReal (2 ^ Module.finrank ℝ E * √↑L.determinant) < MeasureTheory.volume K) : ∃ (y : ↥L.carrier), y ≠ 0 ∧ φ y ∈ K

Minkowski's convex body theorem for a realized lattice. Let φ realize a nondegenerate integral lattice L in a real inner product space E of dimension n. A convex set K ⊆ E, symmetric about the origin, of volume greater than 2ⁿ · √(det L) contains φ y for some nonzero y ∈ L.

theorem TauCeti.IntegralLattice.IsPosDef.prod_successiveMinimum_mul_pi_pow_le {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) : (∏ i : Fin (Module.finrank ℤ ↥L.carrier), ↑(L.successiveMinimum i)) * Real.pi ^ Module.finrank ℤ ↥L.carrier ≤ 4 ^ Module.finrank ℤ ↥L.carrier * Real.Gamma (↑(Module.finrank ℤ ↥L.carrier) / 2 + 1) ^ 2 * ↑L.determinant

Minkowski's second theorem. The successive minima λ₀, …, λ_{n-1} of a positive definite integral lattice of rank n satisfy (∏ᵢ λᵢ) · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L, that is, ∏ᵢ λᵢ ≤ cₙⁿ · det L with cₙ = (4 / π) · Γ(n/2 + 1) ^ (2/n) the constant of Minkowski's bound for the minimum.

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

Minkowski's bound for the minimum, without roots. A positive definite integral lattice of rank n satisfies (min L)ⁿ · πⁿ ≤ 4ⁿ · Γ(n/2 + 1)² · det L.

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

Minkowski's bound for the minimum. A positive definite integral lattice of rank n satisfies min L ≤ (4 / π) · Γ(n/2 + 1) ^ (2/n) · (det L) ^ (1/n).