Minkowski's second theorem

For a lattice L in a finite-dimensional real normed space E of dimension n and a symmetric convex body B, Minkowski's second theorem is the pair of inequalities

2 ^ n / n !  *  covolume L  ≤  (∏ i < n, λ i) * volume B  ≤  2 ^ n * covolume L,

with λ i the successive minima of Layer 4.1. This file proves both, and the two pieces of Cassels' route that are statements in their own right.

Main results

• ZLattice.covolume_le_prod_successiveMinimum_mul_measure: the lower bound. The independent lattice vectors realizing the minima, divided by their minima, span a cross-polytope inside B of volume 2 ^ n / n ! times the covolume of the lattice they generate, divided by ∏ i, λ i; and that covolume is a positive integer multiple of the covolume of L.
• ZLattice.prod_successiveMinimum_mul_measure_le: the upper bound, the substantial half — the direction Layer 5 and 6.3 consume. Weyl's proof, through Cassels' Theorem IV, which is ZLattice.pow_mul_measure_inter_add_le of ArithmeticHeights/QuotientFubini.lean: the measure of the image of the open dilate {gauge B < t} in E ⧸ L is scaled up one minimum at a time, from t = λ 0 / 2 — where the dilate injects into the quotient — to t = λ (n - 1) / 2, where it is bounded by the covolume.
• ZLattice.pow_successiveMinimum_zero_mul_measure_le: λ 0 ^ n * volume B ≤ 2 ^ n * covolume L, which is Minkowski's first theorem read homogeneously. It is the upper bound with ∏ i < n, λ i weakened to λ 0 ^ n, and it is everything the first theorem gives.
• ZLattice.exists_basis_mem_span_int_of_gauge_lt: Cassels' Chapter VIII, Lemma 2 — a ℤ-basis of L against which every lattice point of gauge below the j-th minimum is an integer combination of the first j members. Layer 4.6 consumes it; the upper bound below does not.

Implementation notes

⚠ The reduction that would make the upper bound easy is false. The worked example at the end of this file machine-checks that shrinking one coordinate of a symmetric convex body can leave the body. The linear map sending the realizing vector v i to (λ i / λ (n - 1)) • v i has determinant ∏ λ i / λ (n - 1) ^ n and nondecreasing coordinate factors in (0, 1], which is exactly the shape that example refutes: such a map need not send the body into itself, so the upper bound is not the statement that some one set is a packing, and no rescaling of the body makes it one. Weyl's proof replaces the set inclusion by a measure estimate in the quotient E ⧸ L, and is a genuinely different argument.

⚠ Neither inequality needs the body closed, bounded away from nothing, or compact. The lower bound uses the vectors through gauge B (v i) = λ i and meets the body through mem_smul_of_gauge_lt, the half of the gauge dictionary that holds for any body. The upper bound is chained on the open dilates {gauge B < t}, which is what lets the separation hypothesis of Cassels' Theorem IV hold at 2 t = λ J rather than only below it; the body and its interior have the same measure because a convex set has null frontier. Only ZLattice.pow_successiveMinimum_zero_mul_measure_le carries IsCompact B, and only because Mathlib's form of Minkowski's first theorem does.

⚠ Cassels' Lemma 2 is not on the path to the upper bound. He needs the adapted basis because he works in coordinates, where the integrality of the first J coordinates is how one sees that the translation stays inside the sublattice. Coordinate-free the sublattice L ∩ span (v 0, …, v (J - 1)) is at hand, and the only thing the estimate wants of it is its ℤ-rank, which is the ℝ-dimension of its span by ZLattice.finrank_int_eq_finrank_real. The lemma stays in this file because Layer 4.6 does want the basis.

References

J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer (1959), Chapter VIII §4, Theorem V: both inequalities, as (12) and (13) of VIII.1. The lower bound is the cross-polytope computation on p. 218; pow_successiveMinimum_zero_mul_measure_le is the inequality (11) there; the upper bound is Weyl's argument of §4.2, whose kernel is Cassels' Theorem IV. E. Bombieri and W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Appendix C.2.

This is Layer 4.2 of the ArithmeticHeights roadmap.

The lower bound

theorem ZLattice.covolume_le_prod_successiveMinimum_mul_measure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : Set E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hB₀ : Convex ℝ B) (hB₁ : ∀ x ∈ B, -x ∈ B) (hB₂ : (interior B).Nonempty) (hB₃ : Bornology.IsBounded B) : 2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * covolume L μ ≤ (∏ i ∈ Finset.range (Module.finrank ℝ E), successiveMinimum L B i) * (μ B).toReal

Minkowski's second theorem, the lower bound (Cassels, Chapter VIII, Theorem V, the inequality (13) of VIII.1). The independent lattice vectors v i realizing the successive minima, scaled to gauge one, span a cross-polytope of volume 2 ^ n / n ! times |det v| inside the body, and |det v| is an integer multiple of the covolume of L.

⚠ No closedness or compactness of the body is needed.

The upper bound for the zeroth minimum

theorem ZLattice.pow_successiveMinimum_zero_mul_measure_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : Set E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [Nontrivial E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hB₀ : Convex ℝ B) (hB₁ : ∀ x ∈ B, -x ∈ B) (hB₂ : (interior B).Nonempty) (hB₅ : IsCompact B) : successiveMinimum L B 0 ^ Module.finrank ℝ E * (μ B).toReal ≤ 2 ^ Module.finrank ℝ E * covolume L μ

