Successive minima of an arbitrary set with respect to a submodule

For a ℤ-submodule L of a real normed space E, an arbitrary set s ⊆ E and i : ℕ, the i-th successive minimum MeasureTheory.successiveMin L s i is the infimum of the r : ℝ≥0 such that the vectors of L in the dilate r • s span a real subspace of dimension greater than i. No geometric hypothesis is imposed on s or L, so indices at or beyond the rank of L take the junk value sInf ∅ = 0.

On a convex body with 0 in its interior these are the body minima ZLattice.successiveMin (MeasureTheory.coe_successiveMin), which carry the geometric theory: attainment, positivity and Minkowski's second theorem.

Main definitions

• MeasureTheory.successiveMin L s i: the i-th successive minimum of s with respect to L.

Main results

• MeasureTheory.successiveMin_of_finrank_le, MeasureTheory.successiveMin_of_setFinrank_le and MeasureTheory.successiveMin_of_finrank_int_le: the minima vanish at indices beyond the dimension of E, beyond the real rank of L, and, for discrete L, beyond its integer rank.
• MeasureTheory.exists_lt_setFinrank_smul_inter: for discrete L and absorbent s, the infimum defining a minimum below the integer rank of L is over a nonempty set.
• MeasureTheory.successiveMin_mono: below the integer rank the minima are nondecreasing.
• MeasureTheory.successiveMin_le_of_lt_setFinrank and MeasureTheory.lt_setFinrank_smul_inter_of_successiveMin_lt: a dilate whose lattice vectors span a subspace of dimension greater than i bounds the i-th minimum from above, and conversely, for discrete L, i < finrank ℤ L and an absorbent set star-convex about 0, every dilate by a factor strictly above the minimum is such a dilate.
• MeasureTheory.exists_linearIndependent_of_successiveMin_lt: for discrete L, i < finrank ℤ L and a convex neighbourhood of 0, every dilate by a factor strictly above the i-th minimum contains i + 1 linearly independent vectors of L.
• MeasureTheory.lt_setFinrank_successiveMin_smul: for discrete L, i < finrank ℤ L and a compact convex neighbourhood of 0, the infimum is attained: the dilate by the i-th minimum itself contains vectors of L spanning a real subspace of dimension greater than i.
• MeasureTheory.setOf_lt_setFinrank_smul_inter_eq_Ici and MeasureTheory.isClosed_setOf_lt_setFinrank_smul_inter: in that setting the factors defining the i-th minimum form the closed half-line above it.
• MeasureTheory.exists_directional_set', MeasureTheory.exists_directional_set and MeasureTheory.exists_directional_basis: for discrete L and a compact convex neighbourhood s of 0, some finrank ℤ L independent vectors of L have their j-th member in the dilate of s by the j-th minimum; for a full lattice they form a real basis of E. They need not form a basis of L over ℤ.

References

The definition, its name and the statements of the lemmas follow the successive-minima proposal for Mathlib by Kevin H. Wilson, Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean at https://github.com/khwilson/mathlib4/blob/8423d1c878e50d8504a230ffd9b6ec76ce6a08eb/Mathlib/MeasureTheory/Group/GeometryOfNumbers.lean (Apache 2.0, by Alex J. Best, Yaël Dillies and Kevin H. Wilson).

noncomputable def MeasureTheory.successiveMin {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) (s : Set E) (i : ℕ) : NNReal

The i-th successive minimum of a set s around the origin with respect to a submodule L: the infimum of the r : ℝ≥0 such that r • s ∩ L spans a real subspace of dimension greater than i. The index is zero-based, so successiveMin L s 0 is the first minimum. At indices for which no such r exists, for instance beyond the dimension of E, its value is the junk value 0.

theorem MeasureTheory.successiveMin_def {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) (s : Set E) (i : ℕ) : successiveMin L s i = sInf {r : NNReal | i < Set.finrank ℝ (r • s ∩ ↑L)}

theorem MeasureTheory.successiveMin_le_of_lt_setFinrank {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} {r : NNReal} (hr : i < Set.finrank ℝ (r • s ∩ ↑L)) : successiveMin L s i ≤ r

A dilate r • s whose vectors of L span a real subspace of dimension greater than i bounds the i-th successive minimum from above.

@[simp]

theorem MeasureTheory.successiveMin_of_finrank_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] (hi : Module.finrank ℝ E ≤ i) : successiveMin L s i = 0

The successive minima vanish at every index at least the dimension of the ambient space.

@[simp]

theorem MeasureTheory.successiveMin_of_setFinrank_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] (hi : Set.finrank ℝ ↑L ≤ i) : successiveMin L s i = 0

The successive minima vanish at every index at least the real rank of L.

theorem MeasureTheory.successiveMin_of_finrank_int_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hi : Module.finrank ℤ ↥L ≤ i) : successiveMin L s i = 0

For a discrete L, the successive minima vanish at every index at least the integer rank of L.

theorem MeasureTheory.exists_lt_setFinrank_smul_inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hs : Absorbent ℝ s) (hi : i < Module.finrank ℤ ↥L) : ∃ (r : NNReal), i < Set.finrank ℝ (r • s ∩ ↑L)

Below the integer rank of a discrete L, some dilate of an absorbent set s contains vectors of L spanning a real subspace of dimension greater than i: the infimum defining successiveMin L s i is taken over a nonempty set.

