def IntegerProgramming.IP.IsFeasible {m n : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : Prop

def IntegerProgramming.Lattice (n : ℕ) (b : Fin n → EuclideanSpace ℝ (Fin n)) : Set (EuclideanSpace ℝ (Fin n))

theorem IntegerProgramming.lattice_approx_bound_sum {n : ℕ} (b : Fin n → EuclideanSpace ℝ (Fin n)) (h_sorted : ∀ (i j : Fin n), i ≤ j → ‖b i‖ ^ 2 ≤ ‖b j‖ ^ 2) (x : EuclideanSpace ℝ (Fin n)) : ∃ y ∈ Lattice n b, ‖x - y‖ ^ 2 ≤ 1 / 4 * ∑ i : Fin n, ‖b i‖ ^ 2

theorem IntegerProgramming.lattice_approx_bound_chain {n : ℕ} (hn : 0 < n) (b : Fin n → EuclideanSpace ℝ (Fin n)) (h_sorted : ∀ (i j : Fin n), i ≤ j → ‖b i‖ ^ 2 ≤ ‖b j‖ ^ 2) (x : EuclideanSpace ℝ (Fin n)) : ∃ y ∈ Lattice n b, ‖x - y‖ ^ 2 ≤ 1 / 4 * ∑ i : Fin n, ‖b i‖ ^ 2 ∧ ‖x - y‖ ^ 2 ≤ ↑n / 4 * ‖b ⟨n - 1, ⋯⟩‖ ^ 2

noncomputable def IntegerProgramming.layerSpacingBound (m : ℕ) : ℝ

theorem IntegerProgramming.layerSpacingBound_pos {m : ℕ} (hm : 0 < m) : 0 < layerSpacingBound m

noncomputable def IntegerProgramming.fritzJohnRadius (n : ℕ) : ℝ

noncomputable def IntegerProgramming.layerCountBound (k : ℕ) : ℕ

theorem IntegerProgramming.layerCountBound_pos (k : ℕ) : 0 < layerCountBound k

def IntegerProgramming.lenstraBound : ℕ → ℕ

theorem IntegerProgramming.lenstraBound_pos (n : ℕ) : 0 < lenstraBound n

theorem IntegerProgramming.layerCountBound_ge_ceil_ratio (k : ℕ) (hk : 0 < k) : ↑(layerCountBound k) ≥ 2 * fritzJohnRadius k / layerSpacingBound k

noncomputable def IntegerProgramming.candidateBox (n : ℕ) : Finset (Fin n → ℤ)

theorem IntegerProgramming.candidateBox_card (n : ℕ) : (candidateBox n).card = (2 * lenstraBound n + 1) ^ n

theorem IntegerProgramming.fritz_john_lll_geometric_containment {n : ℕ} (hn : 0 < n) {m : ℕ} (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) (hfeas : IP.IsFeasible A b) : ∃ (basis : Fin n → EuclideanSpace ℝ (Fin n)) (P : EuclideanSpace ℝ (Fin n)), IsLLLReduced basis ∧ (∀ (i j : Fin n), i ≤ j → ‖basis i‖ ^ 2 ≤ ‖basis j‖ ^ 2) ∧ ‖basis ⟨n - 1, ⋯⟩‖ ≥ 2 / √↑n ∧ ∀ (x : Fin n → ℤ), A.mulVec (Int.cast ∘ x) ≤ b → ∑ i : Fin n, ↑(x i) • basis i ∈ Metric.ball P (fritzJohnRadius n)

theorem IntegerProgramming.layerCountBound_le_lenstraBound (k n : ℕ) (hk : k ≤ n) : layerCountBound k ≤ lenstraBound n

theorem IntegerProgramming.lattice_coord_projection_bound {n : ℕ} (hn : 0 < n) (basis : Fin n → EuclideanSpace ℝ (Fin n)) (P : EuclideanSpace ℝ (Fin n)) (hred : IsLLLReduced basis) (hsorted : ∀ (i j : Fin n), i ≤ j → ‖basis i‖ ^ 2 ≤ ‖basis j‖ ^ 2) (hbn : ‖basis ⟨n - 1, ⋯⟩‖ ≥ 2 / √↑n) (c : Fin n → ℤ) (hball : ∑ i : Fin n, ↑(c i) • basis i ∈ Metric.ball P (fritzJohnRadius n)) (i : Fin n) : |↑(c i)| * layerSpacingBound n ≤ fritzJohnRadius n

theorem IntegerProgramming.lattice_coord_bound_in_ball {n : ℕ} (hn : 0 < n) (basis : Fin n → EuclideanSpace ℝ (Fin n)) (P : EuclideanSpace ℝ (Fin n)) (hred : IsLLLReduced basis) (hsorted : ∀ (i j : Fin n), i ≤ j → ‖basis i‖ ^ 2 ≤ ‖basis j‖ ^ 2) (hbn : ‖basis ⟨n - 1, ⋯⟩‖ ≥ 2 / √↑n) (c : Fin n → ℤ) (hball : ∑ i : Fin n, ↑(c i) • basis i ∈ Metric.ball P (fritzJohnRadius n)) (i : Fin n) : |c i| ≤ ↑(lenstraBound n)

theorem IntegerProgramming.lenstra_solution_in_candidateBox (n m : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : IP.IsFeasible A b → ∃ x ∈ candidateBox n, A.mulVec (Int.cast ∘ x) ≤ b

theorem IntegerProgramming.lenstra_ip_fpt (n m : ℕ) (A : Matrix (Fin m) (Fin n) ℝ) (b : Fin m → ℝ) : (candidateBox n).card ≤ (2 * lenstraBound n + 1) ^ n ∧ (IP.IsFeasible A b → ∃ x ∈ candidateBox n, A.mulVec (Int.cast ∘ x) ≤ b)