Shortest lattice vectors, greedy flags and Blichfeldt's bound

Main results

• ZLattice.exists_shortest_vector_notMem: if a real subspace U of a finite-dimensional normed space does not contain the full-rank lattice L, some vector of L outside U has minimal norm among the vectors of L outside U. Iterating this gives the greedy successive-minima flag of L.
• ZLattice.measureReal_le_covolume: Blichfeldt's principle; a measurable set whose distinct points never differ by a lattice vector has volume at most the covolume.

The greedy flag is built one vector at a time with Fin.snoc; the following lemmas describe the initial segments of such a tuple, and count the pairs of its indices:

• Fin.snoc_image_Iio_castSucc: Fin.snoc v x '' Set.Iio i.castSucc = v '' Set.Iio i.
• Fin.snoc_image_Iio_last: Fin.snoc v x '' Set.Iio (Fin.last k) = Set.range v.
• Fin.sum_card_Ioi: there are n.choose 2 pairs i < j in Fin n.

theorem Fin.snoc_image_Iio_castSucc {α : Type u_1} {k : ℕ} (v : Fin k → α) (x : α) (i : Fin k) : snoc v x '' Set.Iio i.castSucc = v '' Set.Iio i

Below i.castSucc, Fin.snoc v x takes the same values as v below i.

theorem Fin.snoc_image_Iio_last {α : Type u_1} {k : ℕ} (v : Fin k → α) (x : α) : snoc v x '' Set.Iio (last k) = Set.range v

Below Fin.last k, Fin.snoc v x takes exactly the values of v.

theorem Fin.sum_card_Ioi (n : ℕ) : ∑ i : Fin n, (Finset.Ioi i).card = n.choose 2

Counting the pairs i < j in Fin n by their smaller element gives n.choose 2.

theorem ZLattice.exists_shortest_vector_notMem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (U : Submodule ℝ E) (hU : U ≠ ⊤) : ∃ v ∈ L, v ∉ U ∧ ∀ x ∈ L, x ∉ U → ‖v‖ ≤ ‖x‖

If a real subspace U does not contain the full-rank lattice L, some lattice vector outside U has minimal norm among all lattice vectors outside U.

theorem ZLattice.measureReal_le_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) [μ.IsAddHaarMeasure] {S : Set E} (hS : MeasurableSet S) (hsep : ∀ x ∈ S, ∀ y ∈ S, x - y ∈ L → x = y) : μ.real S ≤ covolume L μ

Blichfeldt's principle: a measurable set whose distinct points never differ by a lattice vector has volume at most the covolume of the lattice.