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 (* for some simp-rules *) begin (* TODO: move into theory Norms *) 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