The central slice of the cube, and lattice bases in the sup norm

For a subspace W of the Euclidean space ℝ^ι, the central slice W ∩ [-1, 1]^ι of the cube is a symmetric convex body in W with 0 in its interior, Submodule.cubeSlice W. Its gauge is the sup norm max_i |x i|, not the Euclidean norm that W inherits, and by Vaaler's cube-slicing theorem Submodule.two_pow_finrank_le_volume_setOf_forall_abs_le_one (after unfolding Submodule.coe_cubeSlice) its volume is at least 2 ^ k, where k = finrank ℝ W.

The successive minima of a lattice L in W with respect to the cube slice therefore measure L in the sup norm, and Cassels' basis from the minima gives a ℤ-basis of L the product of whose sup norms is at most k! / 2 ^ (k - 1) times the product of the minima. For the lattice of integral points of a subspace V of ℚ^ι, for instance the space of solutions of a system of linear equations with integer coefficients, this is a ℤ-basis of the whole of V ∩ ℤ^ι, not only of a sublattice of finite index. Minkowski's second theorem, against the lower bound 2 ^ k for the volume of the cube slice, bounds the product of the minima by the covolume of L; with it, these bases are the integral kernel bases of bounded sup norm of Bombieri and Vaaler.

Main definitions

• Submodule.cubeSlice W: the central slice W ∩ [-1, 1]^ι of the cube, as a convex body in W.

Main results

• Submodule.gauge_cubeSlice: the gauge of the cube slice is the sup norm.
• ZLattice.exists_basis_prod_norm_le_prod_successiveMin_cubeSlice: a ℤ-basis of a full lattice in W whose product of sup norms is at most k! / 2 ^ (k - 1) times the product of the minima.
• Submodule.exists_basis_intPoints_prod_norm_le_prod_successiveMin: the same for the integral points of a rational subspace.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter V, Lemma 8.
• E. Bombieri and J. Vaaler, On Siegel's lemma, Invent. Math. 73 (1983), 11–32, Theorem 2.
• I. Aliev and M. Henk, Minkowski's successive minima in convex and discrete geometry, Commun. Math. 31 (2023), 35–59, §6.

def Submodule.cubeSlice {ι : Type u_1} [Fintype ι] (W : Submodule ℝ (EuclideanSpace ℝ ι)) : ConvexBody ↥W

The central slice W ∩ [-1, 1]^ι of the cube, as a convex body in the subspace W of the Euclidean space ℝ^ι: the points of W all of whose coordinates are at most 1 in absolute value.

@[simp]

theorem Submodule.coe_cubeSlice {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} : ↑W.cubeSlice = {x : ↥W | ∀ (i : ι), |(↑x).ofLp i| ≤ 1}

As a set, the cube slice consists of the points of W all of whose coordinates are at most 1 in absolute value.

@[simp]

theorem Submodule.mem_cubeSlice {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} {x : ↥W} : x ∈ W.cubeSlice ↔ ∀ (i : ι), |(↑x).ofLp i| ≤ 1

A point of W lies in the cube slice when all its coordinates are at most 1 in absolute value.

theorem Submodule.neg_mem_cubeSlice {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} {x : ↥W} : -x ∈ W.cubeSlice ↔ x ∈ W.cubeSlice

The cube slice is symmetric about 0.

theorem Submodule.zero_mem_interior_cubeSlice {ι : Type u_1} [Fintype ι] (W : Submodule ℝ (EuclideanSpace ℝ ι)) : 0 ∈ interior ↑W.cubeSlice

The cube slice is a neighbourhood of 0 in W.

theorem Submodule.gauge_cubeSlice {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} (x : ↥W) : gauge (↑W.cubeSlice) x = ‖(↑x).ofLp‖

The gauge of the cube slice is the sup norm max_i |x i| of the coordinates.

theorem Submodule.mem_smul_cubeSlice_iff {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} {t : ℝ} (ht : 0 < t) {x : ↥W} : x ∈ t • ↑W.cubeSlice ↔ ∀ (i : ι), |(↑x).ofLp i| ≤ t

For 0 < t, the dilate t • cubeSlice W consists of the points of W all of whose coordinates are at most t in absolute value.

theorem ZLattice.exists_basis_prod_norm_le_prod_successiveMin_cubeSlice {ι : Type u_1} [Fintype ι] {W : Submodule ℝ (EuclideanSpace ℝ ι)} (L : Submodule ℤ ↥W) [DiscreteTopology ↥L] [IsZLattice ℝ L] : ∃ (b : Module.Basis (Fin (Module.finrank ℝ ↥W)) ℤ ↥L), ∏ j : Fin (Module.finrank ℝ ↥W), ‖(↑↑(b j)).ofLp‖ ≤ ↑(Module.finrank ℝ ↥W).factorial / 2 ^ (Module.finrank ℝ ↥W - 1) * ∏ j : Fin (Module.finrank ℝ ↥W), successiveMin L W.cubeSlice j

A lattice basis from the minima, in the sup norm. A full lattice L in a subspace W of the Euclidean space ℝ^ι has a ℤ-basis b with ∏ j, ‖b j‖ ≤ k! / 2 ^ (k - 1) * ∏ j, successiveMin L (cubeSlice W) j, where ‖b j‖ is the sup norm of the coordinates of b j and k = finrank ℝ W.

theorem Submodule.exists_basis_intPoints_prod_norm_le_prod_successiveMin {ι : Type u_1} [Fintype ι] (V : Submodule ℚ (ι → ℚ)) : ∃ (b : Module.Basis (Fin (Module.finrank ℝ ↥V.realSpan)) ℤ ↥V.intPoints), ∏ j : Fin (Module.finrank ℝ ↥V.realSpan), ‖↑(b j)‖ ≤ ↑(Module.finrank ℝ ↥V.realSpan).factorial / 2 ^ (Module.finrank ℝ ↥V.realSpan - 1) * ∏ j : Fin (Module.finrank ℝ ↥V.realSpan), ZLattice.successiveMin V.intLattice V.realSpan.cubeSlice j

A basis of the integral points from the minima, in the sup norm. For a subspace V of ℚ^ι of dimension k (stated as finrank ℝ V.realSpan, which is finrank ℚ V by finrank_realSpan), the integral points V ∩ ℤ^ι have a ℤ-basis b with ∏ j, ‖b j‖ ≤ k! / 2 ^ (k - 1) * ∏ j, λ j, where ‖b j‖ = max_i |b j i| is the sup norm and the λ j are the successive minima of V ∩ ℤ^ι, as the lattice V.intLattice in the real span of V, with respect to the slice of the cube [-1, 1]^ι.