Successive minima of integral lattices

The successive minima are squared norms, rather than lengths. With indices starting at zero, L.successiveMinimum i is the least natural bound containing i + 1 linearly independent lattice vectors. Indices lie in Fin (Module.finrank ℤ L), so there are no successive minima in rank zero. Linear independence is over ℤ, equivalently over ℚ after embedding in the ambient rational space.

The construction is defined for every integral lattice. For positive semidefinite lattices each successive minimum is represented by a nonzero vector, the first is the ordinary minimum, and an independent family attains all values simultaneously. The sequence is nondecreasing. For positive definite lattices the values are positive. The characterization by independent bounded vectors is intended for estimates and reduction theory; it does not assert that those vectors form an integral basis. A vector independent of i vectors whose norms are bounded by the first i successive minima has norm at least the next one; this is the lattice-theoretic input to Minkowski's second theorem.

References

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

noncomputable def TauCeti.IntegralLattice.successiveMinimum {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) : ℕ

The (i + 1)-st successive minimum, measured as an integral squared norm. It is the least natural bound containing i + 1 independent lattice vectors.

theorem TauCeti.IntegralLattice.successiveMinimum_def {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) : L.successiveMinimum i = sInf {c : ℕ | ∃ (x : Fin (↑i + 1) → ↥L.carrier), LinearIndependent ℤ x ∧ ∀ (j : Fin (↑i + 1)), L.integralNorm (x j) ≤ ↑c}

The defining infimum of the successive minimum.

theorem TauCeti.IntegralLattice.exists_linearIndependent_integralNorm_le_successiveMinimum {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) : ∃ (x : Fin (↑i + 1) → ↥L.carrier), LinearIndependent ℤ x ∧ ∀ (j : Fin (↑i + 1)), L.integralNorm (x j) ≤ ↑(L.successiveMinimum i)

Each successive minimum contains the required number of independent bounded vectors.

theorem TauCeti.IntegralLattice.successiveMinimum_le_of_linearIndependent {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) {c : ℕ} {x : Fin (↑i + 1) → ↥L.carrier} (hx : LinearIndependent ℤ x) (hc : ∀ (j : Fin (↑i + 1)), L.integralNorm (x j) ≤ ↑c) : L.successiveMinimum i ≤ c

A successive minimum is at most any bound containing enough independent vectors.

theorem TauCeti.IntegralLattice.successiveMinimum_le_iff {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) (c : ℕ) : L.successiveMinimum i ≤ c ↔ ∃ (x : Fin (↑i + 1) → ↥L.carrier), LinearIndependent ℤ x ∧ ∀ (j : Fin (↑i + 1)), L.integralNorm (x j) ≤ ↑c

A natural bound reaches the successive minimum exactly when it contains enough independent lattice vectors.

theorem TauCeti.IntegralLattice.monotone_successiveMinimum {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) : Monotone L.successiveMinimum

Successive minima form a nondecreasing sequence.

@[simp]

theorem TauCeti.IntegralLattice.IsPosSemidef.successiveMinimum_zero {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) (h : 0 < Module.finrank ℤ ↥L.carrier) : L.successiveMinimum ⟨0, h⟩ = L.minimum

The first successive minimum of a positive semidefinite lattice is its ordinary minimum.

theorem TauCeti.IntegralLattice.exists_integralNorm_le_successiveMinimum_not_mem_span {V : Type u} [AddCommGroup V] [Module ℚ V] (L : IntegralLattice V) (i : Fin (Module.finrank ℤ ↥L.carrier)) (x : Fin ↑i → ↥L.carrier) : ∃ (y : ↥L.carrier), L.integralNorm y ≤ ↑(L.successiveMinimum i) ∧ ↑y ∉ Submodule.span ℚ (Set.range fun (j : Fin ↑i) => ↑(x j))

At the next successive minimum there is a bounded vector outside the rational span of any family of fewer vectors.

theorem TauCeti.IntegralLattice.IsPosSemidef.successiveMinimum_le_integralNorm_of_linearIndependent {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) (i : Fin (Module.finrank ℤ ↥L.carrier)) {x : Fin ↑i → ↥L.carrier} (hx : ∀ (j : Fin ↑i), L.integralNorm (x j) ≤ ↑(L.successiveMinimum (Fin.castLE ⋯ j))) {z : ↥L.carrier} (hz : LinearIndependent ℤ (Fin.snoc x z)) : ↑(L.successiveMinimum i) ≤ L.integralNorm z

In a positive semidefinite lattice, let x₀, …, x_{i-1} be lattice vectors of norms at most the corresponding successive minima. Every vector z for which x₀, …, x_{i-1}, z are linearly independent has norm at least the next successive minimum λᵢ. For a family attaining the successive minima, this bounds below every vector outside the span of its first i members.

theorem TauCeti.IntegralLattice.IsPosSemidef.exists_linearIndependent_fin_integralNorm_eq_successiveMinimum_of_le {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) (m : ℕ) (hm : m ≤ Module.finrank ℤ ↥L.carrier) : ∃ (x : Fin m → ↥L.carrier), LinearIndependent ℤ x ∧ (∀ (j : Fin m), L.integralNorm (x j) = ↑(L.successiveMinimum ⟨↑j, ⋯⟩)) ∧ ∀ (y : ↥L.carrier), ↑y ∉ Submodule.span ℚ (Set.range fun (j : Fin m) => ↑(x j)) → ∀ (j : Fin m), L.integralNorm (x j) ≤ L.integralNorm y

Greedy construction of m independent vectors realising the first m successive minima, each at most every vector outside the span of the chosen ones.

theorem TauCeti.IntegralLattice.IsPosSemidef.exists_linearIndependent_integralNorm_eq_successiveMinimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) : ∃ (x : Fin (Module.finrank ℤ ↥L.carrier) → ↥L.carrier), LinearIndependent ℤ x ∧ ∀ (i : Fin (Module.finrank ℤ ↥L.carrier)), L.integralNorm (x i) = ↑(L.successiveMinimum i)

A positive semidefinite lattice admits independent vectors attaining all successive minima simultaneously. These vectors are not asserted to be an integral basis.

theorem TauCeti.IntegralLattice.IsPosSemidef.exists_ne_zero_integralNorm_eq_successiveMinimum {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosSemidef) (i : Fin (Module.finrank ℤ ↥L.carrier)) : ∃ (x : ↥L.carrier), x ≠ 0 ∧ L.integralNorm x = ↑(L.successiveMinimum i)

Every successive minimum of a positive semidefinite lattice is the norm of a nonzero vector. This asserts attainment as a squared norm, rather than merely existence of a bounding infimum.

theorem TauCeti.IntegralLattice.IsPosDef.successiveMinimum_pos {V : Type u} [AddCommGroup V] [Module ℚ V] {L : IntegralLattice V} (hL : L.IsPosDef) (i : Fin (Module.finrank ℤ ↥L.carrier)) : 0 < L.successiveMinimum i

Successive minima of a positive definite lattice are positive.

theorem TauCeti.IntegralLattice.Isometry.successiveMinimum_eq {V : Type u} [AddCommGroup V] [Module ℚ V] {W : Type v} [AddCommGroup W] [Module ℚ W] {L : IntegralLattice V} {M : IntegralLattice W} (e : L.Isometry M) (i : Fin (Module.finrank ℤ ↥L.carrier)) : L.successiveMinimum i = M.successiveMinimum (Fin.cast ⋯ i)

The successive minimum is invariant under isometry; indices are transported by equality of carrier ranks.