Theory Linear_Bound_Argument
section ‹Linear Bound Argument - General ›
text ‹Lemmas to enable general reasoning using the linear bound argument for combinatorial proofs.
Jukna \<^cite>‹"juknaExtremalCombinatorics2011"› presents a good overview of the mathematical background
this theory is based on and applications ›
theory Linear_Bound_Argument imports Incidence_Matrices Jordan_Normal_Form.DL_Rank
Jordan_Normal_Form.Ring_Hom_Matrix
begin
subsection ‹Vec Space Extensions›
text ‹Simple extensions to the existing vector space locale on linear independence ›
context vec_space
begin
lemma lin_indpt_set_card_lt_dim:
fixes A :: "'a vec set"
assumes "A ⊆ carrier_vec n"
assumes "lin_indpt A"
shows "card A ≤ dim"
using assms(1) assms(2) fin_dim li_le_dim(2) by blast
lemma lin_indpt_dim_col_lt_dim:
fixes A :: "'a mat"
assumes "A ∈ carrier_mat n nc"
assumes "distinct (cols A)"
assumes "lin_indpt (set (cols A))"
shows "nc ≤ dim"
proof -
have b: "card (set (cols A)) = dim_col A" using cols_length assms(2)
by (simp add: distinct_card)
have "set (cols A) ⊆ carrier_vec n" using assms(1) cols_dim by blast
thus ?thesis using lin_indpt_set_card_lt_dim assms b by auto
qed
lemma lin_comb_imp_lin_dep_fin:
fixes A :: "'a vec set"
assumes "finite A"
assumes "A ⊆ carrier_vec n"
assumes "lincomb c A = 0⇩v n"
assumes "∃ a. a ∈ A ∧ c a ≠ 0"
shows "lin_dep A"
unfolding lin_dep_def using assms lincomb_as_lincomb_list_distinct sumlist_nth by auto
text ‹While a trivial definition, this enables us to directly reference the definition outside
of a locale context, as @{term "lin_indpt"} is an inherited definition ›
definition lin_indpt_vs:: "'a vec set ⇒ bool" where
"lin_indpt_vs A ⟷ lin_indpt A"
lemma lin_comb_sum_lin_indpt:
fixes A :: "'a vec list"
assumes "set (A) ⊆ carrier_vec n"
assumes "distinct A"
assumes "⋀ f. lincomb_list (λi. f (A ! i)) A = 0⇩v n ⟹ ∀v∈ (set A). f v = 0"
shows "lin_indpt (set A)"
by (rule finite_lin_indpt2, auto simp add: assms lincomb_as_lincomb_list_distinct)
lemma lin_comb_mat_lin_indpt:
fixes A :: "'a vec list"
assumes "set (A) ⊆ carrier_vec n"
assumes "distinct A"
assumes "⋀ f. mat_of_cols n A *⇩v vec (length A) (λi. f (A ! i)) = 0⇩v n ⟹ ∀v∈ (set A). f v = 0"
shows "lin_indpt (set A)"
proof (rule lin_comb_sum_lin_indpt, auto simp add: assms)
fix f v
have "⋀ v. v ∈ set A ⟹ dim_vec v = n"
using assms by auto
then show "lincomb_list (λi. f (A ! i)) A = 0⇩v n ⟹ v ∈ set A ⟹ f v = 0"
using lincomb_list_as_mat_mult[of A "(λi. f (A ! i))"] assms(3)[of f] by auto
qed
lemma lin_comb_mat_lin_indpt_vs:
fixes A :: "'a vec list"
assumes "set (A) ⊆ carrier_vec n"
assumes "distinct A"
assumes "⋀ f. mat_of_cols n A *⇩v vec (length A) (λi. f (A ! i)) = 0⇩v n ⟹ ∀v∈ (set A). f v = 0"
shows "lin_indpt_vs (set A)"
using lin_comb_mat_lin_indpt lin_indpt_vs_def assms by auto
end
subsection ‹Linear Bound Argument Lemmas›
text ‹Three general representations of the linear bound argument, requiring a direct fact of
linear independence onthe rows of the vector space over either a set A of vectors, list xs of vectors
or a Matrix' columns ›
lemma lin_bound_arg_general_set:
fixes A ::"('a :: {field})vec set"
assumes "A ⊆ carrier_vec nr"
assumes "vec_space.lin_indpt_vs nr A"
shows "card A ≤ nr"
using vec_space.lin_indpt_set_card_lt_dim[of "A" "nr"] vec_space.lin_indpt_vs_def[of nr A]
vec_space.dim_is_n assms by metis
lemma lin_bound_arg_general_list:
fixes xs ::"('a :: {field})vec list"
assumes "distinct xs"
assumes "(set xs) ⊆ carrier_vec nr"
assumes "vec_space.lin_indpt_vs nr (set xs)"
shows "length (xs) ≤ nr"
using lin_bound_arg_general_set[of "set xs" nr] distinct_card assms
by force
lemma lin_bound_arg_general:
fixes A ::"('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A ∈ carrier_mat nr nc"
assumes "vec_space.lin_indpt_vs nr (set (cols A))"
shows "nc ≤ nr"
proof -
have ss: "set (cols A) ⊆ carrier_vec nr" using assms cols_dim by blast
have "length (cols A) = nc"
using assms(2) cols_length by blast
thus ?thesis using lin_bound_arg_general_list[of "cols A" "nr"] ss assms by simp
qed
text‹The linear bound argument lemma on a matrix requiring the lower level assumption on a linear
combination. This removes the need to directly refer to any aspect of the linear algebra libraries ›
lemma lin_bound_argument:
fixes A :: "('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A ∈ carrier_mat nr nc"
assumes "⋀ f. A *⇩v vec nc (λi. f (col A i)) = 0⇩v nr ⟹ ∀v∈ (set (cols A)). f v = 0"
shows "nc ≤ nr"
proof (intro lin_bound_arg_general[of "A" nr nc] vec_space.lin_comb_mat_lin_indpt_vs, simp_all add: assms)
show "set (cols A) ⊆ carrier_vec nr" using assms cols_dim by blast
next
have mA: "mat_of_cols nr (cols A) = A" using mat_of_cols_def assms by auto
have "⋀ f. vec (dim_col A) (λi. f (cols A ! i)) = vec nc (λi. f (col A i))"
proof (intro eq_vecI, simp_all add: assms)
show "⋀f i. i < nc ⟹ vec (dim_col A) (λi. f (cols A ! i)) $ i = f (col A i)"
using assms(2) by force
show "dim_col A = nc " using assms by simp
qed
then show "⋀f. mat_of_cols nr (cols A) *⇩v vec (dim_col A) (λi. f (cols A ! i)) = 0⇩v nr ⟹
∀v∈set (cols A). f v = 0"
using mA assms(3) by metis
qed
text ‹A further extension to present the linear combination directly as a sum. This manipulation from
vector product to a summation was found to commonly be repeated in proofs applying this rule ›
lemma lin_bound_argument2:
fixes A :: "('a :: {field}) mat"
assumes "distinct (cols A)"
assumes "A ∈ carrier_mat nr nc"
assumes "⋀ f. vec nr (λi. ∑ j ∈ {0..<nc} . f (col A j) * (col A j) $ i) = 0⇩v nr ⟹
∀v∈ (set (cols A)). f v = 0"
shows "nc ≤ nr"
proof (intro lin_bound_argument[of A nr nc], simp add: assms, simp add: assms)
fix f
have "A *⇩v vec nc (λi. f (col A i)) =
vec (dim_row A) (λi. ∑ j ∈ {0..<nc} . (row A i $ j) * f (col A j))"
by (auto simp add: mult_mat_vec_def scalar_prod_def assms(2))
also have "... = vec (dim_row A) (λi. ∑ j ∈ {0..<nc} . f (col A j) * (col A j $ i))"
using assms(2) by (intro eq_vecI, simp_all) (meson mult.commute)
finally show "A *⇩v vec nc (λi. f (col A i)) = 0⇩v nr ⟹ ∀v∈set (cols A). f v = 0"
using assms(3)[of f] assms(2) by fastforce
qed
end