Minkowski's second theorem

Let L be a full lattice in an n-dimensional real normed space E, let μ be an additive Haar measure on E, and let K be a convex set symmetric about the origin. Minkowski's second theorem bounds the product of the successive minima λ₀ ≤ ⋯ ≤ λₙ₋₁ of L with respect to K from both sides:

2ⁿ / n! · covolume L μ ≤ λ₀ ⋯ λₙ₋₁ · μ K ≤ 2ⁿ · covolume L μ.

The lower bound assumes that K is a convex body with 0 in its interior. Both bounds are sharp: weighted cross-polytopes attain the lower one and weighted boxes the upper one.

Since λ₀ ≤ λᵢ for every i, the upper bound strengthens Minkowski's first theorem λ₀ⁿ · μ K ≤ 2ⁿ · covolume L μ, and it is the bound against which the products of the gauges of short lattice bases (such as fundamental systems of units, or bases of the integer kernel of a matrix) are measured.

The main statement of the upper bound does not use a successive-minima function. It takes ℝ-independent lattice vectors a i and nonnegative numbers g i such that every lattice vector v with gauge K v < g j lies in the span of a 0, …, a (j - 1). Independent vectors realizing the successive minima satisfy this with g = λ: if gauge K v < λ_j and i ≤ j is least with λ_i > gauge K v, then a 0, …, a (i - 1) and v lie in (gauge K v) • K, so v is in the span of a 0, …, a (i - 1) (ZLattice.mem_span_image_Iio_of_gauge_lt_successiveMin). Conversely, every such g satisfies g j ≤ λ_j.

Main results

• ZLattice.prod_mul_measure_le_two_pow_mul_covolume: (∏ i, g i) * μ K ≤ 2 ^ n * covolume L μ.
• ZLattice.prod_successiveMin_mul_measure_le_two_pow_mul_covolume: the classical form λ₀ ⋯ λₙ₋₁ · μ K ≤ 2ⁿ · covolume L μ for a symmetric convex body K, and its real-valued form ZLattice.prod_successiveMin_mul_measureReal_le_two_pow_mul_covolume.
• ZLattice.prod_successiveMin_le_covolume_of_two_pow_finrank_le: λ₀ ⋯ λₙ₋₁ ≤ covolume L μ for a symmetric convex body K with 2ⁿ ≤ μ K.
• ZLattice.successiveMin_pow_mul_measureReal_le_two_pow_mul_covolume: Minkowski's first theorem on the successive minima, λ₀ⁿ · μ K ≤ 2ⁿ · covolume L μ, for a symmetric convex body K.
• Convex.prod_mul_volume_real_le_two_pow: the upper bound for the integer lattice ℤⁿ ⊆ ℝⁿ in coordinates. If K ⊆ ℝⁿ is convex and symmetric and every integer vector z with gauge K z < a i has z j = 0 for all j ≥ i, then (∏ i, a i) · vol K ≤ 2ⁿ.
• ZLattice.two_pow_div_factorial_mul_covolume_le_prod_mul_measure: the lower bound 2 ^ n / n! * covolume L μ ≤ (∏ i, a i) * μ K for a basis b of lattice vectors with b i ∈ a i • K.
• ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measure: the classical lower bound 2ⁿ / n! · covolume L μ ≤ λ₀ ⋯ λₙ₋₁ · μ K for a symmetric convex body K with 0 in its interior, and its real-valued form ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measureReal.

Proof of the upper bound

Coordinates in a ℤ-basis of L adapted to the flag spanned by the a i (ZLattice.exists_basis_span_image_eq_flag) reduce the statement to L = ℤⁿ ⊆ ℝⁿ, with span (a 0, …, a (j - 1)) the span of the first j coordinate vectors, and to the open convex set C = ½ • interior K, whose volume is 2⁻ⁿ μ K / covolume L μ (ZLattice.volume_image_eq_measure_div_covolume). The hypothesis says that two points of g j • C whose difference is an integer vector agree in all coordinates from the j-th on.

For m ≤ n, fold a set Y ⊆ ℝⁿ modulo the integer vectors supported on the first m coordinates into the slab where those coordinates lie in [0, 1). Folding all n coordinates gives a subset of the unit cube, of volume at most 1. Folding no coordinate does nothing. Write Vₘ(t) for the volume of the m-fold of t • C. Two estimates relate these volumes:

• unfolding (volume_fold_le_fold_succ): Vₘ(t) ≤ Vₘ₊₁(t) when t ≤ g m, because the translates of the m-fold of t • C by integer multiples of the m-th coordinate vector are then pairwise disjoint;
• dilation (volume_fold_smul): ρ ^ (n - m) · Vₘ(t) ≤ Vₘ(ρ t) for ρ ≥ 1. On each fibre over the last n - m coordinates, ρ times a nonempty convex set contains a translate of it, and the folded volume of a set is translation invariant.

Chaining them from V₀(g 0) = g 0 ^ n · vol C up to Vₙ(g (n - 1)) ≤ 1 gives g 0 ⋯ g (n - 1) · vol C ≤ 1.

