An orthonormal flag adapted to greedy lattice vectors. A small coordinate box in this flag contains no nonzero lattice vector.
theorem
CCDN.exists_orthonormal_basis_with_same_flag
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
[FiniteDimensional ℝ E]
{n : ℕ}
(b : Module.Basis (Fin n) ℝ E)
:
∃ (c : OrthonormalBasis (Fin n) ℝ E),
∀ (i : Fin n), Submodule.span ℝ (⇑c '' Set.Iio i) = Submodule.span ℝ (⇑b '' Set.Iio i)
Every basis b of a finite-dimensional real inner product space has an orthonormal basis c
(its Gram–Schmidt orthonormalisation) spanning the same flag: for each i, the vectors with
index < i of c and of b span the same subspace.
theorem
CCDN.lattice_flag_coordinate_box_zero
{E : Type u_1}
[NormedAddCommGroup E]
[InnerProductSpace ℝ E]
{n : ℕ}
(hn : 0 < n)
(L : Submodule ℤ E)
(c : OrthonormalBasis (Fin n) ℝ E)
(a : Fin n → ℝ)
(hpos : ∀ (i : Fin n), 0 < a i)
(hmono : Monotone a)
(hminimum : ∀ (i : Fin n), ∀ x ∈ L, x ∉ Submodule.span ℝ (⇑c '' Set.Iio i) → a i ≤ ‖x‖)
{x : E}
(hx : x ∈ L)
(hbox : ∀ (i : Fin n), |(c.toBasis.repr x) i| < a i / ↑n)
:
With side lengths equal to the flag minima divided by dimension, the open symmetric coordinate box has no nonzero lattice vector.