Theory LLL_Number_Bounds
subsection ‹Explicit Bounds for Size of Numbers that Occur During LLL Algorithm›
text ‹The LLL invariant does not contain bounds on the number that occur during the execution.
We here strengthen the invariant so that it enforces bounds on the norms of the $f_i$ and $g_i$
and we prove that the stronger invariant is maintained throughout the execution of the LLL algorithm.
Based on the stronger invariant we prove bounds on the absolute values of the $\mu_{i,j}$,
and on the absolute values of the numbers in the vectors $f_i$ and $g_i$.
Moreover, we further show that also the denominators in all of these numbers doesn't grow to much.
Finally, we prove that each number (i.e., numerator or denominator) during the execution
can be represented with at most ${\cal O}(m \cdot \log(M \cdot n))$ bits, where
$m$ is the number of input vectors, $n$ is the dimension of the input vectors,
and $M$ is the maximum absolute value of all numbers in the input vectors.
Hence, each arithmetic operation in the LLL algorithm can be performed in polynomial time.›
theory LLL_Number_Bounds
imports LLL
Gram_Schmidt_Int
begin
context LLL
begin
text ‹The bounds for the $f_i$ distinguishes whether we are inside or outside the inner for-loop.›
definition f_bound :: "bool ⇒ nat ⇒ int vec list ⇒ bool" where
"f_bound outside ii fs = (∀ i < m. sq_norm (fs ! i) ≤ (if i ≠ ii ∨ outside then int (N * m) else
int (4 ^ (m - 1) * N ^ m * m * m)))"
definition g_bnd :: "rat ⇒ int vec list ⇒ bool" where
"g_bnd B fs = (∀ i < m. sq_norm (gso fs i) ≤ B)"
definition "μ_bound_row fs bnd i = (∀ j ≤ i. (μ fs i j)^2 ≤ bnd)"
abbreviation "μ_bound_row_inner fs i j ≡ μ_bound_row fs (4 ^ (m - 1 - j) * of_nat (N ^ (m - 1) * m)) i"
definition "LLL_bound_invariant outside upw i fs =
(LLL_invariant upw i fs ∧ f_bound outside i fs ∧ g_bound fs)"
lemma bound_invD: assumes "LLL_bound_invariant outside upw i fs"
shows "LLL_invariant upw i fs" "f_bound outside i fs" "g_bound fs"
using assms unfolding LLL_bound_invariant_def by auto
lemma bound_invI: assumes "LLL_invariant upw i fs" "f_bound outside i fs" "g_bound fs"
shows "LLL_bound_invariant outside upw i fs"
using assms unfolding LLL_bound_invariant_def by auto
lemma μ_bound_rowI: assumes "⋀ j. j ≤ i ⟹ (μ fs i j)^2 ≤ bnd"
shows "μ_bound_row fs bnd i"
using assms unfolding μ_bound_row_def by auto
lemma μ_bound_rowD: assumes "μ_bound_row fs bnd i" "j ≤ i"
shows "(μ fs i j)^2 ≤ bnd"
using assms unfolding μ_bound_row_def by auto
lemma μ_bound_row_1: assumes "μ_bound_row fs bnd i"
shows "bnd ≥ 1"
proof -
interpret gs1: gram_schmidt_fs n "RAT fs" .
show ?thesis
using μ_bound_rowD[OF assms, of i]
by (auto simp: gs1.μ.simps)
qed
lemma reduced_μ_bound_row: assumes red: "reduced fs i"
and ii: "ii < i"
shows "μ_bound_row fs 1 ii"
proof (intro μ_bound_rowI)
fix j
assume "j ≤ ii"
interpret gs1: gram_schmidt_fs n "RAT fs" .
show "(μ fs ii j)^2 ≤ 1"
proof (cases "j < ii")
case True
from red[unfolded gram_schmidt_fs.reduced_def, THEN conjunct2, rule_format, OF ii True]
have "abs (μ fs ii j) ≤ 1/2" by auto
from mult_mono[OF this this]
show ?thesis by (auto simp: power2_eq_square)
qed (auto simp: gs1.μ.simps)
qed
lemma f_bound_True_arbitrary: assumes "f_bound True ii fs"
shows "f_bound outside j fs"
unfolding f_bound_def
proof (intro allI impI, rule ccontr, goal_cases)
case (1 i)
from 1 have nz: "∥fs ! i∥⇧2 ≠ 0" by (auto split: if_splits)
hence gt: "∥fs ! i∥⇧2 > 0" using sq_norm_vec_ge_0[of "fs ! i"] by auto
from assms(1)[unfolded f_bound_def, rule_format, OF 1(1)]
have one: "∥fs ! i∥⇧2 ≤ int (N * m) * 1" by auto
from less_le_trans[OF gt one] have N0: "N ≠ 0" by (cases "N = 0", auto)
note one
also have "int (N * m) * 1 ≤ int (N * m) * int (4 ^ (m - 1) * N ^ (m - 1) * m)"
by (rule mult_left_mono, unfold of_nat_mult, intro mult_ge_one, insert 1 N0, auto)
also have "… = int (4 ^ (m - 1) * N ^ (Suc (m - 1)) * m * m)" unfolding of_nat_mult by simp
also have "Suc (m - 1) = m" using 1 by simp
finally show ?case using one 1 by (auto split: if_splits)
qed
context fixes fs :: "int vec list"
assumes lin_indep: "lin_indep fs"
and len: "length fs = m"
begin
interpretation fs: fs_int_indpt n fs
by (standard) (use lin_indep in simp)
lemma sq_norm_fs_mu_g_bound: assumes i: "i < m"
and mu_bound: "μ_bound_row fs bnd i"
and g_bound: "g_bound fs"
shows "of_int ∥fs ! i∥⇧2 ≤ of_nat (Suc i * N) * bnd"
proof -
have "of_int ∥fs ! i∥⇧2 = (∑j←[0..<Suc i]. (μ fs i j)⇧2 * ∥gso fs j∥⇧2)"
by (rule fs.sq_norm_fs_via_sum_mu_gso) (use assms lin_indep len in auto)
also have "… ≤ (∑j←[0..<Suc i]. bnd * of_nat N)"
proof (rule sum_list_ge_mono, force, unfold length_map length_upt,
subst (1 2) nth_map_upt, force, goal_cases)
case (1 j)
hence ji: "j ≤ i" by auto
from g_bound[unfolded g_bound_def] i ji
have GB: "sq_norm (gso fs j) ≤ of_nat N" by auto
show ?case
by (rule mult_mono, insert μ_bound_rowD[OF mu_bound ji]
GB order.trans[OF zero_le_power2], auto)
qed
also have "… = of_nat (Suc i) * (bnd * of_nat N)" unfolding sum_list_triv length_upt by simp
also have "… = of_nat (Suc i * N) * bnd" unfolding of_nat_mult by simp
finally show ?thesis .
qed
end
lemma increase_i_bound: assumes LLL: "LLL_bound_invariant True upw i fs"
and i: "i < m"
and upw: "upw ⟹ i = 0"
and red_i: "i ≠ 0 ⟹ sq_norm (gso fs (i - 1)) ≤ α * sq_norm (gso fs i)"
shows "LLL_bound_invariant True True (Suc i) fs"
proof -
from bound_invD[OF LLL] have LLL: "LLL_invariant upw i fs"
and "f_bound True i fs" and gbnd: "g_bound fs" by auto
hence fbnd: "f_bound True (Suc i) fs" by (auto simp: f_bound_def)
from increase_i[OF LLL i upw red_i]
have inv: "LLL_invariant True (Suc i) fs" and "LLL_measure (Suc i) fs < LLL_measure i fs" (is ?g2)
by auto
show "LLL_bound_invariant True True (Suc i) fs"
by (rule bound_invI[OF inv fbnd gbnd])
qed
text ‹Addition step preserves @{term "LLL_bound_invariant False"}›
lemma basis_reduction_add_row_main_bound: assumes Linv: "LLL_bound_invariant False True i fs"
and i: "i < m" and j: "j < i"
and c: "c = round (μ fs i j)"
and fs': "fs' = fs[ i := fs ! i - c ⋅⇩v fs ! j]"
and mu_small: "μ_small_row i fs (Suc j)"
and mu_bnd: "μ_bound_row_inner fs i (Suc j)"
shows "LLL_bound_invariant False True i fs'"
"μ_bound_row_inner fs' i j"
proof (rule bound_invI)
from bound_invD[OF Linv]
have Linv: "LLL_invariant True i fs" and fbnd: "f_bound False i fs" and gbnd: "g_bound fs"
by auto
note Linvw = LLL_inv_imp_w[OF Linv]
note main = basis_reduction_add_row_main[OF Linvw i j fs']
note main = main(2)[OF Linv] main(3,5-)
note main = main(1) main(2)[OF c mu_small] main(3-)
show Linv': "LLL_invariant True i fs'" by fact
define bnd :: rat where bnd: "bnd = 4 ^ (m - 1 - Suc j) * of_nat (N ^ (m - 1) * m)"
note mu_bnd = mu_bnd[folded bnd]
note inv = LLL_invD[OF Linv]
let ?mu = "μ fs"
let ?mu' = "μ fs'"
from j have "j ≤ i" by simp
let ?R = rat_of_int
have mu_bound_factor: "μ_bound_row fs' (4 * bnd) i"
proof (intro μ_bound_rowI)
fix k
assume ki: "k ≤ i"
from μ_bound_rowD[OF mu_bnd] have bnd_i: "⋀ j. j ≤ i ⟹ (?mu i j)^2 ≤ bnd" by auto
have bnd_ik: "(?mu i k)⇧2 ≤ bnd" using bnd_i[OF ki] by auto
have bnd_ij: "(?mu i j)⇧2 ≤ bnd" using bnd_i[OF ‹j ≤ i›] by auto
from μ_bound_row_1[OF mu_bnd] have bnd1: "bnd ≥ 1" "bnd ≥ 0" by auto
show "(?mu' i k)⇧2 ≤ 4 * bnd"
proof (cases "k > j")
case True
show ?thesis
by (subst main(5), (insert True ki i bnd1, auto)[3], intro order.trans[OF bnd_ik], auto)
next
case False
hence kj: "k ≤ j" by auto
show ?thesis
proof (cases "k = j")
case True
have small: "abs (?mu' i k) ≤ 1/2" using main(2) j unfolding True μ_small_row_def by auto
show ?thesis using mult_mono[OF small small] using bnd1
by (auto simp: power2_eq_square)
next
case False
with kj have k_j: "k < j" by auto
define M where "M = max (abs (?mu i k)) (max (abs (?mu i j)) (1/2))"
have M0: "M ≥ 0" unfolding M_def by auto
let ?new_mu = "?mu i k - ?R c * ?mu j k"
have "abs ?new_mu ≤ abs (?mu i k) + abs (?R c * ?mu j k)" by simp
also have "… = abs (?mu i k) + abs (?R c) * abs (?mu j k)" unfolding abs_mult ..
also have "… ≤ abs (?mu i k) + (abs (?mu i j) + 1/2) * (1/2)"
proof (rule add_left_mono[OF mult_mono], unfold c)
show "¦?R (round (?mu i j))¦ ≤ ¦?mu i j¦ + 1 / 2" unfolding round_def by linarith
from inv(10)[unfolded gram_schmidt_fs.reduced_def, THEN conjunct2, rule_format, OF ‹j < i› k_j]
show "¦?mu j k¦ ≤ 1/2" .
qed auto
also have "… ≤ M + (M + M) * (1/2)"
by (rule add_mono[OF _ mult_right_mono[OF add_mono]], auto simp: M_def)
also have "… = 2 * M" by auto
finally have le: "abs ?new_mu ≤ 2 * M" .
have "(?mu' i k)⇧2 = ?new_mu⇧2"
by (subst main(5), insert kj False i j, auto)
also have "… ≤ (2 * M)^2" unfolding abs_le_square_iff[symmetric] using le M0 by auto
also have "… = 4 * M^2" by simp
also have "… ≤ 4 * bnd"
proof (rule mult_left_mono)
show "M^2 ≤ bnd" using bnd_ij bnd_ik bnd1 unfolding M_def
by (auto simp: max_def power2_eq_square)
qed auto
finally show ?thesis .
qed
qed
qed
also have "4 * bnd = (4 ^ (1 + (m - 1 - Suc j)) * of_nat (N ^ (m - 1) * m))" unfolding bnd
by simp
also have "1 + (m - 1 - Suc j) = m - 1 - j" using i j by auto
finally show bnd: "μ_bound_row_inner fs' i j" by auto
show gbnd: "g_bound fs'" using gbnd unfolding g_bound_def
using main(4) by auto
note inv' = LLL_invD[OF Linv']
show "f_bound False i fs'"
unfolding f_bound_def
proof (intro allI impI, goal_cases)
case (1 jj)
show ?case
proof (cases "jj = i")
case False
with 1 fbnd[unfolded f_bound_def] have "∥fs ! jj∥⇧2 ≤ int (N * m)" by auto
thus ?thesis unfolding fs' using False 1 inv(2-) by auto
next
case True
have "of_int ∥fs' ! i∥⇧2 = ∥RAT fs' ! i∥⇧2" using i inv' by (auto simp: sq_norm_of_int)
also have "... ≤ rat_of_nat (Suc i * N) * (4 ^ (m - 1 - j) * rat_of_nat (N ^ (m - 1) * m))"
using sq_norm_fs_mu_g_bound[OF inv'(1,6) i bnd gbnd] i inv'
unfolding sq_norm_of_int[symmetric]
by (auto simp: ac_simps)
also have "… = rat_of_int ( int (Suc i * N) * (4 ^ (m - 1 - j) * (N ^ (m - 1) * m)))"
by simp
finally have "∥fs' ! i∥⇧2 ≤ int (Suc i * N) * (4 ^ (m - 1 - j) * (N ^ (m - 1) * m))" by linarith
also have "… = int (Suc i) * 4 ^ (m - 1 - j) * (int N ^ (Suc (m - 1))) * int m"
unfolding of_nat_mult by (simp add: ac_simps)
also have "… = int (Suc i) * 4 ^ (m - 1 - j) * int N ^ m * int m" using i j by simp
also have "… ≤ int m * 4 ^ (m - 1) * int N ^ m * int m"
by (rule mult_right_mono[OF mult_right_mono[OF mult_mono[OF _ pow_mono_exp]]], insert i, auto)
finally have "∥fs' ! i∥⇧2 ≤ int (4 ^ (m - 1) * N ^ m * m * m)" unfolding of_nat_mult by (simp add: ac_simps)
thus ?thesis unfolding True by auto
qed
qed
qed
end
context LLL_with_assms
begin
subsubsection ‹@{const LLL_bound_invariant} is maintained during execution of @{const reduce_basis}›
lemma basis_reduction_add_rows_enter_bound: assumes binv: "LLL_bound_invariant True True i fs"
and i: "i < m"
shows "LLL_bound_invariant False True i fs"
"μ_bound_row_inner fs i i"
proof (rule bound_invI)
from bound_invD[OF binv]
have Linv: "LLL_invariant True i fs" (is ?g1) and fbnd: "f_bound True i fs"
and gbnd: "g_bound fs" by auto
note Linvw = LLL_inv_imp_w[OF Linv]
interpret fs: fs_int' n m fs_init fs
by standard (use Linvw in auto)
note inv = LLL_invD[OF Linv]
show "LLL_invariant True i fs" by fact
show fbndF: "f_bound False i fs" using f_bound_True_arbitrary[OF fbnd] .
have N0: "N > 0" using LLL_inv_N_pos[OF Linvw gbnd] i by auto
{
fix j
assume ji: "j < i"
have "(μ fs i j)⇧2 ≤ gs.Gramian_determinant (RAT fs) j * ∥RAT fs ! i∥⇧2"
using ji i inv by (intro fs.gs.mu_bound_Gramian_determinant) (auto)
also have "gs.Gramian_determinant (RAT fs) j = of_int (d fs j)" unfolding d_def
by (subst fs.of_int_Gramian_determinant, insert ji i inv(2-), auto simp: set_conv_nth)
also have "∥RAT fs ! i∥⇧2 = of_int ∥fs ! i∥⇧2" using i inv(2-) by (auto simp: sq_norm_of_int)
also have "of_int (d fs j) * … ≤ rat_of_nat (N^j) * of_int ∥fs ! i∥⇧2"
by (rule mult_right_mono, insert ji i d_approx[OF Linvw gbnd, of j], auto)
also have "… ≤ rat_of_nat (N^(m-2)) * of_int (int (N * m))"
by (intro mult_mono, unfold of_nat_le_iff of_int_le_iff, rule pow_mono_exp,
insert fbnd[unfolded f_bound_def, rule_format, of i] N0 ji i, auto)
also have "… = rat_of_nat (N^(m-2) * N * m)" by simp
also have "N^(m-2) * N = N^(Suc (m - 2))" by simp
also have "Suc (m - 2) = m - 1" using ji i by auto
finally have "(μ fs i j)⇧2 ≤ of_nat (N ^ (m - 1) * m)" .
} note mu_bound = this
show mu_bnd: "μ_bound_row_inner fs i i"
proof (rule μ_bound_rowI)
fix j
assume j: "j ≤ i"
have "(μ fs i j)⇧2 ≤ 1 * of_nat (N ^ (m - 1) * m)"
proof (cases "j = i")
case False
with mu_bound[of j] j show ?thesis by auto
next
case True
show ?thesis unfolding True fs.gs.μ.simps using i N0 by auto
qed
also have "… ≤ 4 ^ (m - 1 - i) * of_nat (N ^ (m - 1) * m)"
by (rule mult_right_mono, auto)
finally show "(μ fs i j)⇧2 ≤ 4 ^ (m - 1 - i) * rat_of_nat (N ^ (m - 1) * m)" .
qed
show "g_bound fs" by fact
qed
lemma basis_basis_reduction_add_rows_loop_leave:
assumes binv: "LLL_bound_invariant False True i fs"
and mu_small: "μ_small_row i fs 0"
and mu_bnd: "μ_bound_row_inner fs i 0"
and i: "i < m"
shows "LLL_bound_invariant True False i fs"
proof -
note Linv = bound_invD(1)[OF binv]
from mu_small have mu_small: "μ_small fs i" unfolding μ_small_row_def μ_small_def by auto
note inv = LLL_invD[OF Linv]
interpret gs1: gram_schmidt_fs_int n "RAT fs"
by (standard) (use inv gs.lin_indpt_list_def in ‹auto simp add: vec_hom_Ints›)
note fbnd = bound_invD(2)[OF binv]
note gbnd = bound_invD(3)[OF binv]
{
fix ii
assume ii: "ii < m"
have "∥fs ! ii∥⇧2 ≤ int (N * m)"
proof (cases "ii = i")
case False
thus ?thesis using ii fbnd[unfolded f_bound_def] by auto
next
case True
have row: "μ_bound_row fs 1 i"
proof (intro μ_bound_rowI)
fix j
assume j: "j ≤ i"
from mu_small[unfolded μ_small_def, rule_format, of j]
have "abs (μ fs i j) ≤ 1" using j unfolding μ_small_def by (cases "j = i", force simp: gs1.μ.simps, auto)
from mult_mono[OF this this] show "(μ fs i j)⇧2 ≤ 1" by (auto simp: power2_eq_square)
qed
have "rat_of_int ∥fs ! i∥⇧2 ≤ rat_of_int (int (Suc i * N))"
using sq_norm_fs_mu_g_bound[OF inv(1,6) i row gbnd] by auto
hence "∥fs ! i∥⇧2 ≤ int (Suc i * N)" by linarith
also have "… = int N * int (Suc i)" unfolding of_nat_mult by simp
also have "… ≤ int N * int m"
by (rule mult_left_mono, insert i, auto)
also have "… = int (N * m)" by simp
finally show ?thesis unfolding True .
qed
}
hence f_bound: "f_bound True i fs" unfolding f_bound_def by auto
with binv show ?thesis using basis_reduction_add_row_done[OF Linv i assms(2)]
by (auto simp: LLL_bound_invariant_def)
qed
lemma basis_reduction_add_rows_loop_bound: assumes
binv: "LLL_bound_invariant False True i fs"
and mu_small: "μ_small_row i fs j"
and mu_bnd: "μ_bound_row_inner fs i j"
and res: "basis_reduction_add_rows_loop i fs j = fs'"
and i: "i < m"
and j: "j ≤ i"
shows "LLL_bound_invariant True False i fs'"
using assms
proof (induct j arbitrary: fs)
case (0 fs)
note binv = 0(1)
from basis_basis_reduction_add_rows_loop_leave[OF 0(1-3) i] 0(4)
show ?case by auto
next
case (Suc j fs)
note binv = Suc(2)
note Linv = bound_invD(1)[OF binv]
note Linvw = LLL_inv_imp_w[OF Linv]
from Suc have j: "j < i" by auto
let ?c = "round (μ fs i j)"
note step = basis_reduction_add_row_main_bound[OF Suc(2) i j refl refl Suc(3-4)]
note step' = basis_reduction_add_row_main(2,3,5)[OF Linvw i j refl]
note step' = step'(1)[OF Linv] step'(2-)
show ?case
proof (cases "?c = 0")
case True
note inv = LLL_invD[OF Linv]
from inv(5)[OF i] inv(5)[of j] i j
have id: "fs[i := fs ! i - 0 ⋅⇩v fs ! j] = fs"
by (intro nth_equalityI, insert inv i, auto)
show ?thesis
by (rule Suc(1), insert step step' id True Suc(2-), auto)
next
case False
show ?thesis using Suc(1)[OF step(1) step'(2) step(2)] Suc(2-) False step'(3) by auto
qed
qed
lemma basis_reduction_add_rows_bound: assumes
binv: "LLL_bound_invariant True upw i fs"
and res: "basis_reduction_add_rows upw i fs = fs'"
and i: "i < m"
shows "LLL_bound_invariant True False i fs'"
proof -
note def = basis_reduction_add_rows_def
show ?thesis
proof (cases upw)
case False
with res binv show ?thesis by (simp add: def)
next
case True
with binv have binv: "LLL_bound_invariant True True i fs" by auto
note start = basis_reduction_add_rows_enter_bound[OF this i]
from res[unfolded def] True
have "basis_reduction_add_rows_loop i fs i = fs'" by auto
from basis_reduction_add_rows_loop_bound[OF start(1) μ_small_row_refl start(2) this i le_refl]
show ?thesis by auto
qed
qed
lemma g_bnd_swap:
assumes i: "i < m" "i ≠ 0"
and Linv: "LLL_invariant_weak fs"
and mu_F1_i: "¦μ fs i (i-1)¦ ≤ 1 / 2"
and cond: "sq_norm (gso fs (i - 1)) > α * sq_norm (gso fs i)"
and fs'_def: "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]"
and g_bnd: "g_bnd B fs"
shows "g_bnd B fs'"
proof -
note inv = LLL_inv_wD[OF Linv]
have choice: "fs' ! k = fs ! k ∨ fs' ! k = fs ! i ∨ fs' ! k = fs ! (i - 1)" for k
unfolding fs'_def using i inv(6) by (cases "k = i"; cases "k = i - 1", auto)
let ?g1 = "λ i. gso fs i"
let ?g2 = "λ i. gso fs' i"
let ?n1 = "λ i. sq_norm (?g1 i)"
let ?n2 = "λ i. sq_norm (?g2 i)"
from g_bnd[unfolded g_bnd_def] have short: "⋀ k. k < m ⟹ ?n1 k ≤ B" by auto
from short[of "i - 1"] i
have short_im1: "?n1 (i - 1) ≤ B" by auto
note swap = basis_reduction_swap_main[OF Linv disjI2[OF mu_F1_i] i cond fs'_def]
note updates = swap(4,5)
note Linv' = swap(1)
note inv' = LLL_inv_wD[OF Linv']
note inv = LLL_inv_wD[OF Linv]
interpret gs1: gram_schmidt_fs_int n "RAT fs"
by (standard) (use inv gs.lin_indpt_list_def in ‹auto simp add: vec_hom_Ints›)
interpret gs2: gram_schmidt_fs_int n "RAT fs'"
by (standard) (use inv' gs.lin_indpt_list_def in ‹auto simp add: vec_hom_Ints›)
let ?mu1 = "μ fs"
let ?mu2 = "μ fs'"
let ?mu = "?mu1 i (i - 1)"
have mu: "abs ?mu ≤ 1/2" using mu_F1_i .
have "?n2 (i - 1) = ?n1 i + ?mu * ?mu * ?n1 (i - 1)"
by (subst updates(2), insert i, auto)
also have "… = inverse α * (α * ?n1 i) + (?mu * ?mu) * ?n1 (i - 1)"
using α by auto
also have "… ≤ inverse α * ?n1 (i - 1) + (abs ?mu * abs ?mu) * ?n1 (i - 1)"
by (rule add_mono[OF mult_left_mono], insert cond α, auto)
also have "… = (inverse α + abs ?mu * abs ?mu) * ?n1 (i - 1)" by (auto simp: field_simps)
also have "… ≤ (inverse α + (1/2) * (1/2)) * ?n1 (i - 1)"
by (rule mult_right_mono[OF add_left_mono[OF mult_mono]], insert mu, auto)
also have "inverse α + (1/2) * (1/2) = reduction" unfolding reduction_def using α0
by (auto simp: field_simps)
also have "… * ?n1 (i - 1) ≤ 1 * ?n1 (i - 1)"
by (rule mult_right_mono, auto simp: reduction)
finally have n2im1: "?n2 (i - 1) ≤ ?n1 (i - 1)" by simp
show "g_bnd B fs'" unfolding g_bnd_def
proof (intro allI impI)
fix k
assume km: "k < m"
consider (ki) "k = i" | (im1) "k = i - 1" | (other) "k ≠ i" "k ≠ i-1" by blast
thus "?n2 k ≤ B"
proof cases
case other
from short[OF km] have "?n1 k ≤ B" by auto
also have "?n1 k = ?n2 k" using km other
by (subst updates(2), auto)
finally show ?thesis by simp
next
case im1
have "?n2 k = ?n2 (i - 1)" unfolding im1 ..
also have "… ≤ ?n1 (i - 1)" by fact
also have "… ≤ B" using short_im1 by auto
finally show ?thesis by simp
next
case ki
have "?n2 k = ?n2 i" unfolding ki using i by auto
also have "… ≤ ?n1 (i - 1)"
proof -
let ?f1 = "λ i. RAT fs ! i"
let ?f2 = "λ i. RAT fs' ! i"
define u where "u = gs.sumlist (map (λj. ?mu1 (i - 1) j ⋅⇩v ?g1 j) [0..<i - 1])"
define U where "U = ?f1 ` {0 ..< i - 1} ∪ {?f1 i}"
have g2i: "?g2 i ∈ Rn" using i inv' by simp
have U: "U ⊆ Rn" unfolding U_def using inv i by auto
have uU: "u ∈ gs.span U"
proof -
have im1: "i - 1 ≤ m" using i by auto
have G1: "?g1 ` {0..< i - 1} ⊆ Rn" using inv(5) i by auto
have "u ∈ gs.span (?g1 ` {0 ..< i - 1})" unfolding u_def
by (rule gs.sumlist_in_span[OF G1], unfold set_map, insert G1,
auto intro!: gs.smult_in_span intro: gs.span_mem)
also have "gs.span (?g1 ` {0 ..< i - 1}) = gs.span (?f1 ` {0 ..< i - 1})"
apply(subst gs1.partial_span, insert im1 inv, unfold gs.lin_indpt_list_def)
apply(blast)
apply(rule arg_cong[of _ _ gs.span])
apply(subst nth_image[symmetric])
by (insert i inv, auto)
also have "… ⊆ gs.span U" unfolding U_def
by (rule gs.span_is_monotone, auto)
finally show ?thesis .
qed
from i have im1: "i - 1 < m" by auto
have u: "u ∈ Rn" using uU U by simp
have id_u: "u + (?g1 (i - 1) - ?g2 i) = u + ?g1 (i - 1) - ?g2 i"
using u g2i inv(5)[OF im1] by auto
have list_id: "[0..<Suc (i - 1)] = [0..< i - 1] @ [i - 1]"
"map f [x] = [f x]" for f x by auto
have "gs.is_oc_projection (gs2.gso i) (gs.span (gs2.gso ` {0..<i})) ((RAT fs') ! i)"
using i inv' unfolding gs.lin_indpt_list_def
by (intro gs2.gso_oc_projection_span(2)) auto
then have "gs.is_oc_projection (?g2 i) (gs.span (gs2.gso ` {0 ..< i})) (?f1 (i - 1))"
unfolding fs'_def using inv(6) i by auto
also have "?f1 (i - 1) = u + ?g1 (i - 1) "
apply(subst gs1.fi_is_sum_of_mu_gso, insert im1 inv, unfold gs.lin_indpt_list_def)
apply(blast)
unfolding list_id map_append u_def
by (subst gs.M.sumlist_snoc, insert i, auto simp: gs1.μ.simps intro!: inv(5))
also have "gs.span (gs2.gso ` {0 ..< i}) = gs.span (set (take i (RAT fs')))"
using inv' ‹i < m› unfolding gs.lin_indpt_list_def
by (subst gs2.partial_span) auto
also have "set (take i (RAT fs')) = ?f2 ` {0 ..< i}" using inv'(6) i
by (subst nth_image[symmetric], auto)
also have "{0 ..< i} = {0 ..< i - 1} ∪ {(i - 1)}" using i by auto
also have "?f2 ` … = ?f2 ` {0 ..< i - 1} ∪ {?f2 (i - 1)}" by auto
also have "… = U" unfolding U_def fs'_def
by (rule arg_cong2[of _ _ _ _ "(∪)"], insert i inv(6), force+)
finally have "gs.is_oc_projection (?g2 i) (gs.span U) (u + ?g1 (i - 1))" .
hence proj: "gs.is_oc_projection (?g2 i) (gs.span U) (?g1 (i - 1))"
unfolding gs.is_oc_projection_def using gs.span_add[OF U uU, of "?g1 (i - 1) - ?g2 i"]
inv(5)[OF im1] g2i u id_u by (auto simp: U)
from gs.is_oc_projection_sq_norm[OF this gs.span_is_subset2[OF U] inv(5)[OF im1]]
show "?n2 i ≤ ?n1 (i - 1)" .
qed
also have "… ≤ B" by fact
finally show ?thesis .
qed
qed
qed
lemma basis_reduction_swap_bound: assumes
binv: "LLL_bound_invariant True False i fs"
and res: "basis_reduction_swap i fs = (upw',i',fs')"
and cond: "sq_norm (gso fs (i - 1)) > α * sq_norm (gso fs i)"
and i: "i < m" "i ≠ 0"
shows "LLL_bound_invariant True upw' i' fs'"
proof (rule bound_invI)
note Linv = bound_invD(1)[OF binv]
from basis_reduction_swap[OF Linv res cond i]
show Linv': "LLL_invariant upw' i' fs'" by auto
from res[unfolded basis_reduction_swap_def]
have id: "i' = i - 1" "fs' = fs[i := fs ! (i - 1), i - 1 := fs ! i]" by auto
from LLL_invD(6)[OF Linv] i
have choice: "fs' ! k = fs ! k ∨ fs' ! k = fs ! i ∨ fs' ! k = fs ! (i - 1)" for k
unfolding id by (cases "k = i"; cases "k = i - 1", auto)
from bound_invD(2)[OF binv] i
show "f_bound True i' fs'" unfolding id(1) f_bound_def
proof (intro allI impI, goal_cases)
case (1 k)
thus ?case using choice[of k] by auto
qed
from bound_invD(3)[OF binv, unfolded g_bound_def]
have gbnd: "g_bnd (of_nat N) fs" unfolding g_bnd_def .
from LLL_invD(11)[OF Linv, unfolded μ_small_def] i
have "abs (μ fs i (i - 1)) ≤ 1/2" by auto
from g_bnd_swap[OF i LLL_inv_imp_w[OF Linv] this cond id(2) gbnd]
have "g_bnd (rat_of_nat N) fs'" .
thus "g_bound fs'" unfolding g_bnd_def g_bound_def .
qed
lemma basis_reduction_step_bound: assumes
binv: "LLL_bound_invariant True upw i fs"
and res: "basis_reduction_step upw i fs = (upw',i',fs')"
and i: "i < m"
shows "LLL_bound_invariant True upw' i' fs'"
proof -
note def = basis_reduction_step_def
obtain fs'' where fs'': "basis_reduction_add_rows upw i fs = fs''" by auto
show ?thesis
proof (cases "i = 0")
case True
from increase_i_bound[OF binv i True] res True
show ?thesis by (auto simp: def)
next
case False
hence id: "(i = 0) = False" by auto
note res = res[unfolded def id if_False fs'' Let_def]
let ?x = "sq_norm (gso fs'' (i - 1))"
let ?y = "α * sq_norm (gso fs'' i)"
from basis_reduction_add_rows_bound[OF binv fs'' i]
have binv: "LLL_bound_invariant True False i fs''" by auto
show ?thesis
proof (cases "?x ≤ ?y")
case True
from increase_i_bound[OF binv i _ True] True res
show ?thesis by auto
next
case gt: False
hence "?x > ?y" by auto
from basis_reduction_swap_bound[OF binv _ this i False] gt res
show ?thesis by auto
qed
qed
qed
lemma basis_reduction_main_bound: assumes "LLL_bound_invariant True upw i fs"
and res: "basis_reduction_main (upw,i,fs) = fs'"
shows "LLL_bound_invariant True True m fs'"
using assms
proof (induct "LLL_measure i fs" arbitrary: i fs upw rule: less_induct)
case (less i fs upw)
have id: "LLL_bound_invariant True upw i fs = True" using less by auto
note res = less(3)[unfolded basis_reduction_main.simps[of upw i fs] id]
note inv = less(2)
note IH = less(1)
note Linv = bound_invD(1)[OF inv]
show ?case
proof (cases "i < m")
case i: True
obtain i' fs' upw' where step: "basis_reduction_step upw i fs = (upw',i',fs')"
(is "?step = _") by (cases ?step, auto)
note decrease = basis_reduction_step(2)[OF Linv step i]
from IH[OF decrease basis_reduction_step_bound(1)[OF inv step i]] res[unfolded step] i Linv
show ?thesis by auto
next
case False
with LLL_invD[OF Linv] have i: "i = m" by auto
with False res inv have "LLL_bound_invariant True upw m fs'" by auto
thus ?thesis by (auto simp: LLL_invariant_def LLL_bound_invariant_def)
qed
qed
lemma LLL_inv_initial_state_bound: "LLL_bound_invariant True True 0 fs_init"
proof (intro bound_invI[OF LLL_inv_initial_state _ g_bound_fs_init])
{
fix i
assume i: "i < m"
let ?N = "map (nat o sq_norm) fs_init"
let ?r = rat_of_int
from i have mem: "nat (sq_norm (fs_init ! i)) ∈ set ?N" using fs_init len unfolding set_conv_nth by force
from mem_set_imp_le_max_list[OF _ mem]
have FN: "nat (sq_norm (fs_init ! i)) ≤ N" unfolding N_def by force
hence "∥fs_init ! i∥⇧2 ≤ int N" using i by auto
also have "… ≤ int (N * m)" using i by fastforce
finally have f_bnd: "∥fs_init ! i∥⇧2 ≤ int (N * m)" .
}
thus "f_bound True 0 fs_init" unfolding f_bound_def by auto
qed
lemma reduce_basis_bound: assumes res: "reduce_basis = fs"
shows "LLL_bound_invariant True True m fs"
using basis_reduction_main_bound[OF LLL_inv_initial_state_bound res[unfolded reduce_basis_def]] .
subsubsection ‹Bound extracted from @{term LLL_bound_invariant}.›
fun f_bnd :: "bool ⇒ nat" where
"f_bnd False = 2 ^ (m - 1) * N ^ m * m"
| "f_bnd True = N * m"
lemma f_bnd_mono: "f_bnd outside ≤ f_bnd False"
proof (cases outside)
case out: True
show ?thesis
proof (cases "N = 0 ∨ m = 0")
case True
thus ?thesis using out by auto
next
case False
hence 0: "N > 0" "m > 0" by auto
let ?num = "(2 ^ (m - 1) * N ^ m)"
have "(N * m) * 1 ≤ (N * m) * (2 ^ (m - 1) * N ^ (m - 1))"
by (rule mult_left_mono, insert 0, auto)
also have "… = 2 ^ (m - 1) * N ^ (Suc (m - 1)) * m " by simp
also have "Suc (m - 1) = m" using 0 by simp
finally show ?thesis using out by auto
qed
qed auto
lemma aux_bnd_mono: "N * m ≤ (4 ^ (m - 1) * N ^ m * m * m)"
proof (cases "N = 0 ∨ m = 0")
case False
hence 0: "N > 0" "m > 0" by auto
let ?num = "(4 ^ (m - 1) * N ^ m * m * m)"
have "(N * m) * 1 ≤ (N * m) * (4 ^ (m - 1) * N ^ (m - 1) * m)"
by (rule mult_left_mono, insert 0, auto)
also have "… = 4 ^ (m - 1) * N ^ (Suc (m - 1)) * m * m" by simp
also have "Suc (m - 1) = m" using 0 by simp
finally show "N * m ≤ ?num" by simp
qed auto
context fixes outside upw k fs
assumes binv: "LLL_bound_invariant outside upw k fs"
begin
lemma LLL_f_bnd:
assumes i: "i < m" and j: "j < n"
shows "¦fs ! i $ j¦ ≤ f_bnd outside"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd] i have N0: "N > 0" by auto
note inv = LLL_invD[OF inv]
from inv i have fsi: "fs ! i ∈ carrier_vec n" by auto
have one: "¦fs ! i $ j¦^1 ≤ ¦fs ! i $ j¦^2"
by (cases "fs ! i $ j ≠ 0", intro pow_mono_exp, auto)
let ?num = "(4 ^ (m - 1) * N ^ m * m * m)"
let ?sq_bnd = "if i ≠ k ∨ outside then int (N * m) else int ?num"
have "¦fs ! i $ j¦^2 ≤ ∥fs ! i∥⇧2" using fsi j by (metis vec_le_sq_norm)
also have "… ≤ ?sq_bnd"
using fbnd[unfolded f_bound_def, rule_format, OF i] by auto
finally have two: "(fs ! i $ j)^2 ≤ ?sq_bnd" by simp
show ?thesis
proof (cases outside)
case True
with one two show ?thesis by auto
next
case False
let ?num2 = "(2 ^ (m - 1) * N ^ m * m)"
have four: "(4 :: nat) = 2^2" by auto
have "(fs ! i $ j)^2 ≤ int (max (N * m) ?num)"
by (rule order.trans[OF two], auto simp: of_nat_mult[symmetric] simp del: of_nat_mult)
also have "max (N * m) ?num = ?num" using aux_bnd_mono by presburger
also have "int ?num = int ?num * 1" by simp
also have "… ≤ int ?num * N ^ m"
by (rule mult_left_mono, insert N0, auto)
also have "… = int (?num * N ^ m)" by simp
also have "?num * N ^ m = ?num2^2" unfolding power2_eq_square four power_mult_distrib
by simp
also have "int … = (int ?num2)^2" by simp
finally have "(fs ! i $ j)⇧2 ≤ (int (f_bnd outside))⇧2" using False by simp
thus ?thesis unfolding abs_le_square_iff[symmetric] by simp
qed
qed
lemma LLL_gso_bound:
assumes i: "i < m" and j: "j < n"
and quot: "quotient_of (gso fs i $ j) = (num, denom)"
shows "¦num¦ ≤ N ^ m"
and "¦denom¦ ≤ N ^ m"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
note * = LLL_invD[OF inv]
interpret fs: fs_int' n m fs_init fs
by standard (use invw in auto)
note d_approx[OF invw gbnd i, unfolded d_def]
let ?r = "rat_of_int"
have int: "(gs.Gramian_determinant (RAT fs) i ⋅⇩v (gso fs i)) $ j ∈ ℤ"
proof -
have "of_int_hom.vec_hom (fs ! j) $ i ∈ ℤ" if "i < n" "j < m" for i j
using that assms * by (intro vec_hom_Ints) (auto)
then show ?thesis
using * gs.gso_connect snd_gram_schmidt_int assms unfolding gs.lin_indpt_list_def
by (intro fs.gs.d_gso_Ints) (auto)
qed
have gsi: "gso fs i ∈ Rn" using *(5)[OF i] .
have gs_sq: "¦(gso fs i $ j)¦⇧2 ≤ rat_of_nat N"
by(rule order_trans, rule vec_le_sq_norm[of _ n])
(use gsi assms gbnd * LLL.g_bound_def in auto)
from i have "m * m ≠ 0"
by auto
then have N0: "N ≠ 0"
using less_le_trans[OF LLL_D_pos[OF invw] D_approx[OF invw gbnd]] by auto
have "¦(gso fs i $ j)¦ ≤ max 1 ¦(gso fs i $ j)¦"
by simp
also have "… ≤ (max 1 ¦gso fs i $ j¦)⇧2"
by (rule self_le_power, auto)
also have "… ≤ of_nat N"
using gs_sq N0 unfolding max_def by auto
finally have gs_bound: "¦(gso fs i $ j)¦ ≤ of_nat N" .
have "gs.Gramian_determinant (RAT fs) i = rat_of_int (gs.Gramian_determinant fs i)"
using assms *(4-6) carrier_vecD nth_mem by (intro fs.of_int_Gramian_determinant) (simp, blast)
with int have "(of_int (d fs i) ⋅⇩v gso fs i) $ j ∈ ℤ"
unfolding d_def by simp
also have "(of_int (d fs i) ⋅⇩v gso fs i) $ j = of_int (d fs i) * (gso fs i $ j)"
using gsi i j by auto
finally have l: "of_int (d fs i) * gso fs i $ j ∈ ℤ"
by auto
have num: "rat_of_int ¦num¦ ≤ of_int (d fs i * int N)" and denom: "denom ≤ d fs i"
using quotient_of_bounds[OF quot l LLL_d_pos[OF invw] gs_bound] i by auto
from num have num: "¦num¦ ≤ d fs i * int N"
by linarith
from d_approx[OF invw gbnd i] have d: "d fs i ≤ int (N ^ i)"
by linarith
from denom d have denom: "denom ≤ int (N ^ i)"
by auto
note num also have "d fs i * int N ≤ int (N ^ i) * int N"
by (rule mult_right_mono[OF d], auto)
also have "… = int (N ^ (Suc i))"
by simp
finally have num: "¦num¦ ≤ int (N ^ (i + 1))"
by auto
{
fix jj
assume "jj ≤ i + 1"
with i have "jj ≤ m" by auto
from pow_mono_exp[OF _ this, of N] N0
have "N^jj ≤ N^m" by auto
hence "int (N^jj) ≤ int (N^m)" by linarith
} note j_m = this
have "¦denom¦ = denom"
using quotient_of_denom_pos[OF quot] by auto
also have "… ≤ int (N ^ i)"
by fact
also have "… ≤ int (N ^ m)"
by (rule j_m, auto)
finally show "¦denom¦ ≤ int (N ^ m)"
by auto
show "¦num¦ ≤ int (N ^ m)"
using j_m[of "i+1"] num by auto
qed
lemma LLL_f_bound:
assumes i: "i < m" and j: "j < n"
shows "¦fs ! i $ j¦ ≤ N ^ m * 2 ^ (m - 1) * m"
proof -
have "¦fs ! i $ j¦ ≤ int (f_bnd outside)" using LLL_f_bnd[OF i j] by auto
also have "… ≤ int (f_bnd False)" using f_bnd_mono[of outside] by presburger
also have "… = int (N ^ m * 2 ^ (m - 1) * m)" by simp
finally show ?thesis .
qed
lemma LLL_d_bound:
assumes i: "i ≤ m"
shows "abs (d fs i) ≤ N ^ i ∧ abs (d fs i) ≤ N ^ m"
proof (cases "m = 0")
case True
with i have id: "m = 0" "i = 0" by auto
show ?thesis unfolding id(2) using id unfolding gs.Gramian_determinant_0 d_def by auto
next
case m: False
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd] m have N: "N > 0" by auto
let ?r = rat_of_int
from d_approx_main[OF invw gbnd i m]
have "rat_of_int (d fs i) ≤ of_nat (N ^ i)"
by auto
hence one: "d fs i ≤ N ^ i" by linarith
also have "… ≤ N ^ m" unfolding of_nat_le_iff
by (rule pow_mono_exp, insert N i, auto)
finally have "d fs i ≤ N ^ m" by simp
with LLL_d_pos[OF invw i] one
show ?thesis by auto
qed
lemma LLL_mu_abs_bound:
assumes i: "i < m"
and j: "j < i"
shows "¦μ fs i j¦ ≤ rat_of_nat (N ^ (m - 1) * 2 ^ (m - 1) * m)"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd] i have N: "N > 0" by auto
note * = LLL_invD[OF inv]
interpret fs: fs_int' n m fs_init fs
by standard (use invw in auto)
let ?mu = "μ fs i j"
from j i have jm: "j < m" by auto
from d_approx[OF invw gbnd jm]
have dj: "d fs j ≤ int (N ^ j)" by linarith
let ?num = "4 ^ (m - 1) * N ^ m * m * m"
let ?bnd = "N^(m - 1) * 2 ^ (m - 1) * m"
from fbnd[unfolded f_bound_def, rule_format, OF i]
aux_bnd_mono[folded of_nat_le_iff[where ?'a = int]]
have sq_f_bnd: "sq_norm (fs ! i) ≤ int ?num" by (auto split: if_splits)
have four: "(4 :: nat) = 2^2" by auto
have "?mu^2 ≤ (gs.Gramian_determinant (RAT fs) j) * sq_norm (RAT fs ! i)"
proof -
have 1: "of_int_hom.vec_hom (fs ! j) $ i ∈ ℤ" if "i < n" "j < length fs" for j i
using * that by (metis vec_hom_Ints)
then show ?thesis
by (intro fs.gs.mu_bound_Gramian_determinant[OF j], insert * j i,
auto simp: set_conv_nth gs.lin_indpt_list_def)
qed
also have "sq_norm (RAT fs ! i) = of_int (sq_norm (fs ! i))"
unfolding sq_norm_of_int[symmetric] using *(6) i by auto
also have "(gs.Gramian_determinant (RAT fs) j) = of_int (d fs j)"
unfolding d_def by (rule fs.of_int_Gramian_determinant, insert i j *(3,6), auto simp: set_conv_nth)
also have "… * of_int (sq_norm (fs ! i)) = of_int (d fs j * sq_norm (fs ! i))" by simp
also have "… ≤ of_int (int (N^j) * int ?num)" unfolding of_int_le_iff
by (rule mult_mono[OF dj sq_f_bnd], auto)
also have "… = of_nat (N^(j + m) * (4 ^ (m - 1) * m * m))" by (simp add: power_add)
also have "… ≤ of_nat (N^( (m - 1) + (m-1)) * (4 ^ (m - 1) * m * m))" unfolding of_nat_le_iff
by (rule mult_right_mono[OF pow_mono_exp], insert N j i jm, auto)
also have "… = of_nat (?bnd^2)"
unfolding four power_mult_distrib power2_eq_square of_nat_mult by (simp add: power_add)
finally have "?mu^2 ≤ (of_nat ?bnd)^2" by auto
from this[folded abs_le_square_iff]
show "abs ?mu ≤ of_nat ?bnd" by auto
qed
lemma LLL_dμ_bound:
assumes i: "i < m" and j: "j < i"
shows "abs (dμ fs i j) ≤ N ^ (2 * (m - 1)) * 2 ^ (m - 1) * m"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
interpret fs: fs_int' n m fs_init fs
by standard (use invw in auto)
from LLL_inv_N_pos[OF invw gbnd] i have N: "N > 0" by auto
from j i have jm: "j < m - 1" "j < m" by auto
let ?r = rat_of_int
from LLL_d_bound[of "Suc j"] jm
have "abs (d fs (Suc j)) ≤ N ^ Suc j" by linarith
also have "… ≤ N ^ (m - 1)" unfolding of_nat_le_iff
by (rule pow_mono_exp, insert N jm, auto)
finally have dsj: "abs (d fs (Suc j)) ≤ int N ^ (m - 1)" by auto
from fs.dμ[of j i] j i LLL_invD[OF inv]
have "?r (abs (dμ fs i j)) = abs (?r (d fs (Suc j)) * μ fs i j)"
unfolding d_def fs.d_def dμ_def fs.dμ_def by auto
also have "… = ?r (abs (d fs (Suc j))) * abs (μ fs i j)" by (simp add: abs_mult)
also have "… ≤ ?r (int N ^ (m - 1)) * rat_of_nat (N ^ (m - 1) * 2 ^ (m - 1) * m)"
by (rule mult_mono[OF _ LLL_mu_abs_bound[OF i j]], insert dsj, linarith, auto)
also have "… = ?r (int (N ^ ((m - 1) + (m - 1)) * 2 ^ (m - 1) * m))"
by (simp add: power_add)
also have "(m - 1) + (m - 1) = 2 * (m - 1)" by simp
finally show "abs (dμ fs i j) ≤ N ^ (2 * (m - 1)) * 2 ^ (m - 1) * m" by linarith
qed
lemma LLL_mu_num_denom_bound:
assumes i: "i < m"
and quot: "quotient_of (μ fs i j) = (num, denom)"
shows "¦num¦ ≤ N ^ (2 * m) * 2 ^ m * m"
and "¦denom¦ ≤ N ^ m"
proof (atomize(full))
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs" by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd] i have N: "N > 0" by auto
note * = LLL_invD[OF inv]
interpret fs: fs_int' n m fs_init fs
by standard (use invw in auto)
let ?mu = "μ fs i j"
let ?bnd = "N^(m - 1) * 2 ^ (m - 1) * m"
show "¦num¦ ≤ N ^ (2 * m) * 2 ^ m * m ∧ ¦denom¦ ≤ N ^ m"
proof (cases "j < i")
case j: True
with i have jm: "j < m" by auto
from LLL_d_pos[OF invw, of "Suc j"] i j have dsj: "0 < d fs (Suc j)" by auto
from quotient_of_square[OF quot]
have quot_sq: "quotient_of (?mu^2) = (num * num, denom * denom)"
unfolding power2_eq_square by auto
from LLL_mu_abs_bound[OF assms(1) j]
have mu_bound: "abs ?mu ≤ of_nat ?bnd" by auto
have "gs.Gramian_determinant (RAT fs) (Suc j) * ?mu ∈ ℤ"
by (rule fs.gs.d_mu_Ints,
insert j *(1,3-6) i, auto simp: set_conv_nth gs.lin_indpt_list_def vec_hom_Ints)
also have "(gs.Gramian_determinant (RAT fs) (Suc j)) = of_int (d fs (Suc j))"
unfolding d_def by (rule fs.of_int_Gramian_determinant, insert i j *(3,6), auto simp: set_conv_nth)
finally have ints: "of_int (d fs (Suc j)) * ?mu ∈ ℤ" .
from LLL_d_bound[of "Suc j"] jm
have d_j: "d fs (Suc j) ≤ N ^ m" by auto
note quot_bounds = quotient_of_bounds[OF quot ints dsj mu_bound]
have "abs denom ≤ denom" using quotient_of_denom_pos[OF quot] by auto
also have "… ≤ d fs (Suc j)" by fact
also have "… ≤ N ^ m" by fact
finally have denom: "abs denom ≤ N ^ m" by auto
from quot_bounds(1) have "¦num¦ ≤ d fs (Suc j) * int ?bnd"
unfolding of_int_le_iff[symmetric, where ?'a = rat] by simp
also have "… ≤ N ^ m * int ?bnd" by (rule mult_right_mono[OF d_j], auto)
also have "… = (int N ^ (m + (m - 1))) * (2 ^ (m - 1)) * int m" unfolding power_add of_nat_mult by simp
also have "… ≤ (int N ^ (2 * m)) * (2 ^ m) * int m" unfolding of_nat_mult
by (intro mult_mono pow_mono_exp, insert N, auto)
also have "… = int (N ^ (2 * m) * 2 ^ m * m)" by simp
finally have num: "¦num¦ ≤ N ^ (2 * m) * 2 ^ m * m" .
from denom num show ?thesis by blast
next
case False
hence "?mu = 0 ∨ ?mu = 1" unfolding fs.gs.μ.simps by auto
hence "quotient_of ?mu = (1,1) ∨ quotient_of ?mu = (0,1)" by auto
from this[unfolded quot] show ?thesis using N i by (auto intro!: mult_ge_one)
qed
qed
text ‹Now we have bounds on each number $(f_i)_j$, $(g_i)_j$, and $\mu_{i,j}$, i.e.,
for rational numbers bounds on the numerators and denominators.›
lemma logN_le_2log_Mn: assumes m: "m ≠ 0" "n ≠ 0" and N: "N > 0"
shows "log 2 N ≤ 2 * log 2 (M * n)"
proof -
have "N ≤ nat M * nat M * n * 1" using N_le_MMn m by auto
also have "… ≤ nat M * nat M * n * n" by (intro mult_mono, insert m, auto)
finally have NM: "N ≤ nat M * nat M * n * n" by simp
with N have "nat M ≠ 0" by auto
hence M: "M > 0" by simp
have "log 2 N ≤ log 2 (M * M * n * n)"
proof (subst log_le_cancel_iff)
show "real N ≤ (M * M * int n * int n)" using NM[folded of_nat_le_iff[where ?'a = real]] M
by simp
qed (insert N M m, auto)
also have "… = log 2 (of_int (M * n) * of_int (M * n))"
unfolding of_int_mult by (simp add: ac_simps)
also have "… = 2 * log 2 (M * n)"
by (subst log_mult, insert m M, auto)
finally show "log 2 N ≤ 2 * log 2 (M * n)" by auto
qed
text ‹We now prove a combined size-bound for all of these numbers. The bounds clearly indicate
that the size of the numbers grows at most polynomial, namely the sizes are roughly
bounded by ${\cal O}(m \cdot \log(M \cdot n))$ where $m$ is the number of vectors, $n$ is the dimension
of the vectors, and $M$ is the maximum absolute value that occurs in the input to the LLL algorithm.›
lemma combined_size_bound: fixes number :: int
assumes i: "i < m" and j: "j < n"
and x: "x ∈ {of_int (fs ! i $ j), gso fs i $ j, μ fs i j}"
and quot: "quotient_of x = (num, denom)"
and number: "number ∈ {num, denom}"
and number0: "number ≠ 0"
shows "log 2 ¦number¦ ≤ 2 * m * log 2 N + m + log 2 m"
"log 2 ¦number¦ ≤ 4 * m * log 2 (M * n) + m + log 2 m"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs"
by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd] i have N: "N > 0" by auto
let ?bnd = "N ^ (2 * m) * 2 ^ m * m"
have "N ^ m * int 1 ≤ N ^ (2 * m) * (2^m * int m)"
by (rule mult_mono, unfold of_nat_le_iff, rule pow_mono_exp, insert N i, auto)
hence le: "int (N ^ m) ≤ N ^ (2 * m) * 2^m * m" by auto
from x consider (xfs) "x = of_int (fs ! i $ j)" | (xgs) "x = gso fs i $ j" | (xmu) "x = μ fs i j"
by auto
hence num_denom_bound: "¦num¦ ≤ ?bnd ∧ ¦denom¦ ≤ N ^ m"
proof (cases)
case xgs
from LLL_gso_bound[OF i j quot[unfolded xgs]] le
show ?thesis by auto
next
case xmu
from LLL_mu_num_denom_bound[OF i, of j, OF quot[unfolded xmu]]
show ?thesis by auto
next
case xfs
have "¦denom¦ = 1" using quot[unfolded xfs] by auto
also have "… ≤ N ^ m" using N by auto
finally have denom: "¦denom¦ ≤ N ^ m" .
have "¦num¦ = ¦fs ! i $ j¦" using quot[unfolded xfs] by auto
also have "… ≤ int (N ^ m * 2 ^ (m - 1) * m)" using LLL_f_bound[OF i j] by auto
also have "… ≤ ?bnd" unfolding of_nat_mult of_nat_power
using N by (auto intro!: mult_mono pow_mono_exp)
finally show ?thesis using denom by auto
qed
from number consider (num) "number = num" | (denom) "number = denom" by auto
hence number_bound: "¦number¦ ≤ ?bnd"
proof (cases)
case num
with num_denom_bound show ?thesis by auto
next
case denom
with num_denom_bound have "¦number¦ ≤ N ^ m" by auto
with le show ?thesis by auto
qed
from number_bound have bnd: "of_int ¦number¦ ≤ real ?bnd" by linarith
have "log 2 ¦number¦ ≤ log 2 ?bnd"
by (subst log_le_cancel_iff, insert number0 bnd, auto)
also have "… = log 2 (N^(2 * m) * 2^m) + log 2 m"
by (subst log_mult[symmetric], insert i N, auto)
also have "… = log 2 (N^(2 * m)) + log 2 (2^m) + log 2 m"
by (subst log_mult[symmetric], insert i N, auto)
also have "log 2 (N^(2 * m)) = log 2 (N powr (2 * m))"
by (rule arg_cong[of _ _ "log 2"], subst powr_realpow, insert N, auto)
also have "… = (2 * m) * log 2 N"
by (subst log_powr, insert N, auto)
finally show boundN: "log 2 ¦number¦ ≤ 2 * m * log 2 N + m + log 2 m" by simp
also have "… ≤ 2 * m * (2 * log 2 (M * n)) + m + log 2 m"
by (intro add_right_mono mult_mono logN_le_2log_Mn N, insert i j N, auto)
finally show "log 2 ¦number¦ ≤ 4 * m * log 2 (M * n) + m + log 2 m" by simp
qed
text ‹And a combined size bound for an integer implementation which stores values
$f_i$, $d_{j+1}\mu_{ij}$ and $d_i$.›
interpretation fs: fs_int_indpt n fs_init
by (standard) (use lin_dep in auto)
lemma fs_gs_N_N': assumes "m ≠ 0"
shows "fs.gs.N = of_nat N"
proof -
have 0: "Max (sq_norm ` set fs_init) ∈ sq_norm ` set fs_init"
using len assms by auto
then have 1: " nat (Max (sq_norm ` set fs_init)) ∈ (nat ∘ sq_norm) ` set fs_init"
by (auto)
have [simp]: "0 ≤ Max (sq_norm ` set fs_init)"
using 0 by force
have [simp]: "sq_norm ` of_int_hom.vec_hom ` set fs_init = rat_of_int ` sq_norm ` set fs_init"
by (auto simp add: sq_norm_of_int image_iff)
then have [simp]: "rat_of_int (Max (sq_norm ` set fs_init)) ∈ rat_of_int ` sq_norm ` set fs_init"
using 0 by auto
have "(Missing_Lemmas.max_list (map (nat ∘ sq_norm) fs_init)) = Max ((nat ∘ sq_norm) ` set fs_init)"
using assms len by (subst max_list_Max) (auto)
also have "… = nat (Max (sq_norm_vec ` set fs_init))"
using assms 1 by (auto intro!: nat_mono Max_eqI)
also have "int … = Max (sq_norm_vec ` set fs_init)"
by (subst int_nat_eq) (auto)
also have "rat_of_int … = Max (sq_norm ` set (map of_int_hom.vec_hom fs_init))"
by (rule Max_eqI[symmetric]) (auto simp add: sq_norm_of_int)
finally show ?thesis
unfolding N_def fs.gs.N_def by (auto)
qed
lemma fs_gs_N_N: "m ≠ 0 ⟹ real_of_rat fs.gs.N = real N"
using fs_gs_N_N' by simp
lemma combined_size_bound_gso_integer:
assumes "x ∈
{fs.μ' i j |i j. j ≤ i ∧ i < m} ∪
{fs.σs l i j |i j l. i < m ∧ j ≤ i ∧ l < j}"
and m: "m ≠ 0" and "x ≠ 0" "n ≠ 0"
shows "log 2 ¦real_of_int x¦ ≤ (6 + 6 * m) * log 2 (M * n) + log 2 m + m"
proof -
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and gbnd: "g_bound fs"
by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd m] have N: "N > 0" by auto
have "log 2 ¦real_of_int x¦ ≤ log 2 m + real (3 + 3 * m) * log 2 N"
using assms len fs.combined_size_bound_integer_log by (auto simp add: fs_gs_N_N)
also have "… ≤ log 2 m + (3 + 3 * m) * (2 * log 2 (M * n))"
using logN_le_2log_Mn assms N by (intro add_left_mono, intro mult_left_mono) (auto)
also have "… = log 2 m + (6 + 6 * m) * log 2 (M * n)"
by (auto simp add: algebra_simps)
finally show ?thesis
by auto
qed
lemma combined_size_bound_integer':
assumes x: "x ∈ {fs ! i $ j | i j. i < m ∧ j < n}
∪ {dμ fs i j | i j. j < i ∧ i < m}
∪ {d fs i | i. i ≤ m}"
(is "x ∈ ?fs ∪ ?dμ ∪ ?d")
and m: "m ≠ 0" and n: "n ≠ 0"
shows "abs x ≤ N ^ (2 * m) * 2 ^ m * m"
"x ≠ 0 ⟹ log 2 ¦x¦ ≤ 2 * m * log 2 N + m + log 2 m" (is "_ ⟹ ?l1 ≤ ?b1")
"x ≠ 0 ⟹ log 2 ¦x¦ ≤ 4 * m * log 2 (M * n) + m + log 2 m" (is "_ ⟹ _ ≤ ?b2")
proof -
let ?bnd = "int N ^ (2 * m) * 2 ^ m * int m"
from bound_invD[OF binv]
have inv: "LLL_invariant upw k fs"
and fbnd: "f_bound outside k fs"
and gbnd: "g_bound fs"
by auto
note invw = LLL_inv_imp_w[OF inv]
from LLL_inv_N_pos[OF invw gbnd m] have N: "N > 0" by auto
let ?r = real_of_int
from x consider (fs) "x ∈ ?fs" | (dμ) "x ∈ ?dμ" | (d) "x ∈ ?d" by auto
hence "abs x ≤ ?bnd"
proof cases
case fs
then obtain i j where i: "i < m" and j: "j < n" and x: "x = fs ! i $ j" by auto
from LLL_f_bound[OF i j, folded x]
have "¦x¦ ≤ int N ^ m * 2 ^ (m - 1) * int m" by simp
also have "… ≤ ?bnd"
by (intro mult_mono pow_mono_exp, insert N, auto)
finally show ?thesis .
next
case dμ
then obtain i j where i: "i < m" and j: "j < i" and x: "x = dμ fs i j" by auto
from LLL_dμ_bound[OF i j, folded x]
have "¦x¦ ≤ int N ^ (2 * (m - 1)) * 2 ^ (m - 1) * int m" by simp
also have "… ≤ ?bnd"
by (intro mult_mono pow_mono_exp, insert N, auto)
finally show ?thesis .
next
case d
then obtain i where i: "i ≤ m" and x: "x = d fs i" by auto
from LLL_d_bound[OF i, folded x]
have "¦x¦ ≤ int N ^ m * 2 ^ 0 * 1" by simp
also have "… ≤ ?bnd"
by (intro mult_mono pow_mono_exp, insert N m, auto)
finally show ?thesis .
qed
thus "abs x ≤ N ^ (2 * m) * 2 ^ m * m" by simp
hence abs: "?r (abs x) ≤ ?r (N ^ (2 * m) * 2 ^ m * m)" by linarith
assume "x ≠ 0" hence x: "abs x > 0" by auto
from abs have "log 2 (abs x) ≤ log 2 (?r (N ^ (2 * m)) * 2 ^ m * ?r m)"
by (subst log_le_cancel_iff, insert x N m, auto)
also have "… = log 2 (?r N ^ (2 * m)) + m + log 2 (?r m)"
using N m by (auto simp: log_mult)
also have "log 2 (?r N ^ (2 * m)) = real (2 * m) * log 2 (?r N)"
by (subst log_nat_power, insert N, auto)
finally show "?l1 ≤ ?b1" by simp
also have "… ≤ 2 * m * (2 * log 2 (M * n)) + m + log 2 m"
by (intro add_right_mono mult_left_mono logN_le_2log_Mn, insert m n N, auto)
finally show "?l1 ≤ ?b2" by simp
qed
lemma combined_size_bound_integer:
assumes x: "x ∈
{fs ! i $ j | i j. i < m ∧ j < n}
∪ {dμ fs i j | i j. j < i ∧ i < m}
∪ {d fs i | i. i ≤ m}
∪ {fs.μ' i j |i j. j ≤ i ∧ i < m}
∪ {fs.σs l i j |i j l. i < m ∧ j ≤ i ∧ l < j}"
(is "?x ∈ ?s1 ∪ ?s2 ∪ ?s3 ∪ ?g1 ∪ ?g2")
and m: "m ≠ 0" and n: "n ≠ 0" and "x ≠ 0" and "0 < M"
shows "log 2 ¦x¦ ≤ (6 + 6 * m) * log 2 (M * n) + log 2 m + m"
proof -
show ?thesis
proof (cases "?x ∈ ?g1 ∪ ?g2")
case True
then show ?thesis
using combined_size_bound_gso_integer assms by simp
next
case False
then have x: "x ∈ ?s1 ∪ ?s2 ∪ ?s3" using x by auto
from combined_size_bound_integer'(3)[OF this m n ‹x ≠ 0›]
have "log 2 ¦x¦ ≤ 4 * m * log 2 (M * n) + m + log 2 m" by simp
also have "… ≤ (6 + 6 * m) * log 2 (M * n) + m + log 2 m"
using assms by (intro add_right_mono, intro mult_right_mono) auto
finally show ?thesis
by simp
qed
qed
end
end
end