Proof of the lower bound

Take a basis b of E made of lattice vectors with b i ∈ λ_i • K (ZLattice.exists_basis_gauge_eq_successiveMin). Since K is convex and symmetric, it contains the weighted cross-polytope {x | ∑ i, λ_i * |b.repr x i| ≤ 1} (Convex.weighted_crosspolytope_subset), whose measure is 2ⁿ / n! / (λ₀ ⋯ λₙ₋₁) times the measure of the fundamental parallelepiped of b (Module.Basis.addHaar_weighted_crosspolytope). That parallelepiped is a fundamental domain of the sublattice spanned by b, so its measure bounds the covolume of L (ZLattice.covolume_le_abs_det_mul_measureReal). The argument works with any Haar measure directly, without transport to a Euclidean space.

References

• J. W. S. Cassels, An Introduction to the Geometry of Numbers, Springer, 1959, Chapter VIII.
• H. Davenport, Minkowski's inequality for the minima associated with a convex body, Quart. J. Math. Oxford 10 (1939), 119–121.
• M. Henk, Successive minima and lattice points, Rend. Circ. Mat. Palermo (2) Suppl. 70 (2002), 377–384, Theorem 1.2 and §3: https://arxiv.org/abs/math/0204158.
• J.-H. Evertse, Geometry of Numbers, §2.3, Theorem 2.9 and the proof of its lower bound, printed pp.24–27: https://pub.math.leidenuniv.nl/~evertsejh/dio19-2.pdf.

Folding modulo integer vectors

The theorem in coordinates

The general theorem

theorem ZLattice.prod_mul_measure_le_two_pow_mul_covolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : Set E} (hK : Convex ℝ K) (hKs : ∀ x ∈ K, -x ∈ K) {n : ℕ} (hn : n = Module.finrank ℝ E) {a : Fin n → E} (haL : ∀ (i : Fin n), a i ∈ L) (ha : LinearIndependent ℝ a) {g : Fin n → ℝ} (hg0 : ∀ (i : Fin n), 0 ≤ g i) (hgap : ∀ (j : Fin n), ∀ v ∈ L, gauge K v < g j → v ∈ Submodule.span ℝ (a '' Set.Iio j)) : ENNReal.ofReal (∏ i : Fin n, g i) * μ K ≤ 2 ^ n * ENNReal.ofReal (covolume L μ)

Minkowski's second theorem, upper bound. Let L be a discrete ℤ-submodule of an n-dimensional real normed space E, μ a Haar measure on E, and K ⊆ E convex and symmetric about 0. Let a 0, …, a (n - 1) be ℝ-linearly independent vectors of L and g 0, …, g (n - 1) nonnegative numbers such that every v ∈ L with gauge K v < g j lies in the span of a 0, …, a (j - 1). Then (∏ i, g i) * μ K ≤ 2 ^ n * covolume L μ. The full independent family already implies that the discrete submodule L is a full lattice.

Independent lattice vectors realizing the successive minima λ₀ ≤ ⋯ ≤ λₙ₋₁ of L with respect to K satisfy the hypothesis with g = λ, which gives the classical form λ₀ ⋯ λₙ₋₁ · μ K ≤ 2ⁿ · covolume L μ.

theorem ZLattice.prod_successiveMin_mul_measure_le_two_pow_mul_covolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hKs : ∀ x ∈ K, -x ∈ K) : ENNReal.ofReal (∏ i : Fin (Module.finrank ℝ E), successiveMin L K i) * μ ↑K ≤ 2 ^ Module.finrank ℝ E * ENNReal.ofReal (covolume L μ)

Minkowski's second theorem, upper bound, in terms of the successive minima. For a full lattice L in a real normed space E of dimension n, a Haar measure μ on E, and a convex body K symmetric about 0, the successive minima λ i = successiveMin L K i satisfy λ₀ ⋯ λₙ₋₁ · μ K ≤ 2ⁿ · covolume L μ. If K has empty interior, its measure is zero.

theorem ZLattice.prod_successiveMin_mul_measureReal_le_two_pow_mul_covolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hKs : ∀ x ∈ K, -x ∈ K) : (∏ i : Fin (Module.finrank ℝ E), successiveMin L K i) * μ.real ↑K ≤ 2 ^ Module.finrank ℝ E * covolume L μ

Minkowski's second theorem, upper bound, in terms of the successive minima and with real measures: λ₀ ⋯ λₙ₋₁ · μ.real K ≤ 2ⁿ · covolume L μ.

theorem ZLattice.prod_successiveMin_le_covolume_of_two_pow_finrank_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hKs : ∀ x ∈ K, -x ∈ K) (hμK : 2 ^ Module.finrank ℝ E ≤ μ ↑K) : ∏ i : Fin (Module.finrank ℝ E), successiveMin L K i ≤ covolume L μ

Minkowski's second theorem for bodies of measure at least 2ⁿ. If a convex body K symmetric about 0 has 2ⁿ ≤ μ K, then the successive minima of L with respect to K satisfy λ₀ ⋯ λₙ₋₁ ≤ covolume L μ. This applies, for instance, to the central slices of the cube [-1, 1]ⁿ, whose volume is at least 2ⁿ by Vaaler's theorem.

