Successive minima need not be attained by a basis

Let L = ℤ⁵ + ℤ · (½, …, ½) in EuclideanSpace ℝ (Fin 5), measured by the Euclidean unit ball. Every nonzero vector of L has norm at least 1: a point of L has all coordinates in ℤ or all coordinates in ½ + ℤ, and in the second case its squared norm is at least 5 / 4. The standard basis vectors e 0, …, e 4 lie in L and have norm 1, so all five successive minima of L are 1, attained by the e i. But the e i span ℤ⁵, which has index two in L, so no basis of L consists of them.

Cassels' basis lemma ZLattice.exists_basis_gauge_le_max_one_mul, applied to the e i, still produces a basis b of L with ‖b i‖ ≤ max 1 ((i + 1) / 2). An explicit such basis is e 0, e 1, e 2, e 3, (½, …, ½), whose last vector has norm √5 / 2 ≤ 5 / 2.

Main results

• TauCeti.GaugeBasisExample.one_le_norm_of_mem_lattice: nonzero vectors of L have norm ≥ 1.
• TauCeti.GaugeBasisExample.relIndex_stdLattice_lattice: ℤ⁵ has index two in L.
• TauCeti.GaugeBasisExample.not_exists_basis_eq_single: the e i are not a basis of L.
• TauCeti.GaugeBasisExample.exists_basis_norm_le: the basis given by Cassels' lemma.
• TauCeti.GaugeBasisExample.norm_basis_le: the explicit basis meets the same bounds.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter V, Lemma 8.

noncomputable def TauCeti.GaugeBasisExample.half : EuclideanSpace ℝ (Fin 5)

The point (½, …, ½) of EuclideanSpace ℝ (Fin 5).

noncomputable def TauCeti.GaugeBasisExample.gen (k : Fin 5) : EuclideanSpace ℝ (Fin 5)

The generators e 0, e 1, e 2, e 3, (½, …, ½) of L.

theorem TauCeti.GaugeBasisExample.gen_four : gen 4 = half

@[simp]

theorem TauCeti.GaugeBasisExample.gen_apply (k j : Fin 5) : (gen k).ofLp j = if k = 4 then 1 / 2 else if j = k then 1 else 0

theorem TauCeti.GaugeBasisExample.single_four_eq : EuclideanSpace.single 4 1 = gen 4 + gen 4 - gen 0 - gen 1 - gen 2 - gen 3

noncomputable def TauCeti.GaugeBasisExample.stdLattice : Submodule ℤ (EuclideanSpace ℝ (Fin 5))

The standard lattice ℤ⁵, spanned by e 0, …, e 4.

noncomputable def TauCeti.GaugeBasisExample.lattice : Submodule ℤ (EuclideanSpace ℝ (Fin 5))

The lattice L = ℤ⁵ + ℤ · (½, …, ½).

theorem TauCeti.GaugeBasisExample.mem_stdLattice_iff {x : EuclideanSpace ℝ (Fin 5)} : x ∈ stdLattice ↔ ∀ (j : Fin 5), ∃ (z : ℤ), ↑z = x.ofLp j

theorem TauCeti.GaugeBasisExample.single_mem_lattice (i : Fin 5) : EuclideanSpace.single i 1 ∈ lattice

theorem TauCeti.GaugeBasisExample.half_mem_lattice : half ∈ lattice

theorem TauCeti.GaugeBasisExample.stdLattice_le_lattice : stdLattice ≤ lattice

theorem TauCeti.GaugeBasisExample.linearIndependent_gen : LinearIndependent ℝ gen

instance TauCeti.GaugeBasisExample.instDiscreteTopologySubtypeEuclideanSpaceRealFinOfNatNatMemSubmoduleIntLattice : DiscreteTopology ↥lattice

L is discrete, since it is spanned by the real basis gen.

theorem TauCeti.GaugeBasisExample.exists_intCast_of_mem_lattice {x : EuclideanSpace ℝ (Fin 5)} (hx : x ∈ lattice) : (∃ (m : ℤ), ↑m = 2 * x.ofLp 4) ∧ ∀ (j : Fin 5), ∃ (z : ℤ), ↑z = x.ofLp j - x.ofLp 4

Every point of L has its last coordinate in ½ℤ, and all its coordinates differ from the last one by integers.

theorem TauCeti.GaugeBasisExample.mem_lattice_iff {x : EuclideanSpace ℝ (Fin 5)} : x ∈ lattice ↔ (∃ (m : ℤ), ↑m = 2 * x.ofLp 4) ∧ ∀ (j : Fin 5), ∃ (z : ℤ), ↑z = x.ofLp j - x.ofLp 4

A point lies in L exactly when its last coordinate is in ½ℤ and all its coordinates differ from the last one by integers.

theorem TauCeti.GaugeBasisExample.one_le_norm_of_mem_lattice {x : EuclideanSpace ℝ (Fin 5)} (hx : x ∈ lattice) (h0 : x ≠ 0) : 1 ≤ ‖x‖

The first minimum of L is 1. Every nonzero vector of L has norm at least 1.

theorem TauCeti.GaugeBasisExample.mem_stdLattice_iff_of_mem_lattice {x : EuclideanSpace ℝ (Fin 5)} (hx : x ∈ lattice) : x ∈ stdLattice ↔ ∃ (z : ℤ), ↑z = x.ofLp 4

A point of L lies in ℤ⁵ exactly when its last coordinate is an integer.

theorem TauCeti.GaugeBasisExample.relIndex_stdLattice_lattice : stdLattice.toAddSubgroup.relIndex lattice.toAddSubgroup = 2

The minima witnesses span a sublattice of index two. ℤ⁵ has index two in L, with (½, …, ½) representing the nontrivial coset.

theorem TauCeti.GaugeBasisExample.not_exists_basis_eq_single : ¬∃ (b : Module.Basis (Fin 5) ℤ ↥lattice), ∀ (i : Fin 5), ↑(b i) = EuclideanSpace.single i 1

The minima witnesses are not a basis. No basis of L consists of the vectors e 0, …, e 4, although they realize all five successive minima of L.

theorem TauCeti.GaugeBasisExample.exists_basis_norm_le : ∃ (b : Module.Basis (Fin 5) ℤ ↥lattice), ∀ (i : Fin 5), ‖↑(b i)‖ ≤ max 1 ((↑↑i + 1) / 2)

Cassels' basis lemma on L. Applied to the minima witnesses e 0, …, e 4, it gives a basis b of L with ‖b i‖ ≤ max 1 ((i + 1) / 2).

@[simp]

theorem TauCeti.GaugeBasisExample.norm_half : ‖half‖ = √5 / 2

noncomputable def TauCeti.GaugeBasisExample.basis : Module.Basis (Fin 5) ℤ ↥lattice

The basis e 0, e 1, e 2, e 3, (½, …, ½) of L.

@[simp]

theorem TauCeti.GaugeBasisExample.basis_apply (i : Fin 5) : ↑(basis i) = gen i

theorem TauCeti.GaugeBasisExample.norm_basis_le (i : Fin 5) : ‖↑(basis i)‖ ≤ max 1 ((↑↑i + 1) / 2)

An explicit basis within Cassels' bounds. The basis e 0, e 1, e 2, e 3, (½, …, ½) satisfies ‖b i‖ ≤ max 1 ((i + 1) / 2); its last vector has norm √5 / 2 ≤ 5 / 2.