theorem MeasureTheory.exists_lt_setFinrank_smul_inter_zLattice {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hs : Absorbent ℝ s) (hi : i < Module.finrank ℝ E) : ∃ (r : NNReal), i < Set.finrank ℝ (r • s ∩ ↑L)

For a full lattice L, the infimum defining successiveMin L s i is taken over a nonempty set at every index below the dimension of E.

theorem MeasureTheory.successiveMin_mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] {j : ℕ} (hs : Absorbent ℝ s) (hij : i ≤ j) (hj : j < Module.finrank ℤ ↥L) : successiveMin L s i ≤ successiveMin L s j

Monotonicity in the index. Below the integer rank of a discrete L, the successive minima of an absorbent set are nondecreasing. Beyond the rank they take the junk value 0.

theorem MeasureTheory.lt_setFinrank_smul_inter_of_successiveMin_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] {r : NNReal} (hsc : StarConvex ℝ 0 s) (hs : Absorbent ℝ s) (hi : i < Module.finrank ℤ ↥L) (hr : successiveMin L s i < r) : i < Set.finrank ℝ (r • s ∩ ↑L)

Below the integer rank of a discrete L, every dilate of an absorbent set s, star-convex about 0, by a factor strictly greater than the i-th successive minimum contains vectors of L spanning a real subspace of dimension greater than i.

theorem MeasureTheory.exists_linearIndependent_of_successiveMin_lt {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] {r : NNReal} (hsc : Convex ℝ s) (hs₀ : s ∈ nhds 0) (hi : i < Module.finrank ℤ ↥L) (hr : successiveMin L s i < r) : ∃ (v : Fin (i + 1) → ↥L), (∀ (j : Fin (i + 1)), ↑(v j) ∈ r • s ∩ ↑L) ∧ LinearIndependent ℤ v

Below the integer rank of a discrete L, every dilate of a convex neighbourhood s of 0 by a factor strictly greater than the i-th successive minimum contains i + 1 linearly independent vectors of L.

theorem MeasureTheory.lt_setFinrank_successiveMin_smul {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) (hi : i < Module.finrank ℤ ↥L) : i < Set.finrank ℝ (successiveMin L s i • s ∩ ↑L)

Attainment of the successive minima. Below the integer rank of a discrete L, the dilate of a compact convex neighbourhood s of 0 by its i-th successive minimum itself contains vectors of L spanning a real subspace of dimension greater than i: the infimum defining successiveMin L s i is a minimum. The set s need not be symmetric.

theorem MeasureTheory.setOf_lt_setFinrank_smul_inter_eq_Ici {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) (hi : i < Module.finrank ℤ ↥L) : {r : NNReal | i < Set.finrank ℝ (r • s ∩ ↑L)} = Set.Ici (successiveMin L s i)

The threshold set is a closed half-line. Below the integer rank of a discrete L, the factors r for which the vectors of L in the dilate r • s of a compact convex neighbourhood s of 0 span a real subspace of dimension greater than i are exactly those at least the i-th successive minimum.

theorem MeasureTheory.isClosed_setOf_lt_setFinrank_smul_inter {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {s : Set E} {i : ℕ} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) (hi : i < Module.finrank ℤ ↥L) : IsClosed {r : NNReal | i < Set.finrank ℝ (r • s ∩ ↑L)}

Below the integer rank of a discrete L, the set of factors r for which the vectors of L in the dilate r • s of a compact convex neighbourhood s of 0 span a real subspace of dimension greater than i is closed.

theorem MeasureTheory.exists_directional_set' {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {s : Set E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) : ∃ (v : Fin (Module.finrank ℤ ↥L) → E), (∀ (j : Fin (Module.finrank ℤ ↥L)), v j ∈ successiveMin L s ↑j • s ∩ ↑L) ∧ LinearIndependent ℝ v

A directional family. For a discrete L and a compact convex neighbourhood s of 0, there are finrank ℤ L real-linearly independent vectors of L whose j-th member lies in the dilate of s by the j-th successive minimum. They need not span L over ℤ; exists_directional_set restates them as an integrally independent family in L. The set s need not be symmetric.

theorem MeasureTheory.exists_directional_set {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {s : Set E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) : ∃ (v : Fin (Module.finrank ℤ ↥L) → ↥L), (∀ (j : Fin (Module.finrank ℤ ↥L)), ↑(v j) ∈ successiveMin L s ↑j • s) ∧ LinearIndependent ℤ v

A directional family in L. For a discrete L and a compact convex neighbourhood s of 0, there are finrank ℤ L linearly independent vectors of L whose j-th member lies in the dilate of s by the j-th successive minimum. They need not form a basis of L.

theorem MeasureTheory.exists_directional_basis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) {s : Set E} [FiniteDimensional ℝ E] [DiscreteTopology ↥L] [IsZLattice ℝ L] (hsc : Convex ℝ s) (hs : IsCompact s) (hs₀ : s ∈ nhds 0) : ∃ (b : Module.Basis (Fin (Module.finrank ℝ E)) ℝ E), ∀ (j : Fin (Module.finrank ℝ E)), b j ∈ successiveMin L s ↑j • s ∩ ↑L

A directional basis. For a full lattice L and a compact convex neighbourhood s of 0, some real basis of E consists of vectors of L whose j-th member lies in the dilate of s by the j-th successive minimum. It need not be a basis of L over ℤ.