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 a bound 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 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 det_bound :: "nat ⇒ 'a :: linordered_idom ⇒ 'a" where
  "det_bound n x = fact n * (x^n)"

lemma det_bound: assumes A: "A ∈ carrier_mat n n"
  and x: "A ∈ Bounded_mat x"
shows "abs (det A) ≤ det_bound 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 signof_def)
  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 n x" unfolding det_bound_def by auto
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