The successive minima of a symmetric convex body #
For a lattice L in a finite-dimensional real normed space E and a symmetric convex body B,
the i-th successive minimum is the least dilation of B that contains i + 1 linearly
independent points of L. This file defines it, proves it positive, monotone and homogeneous of
degree -1 in the body, and proves Cassels' Lemma 1: the minima are attained, by one family of
independent lattice vectors realizing all of them at once.
Main definitions #
ZLattice.successiveMinimum: thei-th successive minimum, as the infimum of the admissible dilations. Fori ≥ finrank ℝ Ethere are none and the value issInf ∅ = 0, so every statement below carriesi < finrank ℝ E.
Main results #
gauge_le_iff_mem_smul: the dictionary between Cassels' distance functions and the convex-body form pinned by the roadmap. Membership int • Bis having gauge at mostt, for a closed body;mem_smul_of_gauge_ltis the half that needs no closedness.ZLattice.successiveMinimum_pos: the minima are positive, which is where boundedness of the body is used, andZLattice.successiveMinimum_eq_zero_of_le: they vanish above the dimension.ZLattice.successiveMinimum_le_of_leandZLattice.successiveMinimum_smul: monotone in the index, homogeneous of degree-1in the body.ZLattice.exists_linearIndependent_gauge_eq_successiveMinimum: Cassels' Lemma 1. There is one linearly independent family of lattice vectors whose gauges are the successive minima. This is what every later proof consumes; its body form isZLattice.exists_linearIndependent_mem_smul_successiveMinimum, which is where closedness of the body is used.Finset.prod_pow_le_prod_range: the regrouping that turns a bound on the product of alld * kminima into a bound on a product ofkd-th powers — what Layers 5.3 and 5.4 spend to pass from the minima of the lattice of ak-dimensionalK-subspace tokheights.ZLattice.successiveMinimum_zero_eq: the zeroth minimum is the least dilation containing a nonzero lattice point — the quantity Minkowski's convex-body theorem bounds — andZLattice.successiveMinimum_zero_le_oneis that theorem read as the casei = 0.
Implementation notes #
The body is carried as four separate hypotheses — convex, symmetric, with nonempty interior,
bounded — plus closedness where it is needed, rather than as one bundled structure, so that each
statement says which of them it uses. Cassels indexes the minima by a distance function F and
dilates {x | F x ≤ 1}; the convex-body form is the pinned one, and gauge_le_iff_mem_smul is
the translation, proved once here.
⚠ Attainment does not need the body to be closed; only its body form does. The family of
ZLattice.exists_linearIndependent_gauge_eq_successiveMinimum realizes the minima as gauges
for any bounded symmetric convex body with nonempty interior, and that statement is the one the
proof produces. Turning gauge B (v j) = λ j into v j ∈ λ j • B is exactly the dictionary, and
exactly what fails for an open body: for the open unit ball no lattice vector lies in λ 0 • B
at all, since anything inside that dilation would already have shown a smaller dilation
admissible. The two statements are therefore kept apart, and only the second carries IsClosed B.
⚠ The minima are not monotone in the index without i < finrank ℝ E. Above the dimension
there is no independent family at all, the set of admissible dilations is empty, and the value is
sInf ∅ = 0. So Monotone (successiveMinimum L B) is false whenever E is nontrivial, and a
statement of Minkowski's second theorem that ranged over all of ℕ would multiply by zero.
References #
J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer (1959), Chapter VIII §1:
the definition, Lemma 1 (attainment) and the elementary properties proved here. E. Bombieri and
W. Gubler, Heights in Diophantine Geometry, Cambridge University Press (2006), Appendix C.2.
Minkowski's first theorem is Mathlib's
MeasureTheory.exists_ne_zero_mem_lattice_of_measure_mul_two_pow_le_measure.
This is Layer 4.1 of the ArithmeticHeights roadmap.
The body and its gauge #
Three facts about a symmetric convex body, none of them about lattices: it is a neighbourhood of the origin, and its dilations are the sublevel sets of its gauge — from below always, and exactly when the body is closed.
A symmetric convex set with nonempty interior is a neighbourhood of 0: the midpoint of an
interior point and its negative is an interior point. This is what makes the body absorbent, and
it is the only use of the symmetry hypothesis in the elementary theory.
Half of the gauge dictionary, and the half that costs nothing: a point of gauge strictly less
than t lies in t • B. No closedness is needed, and this is what the existence statements below
use to exhibit an admissible dilation.
The gauge dictionary. For a closed convex body with 0 in its interior, lying in the
dilation t • B is the same as having gauge at most t. This is the translation between Cassels'
distance functions and the convex-body form of the successive minima, and closedness is exactly
what it costs: for an open body the two sides differ on the boundary.
The i-th successive minimum of a set B with respect to a lattice L: the least
dilation of B containing i + 1 linearly independent points of L. The case i = 0 is the
quantity bounded by Minkowski's convex-body theorem. For i ≥ finrank ℝ E there is no such
family and the value is sInf ∅ = 0, so every statement about the minima carries
i < finrank ℝ E.
Equations
Instances For
An admissible dilation bounds the minimum from above. This and le_successiveMinimum are the
only two ways the infimum is used below.
The minima are homogeneous of degree -1 in the body: dilating the body by c divides every
minimum by c.
Below the dimension, a lower bound for every admissible dilation is a lower bound for the minimum.
Above the dimension the minima vanish: there is no independent family of i + 1 vectors at
all, so the set of admissible dilations is empty and its infimum is the junk value 0. Together
with successiveMinimum_pos this is why every statement about the minima is restricted to
i < finrank ℝ E.
The minima are monotone in the index below the dimension: an independent family of j + 1
vectors contains one of i + 1 vectors, so every dilation admissible at j is admissible at
i. The hypothesis j < finrank ℝ E is not removable — see successiveMinimum_eq_zero_of_le.
The minima are positive. A nonzero lattice point has gauge bounded away from zero, so no small dilation of a bounded body can contain one.
Cassels' Lemma 1: the successive minima are attained. There is a single family of
finrank ℝ E linearly independent lattice vectors whose gauges are the successive minima — not
one family for each index. This is the statement every later proof consumes.
⚠ No closedness of the body is needed here; see
exists_linearIndependent_mem_smul_successiveMinimum for the body form, which does need it.
The body form of Cassels' Lemma 1: the independent lattice vectors realizing the minima lie in
the corresponding dilations of the body. This is the form Minkowski's second theorem and the basis
lemma of Layer 4.6 consume, and IsClosed B is exactly what it costs over the gauge form.
The dependence half of Cassels' Lemma 1. Outside the span of the first j members of a
family realizing the minima there is nothing of gauge below the j-th minimum. The point would
extend those j members to an independent family of j + 1 lattice points, which bounds the
j-th minimum by the largest gauge in the family; the induction on j is what identifies that
largest gauge as the gauge of the new point, since without it the bound is only by the maximum of
the new gauge and the (j - 1)-st minimum, and those can be equal.
Cassels' Lemma 1, completed. A lattice point of gauge below the j-th minimum lies in the
span of the first j members of a family realizing the minima. No hypothesis on j is needed:
above the dimension the minima vanish and no gauge is negative. This is the input to Cassels'
Lemma 2, ZLattice.exists_basis_mem_span_int_of_gauge_lt.
Minkowski's first theorem as the case i = 0 #
The zeroth minimum is the least dilation of the body containing a nonzero lattice point, which is the quantity Minkowski's convex-body theorem bounds. The identity is measure-free; the bound is the only statement in this file that mentions a measure.
The zeroth minimum asks only for a nonzero lattice point: a one-element family is linearly independent exactly when its member is nonzero.
Minkowski's convex-body theorem is the case i = 0. A symmetric convex compact body whose
volume is at least 2 ^ n times the covolume of the lattice has zeroth minimum at most one.
Regrouping a product of minima #
Every d-th term, to the power d, against the whole product. For a nonnegative sequence
that is monotone below N, the product of f (d * j) ^ d over j < k is at most the product of
f i over i < d * k. This is what turns Minkowski's second theorem — a bound on the product of
all d * k successive minima — into a bound on a product of k heights, each of which costs a
d-th power.