A lattice basis with a prescribed nonzero first vector. Every later vector is shortest outside the previous span. A given global lower bound replaces the first vector's norm in the monotone thresholds.

def CCDN.IsPrescribedGreedyLatticeFamily {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] (L : Submodule ℤ E) (w : E) {k : ℕ} (v : Fin (k + 1) → E) : Prop

A prescribed greedy lattice family: linearly independent vectors v of the lattice L with first vector v 0 = w, each later vector v i being a shortest vector of L outside the real span of the preceding vectors.

Equations

• One or more equations did not get rendered due to their size.

theorem CCDN.IsPrescribedGreedyLatticeFamily.first_eq {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {k : ℕ} {v : Fin (k + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) : v 0 = w

The first vector of a prescribed greedy family is the prescribed vector.

theorem CCDN.IsPrescribedGreedyLatticeFamily.mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {k : ℕ} {v : Fin (k + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) (i : Fin (k + 1)) : v i ∈ L

The vectors of a prescribed greedy family lie in the lattice.

theorem CCDN.IsPrescribedGreedyLatticeFamily.norm_le {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {k : ℕ} {v : Fin (k + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) {i : Fin (k + 1)} (hi : i ≠ 0) {x : E} (hx : x ∈ L) (hxU : x ∉ Submodule.span ℝ (v '' Set.Iio i)) : ‖v i‖ ≤ ‖x‖

Every later vector of a prescribed greedy family is a shortest lattice vector outside the span of the preceding ones.

theorem CCDN.exists_prescribed_greedy_lattice_basis {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] (L : Submodule ℤ E) [DiscreteTopology ↥L] [IsZLattice ℝ L] (w : E) (hw : w ∈ L) (hw0 : w ≠ 0) {n : ℕ} (hn : Module.finrank ℝ E = n + 1) : ∃ (b : Module.Basis (Fin (n + 1)) ℝ E), IsPrescribedGreedyLatticeFamily L w ⇑b

Every nonzero vector w of a full lattice L in a real space of dimension n + 1 is the first vector of a basis b of lattice vectors that forms a prescribed greedy lattice family.

def CCDN.prescribedLatticeMinima {E : Type u_1} [NormedAddCommGroup E] {n : ℕ} (v : Fin (n + 1) → E) (δ : ℝ) : Fin (n + 1) → ℝ

The successive thresholds of a prescribed greedy family v: the first is the given lower bound δ, and the i-th for i ≠ 0 is the norm ‖v i‖.

Equations

• CCDN.prescribedLatticeMinima v δ i = if i = 0 then δ else ‖v i‖

theorem CCDN.IsPrescribedGreedyLatticeFamily.minima_pos {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {n : ℕ} {v : Fin (n + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) {δ : ℝ} (hδ : 0 < δ) (i : Fin (n + 1)) : 0 < prescribedLatticeMinima v δ i

For a positive lower bound δ, all thresholds prescribedLatticeMinima v δ of a prescribed greedy lattice family are positive.

theorem CCDN.IsPrescribedGreedyLatticeFamily.minima_mono {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {n : ℕ} {v : Fin (n + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) {δ : ℝ} (hlower : ∀ x ∈ L, x ≠ 0 → δ ≤ ‖x‖) : Monotone (prescribedLatticeMinima v δ)

If δ is a lower bound for the norms of nonzero lattice vectors, then the thresholds prescribedLatticeMinima v δ of a prescribed greedy lattice family are monotone.

theorem CCDN.IsPrescribedGreedyLatticeFamily.minima_outside {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] {L : Submodule ℤ E} {w : E} {n : ℕ} {v : Fin (n + 1) → E} (hv : IsPrescribedGreedyLatticeFamily L w v) {δ : ℝ} (hlower : ∀ x ∈ L, x ≠ 0 → δ ≤ ‖x‖) (i : Fin (n + 1)) (x : E) : x ∈ L → x ∉ Submodule.span ℝ (v '' Set.Iio i) → prescribedLatticeMinima v δ i ≤ ‖x‖

If δ is a lower bound for the norms of nonzero lattice vectors, then every lattice vector outside the span of the vectors of index < i of a prescribed greedy lattice family has norm at least the i-th threshold prescribedLatticeMinima v δ i.

theorem CCDN.prescribedLatticeMinima_prod {E : Type u_1} [NormedAddCommGroup E] {n : ℕ} (v : Fin (n + 1) → E) {w : E} (hw : v 0 = w) {δ : ℝ} (hδ : δ ≠ 0) : ∏ i : Fin (n + 1), ‖v i‖ = ‖w‖ / δ * ∏ i : Fin (n + 1), prescribedLatticeMinima v δ i

The product of the norms ‖v i‖ equals ‖w‖ / δ times the product of the thresholds prescribedLatticeMinima v δ i, where v 0 = w and δ ≠ 0.