Theory Integral_Bounded_Vectors
section ‹Integral and Bounded Matrices and Vectors›
text ‹We define notions of integral vectors and matrices and bounded vectors and matrices
and prove some preservation lemmas. Moreover, we prove two bounds on determinants.›
theory Integral_Bounded_Vectors
imports
Missing_VS_Connect
Sum_Vec_Set
LLL_Basis_Reduction.Gram_Schmidt_2
begin
lemma sq_norm_unit_vec[simp]: assumes i: "i < n"
shows "∥unit_vec n i∥⇧2 = (1 :: 'a :: {comm_ring_1,conjugatable_ring})"
proof -
from i have id: "[0..<n] = [0..<i] @ [i] @ [Suc i ..< n]"
by (metis append_Cons append_Nil diff_zero length_upt list_trisect)
show ?thesis unfolding sq_norm_vec_def unit_vec_def
by (auto simp: o_def id, subst (1 2) sum_list_0, auto)
qed
definition Ints_vec (‹ℤ⇩v›) where
"ℤ⇩v = {x. ∀ i < dim_vec x. x $ i ∈ ℤ}"
definition indexed_Ints_vec where
"indexed_Ints_vec I = {x. ∀ i < dim_vec x. i ∈ I ⟶ x $ i ∈ ℤ}"
lemma indexed_Ints_vec_UNIV: "ℤ⇩v = indexed_Ints_vec UNIV"
unfolding Ints_vec_def indexed_Ints_vec_def by auto
lemma indexed_Ints_vec_subset: "ℤ⇩v ⊆ indexed_Ints_vec I"
unfolding Ints_vec_def indexed_Ints_vec_def by auto
lemma Ints_vec_vec_set: "v ∈ ℤ⇩v = (vec_set v ⊆ ℤ)"
unfolding Ints_vec_def vec_set_def by auto
definition Ints_mat (‹ℤ⇩m›) where
"ℤ⇩m = {A. ∀ i < dim_row A. ∀ j < dim_col A. A $$ (i,j) ∈ ℤ}"
lemma Ints_mat_elements_mat: "A ∈ ℤ⇩m = (elements_mat A ⊆ ℤ)"
unfolding Ints_mat_def elements_mat_def by force
lemma minus_in_Ints_vec_iff[simp]: "(-x) ∈ ℤ⇩v ⟷ (x :: 'a :: ring_1 vec) ∈ ℤ⇩v"
unfolding Ints_vec_vec_set by (auto simp: minus_in_Ints_iff)
lemma minus_in_Ints_mat_iff[simp]: "(-A) ∈ ℤ⇩m ⟷ (A :: 'a :: ring_1 mat) ∈ ℤ⇩m"
unfolding Ints_mat_elements_mat by (auto simp: minus_in_Ints_iff)
lemma Ints_vec_rows_Ints_mat[simp]: "set (rows A) ⊆ ℤ⇩v ⟷ A ∈ ℤ⇩m"
unfolding rows_def Ints_vec_def Ints_mat_def by force
lemma unit_vec_integral[simp,intro]: "unit_vec n i ∈ ℤ⇩v"
unfolding Ints_vec_def by (auto simp: unit_vec_def)
lemma diff_indexed_Ints_vec:
"x ∈ carrier_vec n ⟹ y ∈ carrier_vec n ⟹ x ∈ indexed_Ints_vec I ⟹ y ∈ indexed_Ints_vec I
⟹ x - y ∈ indexed_Ints_vec I"
unfolding indexed_Ints_vec_def by auto
lemma smult_indexed_Ints_vec: "x ∈ ℤ ⟹ v ∈ indexed_Ints_vec I ⟹ x ⋅⇩v v ∈ indexed_Ints_vec I"
unfolding indexed_Ints_vec_def smult_vec_def by simp
lemma add_indexed_Ints_vec:
"x ∈ carrier_vec n ⟹ y ∈ carrier_vec n ⟹ x ∈ indexed_Ints_vec I ⟹ y ∈ indexed_Ints_vec I
⟹ x + y ∈ indexed_Ints_vec I"
unfolding indexed_Ints_vec_def by auto
lemma (in vec_space) lincomb_indexed_Ints_vec: assumes cI: "⋀ x. x ∈ C ⟹ c x ∈ ℤ"
and C: "C ⊆ carrier_vec n"
and CI: "C ⊆ indexed_Ints_vec I"
shows "lincomb c C ∈ indexed_Ints_vec I"
proof -
from C have id: "dim_vec (lincomb c C) = n" by auto
show ?thesis unfolding indexed_Ints_vec_def mem_Collect_eq id
proof (intro allI impI)
fix i
assume i: "i < n" and iI: "i ∈ I"
have "lincomb c C $ i = (∑x∈C. c x * x $ i)"
by (rule lincomb_index[OF i C])
also have "… ∈ ℤ"
by (intro Ints_sum Ints_mult cI, insert i iI CI[unfolded indexed_Ints_vec_def] C, force+)
finally show "lincomb c C $ i ∈ ℤ" .
qed
qed
definition "Bounded_vec (b :: 'a :: linordered_idom) = {x . ∀ i < dim_vec x . abs (x $ i) ≤ b}"
lemma Bounded_vec_vec_set: "v ∈ Bounded_vec b ⟷ (∀ x ∈ vec_set v. abs x ≤ b)"
unfolding Bounded_vec_def vec_set_def by auto
definition "Bounded_mat (b :: 'a :: linordered_idom) =
{A . (∀ i < dim_row A . ∀ j < dim_col A. abs (A $$ (i,j)) ≤ b)}"
lemma Bounded_mat_elements_mat: "A ∈ Bounded_mat b ⟷ (∀ x ∈ elements_mat A. abs x ≤ b)"
unfolding Bounded_mat_def elements_mat_def by auto
lemma Bounded_vec_rows_Bounded_mat[simp]: "set (rows A) ⊆ Bounded_vec B ⟷ A ∈ Bounded_mat B"
unfolding rows_def Bounded_vec_def Bounded_mat_def by force
lemma unit_vec_Bounded_vec[simp,intro]: "unit_vec n i ∈ Bounded_vec (max 1 Bnd)"
unfolding Bounded_vec_def unit_vec_def by auto
lemma unit_vec_int_bounds: "set (unit_vecs n) ⊆ ℤ⇩v ∩ Bounded_vec (of_int (max 1 Bnd))"
unfolding unit_vecs_def by (auto simp: Bounded_vec_def)
lemma Bounded_matD: assumes "A ∈ Bounded_mat b"
"A ∈ carrier_mat nr nc"
shows "i < nr ⟹ j < nc ⟹ abs (A $$ (i,j)) ≤ b"
using assms unfolding Bounded_mat_def by auto
lemma Bounded_vec_mono: "b ≤ B ⟹ Bounded_vec b ⊆ Bounded_vec B"
unfolding Bounded_vec_def by auto
lemma Bounded_mat_mono: "b ≤ B ⟹ Bounded_mat b ⊆ Bounded_mat B"
unfolding Bounded_mat_def by force
lemma finite_Bounded_vec_Max:
assumes A: "A ⊆ carrier_vec n"
and fin: "finite A"
shows "A ⊆ Bounded_vec (Max { abs (a $ i) | a i. a ∈ A ∧ i < n})"
proof
let ?B = "{ abs (a $ i) | a i. a ∈ A ∧ i < n}"
have fin: "finite ?B"
by (rule finite_subset[of _ "(λ (a,i). abs (a $ i)) ` (A × {0 ..< n})"], insert fin, auto)
fix a
assume a: "a ∈ A"
show "a ∈ Bounded_vec (Max ?B)"
unfolding Bounded_vec_def
by (standard, intro allI impI Max_ge[OF fin], insert a A, force)
qed
definition is_det_bound :: "(nat ⇒ 'a :: linordered_idom ⇒ 'a) ⇒ bool" where
"is_det_bound f = (∀ A n x. A ∈ carrier_mat n n ⟶ A ∈ Bounded_mat x ⟶ abs (det A) ≤ f n x)"
lemma is_det_bound_ge_zero: assumes "is_det_bound f"
and "x ≥ 0"
shows "f n x ≥ 0"
using assms(1)[unfolded is_det_bound_def, rule_format, of "0⇩m n n" n x]
using assms(2) unfolding Bounded_mat_def by auto
definition det_bound_fact :: "nat ⇒ 'a :: linordered_idom ⇒ 'a" where
"det_bound_fact n x = fact n * (x^n)"
lemma det_bound_fact: "is_det_bound det_bound_fact"
unfolding is_det_bound_def
proof (intro allI impI)
fix A :: "'a :: linordered_idom mat" and n x
assume A: "A ∈ carrier_mat n n"
and x: "A ∈ Bounded_mat x"
show "abs (det A) ≤ det_bound_fact n x"
proof -
have "abs (det A) = abs (∑p | p permutes {0..<n}. signof p * (∏i = 0..<n. A $$ (i, p i)))"
unfolding det_def'[OF A] ..
also have "… ≤ (∑p | p permutes {0..<n}. abs (signof p * (∏i = 0..<n. A $$ (i, p i))))"
by (rule sum_abs)
also have "… = (∑p | p permutes {0..<n}. (∏i = 0..<n. abs (A $$ (i, p i))))"
by (rule sum.cong[OF refl], auto simp: abs_mult abs_prod sign_def simp flip: of_int_abs)
also have "… ≤ (∑p | p permutes {0..<n}. (∏i = 0..<n. x))"
by (intro sum_mono prod_mono conjI Bounded_matD[OF x A], auto)
also have "… = fact n * x^n" by (auto simp add: card_permutations)
finally show "abs (det A) ≤ det_bound_fact n x" unfolding det_bound_fact_def by auto
qed
qed
lemma (in gram_schmidt_fs) Gramian_determinant_det: assumes A: "A ∈ carrier_mat n n"
shows "Gramian_determinant (rows A) n = det A * det A"
proof -
have [simp]: "mat_of_rows n (rows A) = A" using A
by (intro eq_matI, auto)
show ?thesis using A
unfolding Gramian_determinant_def
by (subst Gramian_matrix_alt_def, force, simp add: Let_def, subst det_mult[of _ n],
auto simp: det_transpose)
qed
lemma (in gram_schmidt_fs_lin_indpt) det_bound_main: assumes rows: "rows A = fs"
and A: "A ∈ carrier_mat n n"
and n0: "n > 0"
and Bnd: "A ∈ Bounded_mat c"
shows
"(abs (det A))^2 ≤ of_nat n ^ n * c ^ (2 * n)"
proof -
from n0 A Bnd have "abs (A $$ (0,0)) ≤ c" by (auto simp: Bounded_mat_def)
hence c0: "c ≥ 0" by auto
from n0 A rows have fs: "set fs ≠ {}" by (auto simp: rows_def)
from rows A have len: "length fs = n" by auto
have "(abs (det A))^2 = det A * det A" unfolding power2_eq_square by simp
also have "… = d n" using Gramian_determinant_det[OF A] unfolding rows by simp
also have "… = (∏j<n. ∥gso j∥⇧2)"
by (rule Gramian_determinant(1), auto simp: len)
also have "… ≤ (∏j<n. N)"
by (rule prod_mono, insert N_gso, auto simp: len)
also have "… = N^n" by simp
also have "… ≤ (of_nat n * c^2)^n"
proof (rule power_mono)
show "0 ≤ N" using N_ge_0 len n0 by auto
show "N ≤ of_nat n * c^2" unfolding N_def
proof (intro Max.boundedI, force, use fs in force, clarify)
fix f
assume "f ∈ set fs"
from this[folded rows] obtain i where i: "i < n" and f: "f = row A i"
using A unfolding rows_def by auto
have "∥f∥⇧2 = (∑x←list_of_vec (row A i). x^2)"
unfolding f sq_norm_vec_def power2_eq_square by simp
also have "list_of_vec (row A i) = map (λ j. A $$ (i,j)) [0..<n]"
using i A by (intro nth_equalityI, auto)
also have "sum_list (map power2 (map (λj. A $$ (i, j)) [0..<n])) ≤
sum_list (map (λ j. c^2) [0..<n])" unfolding map_map o_def
proof (intro sum_list_mono)
fix j
assume "j ∈ set [0 ..< n]"
hence j: "j < n" by auto
from Bnd i j A have "¦A $$ (i, j)¦ ≤ c" by (auto simp: Bounded_mat_def)
thus "(A $$ (i, j))⇧2 ≤ c⇧2"
by (meson abs_ge_zero order_trans power2_le_iff_abs_le)
qed
also have "… = (∑j <n. c⇧2)"
unfolding interv_sum_list_conv_sum_set_nat by auto
also have "… = of_nat n * c⇧2" by auto
finally show "∥f∥⇧2 ≤ of_nat n * c⇧2" .
qed
qed
also have "… = (of_nat n)^n * (c⇧2 ^ n)" by (auto simp: algebra_simps)
also have "… = of_nat n ^n * c^(2 * n)" unfolding power_mult[symmetric]
by (simp add: ac_simps)
finally show ?thesis .
qed
lemma det_bound_hadamard_squared: fixes A::"'a :: trivial_conjugatable_linordered_field mat"
assumes A: "A ∈ carrier_mat n n"
and Bnd: "A ∈ Bounded_mat c"
shows "(abs (det A))^2 ≤ of_nat n ^ n * c ^ (2 * n)"
proof (cases "n > 0")
case n: True
from n A Bnd have "abs (A $$ (0,0)) ≤ c" by (auto simp: Bounded_mat_def)
hence c0: "c ≥ 0" by auto
let ?us = "map (row A) [0 ..< n]"
interpret gso: gram_schmidt_fs n ?us .
have len: "length ?us = n" by simp
have us: "set ?us ⊆ carrier_vec n" using A by auto
let ?vs = "map gso.gso [0..<n]"
show ?thesis
proof (cases "carrier_vec n ⊆ gso.span (set ?us)")
case False
from mat_of_rows_rows[unfolded rows_def,of A] A gram_schmidt.non_span_det_zero[OF len False us]
have zero: "det A = 0" by auto
show ?thesis unfolding zero using c0 by simp
next
case True
with us len have basis: "gso.basis_list ?us" unfolding gso.basis_list_def by auto
note in_dep = gso.basis_list_imp_lin_indpt_list[OF basis]
interpret gso: gram_schmidt_fs_lin_indpt n ?us
by (standard) (use in_dep gso.lin_indpt_list_def in auto)
from gso.det_bound_main[OF _ A n Bnd]
show ?thesis using A by (auto simp: rows_def)
qed
next
case False
with A show ?thesis by auto
qed
definition det_bound_hadamard :: "nat ⇒ int ⇒ int" where
"det_bound_hadamard n c = (sqrt_int_floor ((int n * c^2)^n))"
lemma det_bound_hadamard_altdef[code]:
"det_bound_hadamard n c = (if n = 1 ∨ even n then int n ^ (n div 2) * (abs c)^n else sqrt_int_floor ((int n * c^2)^n))"
proof (cases "n = 1 ∨ even n")
case False
thus ?thesis unfolding det_bound_hadamard_def by auto
next
case True
define thesis where "thesis = ?thesis"
have "thesis ⟷ sqrt_int_floor ((int n * c^2)^n) = int n ^ (n div 2) * abs c^n"
using True unfolding thesis_def det_bound_hadamard_def by auto
also have "(int n * c^2)^n = int n^n * c^(2 * n)"
unfolding power_mult[symmetric] power_mult_distrib by (simp add: ac_simps)
also have "int n^n = int n ^ (2 * (n div 2))" using True by auto
also have "… * c^(2 * n) = (int n ^ (n div 2) * c^n)^2"
unfolding power_mult_distrib power_mult[symmetric] by (simp add: ac_simps)
also have "sqrt_int_floor … = int n ^ (n div 2) * ¦c¦ ^ n"
unfolding sqrt_int_floor of_int_power real_sqrt_abs of_int_abs[symmetric] floor_of_int
abs_mult power_abs by simp
finally have thesis by auto
thus ?thesis unfolding thesis_def by auto
qed
lemma det_bound_hadamard: "is_det_bound det_bound_hadamard"
unfolding is_det_bound_def
proof (intro allI impI)
fix A :: "int mat" and n c
assume A: "A ∈ carrier_mat n n" and BndA: "A ∈ Bounded_mat c"
let ?h = rat_of_int
let ?hA = "map_mat ?h A"
let ?hc = "?h c"
from A have hA: "?hA ∈ carrier_mat n n" by auto
from BndA have Bnd: "?hA ∈ Bounded_mat ?hc"
unfolding Bounded_mat_def
by (auto, unfold of_int_abs[symmetric] of_int_le_iff, auto)
have sqrt: "sqrt ((real n * (real_of_int c)⇧2) ^ n) ≥ 0"
by simp
from det_bound_hadamard_squared[OF hA Bnd, unfolded of_int_hom.hom_det of_int_abs[symmetric]]
have "?h ( ¦det A¦^2) ≤ ?h (int n ^ n * c ^ (2 * n))" by simp
from this[unfolded of_int_le_iff]
have "¦det A¦^2 ≤ int n ^ n * c ^ (2 * n)" .
also have "… = (int n * c^2)^n" unfolding power_mult power_mult_distrib by simp
finally have "¦det A¦⇧2 ≤ (int n * c⇧2) ^ n" by simp
hence "sqrt_int_floor (¦det A¦⇧2) ≤ sqrt_int_floor ((int n * c⇧2) ^ n)"
unfolding sqrt_int_floor by (intro floor_mono real_sqrt_le_mono, linarith)
also have "sqrt_int_floor (¦det A¦⇧2) = ¦det A¦" by (simp del: of_int_abs add: of_int_abs[symmetric])
finally show "¦det A¦ ≤ det_bound_hadamard n c" unfolding det_bound_hadamard_def by simp
qed
lemma n_pow_n_le_fact_square: "n ^ n ≤ (fact n)^2"
proof -
define ii where "ii (i :: nat) = (n + 1 - i)" for i
have id: "ii ` {1..n} = {1..n}" unfolding ii_def
proof (auto, goal_cases)
case (1 i)
hence i: "i = (-) (Suc n) (ii i)" unfolding ii_def by auto
show ?case by (subst i, rule imageI, insert 1, auto simp: ii_def)
qed
have "(fact n) = (∏{1..n})"
by (simp add: fact_prod)
hence "(fact n)^2 = ((∏{1..n}) * (∏{1..n}))" by (auto simp: power2_eq_square)
also have "… = ((∏{1..n}) * prod (λ i. i) (ii ` {1..n}))"
by (rule arg_cong[of _ _ "λ x. (_ * x)"], rule prod.cong[OF id[symmetric]], auto)
also have "… = ((∏{1..n}) * prod ii {1..n})"
by (subst prod.reindex, auto simp: ii_def inj_on_def)
also have "… = (prod (λ i. i * ii i) {1..n})"
by (subst prod.distrib, auto)
also have "… ≥ (prod (λ i. n) {1..n})"
proof (intro prod_mono conjI, simp)
fix i
assume i: "i ∈ {1 .. n}"
let ?j = "ii i"
show "n ≤ i * ?j"
proof (cases "i = 1 ∨ i = n")
case True
thus ?thesis unfolding ii_def by auto
next
case False
hence min: "min i ?j ≥ 2" using i by (auto simp: ii_def)
have max: "n ≤ 2 * max i ?j" using i by (auto simp: ii_def)
also have "… ≤ min i ?j * max i ?j" using min
by (intro mult_mono, auto)
also have "… = i * ?j" by (cases "i < ?j", auto simp: ac_simps)
finally show ?thesis .
qed
qed
finally show ?thesis by simp
qed
lemma sqrt_int_floor_bound: "0 ≤ x ⟹ (sqrt_int_floor x)^2 ≤ x"
unfolding sqrt_int_floor_def
using root_int_floor_def root_int_floor_pos_lower by auto
lemma det_bound_hadamard_improves_det_bound_fact: assumes c: "c ≥ 0"
shows "det_bound_hadamard n c ≤ det_bound_fact n c"
proof -
have "(det_bound_hadamard n c)^2 ≤ (int n * c⇧2) ^ n" unfolding det_bound_hadamard_def
by (rule sqrt_int_floor_bound, auto)
also have "… = int (n ^ n) * c^(2 * n)" by (simp add: power_mult power_mult_distrib)
also have "… ≤ int ((fact n)^2) * c^(2 * n)"
by (intro mult_right_mono, unfold of_nat_le_iff, rule n_pow_n_le_fact_square, auto)
also have "… = (det_bound_fact n c)^2" unfolding det_bound_fact_def
by (simp add: power_mult_distrib power_mult[symmetric] ac_simps)
finally have "abs (det_bound_hadamard n c) ≤ abs (det_bound_fact n c)"
unfolding abs_le_square_iff .
hence "det_bound_hadamard n c ≤ abs (det_bound_fact n c)" by simp
also have "… = det_bound_fact n c" unfolding det_bound_fact_def using c by auto
finally show ?thesis .
qed
context
begin
private fun syl :: "int ⇒ nat ⇒ int mat" where
"syl c 0 = mat 1 1 (λ _. c)"
| "syl c (Suc n) = (let A = syl c n in
four_block_mat A A (-A) A)"
private lemma syl: assumes c: "c ≥ 0"
shows "syl c n ∈ Bounded_mat c ∧ syl c n ∈ carrier_mat (2^n) (2^n)
∧ det (syl c n) = det_bound_hadamard (2^n) c"
proof (cases "n = 0")
case True
thus ?thesis using c
unfolding det_bound_hadamard_altdef
by (auto simp: Bounded_mat_def det_single)
next
case False
then obtain m where n: "n = Suc m" by (cases n, auto)
show ?thesis unfolding n
proof (induct m)
case 0
show ?case unfolding syl.simps Let_def using c
apply (subst det_four_block_mat[of _ 1]; force?)
apply (subst det_single,
auto simp: Bounded_mat_def scalar_prod_def det_bound_hadamard_altdef power2_eq_square)
done
next
case (Suc m)
define A where "A = syl c (Suc m)"
let ?FB = "four_block_mat A A (- A) A"
define n :: nat where "n = 2 ^ Suc m"
from Suc[folded A_def n_def]
have Bnd: "A ∈ Bounded_mat c"
and A: "A ∈ carrier_mat n n"
and detA: "det A = det_bound_hadamard n c"
by auto
have n2: "2 ^ Suc (Suc m) = 2 * n" unfolding n_def by auto
show ?case unfolding syl.simps(2)[of _ "Suc m"] A_def[symmetric] Let_def n2
proof (intro conjI)
show "?FB ∈ carrier_mat (2 * n) (2 * n)" using A by auto
show "?FB ∈ Bounded_mat c" using Bnd A unfolding Bounded_mat_elements_mat
by (subst elements_four_block_mat_id, auto)
have ev: "even n" and sum: "n div 2 + n div 2 = n" unfolding n_def by auto
have n2: "n * 2 = n + n" by simp
have "det ?FB = det (A * A - A * - A)"
by (rule det_four_block_mat[OF A A _ A], insert A, auto)
also have "A * A - A * - A = A * A + A * A" using A by auto
also have "… = 2 ⋅⇩m (A * A)" using A by auto
also have "det … = 2^n * det (A * A)"
by (subst det_smult, insert A, auto)
also have "det (A * A) = det A * det A" by (rule det_mult[OF A A])
also have "2^n * … = det_bound_hadamard (2 * n) c" unfolding detA
unfolding det_bound_hadamard_altdef by (simp add: ev ac_simps power_add[symmetric] sum n2)
finally show "det ?FB = det_bound_hadamard (2 * n) c" .
qed
qed
qed
lemma det_bound_hadamard_tight:
assumes c: "c ≥ 0"
and "n = 2^m"
shows "∃ A. A ∈ carrier_mat n n ∧ A ∈ Bounded_mat c ∧ det A = det_bound_hadamard n c"
by (rule exI[of _ "syl c m"], insert syl[OF c, of m, folded assms(2)], auto)
end
lemma Ints_matE: assumes "A ∈ ℤ⇩m"
shows "∃ B. A = map_mat of_int B"
proof -
have "∀ ij. ∃ x. fst ij < dim_row A ⟶ snd ij < dim_col A ⟶ A $$ ij = of_int x"
using assms unfolding Ints_mat_def Ints_def by auto
from choice[OF this] obtain f where
f: "∀ i j. i < dim_row A ⟶ j < dim_col A ⟶ A $$ (i,j) = of_int (f (i,j))"
by auto
show ?thesis
by (intro exI[of _ "mat (dim_row A) (dim_col A) f"] eq_matI, insert f, auto)
qed
lemma is_det_bound_of_int: fixes A :: "'a :: linordered_idom mat"
assumes db: "is_det_bound db"
and A: "A ∈ carrier_mat n n"
and "A ∈ ℤ⇩m ∩ Bounded_mat (of_int bnd)"
shows "abs (det A) ≤ of_int (db n bnd)"
proof -
from assms have "A ∈ ℤ⇩m" by auto
from Ints_matE[OF this] obtain B where
AB: "A = map_mat of_int B" by auto
from assms have "A ∈ Bounded_mat (of_int bnd)" by auto
hence "B ∈ Bounded_mat bnd" unfolding AB Bounded_mat_elements_mat
by (auto simp flip: of_int_abs)
from db[unfolded is_det_bound_def, rule_format, OF _ this, of n] AB A
have "¦det B¦ ≤ db n bnd" by auto
thus ?thesis unfolding AB of_int_hom.hom_det
by (simp flip: of_int_abs)
qed
lemma minus_in_Bounded_vec[simp]:
"(-x) ∈ Bounded_vec b ⟷ x ∈ Bounded_vec b"
unfolding Bounded_vec_def by auto
lemma sum_in_Bounded_vecI[intro]: assumes
xB: "x ∈ Bounded_vec B1" and
yB: "y ∈ Bounded_vec B2" and
x: "x ∈ carrier_vec n" and
y: "y ∈ carrier_vec n"
shows "x + y ∈ Bounded_vec (B1 + B2)"
proof -
from x y have id: "dim_vec (x + y) = n" by auto
show ?thesis unfolding Bounded_vec_def mem_Collect_eq id
proof (intro allI impI)
fix i
assume i: "i < n"
with x y xB yB have *: "abs (x $ i) ≤ B1" "abs (y $ i) ≤ B2"
unfolding Bounded_vec_def by auto
thus "¦(x + y) $ i¦ ≤ B1 + B2" using i x y by simp
qed
qed
lemma (in gram_schmidt) lincomb_card_bound: assumes XBnd: "X ⊆ Bounded_vec Bnd"
and X: "X ⊆ carrier_vec n"
and Bnd: "Bnd ≥ 0"
and c: "⋀ x. x ∈ X ⟹ abs (c x) ≤ 1"
and card: "card X ≤ k"
shows "lincomb c X ∈ Bounded_vec (of_nat k * Bnd)"
proof -
from X have dim: "dim_vec (lincomb c X) = n" by auto
show ?thesis unfolding Bounded_vec_def mem_Collect_eq dim
proof (intro allI impI)
fix i
assume i: "i < n"
have "abs (lincomb c X $ i) = abs (∑x∈X. c x * x $ i)"
by (subst lincomb_index[OF i X], auto)
also have "… ≤ (∑x∈X. abs (c x * x $ i))" by auto
also have "… = (∑x∈X. abs (c x) * abs (x $ i))" by (auto simp: abs_mult)
also have "… ≤ (∑x∈X. 1 * abs (x $ i))"
by (rule sum_mono[OF mult_right_mono], insert c, auto)
also have "… = (∑x∈X. abs (x $ i))" by simp
also have "… ≤ (∑x∈X. Bnd)"
by (rule sum_mono, insert i XBnd[unfolded Bounded_vec_def] X, force)
also have "… = of_nat (card X) * Bnd" by simp
also have "… ≤ of_nat k * Bnd"
by (rule mult_right_mono[OF _ Bnd], insert card, auto)
finally show "abs (lincomb c X $ i) ≤ of_nat k * Bnd" by auto
qed
qed
lemma bounded_vecset_sum:
assumes Acarr: "A ⊆ carrier_vec n"
and Bcarr: "B ⊆ carrier_vec n"
and sum: "C = A + B"
and Cbnd: "∃ bndC. C ⊆ Bounded_vec bndC"
shows "A ≠ {} ⟹ (∃ bndB. B ⊆ Bounded_vec bndB)"
and "B ≠ {} ⟹ (∃ bndA. A ⊆ Bounded_vec bndA)"
proof -
{
fix A B :: "'a vec set"
assume Acarr: "A ⊆ carrier_vec n"
assume Bcarr: "B ⊆ carrier_vec n"
assume sum: "C = A + B"
assume Ane: "A ≠ {}"
have "∃ bndB. B ⊆ Bounded_vec bndB"
proof(cases "B = {}")
case Bne: False
from Cbnd obtain bndC where bndC: "C ⊆ Bounded_vec bndC" by auto
from Ane obtain a where aA: "a ∈ A" and acarr: "a ∈ carrier_vec n" using Acarr by auto
let ?M = "{abs (a $ i) | i. i < n}"
have finM: "finite ?M" by simp
define nb where "nb = abs bndC + Max ?M"
{
fix b
assume bB: "b ∈ B" and bcarr: "b ∈ carrier_vec n"
have ab: "a + b ∈ Bounded_vec bndC" using aA bB bndC sum by auto
{
fix i
assume i_lt_n: "i < n"
hence ai_le_max: "abs(a $ i) ≤ Max ?M" using acarr finM Max_ge by blast
hence "abs(a $ i + b $ i) ≤ abs bndC"
using ab bcarr acarr index_add_vec(1) i_lt_n unfolding Bounded_vec_def by auto
hence "abs(b $ i) ≤ abs bndC + abs(a $ i)" by simp
hence "abs(b $ i) ≤ nb" using i_lt_n bcarr ai_le_max unfolding nb_def by simp
}
hence "b ∈ Bounded_vec nb" unfolding Bounded_vec_def using bcarr carrier_vecD by blast
}
hence "B ⊆ Bounded_vec nb" unfolding Bounded_vec_def using Bcarr by auto
thus ?thesis by auto
qed auto
} note theor = this
show "A ≠ {} ⟹ (∃ bndB. B ⊆ Bounded_vec bndB)" using theor[OF Acarr Bcarr sum] by simp
have CBA: "C = B + A" unfolding sum by (rule comm_add_vecset[OF Acarr Bcarr])
show "B ≠ {} ⟹ ∃ bndA. A ⊆ Bounded_vec bndA" using theor[OF Bcarr Acarr CBA] by simp
qed
end