theorem ZLattice.successiveMin_pow_mul_measureReal_le_two_pow_mul_covolume {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hKs : ∀ x ∈ K, -x ∈ K) (hE : 0 < Module.finrank ℝ E) : successiveMin L K ⟨0, hE⟩ ^ Module.finrank ℝ E * μ.real ↑K ≤ 2 ^ Module.finrank ℝ E * covolume L μ

Minkowski's first theorem on the successive minima. For a full lattice L in a real normed space E of positive dimension n, a Haar measure μ on E, and a convex body K symmetric about 0, the first successive minimum λ₀ of L with respect to K satisfies λ₀ⁿ · μ.real K ≤ 2ⁿ · covolume L μ. It follows from the upper bound of Minkowski's second theorem, since λ₀ ≤ λᵢ for every i.

The lower bound

theorem ZLattice.two_pow_div_factorial_mul_covolume_le_prod_mul_measure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : Set E} (hK : Convex ℝ K) (h0 : 0 ∈ K) (hKs : ∀ x ∈ K, -x ∈ K) {ι : Type u_2} [Fintype ι] (b : Module.Basis ι ℝ E) (hbL : ∀ (i : ι), b i ∈ L) {a : ι → ℝ} (ha : ∀ (i : ι), 0 ≤ a i) (hbK : ∀ (i : ι), b i ∈ a i • K) : ENNReal.ofReal (2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * covolume L μ) ≤ ENNReal.ofReal (∏ i : ι, a i) * μ K

Minkowski's second theorem, lower bound, general form. Let L be a discrete ℤ-submodule of an n-dimensional real normed space E, μ a Haar measure on E, and K ⊆ E convex, containing 0 and symmetric about it. If b is a basis of E over ℝ made of vectors of L and the nonnegative numbers a i satisfy b i ∈ a i • K, then 2 ^ n / n! * covolume L μ ≤ (∏ i, a i) * μ K. The basis already implies that L is a full lattice.

A basis attaining the successive minima λ₀ ≤ ⋯ ≤ λₙ₋₁ of L with respect to K satisfies the hypothesis with a = λ, which gives the classical form 2ⁿ / n! · covolume L μ ≤ λ₀ ⋯ λₙ₋₁ · μ K.

theorem ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measure {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hK : 0 ∈ interior ↑K) (hKs : ∀ x ∈ K, -x ∈ K) : ENNReal.ofReal (2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * covolume L μ) ≤ ENNReal.ofReal (∏ i : Fin (Module.finrank ℝ E), successiveMin L K i) * μ ↑K

Minkowski's second theorem, lower bound, in terms of the successive minima. For a full lattice L in a real normed space E of dimension n, a Haar measure μ on E, and a convex body K symmetric about 0 with 0 in its interior, the successive minima λ i = successiveMin L K i satisfy 2ⁿ / n! · covolume L μ ≤ λ₀ ⋯ λₙ₋₁ · μ K.

theorem ZLattice.two_pow_div_factorial_mul_covolume_le_prod_successiveMin_mul_measureReal {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (μ : MeasureTheory.Measure E := by volume_tac) [μ.IsAddHaarMeasure] {K : ConvexBody E} (hK : 0 ∈ interior ↑K) (hKs : ∀ x ∈ K, -x ∈ K) : 2 ^ Module.finrank ℝ E / ↑(Module.finrank ℝ E).factorial * covolume L μ ≤ (∏ i : Fin (Module.finrank ℝ E), successiveMin L K i) * μ.real ↑K

Minkowski's second theorem, lower bound, in terms of the successive minima and with real measures: 2ⁿ / n! · covolume L μ ≤ λ₀ ⋯ λₙ₋₁ · μ.real K.

The upper bound for the integer lattice in coordinates

theorem Convex.prod_mul_volume_real_le_two_pow {n : ℕ} {K : Set (Fin n → ℝ)} (hK : Convex ℝ K) (hKs : ∀ x ∈ K, -x ∈ K) {a : Fin n → ℝ} (ha : ∀ (i : Fin n), 0 ≤ a i) (hgap : ∀ (i : Fin n) (z : Fin n → ℤ), (gauge K fun (j : Fin n) => ↑(z j)) < a i → ∀ (j : Fin n), i ≤ j → z j = 0) : (∏ i : Fin n, a i) * MeasureTheory.volume.real K ≤ 2 ^ n

Minkowski's second theorem, upper bound, for the integer lattice ℤⁿ ⊆ ℝⁿ in coordinates. Let K ⊆ ℝⁿ be convex and symmetric about 0, and let a 0, …, a (n - 1) be nonnegative numbers such that every integer vector z with gauge K z < a i has z j = 0 for all j ≥ i. Then (∏ i, a i) · vol K ≤ 2ⁿ, where vol K is the real-valued volume (zero if K has infinite volume). Neither monotonicity of a nor 0 ∈ interior K is assumed.