theorem Lattices.blichfeldt {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 : MeasureTheory.NullMeasurableSet S μ) (hvol : ENNReal.ofReal (ZLattice.covolume L μ) < μ S) : ∃ z₁ ∈ S, ∃ z₂ ∈ S, z₁ ≠ z₂ ∧ z₁ - z₂ ∈ ↑L

theorem Lattices.minkowski {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) (h_symm : ∀ x ∈ S, -x ∈ S) (h_conv : Convex ℝ S) (hvol : ENNReal.ofReal (ZLattice.covolume L μ) * 2 ^ Module.finrank ℝ E < μ S) : ∃ x ∈ ↑L, x ≠ 0 ∧ x ∈ S

theorem Lattices.minkowski_shortest_vector_bound {n : ℕ} [NeZero n] (L : Submodule ℤ (Fin n → ℝ)) [DiscreteTopology ↥L] [IsZLattice ℝ L] : ∃ x ∈ ↑L, x ≠ 0 ∧ √(∑ i : Fin n, x i ^ 2) ≤ √↑n * ZLattice.covolume L MeasureTheory.volume ^ (1 / ↑n)

def Lattice2D.IsReducedBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) : Prop

def Lattice2D.IsLatticeVector {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v w : E) : Prop

theorem Lattice2D.norm_lattice_vec_ge_norm_u {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) (hred : IsReducedBasis u v) (a b : ℤ) (hab : ¬(a = 0 ∧ b = 0)) : ‖u‖ ≤ ‖↑a • u + ↑b • v‖

theorem Lattice2D.norm_lattice_vec_ge_norm_v {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) (hred : IsReducedBasis u v) (a b : ℤ) (hb : b ≠ 0) : ‖v‖ ≤ ‖↑a • u + ↑b • v‖

theorem Lattice2D.reduced_basis_successive_minima {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (u v : E) (_hu : u ≠ 0) (_hv : v ≠ 0) (_hli : LinearIndependent ℝ ![u, v]) (hred : IsReducedBasis u v) : (∀ (w : E), IsLatticeVector u v w → w ≠ 0 → ‖u‖ ≤ ‖w‖) ∧ ∀ (w : E), IsLatticeVector u v w → (∀ (c : ℝ), w ≠ c • u) → ‖v‖ ≤ ‖w‖

noncomputable def gramSchmidtCoeff {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : Fin n → E) (i k : Fin n) : ℝ

structure IsLLLReduced {n : ℕ} {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (f : Fin n → E) : Prop

• sizeReduced (i k : Fin n) : k < i → |gramSchmidtCoeff f i k| ≤ 1 / 2
• lovasz (i : Fin n) (hi : ↑i + 1 < n) : ‖InnerProductSpace.gramSchmidt ℝ f i‖ ^ 2 ≤ 4 / 3 * ‖InnerProductSpace.gramSchmidt ℝ f ⟨↑i + 1, hi⟩ + gramSchmidtCoeff f ⟨↑i + 1, hi⟩ i • InnerProductSpace.gramSchmidt ℝ f i‖ ^ 2