Theory Babai
theory Babai
imports Babai_Algorithm
begin
text ‹This theory contains the proof of correctness of the algorithm. The main theorem is
"theorem Babai-Correct", under the locale "Babai-with-assms".
To use the theorem, one needs to show that lattice, the vectors in the lattice basis, and the target
vector all have the same dimension, that the lattice basis vectors are linearly independent and form an invertible
matrix, and that the lattice basis is LLL-weakly-reduced.
›
section ‹ Copy-Pasted Material ›
text ‹ The next couple of lemmas are copy-pasted from Modular-arithmetic-LLL-and-HNF-algorithms
(we copy-paste them instead of loading them to avoid excessive loading times) ›
context vec_module
begin
text ‹ This lemma is copy-pasted from Modular-arithmetic-LLL-and-HNF-algorithms
(we copy-paste them instead of loading them to avoid excessive loading times) ›
lemma lattice_of_altdef_lincomb:
assumes "set fs ⊆ carrier_vec n"
shows "lattice_of fs = {y. ∃f. lincomb (of_int ∘ f) (set fs) = y}"
unfolding lincomb_def lattice_of_altdef[OF assms] image_def by auto
text ‹ This lemma is copy-pasted from Modular-arithmetic-LLL-and-HNF-algorithms
(we copy-paste them instead of loading them to avoid excessive loading times) ›
lemma lincomb_as_lincomb_list:
fixes ws f
assumes s: "set ws ⊆ carrier_vec n"
shows "lincomb f (set ws) = lincomb_list (λi. if ∃j<i. ws!i = ws!j then 0 else f (ws ! i)) ws"
using assms
proof (induct ws rule: rev_induct)
case (snoc a ws)
let ?f = "λi. if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)"
let ?g = "λi. (if ∃j<i. (ws @ [a]) ! i = (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) ⋅⇩v (ws @ [a]) ! i"
let ?g2= "(λi. (if ∃j<i. ws ! i = ws ! j then 0 else f (ws ! i)) ⋅⇩v ws ! i)"
have [simp]: "⋀v. v ∈ set ws ⟹ v ∈ carrier_vec n" using snoc.prems(1) by auto
then have ws: "set ws ⊆ carrier_vec n" by auto
have hyp: "lincomb f (set ws) = lincomb_list ?f ws"
by (intro snoc.hyps ws)
show ?case
proof (cases "a∈set ws")
case True
have g_length: "?g (length ws) = 0⇩v n" using True
by (auto, metis in_set_conv_nth nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [0⇩v n]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [0⇩v n]" .
have "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
also have "... = M.sumlist (map ?g [0..<length ws]) + 0⇩v n "
by (metis M.r_zero calculation hyp lincomb_closed lincomb_list_def ws)
also have "... = M.sumlist (map ?g [0..<length ws] @ [0⇩v n])"
by (rule M.sumlist_snoc[symmetric], auto simp add: nth_append)
finally have summlist_rw: "M.sumlist (map ?g2 [0..<length ws])
= M.sumlist (map ?g [0..<length ws] @ [0⇩v n])" .
have "lincomb f (set (ws @ [a])) = lincomb f (set ws)" using True unfolding lincomb_def
by (simp add: insert_absorb)
thus ?thesis
unfolding hyp lincomb_list_def map_rw summlist_rw
by auto
next
case False
have g_length: "?g (length ws) = f a ⋅⇩v a" using False by (auto simp add: nth_append)
have "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [?g (length ws)]"
by auto
also have "... = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" using g_length by simp
finally have map_rw: "(map ?g [0..<length (ws @ [a])]) = (map ?g [0..<length ws]) @ [(f a ⋅⇩v a)]" .
have summlist_rw: "M.sumlist (map ?g2 [0..<length ws]) = M.sumlist (map ?g [0..<length ws])"
by (rule arg_cong[of _ _ "M.sumlist"], intro nth_equalityI, auto simp add: nth_append)
have "lincomb f (set (ws @ [a])) = lincomb f (set (a # ws))" by auto
also have "... = (⨁⇘V⇙v∈set (a # ws). f v ⋅⇩v v)" unfolding lincomb_def ..
also have "... = (⨁⇘V⇙v∈ insert a (set ws). f v ⋅⇩v v)" by simp
also have "... = (f a ⋅⇩v a) + (⨁⇘V⇙v∈ (set ws). f v ⋅⇩v v)"
proof (rule finsum_insert)
show "finite (set ws)" by auto
show "a ∉ set ws" using False by auto
show "(λv. f v ⋅⇩v v) ∈ set ws → carrier_vec n"
using snoc.prems(1) by auto
show "f a ⋅⇩v a ∈ carrier_vec n" using snoc.prems by auto
qed
also have "... = (f a ⋅⇩v a) + lincomb f (set ws)" unfolding lincomb_def ..
also have "... = (f a ⋅⇩v a) + lincomb_list ?f ws" using hyp by auto
also have "... = lincomb_list ?f ws + (f a ⋅⇩v a)"
using M.add.m_comm lincomb_list_carrier snoc.prems by auto
also have "... = lincomb_list (λi. if ∃j<i. (ws @ [a]) ! i
= (ws @ [a]) ! j then 0 else f ((ws @ [a]) ! i)) (ws @ [a])"
proof (unfold lincomb_list_def map_rw summlist_rw, rule M.sumlist_snoc[symmetric])
show "set (map ?g [0..<length ws]) ⊆ carrier_vec n" using snoc.prems
by (auto simp add: nth_append)
show "f a ⋅⇩v a ∈ carrier_vec n"
using snoc.prems by auto
qed
finally show ?thesis .
qed
qed auto
end
context
begin
interpretation vec_module "TYPE(int)" .
text ‹ This lemma is copy-pasted from Modular-arithmetic-LLL-and-HNF-algorithms
(we copy-paste them instead of loading them to avoid excessive loading times) ›
lemma lattice_of_cols_as_mat_mult:
assumes A: "A ∈ carrier_mat n nc"
shows "lattice_of (cols A) = {y∈carrier_vec (dim_row A). ∃x∈carrier_vec (dim_col A). A *⇩v x = y}"
proof -
let ?ws = "cols A"
have set_cols_in: "set (cols A) ⊆ carrier_vec n" using A unfolding cols_def by auto
have "lincomb (of_int ∘ f)(set ?ws) ∈ carrier_vec (dim_row A)" for f
using lincomb_closed A
by (metis (full_types) carrier_matD(1) cols_dim lincomb_closed)
moreover have "∃x∈carrier_vec (dim_col A). A *⇩v x = lincomb (of_int ∘ f) (set (cols A))" for f
proof -
let ?g = "(λv. of_int (f v))"
let ?g' = "(λi. if ∃j<i. ?ws ! i = ?ws ! j then 0 else ?g (?ws ! i))"
have "lincomb (of_int ∘ f) (set (cols A)) = lincomb ?g (set ?ws)" unfolding o_def by auto
also have "... = lincomb_list ?g' ?ws"
by (rule lincomb_as_lincomb_list[OF set_cols_in])
also have "... = mat_of_cols n ?ws *⇩v vec (length ?ws) ?g'"
by (rule lincomb_list_as_mat_mult, insert set_cols_in A, auto)
also have "... = A *⇩v (vec (length ?ws) ?g')" using mat_of_cols_cols A by auto
finally show ?thesis by auto
qed
moreover have "∃f. A *⇩v x = lincomb (of_int ∘ f) (set (cols A))"
if Ax: "A *⇩v x ∈ carrier_vec (dim_row A)" and x: "x ∈ carrier_vec (dim_col A)" for x
proof -
let ?c = "λi. x $ i"
have x_vec: "vec (length ?ws) ?c = x" using x by auto
have "A *⇩v x = mat_of_cols n ?ws *⇩v vec (length ?ws) ?c" using mat_of_cols_cols A x_vec by auto
also have "... = lincomb_list ?c ?ws"
by (rule lincomb_list_as_mat_mult[symmetric], insert set_cols_in A, auto)
also have "... = lincomb (mk_coeff ?ws ?c) (set ?ws)"
by (rule lincomb_list_as_lincomb, insert set_cols_in A, auto)
finally show ?thesis by auto
qed
ultimately show ?thesis unfolding lattice_of_altdef_lincomb[OF set_cols_in]
by (metis (mono_tags, opaque_lifting))
qed
text ‹ This lemma is copy-pasted from Modular-arithmetic-LLL-and-HNF-algorithms
(we copy-paste them instead of loading them to avoid excessive loading times) ›
corollary lattice_of_as_mat_mult:
assumes fs: "set fs ⊆ carrier_vec n"
shows "lattice_of fs = {y∈carrier_vec n. ∃x∈carrier_vec (length fs). (mat_of_cols n fs) *⇩v x = y}"
proof -
have cols_eq: "cols (mat_of_cols n fs) = fs" using cols_mat_of_cols[OF fs] by simp
have m: "(mat_of_cols n fs) ∈ carrier_mat n (length fs)" using mat_of_cols_carrier(1) by auto
show ?thesis using lattice_of_cols_as_mat_mult[OF m] unfolding cols_eq using m by auto
qed
end
section ‹ Locale setup for Babai ›
locale Babai =
fixes M :: "int vec list"
fixes t :: "rat vec"
assumes length_M: "length M = dim_vec t"
begin
abbreviation n where "n ≡ length M"
definition α where "(α::rat) = 4/3"
sublocale LLL n n M α.
abbreviation coset::"rat vec set" where "coset≡{(map_vec rat_of_int x)-t|x. x∈L}"
abbreviation Mt where "Mt ≡ gram_schmidt n (RAT M)"
definition s :: "nat ⇒ rat vec" where
"s i = Babai_Help (uminus t) (RAT M) Mt i"
definition closest_distance_sq:: "real" where
"closest_distance_sq = Inf {real_of_rat (sq_norm x::rat) |x. x ∈ coset}"
end
text ‹Locale setup with additional assumptions required for main theorem›
locale Babai_with_assms = Babai+
fixes mat_M mat_M_inv:: "rat mat"
assumes basis: "lin_indep M"
defines "mat_M ≡ mat_of_cols n (RAT M)"
defines "mat_M_inv ≡
(if (invertible_mat mat_M) then SOME B. (inverts_mat B mat_M) ∧ (inverts_mat mat_M B) else (0⇩m n n))"
assumes inv:"invertible_mat mat_M"
assumes reduced:"weakly_reduced M n"
assumes non_trivial:"0<n"
begin
lemma dim_vecs_in_M:
shows "∀v ∈ set M. dim_vec v = length M"
using basis unfolding gs.lin_indpt_list_def by force
lemma inv1:"mat_M * mat_M_inv = 1⇩m n"
proof-
have dim_m:"dim_row mat_M = n" using dim_vecs_in_M unfolding mat_M_def by fastforce
then have "inverts_mat mat_M mat_M_inv" using inv
unfolding mat_M_inv_def
by (smt (verit, ccfv_SIG) invertible_mat_def some_eq_imp)
then show ?thesis using dim_m unfolding inverts_mat_def by argo
qed
lemma inv2:"mat_M_inv * mat_M = 1⇩m n"
proof-
have dim_m:"dim_col mat_M = n" unfolding mat_M_def by fastforce
have "inverts_mat mat_M_inv mat_M" using inv
unfolding mat_M_inv_def
by (smt (verit, ccfv_SIG) invertible_mat_def some_eq_imp)
then have inv:"mat_M_inv * mat_M = 1⇩m (dim_row mat_M_inv)"
unfolding inverts_mat_def by blast
then have dim_n:"dim_col (1⇩m (dim_row mat_M_inv)) = n"
using dim_m index_mult_mat(3)[of mat_M_inv mat_M] by fastforce
have "(dim_row mat_M_inv)= n"
proof(rule ccontr)
assume "(dim_row mat_M_inv)≠ n"
then have "dim_col (1⇩m (dim_row mat_M_inv)) ≠ n"
by auto
then show False using dim_n by blast
qed
then show ?thesis using inv by argo
qed
sublocale rats: vec_module "TYPE(rat)" n.
lemma M_dim: "dim_row mat_M = n" "dim_col mat_M = n"
apply (metis index_mult_mat(2) index_one_mat(2) inv1)
by (metis index_mult_mat(3) index_one_mat(3) inv2)
lemma M_inv_dim: "dim_row mat_M_inv = n" "dim_col mat_M_inv = n"
apply (metis M_dim(1) index_mult_mat(2) inv1 inv2)
by (metis index_mult_mat(3) index_one_mat(3) inv1)
lemma Babai_to_Help:
shows "s n = Babai_Algorithm.Babai (uminus t) (RAT M)"
using Babai.Babai_def Babai.s_def Babai_Algorithm.Babai_def Babai_axioms by force
section ‹Coordinates›
text ‹ This section sets up the use of the lattice basis and its GS orthogonalization
as coordinate systems and some properties of that coordinate system. The important lemma here
is coord-invariance, which shows that after step i of the algorithm, all coordinates (in both
systems) after n-i are invariant. ›
definition lattice_coord :: "rat vec ⇒ rat vec"
where "lattice_coord a = mat_M_inv *⇩v a"
lemma dim_preserve_lattice_coord:
fixes v::"rat vec"
assumes "dim_vec v=n"
shows "dim_vec (lattice_coord v) = n" unfolding lattice_coord_def mat_M_inv_def using M_inv_dim
by (simp add: mat_M_inv_def)
lemma vec_to_col:
assumes "i < n"
shows "(RAT M)!i = col mat_M i"
unfolding mat_M_def
by (metis Babai_with_assms_axioms Babai_with_assms_axioms_def Babai_with_assms_def M_dim(2)
assms cols_mat_of_cols cols_nth gs.lin_indpt_list_def mat_M_def)
lemma unit:
assumes "i < n"
shows "lattice_coord ((RAT M)!i) = unit_vec n i"
using assms inv2 unfolding lattice_coord_def
by (metis M_dim(1) M_dim(2) M_inv_dim(2) carrier_matI col_mult2 col_one vec_to_col)
lemma linear:
fixes i::nat
fixes v1::"rat vec"
and v2:: "rat vec"
and q:: rat
assumes "dim_vec v1 = n"
assumes dim_2:"dim_vec v2 = n"
assumes "0≤i"
assumes dim_i:"i<n"
shows "(lattice_coord (v1+(q⋅⇩vv2)))$i = (lattice_coord v1)$i + q*((lattice_coord v2)$i)"
using assms
proof(-)
have linear_vec:"(lattice_coord (v1+(q⋅⇩vv2))) = (lattice_coord v1) + q⋅⇩v((lattice_coord v2))"
unfolding lattice_coord_def
by (metis (mono_tags, opaque_lifting) M_inv_dim(2) assms(1) assms(2) carrier_mat_triv
carrier_vec_dim_vec mult_add_distrib_mat_vec mult_mat_vec smult_carrier_vec)
then have 2: "(lattice_coord (v1+(q⋅⇩vv2)))$i= ((lattice_coord v1) + q⋅⇩v((lattice_coord v2)))$i" by auto
also have dim_v2: "dim_vec (lattice_coord v2) = n" using dim_preserve_lattice_coord dim_2 by blast
then have i_in_range: "i<dim_vec (q⋅⇩v(lattice_coord v2))" using dim_v2 dim_i by simp
also have 3:"((lattice_coord v1) + q⋅⇩v((lattice_coord v2)))$i=(lattice_coord v1)$i+
(q⋅⇩v(lattice_coord v2))$i" using i_in_range by simp
also have 4: "(q⋅⇩v(lattice_coord v2))$i=q*(lattice_coord v2)$i" using i_in_range by simp
thus ?thesis unfolding vec_def using linear_vec 2 3 4 by simp
qed
lemma sub_s:
fixes i::nat
assumes "0≤i"
assumes "i<n"
shows "s (Suc i) = (s i) -
( (rat_of_int (calculate_c (s i) Mt (Suc i) ) ) ⋅⇩v (RAT M)!( (dim_vec (s i)) -(Suc i))) "
using assms Babai_Help.simps[of "-t" "RAT M" Mt] unfolding s_def
by (metis update_s.simps)
lemma M_locale_1:
shows "gram_schmidt_fs_Rn n (RAT M)"
by (smt (verit) M_dim(1) M_dim(2) carrier_dim_vec dim_col gram_schmidt_fs_Rn.intro in_set_conv_nth
mat_M_def mat_of_cols_carrier(3) subset_code(1) vec_to_col)
lemma M_locale_2:
shows "gram_schmidt_fs_lin_indpt n (RAT M)"
using basis M_locale_1 gram_schmidt_fs_lin_indpt.intro[of n "(RAT M)"] unfolding gs.lin_indpt_list_def
using gram_schmidt_fs_lin_indpt_axioms.intro by blast
lemma more_dim: "length (RAT M) = n"
by simp
lemma Mt_gso_connect:
fixes j::nat
assumes "j<n"
shows "Mt!j = gs.gso j"
proof(-)
have "Mt = map gs.gso[0..<n]"
using M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
by fastforce
then show ?thesis
using assms
by simp
qed
lemma access_index_M_dim:
assumes "0 ≤ i"
assumes "i < n"
shows "dim_vec (map of_int_hom.vec_hom M ! i) = n"
using assms dim_vecs_in_M
by auto
lemma s_dim:
fixes i::nat
assumes "i≤ n"
shows "dim_vec (s i) = n ∧ (s i) ∈carrier_vec n"
using assms
proof(induct i)
case 0
have unfold1:"s 0 = Babai_Help (uminus t) (RAT M) Mt 0" unfolding s_def by simp
also have unfold2:"Babai_Help (uminus t) (RAT M) Mt 0 = uminus t" unfolding Babai_Help.simps by simp
also have unfold3:"s 0 = uminus t" using unfold1 unfold2 by simp
also have dim_eq:"dim_vec (s 0) = dim_vec (uminus t)" using unfold3 by simp
moreover have dim_minus:"dim_vec (uminus t) = n" by (metis index_uminus_vec(2) length_M)
then have "dim_vec (s 0) = n"
using dim_eq dim_minus
by simp
then have "(s 0) ∈ carrier_vec n"
using carrier_vecI[of "(s 0)" n]
by simp
then show ?case
by simp
next
case (Suc i)
then have leq: "i≤n" by linarith
have sub:"s (Suc i) = (s i) - ( (rat_of_int (calculate_c (s i) Mt (Suc i) ) ) ⋅⇩v (RAT M)!( (dim_vec (s i)) -(Suc i))) "
using sub_s Suc
by auto
moreover have prev_s_dim:"(s i)∈carrier_vec n"
using Suc
by simp
moreover have "dim_vec (s i)=n"
using Suc
by simp
then have "0≤(dim_vec (s i)) -(Suc i)∧ (dim_vec (s i)) -(Suc i)<n"
using Suc
by linarith
then have dim_m:"(dim_vec ((RAT M)!( (dim_vec (s i)) -(Suc i)))) = n"
using access_index_M_dim[of "(dim_vec (s i)) -(Suc i)"]
by simp
then have dim_qm:"dim_vec ( (rat_of_int (calculate_c (s i) Mt (Suc i) ) ) ⋅⇩v
(RAT M)!( (dim_vec (s i)) -(Suc i))) = n"
by simp
then have final_dim:"dim_vec ((s i) -
( (rat_of_int (calculate_c (s i) Mt (Suc i) ) ) ⋅⇩v (RAT M)!( (dim_vec (s i)) -(Suc i)))) = n"
using index_minus_vec(2) prev_s_dim dim_qm
by metis
show ?case
using final_dim sub carrier_vecI[of "s i" n]
by (metis carrier_vec_dim_vec)
qed
lemma dim_vecs_in_Mt:
fixes i::nat
assumes "i<n"
shows "dim_vec (Mt!i) = n"
using Mt_gso_connect[of "i"] M_locale_1 assms gram_schmidt_fs_Rn.gso_dim
by fastforce
lemma upper_tri:
fixes i::nat
and j::nat
assumes "j>i"
assumes "j<n"
shows "((RAT M)!i)∙ (Mt!j) =0"
proof(-)
have "(gs.gso j)∙ (RAT M)!i= 0"
using gram_schmidt_fs_lin_indpt.gso_scalar_zero[of n "(RAT M)" j i]
Mt_gso_connect[of "j"]
assms
M_locale_2
more_dim
by presburger
then have "(Mt!j)∙ ((RAT M)!i)= 0"
using Mt_gso_connect[of "j"] assms
by simp
then show ?thesis
using comm_scalar_prod[of "(Mt!j)" n "((RAT M)!i)"]
carrier_vecI[of "(Mt!j)" n]
carrier_vecI[of "((RAT M)!i)" n]
access_index_M_dim[of i]
dim_vecs_in_Mt[of j]
assms
by auto
qed
lemma one_diag:
fixes i::nat
assumes "0≤i"
assumes "i<n"
shows "((RAT M)!i)∙ (Mt!i)=sq_norm (Mt!i)"
proof(-)
have mu:"((RAT M)!i)∙(Mt!i) = (gs.μ i i)*sq_norm (Mt!i) "
using gram_schmidt_fs_lin_indpt.fi_scalar_prod_gso[of "n" "(RAT M)" i i]
M_locale_2
assms
more_dim
Mt_gso_connect
by presburger
moreover have "gs.μ i i=1"
by (meson gs.μ.elims order_less_imp_not_eq2)
then show ?thesis
using mu
by fastforce
qed
lemma coord_invariance:
fixes j::nat
fixes k::nat
fixes i::nat
assumes "k≤j"
assumes "j+i≤n"
assumes "k>0"
shows "(lattice_coord (s (j+i)))$(n-k) = (lattice_coord (s j))$(n-k)
∧ (s (j+i)) ∙ Mt!(n-k)=(s j) ∙ Mt!(n-k)"
using assms
proof(induct i)
case 0
show ?case by simp
next
case (Suc i)
have "j+ (Suc i) = Suc (j+i)" by simp
then have 1:"s (Suc (j+i)) =s (j + (Suc i))" by simp
then have sub:"s (Suc (j+i) ) =
(s (j+i)) -( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )
⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) )"
using sub_s[of "j+i "] Suc(3) by linarith
then have dim1: "dim_vec (s (j + i)) = n"
using s_dim[of "j+i"] using Suc(3) by auto
then have dim2: "dim_vec
(map of_int_hom.vec_hom M !
(dim_vec (s (j + i)) - Suc (j + i))) = n"
using access_index_M_dim[of "n - Suc (j + i)"] Suc(3)
by auto
have k_in_range:"0≤(n-k) ∧(n-k)<n" using Suc(2) Suc(3) Suc(4)
by simp
have index_in_range:"0≤(dim_vec (s (j+i))) -(Suc (j+i))∧(dim_vec (s (j+i))) -(Suc (j+i))<n"
using Suc(3) s_dim[of "j+i"]
by simp
moreover have carriers: "s (j+i) ∈ carrier_vec n∧
map of_int_hom.vec_hom M ! (dim_vec (s (j + i)) - Suc (j + i))∈carrier_vec n"
using dim1 dim2
carrier_vecI[of "s (j + i)" n]
carrier_vecI[of "map of_int_hom.vec_hom M ! (dim_vec (s (j + i)) - Suc (j + i))" n]
by fast
let ?sSuc = "(s (Suc (j+i)))"
let ?si = "(s (j+i))"
let ?c = "(rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )"
let ?ind = "(dim_vec (s (j+i))) -(Suc (j+i))"
have "?si - ?c⋅⇩v (RAT M)!?ind = ?si + (-?c)⋅⇩v (RAT M)!?ind"
using minus_add_uminus_vec[of ?si n "?c⋅⇩v (RAT M)!?ind"]
carriers
by fastforce
then have "(lattice_coord (?si - ?c⋅⇩v (RAT M)!?ind))$(n-k) =
(lattice_coord(?si))$(n-k) + (-?c)* (lattice_coord((RAT M)!?ind))$(n-k)"
using linear[of ?si "(RAT M)!?ind" "n-k" "-?c"] dim1 dim2 k_in_range
by metis
then have lin_lattice_coord:"(lattice_coord (?sSuc))$(n-k) =
(lattice_coord(?si))$(n-k) - ?c* (lattice_coord((RAT M)!?ind))$(n-k)"
using sub
by algebra
have neq:"Suc (j+i)≠k" using Suc(3) Suc(2) by auto
moreover have "((dim_vec (s (j+i))) -(Suc (j+i)))≠ (n-k)"
using s_dim[of "j+i"] neq Suc(3)
by (metis Suc(2) ‹j + Suc i = Suc (j + i)› diff_0_eq_0 diff_cancel2
diff_commute diff_diff_cancel diff_diff_eq diff_is_0_eq dim1)
moreover have "(lattice_coord ((RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i))) ) )$(n-k)=
(unit_vec n ( (dim_vec (s (j+i))) -(Suc (j+i))))$(n-k)"
using unit[of "dim_vec (s (j+i)) -(Suc (j+i))"] index_in_range by presburger
then have zero:"(lattice_coord ((RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i))) ) )$(n-k) = 0"
unfolding unit_vec_def
using neq calculation(3) k_in_range by fastforce
then have "(lattice_coord (s (Suc (j+i))) )$(n-k) = ( (lattice_coord (s (j+i)))$(n-k)) -
(rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )
*0"
using zero lin_lattice_coord by presburger
then have conclusion1:"(lattice_coord (s (Suc (j+i))) )$(n-k) = ( (lattice_coord (s (j+i)))$(n-k))"
by simp
have init_sub:"(s (Suc (j+i)))∙ Mt!(n-k) = ((s (j+i)) -
( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) ) ⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) ))
∙ (Mt!(n-k))"
using sub
by simp
moreover have carrier_prod:"( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )
⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) )∈carrier_vec n"
using smult_carrier_vec[of "(rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )"
"(RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) )" n] carrier_vecI dim2 by blast
moreover have l:"((s (j+i)) -
( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) ) ⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) ))
∙ (Mt!(n-k)) = (s (j+i))∙ (Mt!(n-k)) - ( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )
⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) )∙ (Mt!(n-k))"
using s_dim[of "j+i"]
assms(2)
access_index_M_dim
dim_vecs_in_Mt
carrier_vecI[of "Mt!(n-k)" n]
carrier_vecI[of "(RAT M)!((dim_vec (s (j+i))) -(Suc (j+i)))" n]
add_scalar_prod_distrib[of
"(s (j+i))"
n
"(rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) ) ⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) )"
" (Mt!(n-k))"]
using calculation(5) carriers k_in_range minus_scalar_prod_distrib by blast
moreover then have lin_scalar_prod:"((s (j+i)) -
( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) ) ⋅⇩v (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) ))
∙ (Mt!(n-k)) = (s (j+i))∙ (Mt!(n-k)) - (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) )
* ((RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) ∙ (Mt!(n-k)))"
by (metis dim2 dim_vecs_in_Mt k_in_range scalar_prod_smult_left)
moreover have step_past_index:"(dim_vec (s (j+i))) -(Suc (j+i))<n-k"
using s_dim[of "j+i"] Suc(3) Suc(2)
by (simp add: calculation(3) diff_le_mono2 dim1 le_SucI nat_less_le trans_le_add1)
moreover have "( (RAT M)!( (dim_vec (s (j+i))) -(Suc (j+i)) ) ∙ (Mt!(n-k) ) ) = 0"
using step_past_index upper_tri[of "(dim_vec (s (j+i))) -(Suc (j+i))" "n-k"] Suc(4)
by simp
then have "(s (Suc (j+i)))∙ Mt!(n-k) = (s (j+i))∙ Mt!(n-k) -
( (rat_of_int (calculate_c (s (j+i)) Mt (Suc (j+i)) ) ) *0)"
using lin_scalar_prod init_sub
by algebra
then have conclusion2:"(s (Suc (j+i)))∙ Mt!(n-k) = (s (j+i))∙ Mt!(n-k)" by auto
show ?case
by (metis Suc(2) Suc(3) Suc(4) Suc.hyps Suc_leD ‹j + Suc i = Suc (j + i)› conclusion1 conclusion2)
qed
lemma small_orth_coord:
fixes i::nat
assumes "1≤i"
assumes "i≤n"
shows "abs ( (s i) ∙ Mt!(n-i)) ≤ (sq_norm (Mt!(n-i)))*(1/2) "
proof(-)
have minus_plus:"Suc (i-1) = i" using assms(1) by auto
then have init_sub:"s i = (s (i-1))-( (rat_of_int (calculate_c (s (i-1)) Mt i ) ) ⋅⇩v (RAT M)!( (dim_vec (s (i-1))) -i))"
using sub_s[of "i-1"]
by (metis (full_types) Suc_le_eq assms(2) less_eq_nat.simps(1))
then have scalar_distrib:"(s i) ∙ Mt!(n-i) = (s (i-1)) ∙ Mt!(n-i)-(( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
⋅⇩v (RAT M)!( (dim_vec (s (i-1))) -i))∙Mt!(n-i))"
using add_scalar_prod_distrib[of "(s (i-1))" n "( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
⋅⇩v (RAT M)!( (dim_vec (s (i-1))) -i))" "Mt!(n-i)"]
s_dim[of "i-1"]
carrier_vecI[of "Mt!(n-i)"]
carrier_vecI[of "(RAT M)!( (dim_vec (s (i-1))) -i)"]
access_index_M_dim[of "( (dim_vec (s (i-1))) -i)"]
dim_vecs_in_Mt[of "n-i"]
init_sub
minus_scalar_prod_distrib[of "(s (i-1))" n "( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
⋅⇩v (RAT M)!( (dim_vec (s (i-1))) -i))" "Mt!(n-i)"]
by (metis Suc_leD assms(2) diff_Suc_less gs.smult_closed le0 minus_plus non_trivial)
also have scalar_commute:"(s (i-1)) ∙ Mt!(n-i)-(( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
⋅⇩v (RAT M)!( (dim_vec (s (i-1))) -i))∙Mt!(n-i)) =
(s (i-1)) ∙ Mt!(n-i)-( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
* (((RAT M)!( (dim_vec (s (i-1))) -i)) ∙Mt!(n-i) ))"
using scalar_prod_smult_left
carrier_vecI[of "Mt!(n-i)"]
carrier_vecI[of "(RAT M)!( (dim_vec (s (i-1))) -i)"]
access_index_M_dim
dim_vecs_in_Mt
by (smt (verit) Suc_le_D assms(2) diff_less index_minus_vec(2) index_smult_vec(2)
init_sub minus_plus s_dim zero_less_Suc)
moreover have index_in_range: "0≤n-i ∧ n-i<n"
using assms(1) assms(2)
by simp
moreover have sq_norm_eq:"((RAT M)!( (dim_vec (s (i-1))) -i)) ∙Mt!(n-i) = sq_norm (Mt!(n-i))"
using one_diag[of "n-i"]
s_dim[of "i-1"]
index_in_range
assms(1)
assms(2)
less_imp_diff_less
by simp
then have "(s i) ∙ Mt!(n-i) = (s (i-1)) ∙ Mt!(n-i)-
( (rat_of_int (calculate_c (s (i-1)) Mt i ) ) * sq_norm (Mt!(n-i)))"
using scalar_distrib scalar_commute sq_norm_eq by argo
then have final_sub:"abs((s i) ∙ Mt!(n-i)) = abs(( (rat_of_int (calculate_c (s (i-1)) Mt i ) )
* sq_norm (Mt!(n-i))) - (s (i-1)) ∙ Mt!(n-i)) "
using abs_minus_commute by simp
then have round_small:"abs(rat_of_int (calculate_c (s (i-1)) Mt i )-
(((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) )
/ (sq_norm_vec (Mt!( (dim_vec (s (i-1))) - i ) ) ) ))≤1/2"
by (metis calculate_c.simps of_int_round_abs_le)
moreover have pos:"0≤ sq_norm (Mt!(n-i))"
by (simp add: sq_norm_vec_ge_0)
then have "(sq_norm (Mt!(n-i)))*abs((rat_of_int (calculate_c (s (i-1)) Mt i )-
(((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) ) /
(sq_norm_vec (Mt!( (dim_vec (s (i-1))) - i ) ) ) )))
≤(sq_norm (Mt!(n-i)))*(1/2)"
using pos round_small mult_left_mono by blast
then have 2:"abs((sq_norm (Mt!(n-i)))*(rat_of_int (calculate_c (s (i-1)) Mt i )-
(((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) ) /
(sq_norm_vec (Mt!( (dim_vec (s (i-1))) - i ) ) ) )) )≤(sq_norm (Mt!(n-i)))*(1/2)"
using pos by (smt (verit) abs_mult abs_of_nonneg)
have "i≤n"
using assms(2) by simp
then have "abs(
(sq_norm (Mt!(n-i)))*(rat_of_int (calculate_c (s (i-1)) Mt i ))-
(sq_norm (Mt!(n-i)))*( ((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) )/
(sq_norm (Mt!(n-i))) )
)≤(sq_norm (Mt!(n-i)))*(1/2) "
using 2
s_dim[of i]
by (smt (verit) Rings.ring_distribs(4) Suc_leD minus_plus s_dim)
then have 1:"abs(
(sq_norm (Mt!(n-i)))*(rat_of_int (calculate_c (s (i-1)) Mt i ))-
((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) )*
( (sq_norm (Mt!(n-i)))/(sq_norm (Mt!(n-i))) )
)≤(sq_norm (Mt!(n-i)))*(1/2) "
using assms(2) s_dim
by (smt (z3) gs.cring_simprules(14) times_divide_eq_right)
moreover have nonzero:"sq_norm (Mt!(n-i))≠0"
using Mt_gso_connect[of "n-i"] assms
by (metis M_locale_2 gram_schmidt_fs_lin_indpt.sq_norm_pos index_in_range length_map rel_simps(70))
moreover have cancel:"(sq_norm (Mt!(n-i)))/(sq_norm (Mt!(n-i)))=1"
using nonzero
by auto
moreover have dim_match:"dim_vec (s (i-1)) = n"
using s_dim[of "i-1"] assms(2)
by linarith
then have final_ineq:"abs(
(sq_norm (Mt!(n-i)))*(rat_of_int (calculate_c (s (i-1)) Mt i ))-
((s (i-1)) ∙ (Mt!( (dim_vec (s (i-1))) - i ) ) )
)≤(sq_norm (Mt!(n-i)))*(1/2) "
using 1 cancel
by (smt (verit) gs.r_one)
then have rearrange_final_ineq: "abs( (rat_of_int (calculate_c (s (i-1)) Mt i ))
* (sq_norm (Mt!(n-i))) - ((s (i-1)) ∙ (Mt!( n - i ) ) ))≤(sq_norm (Mt!(n-i)))*(1/2)"
using dim_match
by algebra
show ?thesis
using final_sub rearrange_final_ineq
by argo
qed
lemma lattice_carrier: "L⊆ carrier_vec n"
proof-
have "x∈carrier_vec n" if x_def:"x∈L" for x
proof-
obtain f where f_def:"x = sumlist (map (λi. (f i)⋅⇩v M!i ) [0..<n])"
using x_def unfolding L_def lattice_of_def by fast
have "(f i)⋅⇩v M!i∈carrier_vec n" if "0≤i∧i<n" for i
using access_index_M_dim[of i]
by (metis carrier_vec_dim_vec map_carrier_vec nth_map smult_closed that)
then have "set (map (λi. (f i)⋅⇩v M!i ) [0..<n]) ⊆ carrier_vec n" by auto
then have "sumlist (map (λi. (f i)⋅⇩v M!i ) [0..<n]) ∈ carrier_vec n" by simp
then show "x∈carrier_vec n" using f_def by fast
qed
then show ?thesis by fast
qed
section ‹Lattice Lemmas›
lemma lattice_sum_close:
fixes u::"int vec" and v::"int vec"
assumes "u∈L" "v∈L"
shows "u+v∈L"
proof -
let ?mM = "mat_of_cols n M"
have 1:"?mM ∈carrier_mat n n" using dim_vecs_in_M by fastforce
have set_M: "set M ⊆ carrier_vec n"
using dim_vecs_in_M carrier_vecI by blast
have as_mat_mult:"lattice_of M = {y∈carrier_vec n. ∃x∈carrier_vec n. ?mM *⇩v x = y}"
using lattice_of_as_mat_mult[OF set_M] by blast
then obtain u1 where u1_def:"u = ?mM *⇩v u1 ∧ u1∈carrier_vec n" using assms unfolding L_def by auto
obtain v1 where v1_def:"v = ?mM *⇩v v1 ∧ v1∈carrier_vec n"
using assms as_mat_mult unfolding L_def by auto
have "u1+v1∈carrier_vec n" using u1_def v1_def by blast
moreover have "?mM*⇩v (u1+v1) = u+v"
using u1_def v1_def 1 mult_add_distrib_mat_vec[of ?mM n n u1 v1]
by metis
moreover have "u+v∈carrier_vec n" using assms lattice_carrier by blast
ultimately show "u+v∈L"
using as_mat_mult unfolding L_def
by blast
qed
lemma lattice_smult_close:
fixes u::"int vec" and q::int
assumes "u∈L"
shows "q⋅⇩v u∈L"
proof-
let ?mM = "mat_of_cols n M"
have 1:"?mM ∈carrier_mat n n" using dim_vecs_in_M by fastforce
have set_M: "set M ⊆ carrier_vec n"
using dim_vecs_in_M carrier_vecI by blast
have as_mat_mult:"lattice_of M = {y∈carrier_vec n. ∃x∈carrier_vec n. ?mM *⇩v x = y}"
using lattice_of_as_mat_mult[OF set_M] by blast
then obtain v::"int vec" where v_def:"u = ?mM *⇩v v∧v∈carrier_vec n"
using assms unfolding L_def by auto
then have "q⋅⇩v v ∈carrier_vec n" by blast
moreover then have "q⋅⇩v u= ?mM *⇩v (q⋅⇩v v)" using 1 v_def by fastforce
ultimately show "q⋅⇩v u ∈ L"
by (metis (mono_tags, lifting) L_def as_mat_mult assms mem_Collect_eq smult_closed)
qed
lemma smult_vec_zero:
fixes v ::"'a::ring vec"
shows "0 ⋅⇩v v = 0⇩v (dim_vec v)"
unfolding smult_vec_def vec_eq_iff
by (auto)
lemma coset_s:
fixes i::nat
assumes "i≤n"
shows "s i ∈coset"
using assms
proof(induct i)
case 0
have "s 0 = -t" unfolding s_def by simp
moreover have carrier_mt:"-t∈carrier_vec n" using length_M carrier_vecI[of t n] by fastforce
ultimately have pzero:"s 0 = of_int_hom.vec_hom (0⇩v n) -t" by fastforce
let ?zero = "λ j. 0"
have "0<length M" using non_trivial by fast
then have "M!0 ∈ set M" by force
then have "M!0∈L" using basis_in_latticeI[of M "M!0"] dim_vecs_in_M carrier_vecI L_def
by blast
then have "0⇩v n ∈L"
using lattice_smult_close[of "M!0" 0] smult_vec_zero[of "M!0"] access_index_M_dim[of 0] non_trivial
unfolding L_def
by fastforce
then show ?case using pzero by blast
next
case (Suc i)
let ?q = "(rat_of_int (calculate_c (s i) Mt (Suc i) ) )"
let ?ind = "( (dim_vec (s i)) -(Suc i))"
have sub:"s (Suc i) = (s i) -
( ?q ⋅⇩v (RAT M)!?ind)"
using sub_s[of i] Suc.prems by linarith
have "s i ∈coset" using Suc by auto
then obtain x where x_def:"x∈L ∧ (s i) = of_int_hom.vec_hom x-t" by blast
have "( ?q ⋅⇩v (RAT M)!?ind)∈ of_int_hom.vec_hom` L"
proof-
have "dim_vec (s i) = n" using s_dim[of i] Suc.prems by fastforce
then have in_range:"?ind<n∧ 0≤?ind" using Suc.prems by simp
then have com_hom:"(RAT M)!(?ind) = of_int_hom.vec_hom (M!?ind)" by auto
have "M!?ind∈set M" using in_range by simp
then have mil:"M!?ind ∈ L" using basis_in_latticeI[of M "M!?ind"] dim_vecs_in_M carrier_vecI L_def
by blast
moreover have "?q⋅⇩v(of_int_hom.vec_hom (M!?ind)) =
of_int_hom.vec_hom ((calculate_c (s i) Mt (Suc i) ) ⋅⇩v M!?ind)"
by fastforce
moreover have "(calculate_c (s i) Mt (Suc i) ) ⋅⇩v M!?ind∈L"
using lattice_smult_close[of "M!?ind" "(calculate_c (s i) Mt (Suc i) )"] mil by simp
ultimately show "( ?q ⋅⇩v (RAT M)!?ind) ∈ of_int_hom.vec_hom` L"
using com_hom
by force
qed
then obtain y where y_def:"( ?q ⋅⇩v (RAT M)!?ind) = of_int_hom.vec_hom y∧ y∈L" by blast
have carrier_x: "x∈carrier_vec n" using lattice_carrier x_def by blast
have carrier_y: "y∈carrier_vec n" using lattice_carrier y_def by blast
then have carrier_my: "-y∈carrier_vec n" by simp
then have 1:"-( ?q ⋅⇩v (RAT M)!?ind) = of_int_hom.vec_hom (-y)" using y_def by fastforce
then have "s (Suc i) = of_int_hom.vec_hom x-t+ of_int_hom.vec_hom (-y)"
using sub x_def y_def 1 by fastforce
then have "s (Suc i) = of_int_hom.vec_hom x + of_int_hom.vec_hom (-y) - t"
using lattice_carrier x_def y_def length_M
by fastforce
moreover have "of_int_hom.vec_hom x + of_int_hom.vec_hom (-y) = of_int_hom.vec_hom (x+ -y)"
using carrier_my carrier_x by fastforce
ultimately have 2:"s (Suc i) = of_int_hom.vec_hom (x+ -y) -t "
by metis
have "-y = -1 ⋅⇩v y" by auto
then have "-y∈L" using lattice_smult_close y_def by simp
then have "x+-y∈L" using lattice_sum_close x_def by simp
then show ?case using 2 by fast
qed
lemma subtract_coset_into_lattice:
fixes v::"rat vec"
fixes w::"rat vec"
assumes "v∈coset"
assumes "w∈coset"
shows " (v-w)∈of_int_hom.vec_hom` L"
proof-
obtain l1 where l1_def:"v=l1-t∧ l1∈of_int_hom.vec_hom` L" using assms(1) by blast
obtain l2 where l2_def:"w = l2-t∧ l2∈of_int_hom.vec_hom` L" using assms(2) by blast
have carrier_l1:"l1 ∈ carrier_vec n" using lattice_carrier l1_def by force
have carrier_l2:"l2 ∈ carrier_vec n" using lattice_carrier l2_def by force
obtain l1p where l1p_def:"l1 = of_int_hom.vec_hom l1p ∧ l1p∈L" using l1_def by fast
obtain l2p where l2p_def:"l2 = of_int_hom.vec_hom l2p ∧ l2p∈L" using l2_def by fast
have "-l2p = -1⋅⇩v l2p" using carrier_l2 by fastforce
then have ml2p:"-l2p∈ L" using lattice_smult_close[of l2p "-1"] l2p_def by presburger
then have "of_int_hom.vec_hom (-l2p)∈ of_int_hom.vec_hom` L" by simp
moreover have "of_int_hom.vec_hom (-l2p) = -l2" using l2p_def by fastforce
then have "l1-l2 = of_int_hom.vec_hom (l1p - l2p)" using l1p_def l2p_def carrier_l1 carrier_l2 by auto
moreover have "l1p-l2p∈L" using lattice_sum_close[of l1p "-l2p"]
l1p_def l2p_def ml2p carrier_l1 carrier_l2
by (simp add: minus_add_uminus_vec)
ultimately have "l1-l2∈ of_int_hom.vec_hom` L" by fast
moreover have "v-w = l1-l2" using l1_def l2_def length_M carrier_vecI carrier_l1 carrier_l2 by force
ultimately show ?thesis by simp
qed
lemma t_in_coset:
shows "uminus t ∈ coset"
using coset_s[of 0] Babai_Help.simps unfolding s_def by simp
section "Lemmas on closest distance"
lemma closest_distance_sq_pos: "closest_distance_sq≥0"
proof-
have "∀N∈ {real_of_rat (sq_norm x::rat) |x. x ∈ coset}. 0≤N"
using sq_norm_vec_ge_0 by auto
moreover have "{real_of_rat (sq_norm x::rat) |x. x ∈ coset}≠{}" using t_in_coset by blast
ultimately have "0≤Inf {real_of_rat (sq_norm x::rat) |x. x ∈ coset}"
by (meson cInf_greatest)
then show ?thesis unfolding closest_distance_sq_def by blast
qed
definition witness:: "rat vec⇒rat ⇒ bool"
where "witness v eps_closest = (sq_norm v ≤ eps_closest ∧ v∈coset∧dim_vec v = n)"
definition epsilon::real where "epsilon = 11/10"
definition close_condition::"rat ⇒ bool"
where "close_condition eps_closest ≡
(if closest_distance_sq = 0 then 0≤ real_of_rat eps_closest
else real_of_rat (eps_closest)>closest_distance_sq)
∧ (real_of_rat (eps_closest)≤epsilon*closest_distance_sq)"
lemma close_rat:
obtains eps_closest::rat
where "close_condition eps_closest"
proof(cases "closest_distance_sq = 0")
case t:True
then have "epsilon*closest_distance_sq = real_of_rat (0::rat)" by simp
then have "real_of_rat (0::rat)≤ epsilon*closest_distance_sq∧closest_distance_sq
≤(real_of_rat (0::rat))"
using t by force
then show ?thesis
using that t unfolding close_condition_def by metis
next
case f:False
then have "0<closest_distance_sq"
using closest_distance_sq_pos by linarith
moreover have "(1::real)<epsilon" unfolding epsilon_def by simp
ultimately have "closest_distance_sq<epsilon*closest_distance_sq" by simp
then show ?thesis
using Rats_dense_in_real[of closest_distance_sq "epsilon*closest_distance_sq"] that
unfolding close_condition_def
by (metis Rats_cases less_eq_real_def)
qed
definition eps_closest::rat
where "eps_closest = (if ∃r. close_condition r then SOME r. close_condition r else 0)"
lemma eps_closest_lemma: "close_condition eps_closest"
using close_rat unfolding eps_closest_def by (metis (full_types))
lemma rational_tri_ineq:
fixes v::"rat vec"
fixes w::"rat vec"
assumes "dim_vec v = dim_vec w"
shows "(sq_norm (v+w))≤ 4*(Max {(sq_norm v), (sq_norm w)})"
proof-
let ?d = "dim_vec w"
let ?M = "Max {(sq_norm v), (sq_norm w)}"
have carr_v:"v∈carrier_vec ?d" using assms carrier_vecI[of v ?d] by fastforce
have carr_w:"w∈carrier_vec ?d" using carrier_vecI[of w ?d] by fastforce
have carr_vw:"v+w∈carrier_vec ?d" using carr_v carr_w add_carrier_vec by blast
have "sq_norm (v+w) = (v+w)∙(v+w)"
by (simp add: sq_norm_vec_as_cscalar_prod)
also have "(v+w)∙(v+w) = v∙(v+w)+w∙(v+w)"
using add_scalar_prod_distrib[of v ?d w "v+w"]
carr_v carr_w carr_vw by blast
also have "v∙(v+w)+w∙(v+w) = v∙v+v∙w+w∙v+w∙w"
using scalar_prod_add_distrib[of v ?d v w]
scalar_prod_add_distrib[of w ?d v w]
carr_v carr_w carr_vw by algebra
also have "v∙w=w∙v"
using carr_v carr_w comm_scalar_prod by blast
also have "v∙v = sq_norm v"
using sq_norm_vec_as_cscalar_prod[of v] by force
also have "w∙w = sq_norm w"
using sq_norm_vec_as_cscalar_prod[of w] by force
finally have "sq_norm (v+w) = sq_norm v + sq_norm w + 2*(w∙v)" by force
also have b1:"sq_norm v≤?M" by force
also have b2:"sq_norm w≤?M" by force
also have "2*(w∙v)≤2*(Max {(sq_norm v), (sq_norm w)})"
proof-
have "(w∙v)^2≤ (sq_norm v) * (sq_norm w)"
using scalar_prod_Cauchy[of w ?d v] carr_w carr_v by algebra
also have "(sq_norm v) * (sq_norm w)≤?M*?M"
using b1 b2 sq_norm_vec_ge_0[of w] sq_norm_vec_ge_0[of v]
mult_mono[of "sq_norm v" ?M "sq_norm w" ?M] by linarith
also have "?M*?M = ?M^2"
using power2_eq_square[of ?M] by presburger
finally have "(w∙v)^2≤?M^2" by blast
also have "(w∙v)^2=abs(w∙v)^2" by force
finally have "abs(w∙v)^2≤?M^2" by presburger
moreover have "0≤abs(w∙v)" by fastforce
moreover have "0≤?M"
using sq_norm_vec_ge_0[of w] sq_norm_vec_ge_0[of v] by fastforce
ultimately have "abs(w∙v)≤?M"
using power2_le_imp_le by blast
also have "(w∙v)≤abs(w∙v)" by force
finally show ?thesis by linarith
qed
finally show ?thesis by auto
qed
lemma witness_exists:
shows "∃v. witness v eps_closest"
proof(cases "closest_distance_sq = 0")
case t:True
have "eps_closest = 0"
using eps_closest_lemma t
unfolding witness_def unfolding close_condition_def
by auto
then have equiv:"?thesis = (∃v. v∈coset∧ (dim_vec v = n) ∧ (sq_norm v) ≤ 0)"
unfolding witness_def eps_closest_def by auto
show ?thesis
proof(rule ccontr)
assume contra:"¬?thesis"
have "{real_of_rat (sq_norm x::rat) |x. x ∈ coset}≠{}" using t_in_coset by fast
then have limit_point:"∃v::rat vec. real_of_rat (sq_norm v) < (eps::real) ∧ v∈coset" if "0<eps" for eps
using t cInf_lessD[of "{real_of_rat (sq_norm x::rat) |x. x ∈ coset}" eps] that
unfolding closest_distance_sq_def by auto
moreover have "0<real_of_rat ((sq_norm ((RAT M)!0) )/ (4*α^(n-1)))"
proof-
have "0<1/(4*α^(n-1))" using non_trivial unfolding α_def by force
moreover have "0< (sq_norm ((RAT M)!0))"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" 0]
gram_schmidt_fs_lin_indpt.sq_norm_gso_le_f[of n "RAT M" 0]
M_locale_2 non_trivial
by fastforce
ultimately show ?thesis by auto
qed
ultimately obtain v::"rat vec" where v_def:"real_of_rat (sq_norm v)
< real_of_rat ((sq_norm ((RAT M)!0) )/ (4*α^(n-1)))∧ v∈coset"
by presburger
then have "dim_vec v = n"
using length_M by force
then have "0< real_of_rat (sq_norm v)"
using equiv contra v_def by auto
then obtain w::"rat vec" where w_def:"real_of_rat (sq_norm w) < real_of_rat (sq_norm v)∧w∈coset"
using limit_point by fast
then have small_w:"real_of_rat (sq_norm w)<real_of_rat ((sq_norm ((RAT M)!0) )/ (4*α^(n-1)))"
using v_def by argo
have lat:"w-v∈ of_int_hom.vec_hom` L" using subtract_coset_into_lattice[of w v]
using v_def w_def by force
then obtain l where l_def:"l∈L∧w-v=of_int_hom.vec_hom l" by blast
then have "of_int_hom.vec_hom l ∈ gs.lattice_of (RAT M)"
using lattice_of_of_int[of M n l] dim_vecs_in_M carrier_vecI L_def by blast
then have lat_hom:"w-v ∈ gs.lattice_of (RAT M)" using l_def by simp
have "sq_norm v ≠ sq_norm w" using w_def by auto
then have neq:"w≠v" by meson
have c1:"w∈carrier_vec n" using length_M w_def lattice_carrier carrier_dim_vec by fastforce
moreover have c2:"v∈carrier_vec n" using length_M v_def lattice_carrier carrier_dim_vec by fastforce
ultimately have c3:"w-v∈carrier_vec n" by simp
have neqzero:"w-v≠0⇩v n"
proof(rule ccontr)
assume c:"¬?thesis"
have "w-v=0⇩v n" using c by blast
then have "w=v+ 0⇩v n" using c1 c2 c3
by (smt (verit, ccfv_SIG) gs.M.add.r_inv_ex minus_add_minus_vec minus_cancel_vec minus_zero_vec right_zero_vec)
then show False using c2 neq by simp
qed
then have "w-v ∈ gs.lattice_of (RAT M) - {0⇩v n}" using lat_hom by blast
moreover have "α^(n-1) * (sq_norm (w-v)) < (sq_norm ((RAT M)!0) )"
proof-
have "w-v = w+ (-v)" by fastforce
then have "sq_norm (w-v) = sq_norm (w+(-v))" by simp
also have "sq_norm (w+(-v)) ≤ 4*Max({sq_norm w, sq_norm (-v)})"
using rational_tri_ineq[of w "-v"] c1 c2 by fastforce
also have "sq_norm (-v) = sq_norm v"
proof-
have "-v = (-1)⋅⇩v v" by fastforce
then have "sq_norm (-v) = ((-1)⋅⇩v v)∙((-1)⋅⇩v v)" using sq_norm_vec_as_cscalar_prod[of "-v"] by force
then have "sq_norm (-v) = (-1)*(-1)*(v∙v)" using c1 c2 by simp
then show ?thesis using sq_norm_vec_as_cscalar_prod[of "v"] by simp
qed
also have "Max({sq_norm w, sq_norm (v)})<((sq_norm ((RAT M)!0) )/ (4*α^(n-1)))"
using v_def small_w of_rat_less by auto
finally have "sq_norm (w-v)<4*((sq_norm ((RAT M)!0) )/ (4*α^(n-1)))" by linarith
then have "sq_norm (w-v)<(sq_norm ((RAT M)!0) )/ (α^(n-1))" by linarith
moreover have p:"0<α^(n-1)" unfolding α_def by fastforce
ultimately show ?thesis using p
by (metis gs.cring_simprules(14) pos_less_divide_eq)
qed
ultimately show False
using gram_schmidt_fs_lin_indpt.weakly_reduced_imp_short_vector[of n "(RAT M)" α "w-v"]
M_locale_2 reduced
unfolding α_def gs.reduced_def L_def by force
qed
next
case False
then have "closest_distance_sq < real_of_rat eps_closest"
using eps_closest_lemma unfolding eps_closest_def close_condition_def
by presburger
moreover have "{real_of_rat (sq_norm x::rat) |x. x ∈ coset}≠{}" using t_in_coset by fast
ultimately obtain l where "l∈{real_of_rat (sq_norm x::rat) |x. x ∈ coset}∧ l< real_of_rat eps_closest"
using closest_distance_sq_pos
unfolding closest_distance_sq_def
by (meson cInf_lessD)
moreover then obtain v::"rat vec" where "l = real_of_rat (sq_norm v) ∧ v∈coset" by blast
ultimately show ?thesis unfolding witness_def lattice_carrier
by (smt (verit) length_M index_minus_vec(2) mem_Collect_eq of_rat_less_eq)
qed
section ‹More linear algebra lemmas›
lemma carrier_Ms:
shows "mat_M ∈carrier_mat n n" "mat_M_inv ∈carrier_mat n n"
using M_dim M_inv_dim
apply blast
by (simp add: M_inv_dim(1) M_inv_dim(2) carrier_matI)
lemma carrier_L:
fixes v::"rat vec"
assumes "dim_vec v = n"
shows "lattice_coord v∈carrier_vec n"
unfolding lattice_coord_def
using mult_mat_vec_carrier[of "mat_M_inv" n n v]
carrier_Ms
carrier_vecI[of "v"]
assms(1)
by fast
lemma sumlist_index_commute:
fixes Lst::"rat vec list"
fixes i::nat
assumes "set Lst⊆carrier_vec n"
assumes "i<n"
shows "(gs.sumlist Lst)$i = sum_list (map (λj. (Lst!j)$i) [0..<(length Lst)])"
using assms
proof(induct Lst)
case Nil
have "gs.sumlist Nil = 0⇩v n" using assms unfolding gs.sumlist_def by auto
then have lhs:"(gs.sumlist Nil)$i = 0" using assms(2) by auto
have "[0..<(length Nil)] = Nil" by simp
then have "(map (λj. (Nil!j)$i) [0..<(length Nil)]) = Nil" by blast
then have "sum_list (map (λj. (Nil!j)$i) [0..<(length Nil)]) = 0" by simp
then show ?case using lhs by simp
next
case (Cons a Lst)
let ?CaLst = "Cons a Lst"
have "set Lst ⊆ carrier_vec n" using Cons.prems by auto
then have carr:"gs.sumlist Lst ∈carrier_vec n" using assms gs.sumlist_carrier[of Lst ]
by blast
have "gs.sumlist (Cons a Lst) = a + gs.sumlist Lst" by simp
then have lhs:"(gs.sumlist ?CaLst)$i = a$i + (gs.sumlist Lst)$i" using assms carr by simp
have "sum_list (map (λj. (?CaLst!j)$i) [0..<(length ?CaLst)]) = sum_list (map (λl. l$i) ?CaLst)"
by (smt (verit) length_map map_eq_conv' map_nth nth_map)
moreover have "sum_list (map (λl. l$i) ?CaLst) = a$i + sum_list (map (λl. l$i) Lst)" by simp
moreover have "sum_list (map (λl. l$i) Lst) = sum_list (map (λj. (Lst!j)$i) [0..<(length Lst)])"
by (smt (verit) length_map map_eq_conv' map_nth nth_map)
moreover have "sum_list (map (λj. (Lst!j)$i) [0..<(length Lst)]) = (gs.sumlist Lst)$i"
using Cons.prems Cons.hyps by simp
ultimately show ?case using lhs
by argo
qed
lemma mat_mul_to_sum_list:
fixes A::"rat mat"
fixes v::"rat vec"
assumes "dim_vec v = dim_col A"
assumes "dim_row A = n"
shows "A*⇩vv = gs.sumlist (map (λj. v$j ⋅⇩v (col A j)) [0 ..< dim_col A])"
proof-
have carrier:"set (map (λj. v $ j ⋅⇩v col A j) [0..<dim_col A]) ⊆ Rn"
by (smt (verit) assms(2) carrier_dim_vec dim_col ex_map_conv index_smult_vec(2) subset_code(1))
have "(A*⇩vv)$i = gs.sumlist (map (λj. v$j ⋅⇩v (col A j)) [0 ..< dim_col A])$i" if small:"i<dim_row A" for i
proof-
let ?rAi = "row A i"
have 1:"(A*⇩vv)$i = ?rAi ∙ v" using small by simp
have 2:"?rAi ∙ v = sum_list (map (λj. (?rAi$j)*(v$j)) [0..<dim_col A])"
using assms sum_set_upt_conv_sum_list_nat unfolding scalar_prod_def by auto
have "?rAi$j*(v$j) = (v$j ⋅⇩v (col A j))$i" if jsmall:"j<dim_col A" for j
unfolding row_def col_def using small jsmall
by force
then have "(map (λj. (?rAi$j)*(v$j)) [0..<dim_col A]) = (map (λj. (v$j ⋅⇩v (col A j))$i) [0..<dim_col A])"
by fastforce
then have "(A*⇩vv)$i = sum_list (map (λj. (v$j ⋅⇩v (col A j))$i) [0..<dim_col A])"
using 1 2 by algebra
then show ?thesis using sumlist_index_commute[of "map (λj. v$j ⋅⇩v (col A j)) [0 ..< dim_col A]" i]
small assms(2) carrier
by (smt (verit) gs.sumlist_vec_index length_map map_equality_iff nth_map subset_code(1))
qed
moreover have "dim_vec (A*⇩vv) = dim_row A" by fastforce
moreover have "dim_vec (gs.sumlist (map (λj. v$j ⋅⇩v (col A j)) [0 ..< dim_col A])) = n"
using carrier by auto
ultimately show ?thesis using assms
by auto
qed
lemma recover_from_lattice_coord:
fixes v::"rat vec"
assumes "dim_vec v = n"
shows "v = gs.sumlist (map (λi. (lattice_coord v)$i ⋅⇩v (RAT M)!i) [0 ..< n]) "
proof -
have "(mat_M * mat_M_inv)*⇩v v= mat_M*⇩v(lattice_coord v)"
unfolding lattice_coord_def
using assms(1) carrier_Ms carrier_vecI[of v]
assoc_mult_mat_vec[of "mat_M" n n mat_M_inv n v]
by presburger
then have "(1⇩m n)*⇩vv=mat_M*⇩v(lattice_coord v)"
using inv1
by simp
then have "v = mat_M*⇩v(lattice_coord v)"
by (metis assms carrier_vec_dim_vec one_mult_mat_vec)
then have pre:"v = gs.sumlist (map (λi. (lattice_coord v)$i ⋅⇩v col mat_M i) [0 ..< dim_col mat_M]) "
using mat_mul_to_sum_list[of "lattice_coord v" "mat_M"]
M_dim
assms
dim_preserve_lattice_coord
by simp
moreover have "col mat_M i = (RAT M)!i" if "i<n" for i
using vec_to_col
by (simp add: that)
ultimately have "(map (λi. (lattice_coord v)$i ⋅⇩v col mat_M i) [0 ..< dim_col mat_M]) =
(map (λi. (lattice_coord v)$i ⋅⇩v (RAT M)!i) [0 ..< n])" using M_dim
by simp
then show "v = gs.sumlist (map (λi. (lattice_coord v)$i ⋅⇩v (RAT M)!i) [0 ..< n])"
using pre by presburger
qed
lemma sumlist_linear_coord:
fixes Lst::"int vec list"
assumes "⋀i. i<length Lst ⟹dim_vec (Lst!i) = n"
shows "lattice_coord (map_vec rat_of_int (sumlist Lst)) = gs.sumlist (map lattice_coord (RAT Lst))"
using assms
proof(induct Lst)
case Nil
have rhs:"gs.sumlist(map lattice_coord (RAT Nil)) = 0⇩v n" by fastforce
have "map_vec rat_of_int (sumlist Nil) = 0⇩v n" by auto
then have "lattice_coord (map_vec rat_of_int (sumlist Nil)) = 0⇩v n"
unfolding lattice_coord_def using M_inv_dim
by (metis carrier_Ms(2) gs.M.add.r_cancel_one' gs.M.zero_closed mult_add_distrib_mat_vec mult_mat_vec_carrier)
then show ?case using rhs by simp
next
case (Cons a Lst)
let ?CaLst = "Cons a Lst"
let ?ra = "of_int_hom.vec_hom a"
have dim:"i∈set ?CaLst ⟹ dim_vec i = n" for i using Cons.prems
by (metis in_set_conv_nth)
then have i_lt: "(i < length Lst ⟹ dim_vec (Lst ! i) = n)" for i
using Cons.prems carrier_dim_vec by auto
have carrier:"set ?CaLst⊆ carrier_vec n" using Cons.prems
using carrier_vecI dim by fast
then have carrier_sumCaLst: "(sumlist ?CaLst)∈carrier_vec n" by force
have carrier_a: "a ∈ carrier_vec n" using carrier by force
have carrier_Lst:"set Lst ⊆ carrier_vec n" using carrier by simp
have lhs:"lattice_coord (map_vec rat_of_int (sumlist ?CaLst)) = (lattice_coord ?ra) + gs.sumlist (map lattice_coord (RAT Lst))"
proof-
have carrier_sumLst: "sumlist Lst∈carrier_vec n" using carrier_Lst by force
have "sumlist ?CaLst = a + sumlist Lst" by force
then have "(map_vec rat_of_int (sumlist ?CaLst)) = ?ra + (map_vec rat_of_int (sumlist Lst))"
using carrier_a carrier_sumLst carrier_sumCaLst by auto
then have "lattice_coord (map_vec rat_of_int (sumlist ?CaLst))
= lattice_coord(?ra) + lattice_coord(map_vec rat_of_int (sumlist Lst))"
unfolding lattice_coord_def
using carrier_sumCaLst carrier_a carrier_sumLst
by (metis carrier_Ms(2) map_carrier_vec mult_add_distrib_mat_vec)
then show ?thesis using i_lt Cons.hyps
by algebra
qed
moreover have rhs:"gs.sumlist (map lattice_coord (RAT ?CaLst)) =
(lattice_coord ?ra) + gs.sumlist (map lattice_coord (RAT Lst))"
by fastforce
ultimately show ?case by argo
qed
lemma integral_sum:
fixes l::nat
assumes "⋀j1. j1 < l ⟹
map f [0..<l] ! j1 ∈ ℤ"
shows "sum_list
(map f [0..<l]) ∈ ℤ"
using assms
proof(induct l)
case 0
have "(map f [0..<0]) = Nil" by auto
then have "sum_list (map f [0..<0]) = 0" by simp
then show ?case by simp
next
case (Suc l)
have nontriv:"Suc l>0" by simp
have break:"sum_list (map f [0..<(Suc l)]) = sum_list (map f [0..<l]) + (f l)" by fastforce
have "l<Suc l" by simp
then have "[0..<(Suc l)]!l = l"
by (metis nth_upt plus_nat.add_0)
moreover then have "f ([0..<(Suc l)] ! l) = (map f [0..<(Suc l)]) ! l"
by (metis One_nat_def Suc_diff_Suc diff_Suc_1 local.nontriv nat_SN.default_gt_zero
nth_map_upt nth_upt plus_1_eq_Suc real_add_less_cancel_right_pos)
ultimately have z:"f l ∈ℤ" using Suc.prems by fastforce
have "⋀j1. j1 < l ⟹
map f [0..<l] ! j1 ∈ ℤ"
by (metis Suc.prems diff_Suc_1' diff_Suc_Suc less_SucI nth_map_upt)
then have "sum_list (map f [0..<l])∈ℤ" using Suc by blast
then show ?case using z break by force
qed
lemma int_coord:
fixes i::nat
assumes "0≤i"
assumes "i<n"
fixes v::"int vec"
assumes "v∈L"
assumes "dim_vec v = n"
shows "(lattice_coord (map_vec rat_of_int v))$i∈ℤ"
proof -
obtain w where w_def:"v = sumlist (map (λ i. of_int (w i) ⋅⇩v M ! i) [0 ..< length M])"
using L_def assms(3) vec_module.lattice_of_def
by blast
let ?Lst = "(map (λ i. of_int (w i) ⋅⇩v M ! i) [0 ..< length M])"
have dims_j:"dim_vec (?Lst!j) = n" if j_lt:"j<length ?Lst" for j
using access_index_M_dim carrier_vecI j_lt by force
let ?recover = "(map lattice_coord (RAT ?Lst))"
have 1:"lattice_coord (map_vec rat_of_int v) = gs.sumlist ?recover"
using sumlist_linear_coord[of ?Lst]
w_def
dims_j
by blast
have int_recover:"⋀j. j<n⟹(?recover!j)$i ∈ℤ∧ (dim_vec (?recover!j)) = n"
proof -
fix j::nat
assume small:"j<n"
have "?recover!j = lattice_coord ((RAT ?Lst)!j) "
using List.nth_map[of j "(RAT ?Lst)" lattice_coord]
small
by simp
then have "?recover!j = lattice_coord (of_int_hom.vec_hom (?Lst!j))"
using List.nth_map[of j ?Lst of_int_hom.vec_hom]
small
by simp
then have "?recover!j = lattice_coord (of_int_hom.vec_hom (of_int (w j) ⋅⇩v M ! j))"
using List.nth_map[of j "[0 ..< length M]" "(λ i. of_int (w i) ⋅⇩v M ! i)"]
small
by simp
then have commuted_maps:"?recover!j = mat_M_inv *⇩v (of_int_hom.vec_hom (of_int (w j) ⋅⇩v M ! j)) "
unfolding lattice_coord_def
by simp
then have "?recover!j = mat_M_inv *⇩v((of_int (of_int (w j))) ⋅⇩v of_int_hom.vec_hom (M ! j)) "
using of_int_hom.vec_hom_smult[of "of_int (w j)" "M ! j"]
by metis
then have "?recover!j = (of_int (of_int (w j))) ⋅⇩v (mat_M_inv *⇩v of_int_hom.vec_hom (M ! j))"
using mult_mat_vec[of "mat_M_inv" n n "of_int_hom.vec_hom (M ! j)" "(of_int (of_int (w j)))"]
carrier_Ms
access_index_M_dim[of j]
carrier_vecI[of "of_int_hom.vec_hom (M ! j)" n]
by (simp add: small)
then have "?recover!j = (of_int (of_int (w j))) ⋅⇩v (lattice_coord (of_int_hom.vec_hom (M ! j)))"
unfolding lattice_coord_def
by simp
then have recover_unit:"?recover!j = (of_int (of_int (w j))) ⋅⇩v (unit_vec n j)"
using unit[of j]
small
by simp
then have "(?recover!j)$i=((of_int (of_int (w j))) ⋅⇩v (unit_vec n j))$i"
by simp
then have "(?recover!j)$i = (of_int (of_int (w j))) * (unit_vec n j)$i"
by (simp add: assms(2))
then have "(?recover!j)$i = (of_int (of_int (w j))) * (if i=j then 1 else 0)"
using small assms(2)
by simp
moreover have "(if i=j then 1 else 0) ∈ℤ"
by simp
moreover have "(of_int (of_int (w j)))∈ℤ"
by simp
moreover have "dim_vec (?recover!j) = n"
using recover_unit
smult_closed[of "(unit_vec n j)" "(of_int (of_int (w j)))"]
unit_vec_carrier[of n j]
by force
ultimately show "(?recover!j)$i ∈ℤ ∧ dim_vec (?recover!j) = n"
by simp
qed
then have "∀v∈set ?recover. dim_vec v = n"
by auto
then have "set ?recover⊆carrier_vec n"
using carrier_vecI
by blast
then have "(gs.sumlist ?recover)$i = sum_list (map (λj. (?recover!j)$i) [0..<(length ?recover)])"
using sumlist_index_commute[of ?recover i] assms
by blast
moreover have "length ?recover = n"
by auto
ultimately have "(gs.sumlist ?recover)$i = sum_list (map (λj. (?recover!j)$i) [0..<n])"
by simp
moreover have "⋀j. j<n ⟹ (map (λj. (?recover!j)$i) [0..<n])!j ∈ℤ"
proof-
fix j::nat
assume jsmall:"j<n"
have "(map (λj. (?recover!j)$i) [0..<n])!j = (λj. (?recover!j)$i) j"
using List.nth_map[of j "[0..<n]" "(λj. (?recover!j)$i)"]
jsmall
by simp
then have "(map (λj. (?recover!j)$i) [0..<n])!j =(?recover!j)$i"
by simp
then show "(map (λj. (?recover!j)$i) [0..<n])!j∈ℤ"
using int_recover[of j] jsmall
by simp
qed
ultimately have "(gs.sumlist ?recover)$i∈ℤ"
using integral_sum[of n "(λj. map lattice_coord
(map of_int_hom.vec_hom (map (λi. of_int (w i) ⋅⇩v M ! i) [0..<n])) !
j $
i)"]
by argo
then show ?thesis
using 1
by simp
qed
lemma int_coord_for_rat:
fixes i::nat
assumes "0≤i"
assumes "i<n"
fixes v::"rat vec"
assumes "v∈of_int_hom.vec_hom` L"
assumes "dim_vec v = n"
shows "(lattice_coord v)$i∈ℤ"
proof-
let ?hom = "of_int_hom.vec_hom"
obtain vint where "v = ?hom vint∧ vint∈L" using assms(3) by blast
moreover then have "(lattice_coord (?hom vint))$i∈ℤ" using int_coord assms by simp
ultimately show ?thesis by simp
qed
section ‹Coord-Invariance›
text ‹ This section shows that the algorithm output matches true closest (or near-closest) vector
in some trailing coordinates. ›
definition I where
"I = (if ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set) ≠ {}
then Max ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set) else -1)"
lemma I_geq:
shows "I≥-1"
unfolding I_def
by simp
lemma I_leq:
shows "I<n"
unfolding I_def
by force
lemma index_geq_I_big:
fixes i::nat
assumes "i>I"
assumes "i<n"
shows "((sq_norm (Mt!i)::rat))>4*eps_closest"
proof(rule ccontr)
assume "¬?thesis"
then have "((sq_norm (Mt!i)::rat))≤4*eps_closest" by linarith
then have i_def:"i∈({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)" using assms by fastforce
then have "({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)≠{}" by fast
moreover then have "I= Max ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)" unfolding I_def by presburger
moreover have "finite ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
by simp
ultimately show False using assms i_def eq_Max_iff by auto
qed
lemma scalar_prod_gs_from_lattice_coord:
fixes i::nat
fixes v::"rat vec"
assumes "dim_vec v = n"
assumes "i<n"
shows "v∙Mt!i=sum_list (map (λk. (lattice_coord v)$k * (((RAT M)!k)∙Mt!i)) [i..<n])"
proof(-)
let ?lc = "lattice_coord v"
let ?recover = "((map (λj. ?lc$j ⋅⇩v (RAT M)!j) [0 ..< n]))"
let ?gsv = "Mt!i"
have "v = gs.sumlist ?recover"
using recover_from_lattice_coord[of v] assms
by blast
then have split_ip:" v ∙ ?gsv = (gs.sumlist (map (λj. ?lc$j ⋅⇩v (RAT M)!j) [0 ..< n]))∙ ?gsv"
by simp
have "⋀u. u∈set ?recover⟹u∈carrier_vec n"
proof(-)
fix u::"rat vec"
assume u_init:"u∈ set ?recover"
then have index_small:"find_index ?recover u < length ?recover"
by (meson find_index_leq_length)
then have carrier_v_ind_M:"(RAT M)!(find_index ?recover u)∈carrier_vec n"
using carrier_vecI[of "(RAT M)!(find_index ?recover u)" n]
access_index_M_dim
by (smt (z3) M_locale_1 gram_schmidt_fs_Rn.f_carrier length_map map_nth)
then have "u=?recover!(find_index ?recover u)"
using u_init
by (simp add: find_index_in_set)
then have "u=(λj. ?lc$j ⋅⇩v (RAT M)!j) (find_index ?recover u) "
using u_init
List.nth_map[of "find_index ?recover u" "[0..<n]" "(λj. ?lc$j ⋅⇩v (RAT M)!j)"]
index_small
by auto
then have "u = ?lc$(find_index ?recover u)⋅⇩v (RAT M)!(find_index ?recover u)"
by simp
then show "u∈carrier_vec n"
using carrier_v_ind_M
smult_carrier_vec[of "?lc$(find_index ?recover u)" "(RAT M)!(find_index ?recover u)" n]
by presburger
qed
then have result_sumlist_L:"v ∙ ?gsv = sum_list (map (λw. w ∙ ?gsv) ?recover)"
using split_ip
gs.scalar_prod_left_sum_distrib[of ?recover ?gsv]
by (metis (no_types, lifting) assms(2) carrier_dim_vec dim_vecs_in_Mt)
let ?L="(map (λw. w ∙ ?gsv) ?recover)"
have 2:"⋀k. k<n⟹?L!k = ?lc$k * ((RAT M)!k∙ ?gsv)"
proof(-)
fix k::nat
assume k_bound:"k<n"
then have "?L!k= (λw. w ∙ ?gsv) (?recover!k)"
by force
then have "?L!k = ?recover!k ∙ ?gsv"
by simp
then have "?L!k = ((λj. (?lc$j ⋅⇩v (RAT M)!j)) k) ∙ ?gsv"
using List.nth_map[of k "[0..<n]" "(λj. (?lc$j ⋅⇩v (RAT M)!j))"] k_bound
by simp
then have "?L!k = (?lc$k ⋅⇩v(RAT M)!k)∙ ?gsv"
by simp
then show "?L!k =?lc$k * ((RAT M)!k∙ ?gsv)"
using smult_scalar_prod_distrib[of "(RAT M)!k" n ?gsv "?L!k"]
access_index_M_dim
dim_vecs_in_Mt[of i]
carrier_vecI[of ?gsv n]
k_bound
assms
by force
qed
moreover have "length ?L = n"
by fastforce
ultimately have 1:"?L = (map (λk. ?lc$k * ((RAT M)!k∙ ?gsv)) [0..<n])"
by auto
moreover then have filt:"⋀k. k<i⟹ (λk. ?lc$k * ((RAT M)!k∙ ?gsv)) k =0"
proof(-)
fix k::nat
assume tri:"k<i"
then have "(?gsv ∙(RAT M)!k) = 0"
using gram_schmidt_fs_lin_indpt.gso_scalar_zero[of n "(RAT M)" i k]
M_locale_2
Mt_gso_connect[of i]
assms(2)
more_dim
by presburger
then have "((RAT M)!k)∙?gsv = 0"
using comm_scalar_prod[of "((RAT M)!k)" n ?gsv ]
access_index_M_dim[of "k"]
tri
assms(2)
dim_vecs_in_Mt[of i]
carrier_vecI[of "?gsv"] carrier_vecI[of "((RAT M)!k)"]
by fastforce
then have "?lc$k * ((RAT M)!k∙ ?gsv) = 0"
by simp
then show "(λk. ?lc$k * ((RAT M)!k∙ ?gsv)) k =0"
by blast
qed
moreover have "k∈ set [0..<n]∧ ¬i≤k⟹k<i"
by linarith
ultimately have "sum_list ?L = sum_list (map (λk. ?lc$k * ((RAT M)!k∙ ?gsv)) (filter (λk. i≤k) [0..<n] ) )"
using sum_list_map_filter[of "[0..<n]" "(λk. i≤k)" "(λk. ?lc$k * ((RAT M)!k∙ ?gsv))" ]
by (metis (no_types, lifting) le_eq_less_or_eq nat_neq_iff)
moreover have "(filter (λk. i≤k) [0..<n] ) = [i..<n]"
using assms(2) bot_nat_0.extremum filter_upt
by presburger
ultimately have "sum_list ?L = sum_list (map (λk. ?lc$k * ((RAT M)!k∙ ?gsv)) [i..<n])"
by presburger
then show ?thesis
using result_sumlist_L
by simp
qed
lemma correct_coord_help:
fixes i::"nat"
assumes "i<(int n)-I"
assumes "witness v (eps_closest)"
assumes "0<i"
shows "(lattice_coord (s i))$(n-i)=(lattice_coord v)$(n-i)
∧ ( (s i) ∙ Mt!(n-i) = v ∙ Mt!(n-i) )"
using assms
proof(induct i rule: less_induct)
case (less i)
let ?lcs = "(lattice_coord (s i))"
let ?lcIs = "λi. lattice_coord (s i)$(n-i)"
let ?lcv = "lattice_coord v"
let ?gsv = "Mt!(n-(i))"
have leq:"(int n)-I≤n+1"
using I_geq
by simp
moreover have nonbase:"0<i"
using less by blast
then have 1:"i≤n"
using leq less
by linarith
moreover have nms:"n-(i)<n"
using 1 nonbase by linarith
ultimately have s_ip:"(s (i)) ∙ ?gsv = sum_list (map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-(i)..<n])"
using scalar_prod_gs_from_lattice_coord[of "s (i)" "n-(i)"]
s_dim[of "i"] by force
have dim_v:"dim_vec v = n"
using assms(2)
unfolding witness_def
by blast
then have v_ip:"v ∙ ?gsv = sum_list (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-(i)..<n])"
unfolding witness_def
using scalar_prod_gs_from_lattice_coord[of v "n-i"]
nms assms(2)
carrier_vecI[of v n]
by satx
have "[n-i..<n]≠[]" using nms by auto
then have split_indices:"[n-(i)..<n] = (n-i) # [n-(i)+1..<n]"
by (simp add: upt_eq_Cons_conv)
then have split_s_list:"(map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-(i)..<n]) =
((λj. ?lcs$j *((RAT M)!j∙ ?gsv)) (n-(i)))#(map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-(i)+1..<n])"
by simp
then have split_s_ip_pre:"(s (i)) ∙ ?gsv = ((λj. ?lcs$j *((RAT M)!j∙ ?gsv)) (n-(i)))
+ sum_list (map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-(i)+1..<n])"
using s_ip
by force
then have split_s_ip: "(s (i)) ∙ ?gsv = ((λj. ?lcs$j *((RAT M)!j∙ ?gsv)) (n-(i)))
+ sum_list (map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])"
by presburger
have split_v_list:"(map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-(i)..<n]) =
((λj. ?lcv$j *((RAT M)!j∙ ?gsv)) (n-(i)))#(map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-(i)+1..<n])"
using split_indices by simp
then have split_v_ip_pre:"v ∙ ?gsv = ((λj. ?lcv$j *((RAT M)!j∙ ?gsv)) (n-(i)))
+ sum_list (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-(i)+1..<n])"
using v_ip
by force
then have split_v_ip:"v ∙ ?gsv = ((λj. ?lcv$j *((RAT M)!j∙ ?gsv)) (n-(i)))
+ sum_list (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])"
by presburger
have use_coord_inv: "(λj. ?lcs$j *((RAT M)!j∙ ?gsv)) k = (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) k" if k_bound: "k<n ∧ k≥n-i+1" for k
proof -
have nmssmall:"n-k<i"
using k_bound by linarith
then have arith:"(n-k)+(i - (n-k)) = i"
using k_bound 1 by linarith
have 2:"0<n-k"
using k_bound by linarith
moreover have 3:"(n-k)+(i - (n-k))≤n"
using 1 arith by linarith
moreover have 4:"n-k≤n-k" by auto
ultimately have 5:"lattice_coord (s (n-k + (i - (n-k)))) $ (n-(n-k)) = lattice_coord (s (n-k)) $ (n-(n-k)) "
using coord_invariance[of "n-k" "n-k" "(i)-(n-k)"] by blast
also have cancel:"n-(n-k) =k"
using k_bound 2 by auto
then have "?lcs$k = ?lcIs (n-k)"
using arith 5 by presburger
moreover have "int (n-k)<int n -I"
using assms nmssmall less by linarith
ultimately have "?lcs$k = ?lcv$(n-(n-k))"
using less(1)[of "n-k"] nmssmall assms(2) 2 by argo
then have "?lcs$k = ?lcv$k"
using cancel by presburger
then have "?lcs$k *((RAT M)!k∙ ?gsv) = ?lcv$k *((RAT M)!k∙ ?gsv)"
by simp
then show "(λj. ?lcs$j *((RAT M)!j∙ ?gsv)) k = (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) k"
by simp
qed
then have "(map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])
= (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])"
by simp
then have "sum_list (map (λj. ?lcs$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])
= sum_list (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])"
by presburger
then have "(s i) ∙ ?gsv =
((λj. ?lcs$j *((RAT M)!j∙ ?gsv)) (n-i)) +
sum_list (map (λj. ?lcv$j *((RAT M)!j∙ ?gsv)) [n-i+1..<n])"
using split_s_ip by argo
then have "(s i) ∙ ?gsv - v ∙ ?gsv =
((λj. ?lcs$j *((RAT M)!j∙ ?gsv)) (n-i))-
((λj. ?lcv$j *((RAT M)!j∙ ?gsv)) (n-i))"
using split_v_ip by linarith
then have "(s i) ∙ ?gsv - v ∙ ?gsv = ((?lcs$(n-i) - ?lcv$(n-i)) * ((RAT M)!(n-i)∙ ?gsv))"
by algebra
then have case_2_from_case_1:"(s i) ∙ ?gsv - v ∙ ?gsv = ((?lcs$(n-i) - ?lcv$(n-i)) * (sq_norm ?gsv))"
using one_diag[of "n- i"] 1 nms
by fastforce
then have "abs ((s i) ∙ ?gsv - v ∙ ?gsv) = abs(?lcs$(n-i) - ?lcv$(n-i)) * abs(sq_norm ?gsv)"
using abs_mult by auto
then have a:"abs ((s i) ∙ ?gsv - v ∙ ?gsv) = abs(?lcs$(n-i) - ?lcv$(n-i)) * (sq_norm ?gsv)"
by (metis abs_of_nonneg sq_norm_vec_ge_0)
have lattice_coord_equal:"?lcs$(n-i) - ?lcv$(n-i)= 0"
proof(rule ccontr)
assume "¬(?lcs$(n-i) - ?lcv$(n-i)= 0)"
then have contra:"?lcs$(n-i) - ?lcv$(n-i) ≠ 0 " by simp
have "?lcs$(n-i) - ?lcv$(n-i) = (?lcs-?lcv)$(n-i)"
using index_minus_vec(1)[of "n-i" ?lcv ?lcs]
dim_preserve_lattice_coord[of v]
assms(2) nms
unfolding witness_def by argo
moreover have "?lcs-?lcv = lattice_coord((s i)-v)"
using mult_minus_distrib_mat_vec
unfolding lattice_coord_def
by (metis "1" carrier_Ms(2) carrier_vecI dim_v s_dim)
ultimately have use_linear:"?lcs$(n-i) - ?lcv$(n-i) = (lattice_coord((s i)-v))$(n-i)"
by presburger
have "(s i)-v∈ of_int_hom.vec_hom` L"
using subtract_coset_into_lattice[of "s i" v]
coset_s[of i]
1 assms(2)
unfolding witness_def
by linarith
then have use_int_coord:"(lattice_coord( ((s i)-v)) )$(n-i)∈ℤ"
using int_coord_for_rat[of "n-i" "((s i)-v)"] 1 nms
by (simp add: dim_v)
then have " abs((lattice_coord( ((s i)-v)) )$(n-i))>0"
using contra use_linear
by linarith
then have " abs((lattice_coord( ((s i)-v)) )$(n-i))≥1"
using use_int_coord
by (simp add: Ints_nonzero_abs_ge1 contra use_linear)
then have "abs(?lcs$(n-i) - ?lcv$(n-i))≥1"
using use_linear by presburger
then have "abs(?lcs$(n-i) - ?lcv$(n-i))*(sq_norm ?gsv)≥sq_norm ?gsv"
using sq_norm_vec_ge_0[of "?gsv"] mult_left_mono[of 1 "abs(?lcs$(n-i) - ?lcv$(n-i))" "sq_norm ?gsv"] by algebra
then have big1:"abs ((s i) ∙ ?gsv - v ∙ ?gsv)≥sq_norm ?gsv"
using a by argo
then have tri_ineq:"abs(v ∙ ?gsv)≥ abs(abs ((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv))"
using cancel_ab_semigroup_add_class.diff_right_commute
cancel_comm_monoid_add_class.diff_cancel diff_zero by linarith
then have smallhalf:"abs((s i) ∙ ?gsv)≤(1/2)*(sq_norm ?gsv)"
using small_orth_coord[of i] nonbase 1
by fastforce
then have "abs((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv)≥ sq_norm ?gsv - (1/2)*(sq_norm ?gsv)"
using big1 by linarith
then have big2:"abs((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv)≥ (1/2)*(sq_norm ?gsv)"
by linarith
then have "abs((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv)≥0"
using sq_norm_vec_ge_0[of "?gsv"] by linarith
then have "abs(abs ((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv))
= abs((s i) ∙ ?gsv - v ∙ ?gsv) -abs((s i) ∙ ?gsv)"
by fastforce
then have "abs(v ∙ ?gsv)≥(1/2)*(sq_norm ?gsv)"
using big2
by linarith
moreover have "(1/2)*(sq_norm ?gsv)≥0"
using sq_norm_vec_ge_0[of ?gsv] by simp
moreover have "abs(v ∙ ?gsv)≥0" by simp
ultimately have "abs(v ∙ ?gsv)^2≥((1/2)*(sq_norm ?gsv))^2"
using nonneg_power_le by blast
moreover have "(sq_norm v) * (sq_norm ?gsv)≥abs(v ∙ ?gsv)^2"
using scalar_prod_Cauchy[of v n ?gsv]
carrier_vecI[of v n] assms(2)
carrier_vecI[of ?gsv] dim_vecs_in_Mt[of "n-i"] nms
unfolding witness_def
by fastforce
ultimately have "sq_norm v * sq_norm ?gsv ≥ ((1/2)*(sq_norm ?gsv))^2"
by order
then have "sq_norm v * sq_norm ?gsv ≥ (1/2)^2 * (sq_norm ?gsv)^2"
by (metis gs.nat_pow_distrib)
then have "sq_norm v * sq_norm ?gsv ≥ 1/4 * (sq_norm ?gsv)^2"
by (smt (z3) numeral_Bit0_eq_double one_power2 power2_eq_square times_divide_times_eq)
moreover have "sq_norm ?gsv > 0"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "n-i"]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
nms by force
ultimately have big:"sq_norm v ≥ 1/4 * sq_norm ?gsv"
by (simp add: power2_eq_square)
have "n-i>I"
using less by linarith
then have big_again:"sq_norm ?gsv > 4*eps_closest"
using index_geq_I_big[of "n-i"] nms by simp
then have "sq_norm v> 1/4 *4*eps_closest"
using big by fastforce
then have "sq_norm v > eps_closest" by auto
then show False
using assms(2)
unfolding witness_def
by linarith
qed
then have piece1: "lattice_coord (s i) $ (n - i) = lattice_coord v $ (n - i)"
using lattice_coord_equal by simp
have "(s i) ∙ ?gsv - v ∙ ?gsv = 0"
using lattice_coord_equal case_2_from_case_1
by algebra
then show ?case using piece1 by simp
qed
lemma correct_coord:
fixes v::"rat vec"
fixes k::nat
assumes "witness v eps_closest"
assumes "I<k"
assumes "k<n"
shows "(s n) ∙ Mt!(k) = v ∙ Mt!(k)"
proof -
have "(s n) ∙ Mt!(k) = (s (n-k)) ∙ Mt!(k)"
using coord_invariance[of "n-k" "n-k" k] assms
by force
moreover have "(s (n-k)) ∙ Mt!(k) = v ∙ Mt!(k)"
using correct_coord_help[of "n-k" v] assms
by simp
ultimately show ?thesis by simp
qed
section ‹Main Theorem›
text ‹ This section culminates in the main theorem.›
lemma sq_norm_from_Mt:
fixes v::"rat vec"
assumes v_carr:"v∈carrier_vec n"
shows "sq_norm v = sum_list (map (λi. (v∙Mt!i)^2/(sq_norm (Mt!i))) [0..<n])"
proof-
let ?Mt_inv_list = "map (λi. (1/sq_norm(Mt!i))⋅⇩v (Mt!i)) [0..<n]"
have nonsing:"?Mt_inv_list!i ∈ carrier_vec n" if i:"0≤i∧i<n" for i
proof-
have "0< sq_norm(Mt!i)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "i"]
M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"] i
by (simp add: M_locale_2)
then have "0<1/sq_norm(Mt!i)" by fastforce
then have "(1/sq_norm(Mt!i))⋅⇩v (Mt!i)∈carrier_vec n"
using carrier_vecI[of "(Mt!i)"] dim_vecs_in_Mt[of i] i by blast
moreover have "?Mt_inv_list!i = (1/sq_norm(Mt!i))⋅⇩v (Mt!i)"
using i by simp
ultimately show ?thesis by argo
qed
let ?Mt_inv_mat = "mat_of_rows n ?Mt_inv_list"
have carrier_mat_inv:"?Mt_inv_mat∈carrier_mat n n" by fastforce
let ?vMt = "?Mt_inv_mat *⇩v v"
have "?vMt$i = ((1/sq_norm(Mt!i))⋅⇩v (Mt!i))∙v" if i:"0≤i∧i<n" for i
using i nonsing[of i] by auto
have dim_vMt:"dim_vec ?vMt = n"
using carrier_mat_inv v_carr by auto
let ?Mt_mat = "mat_of_cols n Mt"
have l:"length Mt = n"
using gs.gram_schmidt_result[of "RAT M" Mt] basis dim_vecs_in_M
unfolding gs.lin_indpt_list_def
by fastforce
then have carrier_mat_Mt:"?Mt_mat∈carrier_mat n n"
using dim_vecs_in_Mt carrier_vecI by auto
then have to_sumlist:"?Mt_mat*⇩v?vMt = gs.sumlist (map (λj. ?vMt$j ⋅⇩v (col ?Mt_mat j)) [0 ..< n])"
using mat_mul_to_sum_list[of ?vMt ?Mt_mat] dim_vMt
by fastforce
have "?vMt$i ⋅⇩v (col ?Mt_mat i) = (1/sq_norm(Mt!i))* ((Mt!i)∙v) ⋅⇩v Mt!i" if i:"0≤i∧i<n" for i
using i l dim_vecs_in_Mt v_carr carrier_vecI by fastforce
then have "(map (λj. ?vMt$j ⋅⇩v (col ?Mt_mat j)) [0 ..< n])
= (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])"
by simp
then have 1:"gs.sumlist (map (λj. ?vMt$j ⋅⇩v (col ?Mt_mat j)) [0 ..< n])
=gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])"
by presburger
then have 2:"?Mt_mat*⇩v?vMt = gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])"
using to_sumlist by argo
have "?Mt_mat *⇩v ?vMt = (?Mt_mat * ?Mt_inv_mat)*⇩v v"
using carrier_mat_Mt carrier_mat_inv v_carr by auto
have "(?Mt_inv_mat*?Mt_mat)$$(i,j) = (1⇩m n)$$(i,j)"
if sensible_indices:"0≤i ∧ i<n ∧ 0≤j ∧ j<n" for i j
proof-
have "(?Mt_inv_mat*?Mt_mat)$$(i,j) = (row ?Mt_inv_mat i)∙(col ?Mt_mat j)"
using sensible_indices carrier_mat_Mt carrier_mat_inv by auto
then have "(?Mt_inv_mat*?Mt_mat)$$(i,j) = ?Mt_inv_list!i∙Mt!j"
using sensible_indices carrier_mat_Mt carrier_mat_inv nonsing
by auto
then have "(?Mt_inv_mat*?Mt_mat)$$(i,j) = ((1/sq_norm(Mt!i))⋅⇩v (Mt!i))∙Mt!j"
using sensible_indices by simp
then have "(?Mt_inv_mat*?Mt_mat)$$(i,j) = (1/sq_norm(Mt!i)) *((Mt!i)∙(Mt!j))"
using dim_vecs_in_Mt[of i] dim_vecs_in_Mt[of j] sensible_indices by auto
moreover have "(1/sq_norm(Mt!i)) *((Mt!i)∙(Mt!j)) = (if i=j then 1 else 0)"
proof(cases "i=j")
case diag:True
have nonzero:"0< sq_norm(Mt!i)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "i"]
M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"] sensible_indices
by (simp add: M_locale_2)
have "(1/sq_norm(Mt!i)) *((Mt!i)∙(Mt!j)) = (1/sq_norm(Mt!i)) * sq_norm(Mt!i)"
using sensible_indices diag sq_norm_vec_as_cscalar_prod[of "Mt!i"] by auto
then have "(1/sq_norm(Mt!i)) *((Mt!i)∙(Mt!j)) = 1"
using nonzero by auto
then show ?thesis using diag by argo
next
case off:False
have nonzero:"0< sq_norm(Mt!i)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "i"]
M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"] sensible_indices
by (simp add: M_locale_2)
then have "0<1/sq_norm(Mt!i)" by simp
moreover have "((Mt!i)∙(Mt!j)) = 0"
using gram_schmidt_fs_lin_indpt.orthogonal[of n "(RAT) M" i j] off sensible_indices
M_locale_1 M_locale_2 gram_schmidt_fs_Rn.main_connect
by force
ultimately show ?thesis using off by algebra
qed
moreover then have "(1/sq_norm(Mt!i)) *((Mt!i)∙(Mt!j)) = (1⇩m n)$$(i,j)"
using sensible_indices unfolding one_mat_def by simp
ultimately show ?thesis by presburger
qed
then have inv_Mt:"(?Mt_inv_mat*?Mt_mat) = 1⇩m n"
using carrier_mat_inv carrier_mat_Mt
by fastforce
then have "?Mt_mat * ?Mt_inv_mat = 1⇩m n"
using mat_mult_left_right_inverse[of ?Mt_inv_mat n ?Mt_mat] carrier_mat_inv carrier_mat_Mt
by argo
then have 3:"(?Mt_mat * ?Mt_inv_mat)*⇩v v = v"
using v_carr by simp
then have 4:"v = gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])"
using v_carr carrier_mat_inv carrier_mat_Mt 1 2 by auto
have "(map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])
= (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v gs.gso j) [0 ..< n])"
using M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "RAT M"]
by auto
then have "gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v Mt!j) [0 ..< n])
= gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v gs.gso j) [0 ..< n])"
by argo
then have "v = gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v gs.gso j) [0 ..< n])"
using 4 by argo
then have "v∙v = gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v gs.gso j) [0 ..< n])∙
gs.sumlist (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v) ⋅⇩v gs.gso j) [0 ..< n])"
by simp
then have a:"v∙v =
sum_list(map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(gs.gso j ∙ gs.gso j)) [0..<n])"
using gram_schmidt_fs_lin_indpt.scalar_prod_lincomb_gso[
of n "RAT M" n "(λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v))" "(λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v))"]
M_locale_2
M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "RAT M"] by force
have "(map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(gs.gso j ∙ gs.gso j)) [0..<n])
= (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j)) [0..<n])"
using M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "RAT M"]
by auto
then have b:"sum_list (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(gs.gso j ∙ gs.gso j)) [0..<n])
=sum_list (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j)) [0..<n])"
by argo
have " (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j) =
(v∙(Mt!j))^2/(sq_norm (Mt!j)) " if sensible_indices:"0≤j∧j<n" for j
proof-
have nonzero:"0< sq_norm(Mt!j)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "j"]
M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"] sensible_indices
by (simp add: M_locale_2)
moreover have "(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j)
= (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*sq_norm (Mt!j)"
using sq_norm_vec_as_cscalar_prod[of "Mt!j"] by force
moreover have "(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)* sq_norm (Mt!j)
= ((Mt!j)∙v)^2 * (1/sq_norm(Mt!j))^2 *sq_norm (Mt!j) "
by (simp add: power2_eq_square)
moreover have "((Mt!j)∙v)^2 * (1/sq_norm(Mt!j))^2 *sq_norm (Mt!j) = ((Mt!j)∙v)^2/(sq_norm(Mt!j))"
using nonzero
by (simp add: divide_divide_eq_left' power2_eq_square)
moreover have "(Mt!j)∙v = v∙(Mt!j)" using v_carr dim_vecs_in_Mt sensible_indices
by (metis carrier_vecI comm_scalar_prod)
ultimately show ?thesis by argo
qed
then have "(map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j)) [0..<n])
= (map (λj. (v∙(Mt!j))^2/(sq_norm(Mt!j))) [0..<n])" by force
then have c:"sum_list (map (λj. (1/sq_norm(Mt!j))* ((Mt!j)∙v)*(1/sq_norm(Mt!j))* ((Mt!j)∙v)*(Mt!j ∙ Mt!j)) [0..<n])
= sum_list (map (λj. (v∙(Mt!j))^2/(sq_norm(Mt!j))) [0..<n])" by argo
then have "v∙v = sum_list (map (λj. (v∙(Mt!j))^2/(sq_norm(Mt!j))) [0..<n])" using a b c by argo
moreover have "v∙v = v∙cv" by force
ultimately show ?thesis using sq_norm_vec_as_cscalar_prod[of v] v_carr by argo
qed
lemma bound_help:
fixes N::nat
shows "real_of_rat ((rat_of_int N)*α^N) * epsilon≤2^N"
proof(induct N)
case 0
then show ?case by simp
next
case (Suc N)
let ?SN = "Suc N"
have "?SN=1∨?SN=2∨2<?SN" by fastforce
then show ?case
proof(elim disjE)
{assume 1:"?SN = 1"
then have "real_of_rat ((rat_of_int ?SN)*α^?SN)*epsilon = real_of_rat ((rat_of_int 1)*4/3)*11/10"
unfolding α_def epsilon_def by auto
also have "real_of_rat ((rat_of_int 1)*4/3)*11/10 = real_of_rat (4/3)*11/10" by force
also have "real_of_rat (4/3)*11/10 =real_of_rat ((4/3)* 11/10)"
by (simp add: of_rat_hom.hom_div)
also have "real_of_rat ((4/3)* 11/10) = real_of_rat (44/30)" by auto
also have "real_of_rat (44/30)≤(2::real)"
by (simp add: of_rat_hom.hom_div)
finally show ?thesis using 1 by simp}
next
{assume 2:"?SN=2"
then have "real_of_rat ((rat_of_int ?SN)*α^?SN)*epsilon = real_of_rat ((rat_of_int 2)*(4/3)^2)*11/10"
unfolding α_def epsilon_def
by (metis int_ops(3) times_divide_eq_right)
also have "((4::rat)/3)^2 = (4*4)/(3*3)"
using power2_eq_square[of "4/3"] times_divide_times_eq[of 4 3 4 3] by metis
also have "(4*(4::rat))/(3*3) = 16/9" by auto
finally have "real_of_rat ((rat_of_int ?SN)*α^?SN)*epsilon= real_of_rat ((rat_of_int 2)*(16/9))*11/10"
by blast
also have "(rat_of_int 2)*(16/9) = 32/9" by force
finally have "real_of_rat ((rat_of_int ?SN)*α^?SN)*epsilon = real_of_rat (32 / 9) * 11 / 10"
by simp
also have "real_of_rat (32 / 9) * 11 / 10 = real_of_rat (32 / 9 *( 11 / 10))"
using of_rat_hom.hom_mult[of "32/9" "11/10"]
by (simp add: of_rat_hom.hom_div)
also have "real_of_rat (32 / 9 *( 11 / 10)) = real_of_rat (352/90)"
using times_divide_times_eq[of 32 9 11 10] by force
also have "352/90≤(4::rat)" by linarith
also have "(4::rat) = 2^?SN" using 2 by auto
finally show ?thesis
by (simp add: "2" gs.cring_simprules(14) int_ops(3) of_rat_hom.hom_power of_rat_less_eq)}
next
{assume ind:"?SN>2"
then have "N>0" by simp
then have "?SN = N*(?SN/N)" by auto
moreover have "α^?SN = α^N*α" by auto
ultimately have "real_of_rat ((rat_of_int ?SN)*α^?SN) = (N*(?SN/N)) * (real_of_rat (α^N*α))"
by (metis of_int_of_nat_eq of_rat_mult of_rat_of_nat_eq)
also have "(N*(?SN/N)) * real_of_rat (α^N*α) = real_of_rat ((rat_of_int N) * α^N) * ((?SN/N) *(real_of_rat α))"
by (simp add: ‹real (Suc N) = real N * (real (Suc N) / real N)› gs.cring_simprules(11) mult_of_int_commute of_rat_divide of_rat_mult)
finally have "real_of_rat ((rat_of_int ?SN)*α^?SN) * epsilon = real_of_rat ((rat_of_int N) * α^N) * ((?SN/N) *(real_of_rat α)) * epsilon"
by presburger
then have "real_of_rat ((rat_of_int ?SN)*α^?SN) * epsilon = real_of_rat ((rat_of_int N) * α^N) * epsilon * ((?SN/N) *(real_of_rat α))"
by argo
moreover have "((?SN/N) *(real_of_rat α))≤2"
proof-
have N_big:"2≤N" using ind
by force
then have "4≤2*N" by fastforce
then have "4*N+4≤6*N" by fastforce
then have "4/3*(Suc N)≤2*N" by auto
moreover have "0<1/N" using N_big by simp
ultimately have " (4/3*?SN)* (1/N)≤ 2*N*(1/N)"
using N_big mult_right_mono[of "(4/3*?SN)" "2*N" "(1/N)"] by linarith
then have "(4/3*?SN)/N≤ 2*N/N" by argo
then have "4/3*(?SN / N)≤ 2*(N/N)" by linarith
then have "4/3*(?SN/N)≤ 2" using N_big by auto
moreover have "4/3 = real_of_rat α" using of_rat_divide unfolding α_def
by (metis of_rat_numeral_eq)
ultimately have "(real_of_rat α)*(?SN/N)≤ 2" by algebra
then show ?thesis by argo
qed
moreover have
"0≤real_of_rat (rat_of_int (int N) * α ^ N) * epsilon" unfolding α_def epsilon_def by force
moreover have "0≤(real_of_rat α)*(?SN/N)" unfolding α_def by simp
ultimately have "real_of_rat ((rat_of_int ?SN)*α^?SN) * epsilon≤2^N * 2"
using Suc mult_mono[of
"real_of_rat (rat_of_int (int N) * α ^ N) * epsilon"
"2^N"
"((?SN/N) *(real_of_rat α))"
2] by argo
then show ?thesis by simp}
qed
qed
lemma present_bound_nicely:
fixes N::nat
shows "real_of_rat ((rat_of_int N)*α^N* eps_closest)≤2^N*closest_distance_sq"
proof-
have "real_of_rat eps_closest≤ epsilon*closest_distance_sq"
using eps_closest_lemma unfolding close_condition_def by fastforce
moreover have "0≤(rat_of_int N)*α^N" unfolding α_def by simp
ultimately have "real_of_rat ((rat_of_int N)*α^N * eps_closest)≤ real_of_rat ((rat_of_int N)*α^N) * epsilon*closest_distance_sq"
by (metis ab_semigroup_mult_class.mult_ac(1) mult_left_mono of_rat_hom.hom_mult zero_le_of_rat_iff)
also have "real_of_rat ((rat_of_int N)*α^N) * epsilon*closest_distance_sq≤2^N*closest_distance_sq"
using bound_help[of N] closest_distance_sq_pos mult_right_mono by fast
finally show ?thesis by force
qed
lemma basis_decay:
fixes i::nat
fixes j::nat
assumes "i<n"
assumes "i+j<n"
shows "sq_norm (Mt!i)≤ α^j*sq_norm(Mt!(i+j))"
using assms
proof(induct j)
case 0
have "α^0 = 1" by simp
moreover have "sq_norm (Mt!i) = sq_norm(Mt!(i+0))" by simp
moreover have "0≤ sq_norm(Mt!i)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" i]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
assms by force
moreover have "(0::rat)≤(1::rat)" by force
ultimately show ?case by simp
next
case (Suc j)
have "(1::rat) ≤α" unfolding α_def by fastforce
moreover have "n≥0" by simp
ultimately have "(1::rat)≤α^j" by simp
moreover have "sq_norm (Mt!(i+j))≤α*(sq_norm (Mt!(i+Suc j)))"
using reduced M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"] Suc.prems
unfolding gs.reduced_def gs.weakly_reduced_def
by force
moreover have "0≤ sq_norm (Mt!(i+j))"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "i+j"]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
Suc.prems by force
ultimately have "α^j*sq_norm (Mt!(i+j))≤α^j*α*(sq_norm (Mt!(i+Suc j)))"
by simp
moreover have "sq_norm(Mt!i)≤ α^j * sq_norm (Mt!(i+j))"
using Suc by linarith
ultimately have "sq_norm(Mt!i)≤α^j*α*(sq_norm (Mt!(i+Suc j)))" by order
moreover have "α^j*α = α^(Suc j)" by simp
ultimately show ?case by argo
qed
lemma basis_decay_cor:
fixes i::nat
fixes j::nat
assumes "i<n"
assumes "j<n"
assumes "i≤j"
shows "sq_norm (Mt!i)≤ α^n*sq_norm(Mt!j)"
proof-
have 1:"sq_norm (Mt!i)≤ α^(j-i)*sq_norm(Mt!j)"
using basis_decay[of i "j-i"] assms
by simp
have "α^(j-i)≤α^n" using assms unfolding α_def by force
then have "α^(j-i)*sq_norm(Mt!j)≤α^n*sq_norm(Mt!j)"
using mult_right_mono by blast
then show ?thesis using 1 by order
qed
theorem Babai_Correct:
shows "real_of_rat ((sq_norm (s n))::rat) ≤ 2^n * closest_distance_sq∧ s n ∈ coset"
proof-
let ?s = "s n"
let ?component = "(λi. (?s∙Mt!i)^2/(sq_norm (Mt!i)))"
obtain v where wit_v:"witness v (eps_closest)"
using witness_exists by force
have split_norm:"sq_norm ?s = sum_list (map ?component [0..<n])"
using s_dim[of n] sq_norm_from_Mt[of ?s] by fast
have "I+1∈ℕ" using I_geq
using Nats_0 Nats_1 Nats_add R.add.l_inv_ex R.add.r_inv_ex add_diff_cancel_right'
cring_simprules(21) rangeI range_abs_Nats verit_la_disequality verit_minus_simplify(3)
zabs_def zle_add1_eq_le by auto
then obtain Inat where Inat_def:"int Inat = I+1"
using Nats_cases by metis
then have Inat_small:"Inat≤n" using I_leq by fastforce
then have "[0..<n] = [0..<Inat] @ [Inat..<n]"
by (metis bot_nat_0.extremum_uniqueI le_Suc_ex nat_le_linear upt_add_eq_append)
then have split_norm_sum:"sq_norm ?s = sum_list (map ?component [0..<Inat]) + sum_list (map ?component [Inat..<n])"
using split_norm by force
have "?component i ≤ eps_closest " if i:"Inat≤i∧i<n" for i
proof-
have ge0:"sq_norm (Mt!i) > 0"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" i]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
i by force
then have "?component i = (v∙ Mt!i)^2 / (sq_norm (Mt!i))"
using ge0 correct_coord[of v i] wit_v Inat_def i
by auto
also have "(v∙Mt!i)^2≤ (sq_norm v)*sq_norm (Mt!i)"
using scalar_prod_Cauchy[of v n "Mt!i"]
dim_vecs_in_Mt[of i] carrier_vecI[of v] carrier_vecI[of "Mt!i"] wit_v
i
unfolding witness_def
by algebra
also have "sq_norm v ≤ eps_closest"
using wit_v unfolding witness_def by fast
finally show ?thesis using ge0
by (simp add: divide_right_mono)
qed
then have "⋀x. x∈set [Inat..<n] ⟹ ?component x ≤ (λi. eps_closest) x" by simp
then have "sum_list (map ?component [Inat..<n])≤ sum_list (map (λi. eps_closest) [Inat..<n])"
using sum_list_mono[of "[Inat..<n]" ?component "(λi. eps_closest)"] by argo
then have right_sum:"sum_list (map ?component [Inat..<n])≤(rat_of_nat (n-Inat))*eps_closest"
using sum_list_triv[of "eps_closest" "[Inat..<n]" ] by force
have "(1::rat) ≤α" unfolding α_def by fastforce
moreover have "n≥0" by simp
ultimately have "(1::rat)≤α^n" by simp
moreover have "(0::rat)≤1" by simp
moreover have "0≤(rat_of_nat (n-Inat))*eps_closest"
proof-
have "0≤(rat_of_nat (n-Inat))" using Inat_small by fast
moreover have "0≤eps_closest"
proof(cases "closest_distance_sq = 0")
case t:True
then show ?thesis using eps_closest_lemma closest_distance_sq_pos unfolding close_condition_def
by auto
next
case f:False
then show ?thesis using eps_closest_lemma closest_distance_sq_pos unfolding close_condition_def
by (smt (verit, del_insts) zero_le_of_rat_iff)
qed
ultimately show ?thesis by blast
qed
ultimately have "(rat_of_nat (n-Inat))*eps_closest ≤ (rat_of_nat (n-Inat))*eps_closest * α^n"
using mult_left_mono[of 1 "α^n" "(rat_of_nat (n-Inat))*eps_closest"] by linarith
then have "sum_list (map ?component [Inat..<n])≤(rat_of_nat (n-Inat))*eps_closest*α^n" using right_sum by order
then have right_sum_alpha:"sum_list (map ?component [Inat..<n])≤(rat_of_nat (n-Inat))*α^n*eps_closest"
by algebra
have "sum_list (map ?component [0..<Inat]) + sum_list (map ?component [Inat..<n])≤ (rat_of_int n)*α^n*eps_closest"
proof(cases "Inat = 0")
case Inat:True
then have "sum_list (map ?component [0..<Inat]) = 0" by auto
then have "sum_list (map ?component [0..<Inat]) + sum_list (map ?component [Inat..<n])≤(rat_of_int (n-Inat))*α^n * eps_closest"
using right_sum_alpha by simp
also have "n-Inat = n" using Inat by simp
finally show ?thesis by linarith
next
case False
then have non_zero:"Inat>0" by blast
then have I_not_min:"I≥0" using Inat_def by simp
then have non_empty:"I = Max ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
unfolding I_def by presburger
then have max:"Inat-1= Max({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
using Inat_def by linarith
then have "Inat -1 ∈ ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
proof-
have "finite ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
by simp
moreover have "({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)≠{}"
using I_not_min unfolding I_def by presburger
ultimately show "Inat -1 ∈ ({i∈{0..<n}. ((sq_norm (Mt!i)::rat))≤4*eps_closest}::nat set)"
using max eq_Max_iff by blast
qed
then have 2:"(sq_norm (Mt!(Inat-1))::rat)≤4*eps_closest" by blast
have "(1::rat) ≤α" unfolding α_def by fastforce
moreover have "n≥0" by simp
ultimately have "(1::rat)≤α^n" by simp
then have "((1/4)::rat)≤1/4 * α^n" by auto
then have "(0::rat)<1/4*α^n" by linarith
moreover have "0<(sq_norm (Mt!(Inat-1))::rat)"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" "Inat-1"]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
non_zero Inat_small by force
ultimately have bound:"1/4 *α^n* (sq_norm (Mt!(Inat-1)))≤ ((1/4 * α^n)* 4*eps_closest)"
using 2 by auto
have "?component i ≤ α^n *eps_closest" if list1:"i<Inat" for i
proof-
have 1:"0<n-i" using list1 Inat_small by simp
then have "?s∙Mt!i = (s (n-i))∙Mt!i"
using coord_invariance[of "n-i" "n-i" i] by fastforce
then have "abs(?s∙Mt!i)≤ (1/2)*(sq_norm (Mt!i))"
using small_orth_coord[of "n-i"] 1 by force
then have "(?s∙Mt!i)^2 ≤ ((1/2)*(sq_norm (Mt!i)))^2"
by (meson abs_ge_self abs_le_square_iff ge_trans)
moreover have ge0:"sq_norm (Mt!i) > 0"
using gram_schmidt_fs_lin_indpt.sq_norm_pos[of n "RAT M" i]
M_locale_2 M_locale_1 gram_schmidt_fs_Rn.main_connect[of n "(RAT M)"]
list1 Inat_small by force
ultimately have "?component i ≤((1/2)*(sq_norm (Mt!i)))^2 / (sq_norm (Mt!i))"
using divide_right_mono by auto
also have "((1/2)*(sq_norm (Mt!i)))^2/ (sq_norm (Mt!i)) = 1/4 * (sq_norm (Mt!i))^2/ (sq_norm (Mt!i))"
by (metis (no_types, lifting) gs.cring_simprules(12) numeral_Bit0_eq_double power2_eq_square times_divide_eq_left times_divide_times_eq)
also have "1/4 * (sq_norm (Mt!i))^2/ (sq_norm (Mt!i)) = 1/4 * (sq_norm (Mt!i))"
using ge0 by (simp add: power2_eq_square)
also have "1/4*sq_norm (Mt!i) ≤ 1/4*α^n * (sq_norm (Mt!(Inat-1)))"
using basis_decay_cor[of i "Inat-1"] list1 Inat_small mult_left_mono[
of "sq_norm (Mt!i)" "α^n * (sq_norm (Mt!(Inat-1)))" "1/4"]
by linarith
finally have "?component i ≤ 1/4 * α^n * 4 *eps_closest"
using bound by linarith
also have "1/4 * α^n * 4 * eps_closest=α^n * eps_closest" by force
finally show ?thesis by blast
qed
then have "sum_list (map ?component [0..<Inat])≤ sum_list (map (λi. α^n * eps_closest)[0..<Inat])"
using sum_list_mono[of "[0..<Inat]" ?component "(λi. α^n * eps_closest)"] by fastforce
then have "sum_list (map ?component [0..<Inat])≤ (rat_of_int Inat)*α^n * eps_closest"
using sum_list_triv[of "α^n * eps_closest" "[0..<Inat]"] by auto
then have "(sum_list (map ?component [0..<Inat])) + sum_list (map ?component [Inat..<n])
≤ (rat_of_int Inat)*α^n * eps_closest+(rat_of_int (n-Inat))*α^n * eps_closest"
using right_sum_alpha by linarith
then have "(sum_list (map ?component [0..<Inat])) + sum_list (map ?component [Inat..<n])
≤ ((rat_of_int Inat)+(rat_of_int (n-Inat)))*α^n * eps_closest"
using gs.cring_simprules(13) by auto
then show ?thesis
by (metis (no_types, lifting) Inat_small add_diff_inverse_nat diff_is_0_eq' less_nat_zero_code
of_int_of_nat_eq of_nat_add zero_less_diff)
qed
then have "sq_norm ?s ≤ (rat_of_int n)*α^n * eps_closest"
using split_norm_sum by argo
then have "real_of_rat (sq_norm ?s) ≤ real_of_rat ((rat_of_int n)*α^n * eps_closest)"
by (simp add: of_rat_less_eq)
also have "real_of_rat ((rat_of_int n)*α^n * eps_closest)≤2^n*closest_distance_sq"
using present_bound_nicely[of n]
by blast
finally show ?thesis
using coset_s[of n]
by fast
qed
end
end