Minkowski's first theorem, read homogeneously (Cassels, Chapter VIII, the inequality (11) of VIII.1): the zeroth minimum obeys λ 0 ^ n * volume B ≤ 2 ^ n * covolume L. This is the upper bound of Minkowski's second theorem with ∏ i < n, λ i weakened to λ 0 ^ n, and it is all that the first theorem gives: the substantial half of Layer 4.2 is a different argument.

Cassels' Lemma 2: a basis adapted to the minima

theorem ZLattice.exists_basis_mem_span_int_of_gauge_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : Set E} [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (hB₀ : Convex ℝ B) (hB₁ : ∀ x ∈ B, -x ∈ B) (hB₂ : (interior B).Nonempty) (hB₃ : Bornology.IsBounded B) : ∃ (b : Module.Basis (Fin (Module.finrank ℝ E)) ℤ ↥L), ∀ (j : ℕ), ∀ x ∈ L, gauge B x < successiveMinimum L B j → x ∈ Submodule.span ℤ ((fun (i : Fin (Module.finrank ℝ E)) => ↑(b i)) '' {i : Fin (Module.finrank ℝ E) | ↑i < j})

Cassels' Chapter VIII, Lemma 2. Some ℤ-basis b of L has, for every j, every lattice point of gauge below the j-th minimum an integer combination of b 0, …, b (j - 1).

This is the first of the two pieces Weyl's proof of the upper bound needs, and it is exactly the combination of two things proved elsewhere: the dependence half of Cassels' Lemma 1 (ZLattice.mem_span_of_gauge_lt_successiveMinimum, Layer 4.1), which puts such a point in the ℝ-span of the first j vectors realizing the minima, and the adapted basis (ZLattice.exists_basis_mem_span_int_of_mem_span_real), which makes the lattice points of that span the integer combinations of the first j basis vectors. Cassels proves the second by his Chapter I, Theorem I; neither half is in Mathlib.

⚠ The basis is not the family realizing the minima, and in general cannot be: Layer 4.6 is the statement of how far apart the two can be. What survives is the flag.

The upper bound

Weyl's argument, as Cassels carries it: the measure of the image of the open dilate {gauge B < t} in E ⧸ L grows at least like s ^ (n - J) when t is scaled by s ≥ 1 inside the range where congruence modulo L is congruence modulo L ∩ span (v 0, …, v (J - 1)), and chaining that from the first minimum to the last multiplies the measure of the body by the product of the minima. The estimate itself is ZLattice.pow_mul_measure_inter_add_le of ArithmeticHeights/QuotientFubini.lean; what is here is the chain and the gauge bookkeeping.

theorem ZLattice.prod_successiveMinimum_mul_measure_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {B : Set E} [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hB₀ : Convex ℝ B) (hB₁ : ∀ x ∈ B, -x ∈ B) (hB₂ : (interior B).Nonempty) (hB₃ : Bornology.IsBounded B) : (∏ i ∈ Finset.range (Module.finrank ℝ E), successiveMinimum L B i) * (μ B).toReal ≤ 2 ^ Module.finrank ℝ E * covolume L μ

Minkowski's second theorem, the upper bound (Cassels, Chapter VIII, Theorem V, the inequality (12) of VIII.1): (∏ i < n, λ i) * volume B ≤ 2 ^ n * covolume L. This is the substantial half, the one Layer 5 and 6.3 consume.

The proof is Weyl's, through Cassels' Theorem IV, which is ZLattice.pow_mul_measure_inter_add_le. Write S t for the image of the open dilate {gauge B < t} in E ⧸ L. At t = λ 0 / 2 the dilate injects into the quotient, so m (S t) = t ^ n * volume B; and for 1 ≤ J < n and s = λ J / λ (J - 1) the estimate gives m (S (s t)) ≥ s ^ (n - J) * m (S t) at t = λ (J - 1) / 2, because there congruence modulo L inside the dilate is congruence modulo L ∩ span (v 0, …, v (J - 1)), a sublattice of ℤ-rank at most J. Chaining and bounding m (S (λ (n - 1) / 2)) by the covolume multiplies volume B by the telescoping product λ 0 ^ n * ∏_{J = 1}^{n - 1} (λ J / λ (J - 1)) ^ (n - J) = ∏ i < n, λ i.

⚠ The chain runs on open dilates, and that is what removes closedness. For a closed body the dilate contains points of gauge exactly t, and the separation hypothesis would hold only for 2 t < λ J strictly; for {gauge B < t} it holds at 2 t = λ J, which is where the chain needs it. The body and its interior have the same measure because a convex set has null frontier.

⚠ Cassels' Lemma 2 is not used. He needs the adapted basis because he works in coordinates: the integrality of the first J coordinates is how he sees that the translation stays in the sublattice. Coordinate-free the sublattice L ∩ span (v 0, …, v (J - 1)) is at hand and the only thing wanted of it is its rank, which is the ℝ-dimension of its span by ZLattice.finrank_int_eq_finrank_real.

Why the upper bound is not a packing statement

The upper bound of Minkowski's second theorem would follow at once from the following false statement: for a symmetric convex body B and 0 < c ≤ 1, shrinking one coordinate of a point of B — in the basis realizing the minima, and shrinking the earlier coordinates, whose minima are the smaller ones — keeps it inside B. It fails already in the plane.