noncomputable def LLL.gramSchmidtVec {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) : Fin n → E

noncomputable def LLL.gramSchmidtCoeff {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) (i j : Fin n) : ℝ

def LLL.IsSizeReduced {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) : Prop

def LLL.SatisfiesLovász {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) : Prop

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

• size_reduced : IsSizeReduced b
• lovász : SatisfiesLovász b

theorem LLL.gramSchmidtVec_norm_sq_half {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) (hred : IsLLLReduced b) (i : Fin n) (hi : ↑i + 1 < n) : ‖gramSchmidtVec b ⟨↑i + 1, hi⟩‖ ^ 2 ≥ 1 / 2 * ‖gramSchmidtVec b i‖ ^ 2

theorem LLL.gramSchmidtVec_norm_sq_geometric {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin (n + 1) → E) (hred : IsLLLReduced b) (j : ℕ) (hj : j < n + 1) : ‖gramSchmidtVec b ⟨j, hj⟩‖ ^ 2 ≥ (1 / 2) ^ j * ‖gramSchmidtVec b 0‖ ^ 2

theorem LLL.gramSchmidtVec_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin (n + 1) → E) : gramSchmidtVec b 0 = b 0

theorem LLL.lattice_norm_ge_min_gramSchmidt_norm {n : ℕ} {E : Type u_2} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (b : Fin (n + 1) → E) (v : E) (hv : v ≠ 0) (hv_in : ∃ (c : Fin (n + 1) → ℤ), v = ∑ i : Fin (n + 1), ↑(c i) • b i) : ∃ (i : Fin (n + 1)), ‖gramSchmidtVec b i‖ ≤ ‖v‖

theorem LLL.lll_short_vector_bound {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin (n + 1) → E) (hred : IsLLLReduced b) (v : E) (hv : v ≠ 0) (hv_in : ∃ (c : Fin (n + 1) → ℤ), v = ∑ i : Fin (n + 1), ↑(c i) • b i) : ‖b 0‖ ^ 2 ≤ 2 ^ n * ‖v‖ ^ 2

theorem LLL.lll_shortest_vector_approx {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin (n + 1) → E) (hred : IsLLLReduced b) (lam₁ : ℝ) (hlam₁ : lam₁ > 0) (hlam₁_achieved : ∃ (v : E), v ≠ 0 ∧ (∃ (c : Fin (n + 1) → ℤ), v = ∑ i : Fin (n + 1), ↑(c i) • b i) ∧ ‖v‖ = lam₁) : ‖b 0‖ ≤ 2 ^ (↑n / 2) * lam₁

theorem LLL.reduced_basis_bounds_lemma5 {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (hn : 0 < n) (b : Fin n → E) (hb_reduced : IsLLLReduced b) (det_L : ℝ) (hdet : det_L > 0) (hdet_eq : det_L = ∏ i : Fin n, ‖gramSchmidtVec b i‖) : ∏ i : Fin n, ‖b i‖ ≤ 2 ^ (↑n * (↑n - 1) / 4) * det_L ∧ have H := ↑(Submodule.span ℝ (b '' {i : Fin n | ↑i < n - 1})); have last := ⟨n - 1, ⋯⟩; 2 ^ (-(↑n * (↑n - 1) / 4)) * ‖b last‖ ≤ Metric.infDist (b last) H ∧ Metric.infDist (b last) H ≤ ‖b last‖

def LLL.SatisfiesLovászOriginal {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) : Prop

structure LLL.IsReducedBasis {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {n : ℕ} (b : Fin n → E) : Prop

• size_reduced : IsSizeReduced b
• lovász_original : SatisfiesLovászOriginal b