(* Title: HOL/Analysis/Cartesian_Space.thy Author: Amine Chaieb, University of Cambridge Author: Jose Divasón <jose.divasonm at unirioja.es> Author: Jesús Aransay <jesus-maria.aransay at unirioja.es> Author: Johannes Hölzl, VU Amsterdam Author: Fabian Immler, TUM
*)
section "Linear Algebra on Finite Cartesian Products"
theory Cartesian_Space imports "HOL-Combinatorics.Transposition"
Finite_Cartesian_Product
Linear_Algebra begin
subsection\<^marker>\<open>tag unimportant\<close> \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following is really basic linear algebra, check for overlap? rename subsection? *)
definition"cart_basis = {axis i 1 | i. i\UNIV}"
lemma finite_cart_basis: "finite (cart_basis)"unfolding cart_basis_def using finite_Atleast_Atmost_nat by fastforce
interpretation vec: vector_space "(*s) " by unfold_locales (vector algebra_simps)+
lemma independent_cart_basis: "vec.independent (cart_basis)" proof (rule vec.independent_if_scalars_zero) show"finite (cart_basis)"using finite_cart_basis . fix f::"('a, 'b) vec \ 'a" and x::"('a, 'b) vec" assume eq_0: "(\x\cart_basis. f x *s x) = 0" and x_in: "x \ cart_basis" obtain i where x: "x = axis i 1"using x_in unfolding cart_basis_def by auto have sum_eq_0: "(\x\(cart_basis) - {x}. f x * (x $ i)) = 0" proof (intro sum.neutral ballI) fix y assume y: "y \ cart_basis - {x}" obtain a where a: "y = axis a 1"and a_not_i: "a \ i" using y x unfolding cart_basis_def by auto have"y $ i = 0"unfolding a axis_def using a_not_i by auto thus"f y * y $ i = 0"by simp qed have"0 = (\x\cart_basis. f x *s x) $ i" using eq_0 by simp alsohave"\ = (\x\cart_basis. (f x *s x) $ i)" unfolding sum_component .. alsohave"\ = (\x\cart_basis. f x * (x $ i))" unfolding vector_smult_component .. alsohave"\ = f x * (x $ i) + (\x\(cart_basis) - {x}. f x * (x $ i))" by (rule sum.remove[OF finite_cart_basis x_in]) alsohave"\ = f x * (x $ i)" unfolding sum_eq_0 by simp alsohave"\ = f x" unfolding x axis_def by auto finallyshow"f x = 0" .. qed
lemma span_cart_basis [simp]: "vec.span (cart_basis) = UNIV" proof - have"x \ vec.span cart_basis" for x :: "('a, 'b) vec" proof - let ?f="\v. x $ (THE i. v = axis i 1)" have"x $ i = (\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" for i::'b proof - let ?w = "axis i (1::'a)" have the_eq_i: "(THE a. ?w = axis a 1) = i" by (rule the_equality, auto simp: axis_eq_axis) have sum_eq_0: "(\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0" proof (intro sum.neutral ballI) fix y:: "('a, 'b) vec" assume y: "y \ cart_basis - {?w}" obtain j where j: "y = axis j 1"and i_not_j: "i \ j" using y unfolding cart_basis_def by auto have the_eq_j: "(THE i. y = axis i 1) = j" by (simp add: axis_eq_axis j) show"x $ (THE i. y = axis i 1) * y $ i = 0" by (simp add: axis_def i_not_j j) qed have"(\v\cart_basis. x $ (THE i. v = axis i 1) *s v) $ i
= (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)" by force alsohave"\ = x $ (THE a. ?w = axis a 1) * ?w $ i + (\v\(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i)" by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def) alsohave"\ = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp alsohave"\ = x $ i" unfolding the_eq_i unfolding axis_def by auto finallyshow ?thesis by simp qed thenshow"x \ vec.span (cart_basis)" by (metis (no_types, lifting) vec.span_base vec.span_scale vec.span_sum vec_eq_iff) qed thenshow ?thesis by auto qed
(*Some interpretations:*) interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis" by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
lemma span_vec_eq: "vec.span X = span X" and dim_vec_eq: "vec.dim X = dim X" and dependent_vec_eq: "vec.dependent X = dependent X" and subspace_vec_eq: "vec.subspace X = subspace X" for X::"(real^'n) set" unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def by (auto simp: scalar_mult_eq_scaleR)
lemma linear_componentwise: fixes f:: "'a::field ^'m \ 'a ^ 'n" assumes lf: "Vector_Spaces.linear (*s) (*s) f" shows"(f x)$j = sum (\i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") proof - interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f using lf . let ?M = "(UNIV :: 'm set)" let ?N = "(UNIV :: 'n set)" have fM: "finite ?M"by simp have"?rhs = (sum (\i. (x$i) *s (f (axis i 1))) ?M)$j" unfolding sum_component by simp thenshow ?thesis unfolding lf.sum[symmetric] lf.scale[symmetric] unfolding basis_expansion by auto qed
interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A" using matrix_vector_mul_linear_gen.
lemma matrix_works: assumes lf: "Vector_Spaces.linear (*s) (*s) f" shows"matrix f *v x = f (x::'a::field ^ 'n)" proof - have"\i. (\j\UNIV. x $ j * f (axis j 1) $ i) = f x $ i" by (simp add: Cartesian_Space.linear_componentwise lf) thenshow ?thesis by (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) qed
lemma matrix_of_matrix_vector_mul[simp]: "matrix(\x. A *v (x :: 'a::field ^ 'n)) = A" by (simp add: matrix_eq matrix_works)
lemma matrix_compose_gen: assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \ 'a^'m)" and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \ 'a^_)" shows"matrix (g o f) = matrix g ** matrix f" using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]] by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
lemma matrix_compose: assumes"linear (f::real^'n \ real^'m)" "linear (g::real^'m \ real^_)" shows"matrix (g o f) = matrix g ** matrix f" using matrix_compose_gen[of f g] assms by (simp add: linear_def scalar_mult_eq_scaleR)
lemma left_invertible_transpose: "(\(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \ (\(B). A ** B = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose)
lemma right_invertible_transpose: "(\(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \ (\(B). B ** A = mat 1)" by (metis matrix_transpose_mul transpose_mat transpose_transpose)
lemma linear_matrix_vector_mul_eq: "Vector_Spaces.linear (*s) (*s) f \ linear (f :: real^'n \ real ^'m)" by (simp add: scalar_mult_eq_scaleR linear_def)
lemma matrix_vector_mul[simp]: "Vector_Spaces.linear (*s) (*s) g \ (\y. matrix g *v y) = g" "linear f \ (\x. matrix f *v x) = f" "bounded_linear f \ (\x. matrix f *v x) = f" for f :: "real^'n \ real ^'m" by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
lemma matrix_left_invertible_injective: fixes A :: "'a::field^'n^'m" shows"(\B. B ** A = mat 1) \ inj ((*v) A)" proof safe fix B assume B: "B ** A = mat 1" show"inj ((*v) A)" unfolding inj_on_def by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid) next assume"inj ((*v) A)" from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this] obtain g where"Vector_Spaces.linear (*s) (*s) g" and "g \ (*v) A = id" by blast thenhave"matrix g ** A = mat 1" by (metis matrix_compose_gen matrix_id_mat_1 matrix_of_matrix_vector_mul vec.linear_axioms) thenshow"\B. B ** A = mat 1" by metis qed
lemma matrix_left_invertible_ker: "(\B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \ (\x. A *v x = 0 \ x = 0)" by (simp add: matrix_left_invertible_injective vec.inj_iff_eq_0)
lemma matrix_right_invertible_surjective: "(\B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \ surj (\x. A *v x)" proof - have"\B x. A ** B = mat 1 \ \y. x = A *v y" by (metis matrix_vector_mul_assoc matrix_vector_mul_lid) moreover have"\B. A ** B = mat 1" if "surj ((*v) A)" by (metis (no_types, opaque_lifting) matrix_compose_gen matrix_id_mat_1
matrix_of_matrix_vector_mul vec.linear_axioms
vec.linear_surjective_right_inverse that) ultimatelyshow ?thesis by (auto simp: image_def set_eq_iff surj_def) qed
lemma matrix_left_invertible_independent_columns: fixes A :: "'a::{field}^'n^'m" shows"(\(B::'a ^'m^'n). B ** A = mat 1) \
(\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
(is"?lhs \ ?rhs") proof - let ?U = "UNIV :: 'n set" have"c i = 0" if"\x. A *v x = 0 \ x = 0" "sum (\i. c i *s column i A) ?U = 0" for c i by (metis (no_types) UNIV_I matrix_mult_sum vec_lambda_eta vec_nth_cases zero_vec_def that) moreoverhave"x = 0"if"A *v x = 0" ?rhs for x by (metis (full_types) matrix_mult_sum that vec_eq_iff zero_index) ultimatelyshow ?thesis unfolding matrix_left_invertible_ker by auto qed
lemma matrix_right_invertible_independent_rows: fixes A :: "'a::{field}^'n^'m" shows"(\(B::'a^'m^'n). A ** B = mat 1) \
(\<forall>c. sum (\<lambda>i::'m. c i *s row i A) UNIV = 0 \<longrightarrow> (\<forall>i. c i = 0))" by (simp add: matrix_left_invertible_independent_columns flip: left_invertible_transpose)
lemma matrix_right_invertible_span_columns: "(\(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \
vec.span (columns A) = UNIV" (is "?lhs = ?rhs") proof - let ?U = "UNIV :: 'm set" have fU: "finite ?U"by simp have lhseq: "?lhs \ (\y. \(x::'a^'m). sum (\i. (x$i) *s column i A) ?U = y)" unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def by (simp add: eq_commute) have rhseq: "?rhs \ (\x. x \ vec.span (columns A))" by blast
{ assume h: ?lhs
{ fix x:: "'a ^'n" obtain y :: "'a ^'m"where y: "sum (\i. (y$i) *s column i A) ?U = x" using h lhseq by blast thenhave"x \ vec.span (columns A)" by (metis (mono_tags, lifting) columns_def mem_Collect_eq vec.span_base vec.span_scale vec.span_sum)
} thenhave ?rhs unfolding rhseq by blast } moreover
{ assume h:?rhs let ?P = "\(y::'a ^'n). \(x::'a^'m). sum (\i. (x$i) *s column i A) ?U = y"
{ fix y have"y \ vec.span (columns A)" unfolding h by blast thenhave"?P y" proof (induction rule: vec.span_induct_alt) case base thenshow ?case by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right) next case (step c y1 y2) from step obtain i where i: "i \ ?U" "y1 = column i A" unfolding columns_def by blast obtain x:: "'a ^'m"where x: "sum (\i. (x$i) *s column i A) ?U = y2" using step by blast let ?x = "(\ j. if j = i then c + (x$i) else (x$j))::'a^'m" show ?case proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong) fix j have th: "\xa \ ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" using i(1) by (simp add: field_simps) have"sum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
else (x$xa) * ((column xa A$j))) ?U = sum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U" using th by force alsohave"\ = sum (\xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" by (simp add: sum.distrib) alsohave"\ = c * ((column i A)$j) + sum (\xa. ((x$xa) * ((column xa A)$j))) ?U" unfolding sum.delta[OF fU] using i(1) by simp finallyshow"sum (\xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
else (x$xa) * ((column xa A$j))) ?U
= c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" . qed qed
} thenhave ?lhs unfolding lhseq ..
} ultimatelyshow ?thesis by blast qed
lemma matrix_left_invertible_span_rows_gen: "(\(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \ vec.span (rows A) = UNIV" by (metis columns_transpose matrix_right_invertible_span_columns right_invertible_transpose)
lemma matrix_left_invertible_span_rows: "(\(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \ span (rows A) = UNIV" using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
lemma matrix_left_right_inverse1: fixes A A' :: "'a::{field}^'n^'n" assumes AA': "A ** A' = mat 1" shows"A' ** A = mat 1" proof - have sA: "surj ((*v) A)" using AA' matrix_right_invertible_surjective by auto obtain f' :: "'a ^'n \ 'a ^'n" where f': "Vector_Spaces.linear (*s) (*s) f'" "\x. f' (A *v x) = x" "\x. A *v f' x = x" using sA vec.linear_surjective_isomorphism by blast have"matrix f' ** A = mat 1" by (metis f' matrix_eq matrix_vector_mul_assoc matrix_vector_mul_lid matrix_works) thus"A' ** A = mat 1" by (metis AA' matrix_mul_assoc matrix_mul_lid) qed
lemma matrix_left_right_inverse: fixes A A' :: "'a::{field}^'n^'n" shows"A ** A' = mat 1 \ A' ** A = mat 1" using matrix_left_right_inverse1 by blast
lemma invertible_left_inverse: fixes A :: "'a::{field}^'n^'n" shows"invertible A \ (\(B::'a^'n^'n). B ** A = mat 1)" by (metis invertible_def matrix_left_right_inverse)
lemma invertible_right_inverse: fixes A :: "'a::{field}^'n^'n" shows"invertible A \ (\(B::'a^'n^'n). A** B = mat 1)" by (metis invertible_def matrix_left_right_inverse)
lemma invertible_mult: assumes inv_A: "invertible A" and inv_B: "invertible B" shows"invertible (A**B)" proof - obtain A' where AA': "A ** A' = mat 1"and A'A: "A' ** A = mat 1" using inv_A unfolding invertible_def by blast obtain B' where BB': "B ** B' = mat 1"and B'B: "B' ** B = mat 1" using inv_B unfolding invertible_def by blast have"A ** B ** (B' ** A') = mat 1" by (metis AA' BB' matrix_mul_assoc matrix_mul_rid) moreoverhave"B' ** A' ** (A ** B) = mat 1" by (metis A'A B'B matrix_mul_assoc matrix_mul_rid) ultimatelyshow ?thesis using invertible_def by blast qed
lemma transpose_invertible: fixes A :: "real^'n^'n" assumes"invertible A" shows"invertible (transpose A)" by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
lemma matrix_scaleR_vector_ac: fixes A :: "real^('m::finite)^'n" shows"A *v (k *\<^sub>R v) = k *\<^sub>R A *v v" by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
lemma scaleR_matrix_vector_assoc: fixes A :: "real^('m::finite)^'n" shows"k *\<^sub>R (A *v v) = k *\<^sub>R A *v v" by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
subsection \<open>Some interesting theorems and interpretations\<close>
locale linear_first_finite_dimensional_vector_space =
l?: Vector_Spaces.linear scaleB scaleC f +
B?: finite_dimensional_vector_space scaleB BasisB for scaleB :: "('a::field => 'b::ab_group_add => 'b)" (infixr\<open>*b\<close> 75) and scaleC :: "('a => 'c::ab_group_add => 'c)" (infixr\<open>*c\<close> 75) and BasisB :: "('b set)" and f :: "('b=>'c)"
lemma matrix_vector_mult_in_columnspace: fixes A :: "real^'n^'m" shows"(A *v x) \ span(columns A)" using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq)
lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" by (simp add: subspace_def orthogonal_clauses)
lemma orthogonal_nullspace_rowspace: fixes A :: "real^'n^'m" assumes 0: "A *v x = 0"and y: "y \ span(rows A)" shows"orthogonal x y" using y proof (induction rule: span_induct) case base thenshow ?case by (simp add: subspace_orthogonal_to_vector) next case (step v) thenobtain i where"v = row i A" by (auto simp: rows_def) with 0 show ?case by (metis inner_commute matrix_vector_mul_component orthogonal_def row_def vec_lambda_eta
zero_index) qed
lemma nullspace_inter_rowspace: fixes A :: "real^'n^'m" shows"A *v x = 0 \ x \ span(rows A) \ x = 0" using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right by blast
lemma matrix_vector_mul_injective_on_rowspace: fixes A :: "real^'n^'m" shows"\A *v x = A *v y; x \ span(rows A); y \ span(rows A)\ \ x = y" using nullspace_inter_rowspace [of A "x-y"] by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff)
definition\<^marker>\<open>tag important\<close> rank :: "'a::field^'n^'m=>nat" where row_rank_def_gen: "rank A \ vec.dim(rows A)"
lemma row_rank_def: "rank A = dim (rows A)"for A::"real^'n^'m" by (auto simp: row_rank_def_gen dim_vec_eq)
lemma dim_rows_le_dim_columns: fixes A :: "real^'n^'m" shows"dim(rows A) \ dim(columns A)" proof - have"dim (span (rows A)) \ dim (span (columns A))" proof - obtain B where"independent B""span(rows A) \ span B" and B: "B \ span(rows A)""card B = dim (span(rows A))" using basis_exists [of "span(rows A)"] by metis with span_subspace have eq: "span B = span(rows A)" by auto thenhave inj: "inj_on ((*v) A) (span B)" by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) thenhave ind: "independent ((*v) A ` B)" by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>]) have"dim (span (rows A)) \ card ((*v) A ` B)" by (metis B(2) card_image inj inj_on_subset order.refl span_superset) alsohave"\ \ dim (span (columns A))" using _ ind by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) finallyshow ?thesis . qed thenshow ?thesis by simp qed
lemma column_rank_def: fixes A :: "real^'n^'m" shows"rank A = dim(columns A)" unfolding row_rank_def by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose)
lemma rank_transpose: fixes A :: "real^'n^'m" shows"rank(transpose A) = rank A" by (metis column_rank_def row_rank_def rows_transpose)
lemma matrix_vector_mult_basis: fixes A :: "real^'n^'m" shows"A *v (axis k 1) = column k A" by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
lemma columns_image_basis: fixes A :: "real^'n^'m" shows"columns A = (*v) A ` (range (\i. axis i 1))" by (force simp: columns_def matrix_vector_mult_basis [symmetric])
lemma rank_dim_range: fixes A :: "real^'n^'m" shows"rank A = dim(range (\x. A *v x))" unfolding column_rank_def by (smt (verit, best) columns_image_basis dim_span image_subset_iff iso_tuple_UNIV_I matrix_vector_mult_in_columnspace span_eq)
lemma rank_bound: fixes A :: "real^'n^'m" shows"rank A \ min CARD('m) (CARD('n))" by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff
column_rank_def row_rank_def)
lemma full_rank_injective: fixes A :: "real^'n^'m" shows"rank A = CARD('n) \ inj ((*v) A)" by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
lemma full_rank_surjective: fixes A :: "real^'n^'m" shows"rank A = CARD('m) \ surj ((*v) A)" by (metis (no_types, opaque_lifting) dim_eq_full dim_vec_eq rank_dim_range span_vec_eq vec.span_UNIV vec.span_image vec_dim_card)
lemma less_rank_noninjective: fixes A :: "real^'n^'m" shows"rank A < CARD('n) \ \ inj ((*v) A)" using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
lemma matrix_nonfull_linear_equations_eq: fixes A :: "real^'n^'m" shows"(\x. (x \ 0) \ A *v x = 0) \ rank A \ CARD('n)" by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
lemma rank_eq_0: "rank A = 0 \ A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" for A :: "real^'n^'m" by (auto simp: rank_dim_range matrix_eq)
lemma rank_mul_le_right: fixes A :: "real^'n^'m"and B :: "real^'p^'n" shows"rank(A ** B) \ rank B" proof - have"rank(A ** B) \ dim ((*v) A ` range ((*v) B))" by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) alsohave"\ \ rank B" by (simp add: rank_dim_range dim_image_le) finallyshow ?thesis . qed
lemma rank_mul_le_left: fixes A :: "real^'n^'m"and B :: "real^'p^'n" shows"rank(A ** B) \ rank A" by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
lemma exhaust_2: fixes x :: 2 shows"x = 1 \ x = 2" proof (induct x) case (of_int z) thenhave"z = 0 | z = 1" by fastforce thenshow ?case by auto qed
lemma forall_2: "(\i::2. P i) \ P 1 \ P 2" by (metis exhaust_2)
lemma exhaust_3: fixes x :: 3 shows"x = 1 \ x = 2 \ x = 3" proof (induct x) case (of_int z) thenhave"z = 0 \ z = 1 \ z = 2" by fastforce thenshow ?caseby auto qed
lemma forall_3: "(\i::3. P i) \ P 1 \ P 2 \ P 3" by (metis exhaust_3)
lemma exhaust_4: fixes x :: 4 shows"x = 1 \ x = 2 \ x = 3 \ x = 4" proof (induct x) case (of_int z) thenhave"z = 0 \ z = 1 \ z = 2 \ z = 3" by fastforce thenshow ?caseby auto qed
lemma forall_4: "(\i::4. P i) \ P 1 \ P 2 \ P 3 \ P 4" by (metis exhaust_4)
lemma UNIV_1 [simp]: "UNIV = {1::1}" by auto
lemma UNIV_2: "UNIV = {1, 2::2}" using exhaust_2 by auto
lemma UNIV_3: "UNIV = {1, 2, 3::3}" using exhaust_3 by auto
lemma UNIV_4: "UNIV = {1, 2, 3, 4::4}" using exhaust_4 by auto
lemma sum_1: "sum f (UNIV::1 set) = f 1" unfolding UNIV_1 by simp
lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" unfolding UNIV_2 by simp
lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" unfolding UNIV_3 by (simp add: ac_simps)
lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4" unfolding UNIV_4 by (simp add: ac_simps)
subsection\<^marker>\<open>tag unimportant\<close>\<open>The collapse of the general concepts to dimension one\<close>
lemma vector_one: "(x::'a ^1) = (\ i. (x$1))" by (simp add: vec_eq_iff)
lemma forall_one: "(\(x::'a ^1). P x) \ (\x. P(\ i. x))" by (metis vector_one)
lemma dist_real: "dist(x::real ^ 1) y = \(x$1) - (y$1)\" by (auto simp add: norm_real dist_norm)
subsection\<^marker>\<open>tag unimportant\<close>\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
lemma vector_one_nth [simp]: fixes x :: "'a^1"shows"vec (x $ 1) = x" by (metis vec_def vector_one)
lemma tendsto_at_within_vector_1: fixes S :: "'a :: metric_space set" assumes"(f \ fx) (at x within S)" shows"((\y::'a^1. \ i. f (y $ 1)) \ (vec fx::'a^1)) (at (vec x) within vec ` S)" proof (rule topological_tendstoI) fix T :: "('a^1) set" assume"open T""vec fx \ T" have"\\<^sub>F x in at x within S. f x \ (\x. x $ 1) ` T" using\<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce thenshow"\\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\ i. f (x $ 1)) \ T" unfolding eventually_at dist_norm [symmetric] by (rule ex_forward)
(use\<open>open T\<close> in \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>) qed
lemma forall_vector_1: "(\v::'a::zero^1. P v) \ (\x. P(vector[x]))" by (metis vector_1 vector_one)
lemma forall_vector_2: "(\v::'a::zero^2. P v) \ (\x y. P(vector[x, y]))" proof - have"P v"if"\x y. P (vector [x, y])" for v proof - have"vector [v$1, v$2] = v" unfolding vec_eq_iff by (metis (mono_tags) exhaust_2 vector_2) thenshow ?thesis by (metis that) qed thenshow ?thesis by auto qed
lemma forall_vector_3: "(\v::'a::zero^3. P v) \ (\x y z. P(vector[x, y, z]))" proof - have"P v"if"\x y z. P (vector [x, y, z])" for v proof - have"vector [v$1, v$2, v$3] = v" unfolding vec_eq_iff by (metis (mono_tags) exhaust_3 vector_3) thenshow ?thesis by (metis that) qed thenshow ?thesis by auto qed
subsection\<^marker>\<open>tag unimportant\<close> \<open>lambda skolemization on cartesian products\<close>
lemma lambda_skolem: "(\i. \x. P i x) \ (\x::'a ^ 'n. \i. P i (x $ i))" by (metis vec_lambda_beta)
text\<open>The same result in terms of square matrices.\<close>
text\<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
lemma dot_matrix_product: "(x::real^'n) \ y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
lemma dot_matrix_vector_mul: fixes A B :: "real ^'n ^'n"and x y :: "real ^'n" shows"(A *v x) \ (B *v y) =
(((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" by (metis dot_lmul_matrix dot_matrix_product dot_rowvector_columnvector matrix_mul_assoc vector_transpose_matrix)
lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \i. i \ d \ x$i = 0} = card d"
(is"vec.dim ?A = _") proof (rule vec.dim_unique) let ?B = "((\x. axis x 1) ` d)" have subset_basis: "?B \ cart_basis" by (auto simp: cart_basis_def) show"?B \ ?A" by (auto simp: axis_def) show"vec.independent ((\x. axis x 1) ` d)" using subset_basis by (rule vec.independent_mono[OF vec.independent_Basis]) have"x \ vec.span ?B" if "\i. i \ d \ x $ i = 0" for x::"'a^'n" proof - have"finite ?B" using subset_basis finite_cart_basis by (rule finite_subset) have"x = (\i\UNIV. x $ i *s axis i 1)" by (rule basis_expansion[symmetric]) alsohave"\ = (\i\d. (x $ i) *s axis i 1)" by (rule sum.mono_neutral_cong_right) (auto simp: that) alsohave"\ \ vec.span ?B" by (simp add: vec.span_sum vec.span_clauses) finallyshow"x \ vec.span ?B" . qed thenshow"?A \ vec.span ?B" by auto qed (simp add: card_image inj_on_def axis_eq_axis)
lemma affinity_inverses: assumes m0: "m \ (0::'a::field)" shows"(\x. m *s x + c) \ (\x. inverse(m) *s x + (-(inverse(m) *s c))) = id" "(\x. inverse(m) *s x + (-(inverse(m) *s c))) \ (\x. m *s x + c) = id" using m0 by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
lemma vector_affinity_eq: assumes m0: "(m::'a::field) \ 0" shows"m *s x + c = y \ x = inverse m *s y + -(inverse m *s c)" proof assume h: "m *s x + c = y" hence"m *s x = y - c"by (simp add: field_simps) hence"inverse m *s (m *s x) = inverse m *s (y - c)"by simp thenshow"x = inverse m *s y + - (inverse m *s c)" by (simp add: m0 vec.scale_right_diff_distrib) next assume h: "x = inverse m *s y + - (inverse m *s c)" show"m *s x + c = y"unfolding h using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) qed
lemma vector_eq_affinity: "(m::'a::field) \ 0 ==> (y = m *s x + c \ inverse(m) *s y + -(inverse(m) *s c) = x)" by (metis vector_affinity_eq)
lemma vector_cart: fixes f :: "real^'n \ real" shows"(\ i. f (axis i 1)) = (\i\Basis. f i *\<^sub>R i)" by (simp add: euclidean_eq_iff[where'a="real^'n"]) (simp add: Basis_vec_def inner_axis)
lemma const_vector_cart:"((\ i. d)::real^'n) = (\i\Basis. d *\<^sub>R i)" by (rule vector_cart)
subsection\<^marker>\<open>tag unimportant\<close> \<open>Explicit formulas for low dimensions\<close>
lemma prod_neutral_const: "prod f {(1::nat)..1} = f 1" by simp
lemma prod_2: "prod f {(1::nat)..2} = f 1 * f 2" by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
lemma prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3" by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
subsection \<open>Orthogonality of a matrix\<close>
definition\<^marker>\<open>tag important\<close> "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
lemma orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \ transpose Q ** Q = mat 1" by (metis matrix_left_right_inverse orthogonal_matrix_def)
proposition orthogonal_matrix_mul: fixes A :: "real ^'n^'n" assumes"orthogonal_matrix A""orthogonal_matrix B" shows"orthogonal_matrix(A ** B)" using assms by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
proposition orthogonal_transformation_matrix: fixes f:: "real^'n \ real^'n" shows"orthogonal_transformation f \ linear f \ orthogonal_matrix(matrix f)"
(is"?lhs \ ?rhs") proof - let ?mf = "matrix f" let ?ot = "orthogonal_transformation f" let ?U = "UNIV :: 'n set" have fU: "finite ?U"by simp let ?m1 = "mat 1 :: real ^'n^'n"
{ assume ot: ?ot from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\v w. f v \ f w = v \ w" unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR by blast+
{ fix i j let ?A = "transpose ?mf ** ?mf" have th0: "\b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)" "\b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)" by simp_all from fd[of "axis i 1""axis j 1",
simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul] have"?A$i$j = ?m1 $ i $ j" by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
th0 sum.delta[OF fU] mat_def axis_def)
} thenhave"orthogonal_matrix ?mf" unfolding orthogonal_matrix by vector with lf have ?rhs unfolding linear_def scalar_mult_eq_scaleR by blast
} moreover have ?lhs if"Vector_Spaces.linear (*s) (*s) f" and "orthogonal_matrix ?mf" using that unfolding orthogonal_matrix_def norm_eq orthogonal_transformation by (metis dot_matrix_product dot_matrix_vector_mul linear_matrix_vector_mul_eq matrix_mul_lid matrix_vector_mul(2)) ultimatelyshow ?thesis by (auto simp: linear_def scalar_mult_eq_scaleR) qed
subsection \<open>Finding an Orthogonal Matrix\<close>
text\<open>We can find an orthogonal matrix taking any unit vector to any other.\<close>
lemma orthogonal_matrix_transpose [simp]: "orthogonal_matrix(transpose A) \ orthogonal_matrix A" by (auto simp: orthogonal_matrix_def)
lemma orthogonal_matrix_orthonormal_columns: fixes A :: "real^'n^'n" shows"orthogonal_matrix A \
(\<forall>i. norm(column i A) = 1) \<and>
(\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))" by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
lemma orthogonal_matrix_orthonormal_rows: fixes A :: "real^'n^'n" shows"orthogonal_matrix A \
(\<forall>i. norm(row i A) = 1) \<and>
(\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))" using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
proposition orthogonal_matrix_exists_basis: fixes a :: "real^'n" assumes"norm a = 1" obtains A where"orthogonal_matrix A""A *v (axis k 1) = a" proof - obtain S where"a \ S" "pairwise orthogonal S" and noS: "\x. x \ S \ norm x = 1" and"independent S""card S = CARD('n)""span S = UNIV" using vector_in_orthonormal_basis assms by force thenobtain f0 where"bij_betw f0 (UNIV::'n set) S" by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent) thenobtain f where f: "bij_betw f (UNIV::'n set) S"and a: "a = f k" using bij_swap_iff [of f0 k "inv f0 a"] by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1)) show thesis proof have [simp]: "\i. norm (f i) = 1" using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS) have [simp]: "\i j. i \ j \ orthogonal (f i) (f j)" using\<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close> by (auto simp: pairwise_def bij_betw_def inj_on_def) show"orthogonal_matrix (\ i j. f j $ i)" by (simp add: orthogonal_matrix_orthonormal_columns column_def) show"(\ i j. f j $ i) *v axis k 1 = a" by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong) qed qed
lemma orthogonal_transformation_exists_1: fixes a b :: "real^'n" assumes"norm a = 1""norm b = 1" obtains f where"orthogonal_transformation f""f a = b" proof - obtain k A B where AB: "orthogonal_matrix A""orthogonal_matrix B"and eq: "A *v (axis k 1) = a""B *v (axis k 1) = b" using orthogonal_matrix_exists_basis assms by metis let ?f = "\x. (B ** transpose A) *v x" show thesis proof show"orthogonal_transformation ?f" by (simp add: AB orthogonal_matrix_mul orthogonal_transformation_matrix) next show"?f a = b" using\<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def by (metis eq matrix_mul_rid matrix_vector_mul_assoc) qed qed
proposition orthogonal_transformation_exists: fixes a b :: "real^'n" assumes"norm a = norm b" obtains f where"orthogonal_transformation f""f a = b" proof (cases "a = 0 \ b = 0") case True with assms show ?thesis using that by force next case False thenobtain f where f: "orthogonal_transformation f"and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)" by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"]) show ?thesis using False assms eq f orthogonal_transformation_scaleR that by fastforce qed
subsection \<open>Scaling and isometry\<close>
proposition scaling_linear: fixes f :: "'a::real_inner \ 'a::real_inner" assumes f0: "f 0 = 0" and fd: "\x y. dist (f x) (f y) = c * dist x y" shows"linear f" proof -
{ fix v w have"norm (f x) = c * norm x"for x by (metis dist_0_norm f0 fd) thenhave"f v \ f w = c\<^sup>2 * (v \ w)" unfolding dot_norm_neg dist_norm[symmetric] by (simp add: fd power2_eq_square field_simps)
} thenshow ?thesis unfolding linear_iff vector_eq[where'a="'a"] scalar_mult_eq_scaleR by (simp add: inner_add field_simps) qed
lemma isometry_linear: "f (0::'a::real_inner) = (0::'a) \ \x y. dist(f x) (f y) = dist x y \ linear f" by (rule scaling_linear[where c=1]) simp_all
text\<open>Hence another formulation of orthogonal transformation\<close>
proposition orthogonal_transformation_isometry: "orthogonal_transformation f \ f(0::'a::real_inner) = (0::'a) \ (\x y. dist(f x) (f y) = dist x y)" unfolding orthogonal_transformation by (metis dist_0_norm dist_norm isometry_linear linear_0 linear_diff)
text\<open>Can extend an isometry from unit sphere:\<close>
lemma isometry_sphere_extend: fixes f:: "'a::real_inner \ 'a" assumes f1: "\x. norm x = 1 \ norm (f x) = 1" and fd1: "\x y. \norm x = 1; norm y = 1\ \ dist (f x) (f y) = dist x y" shows"\g. orthogonal_transformation g \ (\x. norm x = 1 \ g x = f x)" proof -
{ fix x y x' y' u v u' v' :: "'a" assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v" "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'" and J: "norm u = 1""norm u' = 1""norm v = 1""norm v' = 1""norm(u' - v') = norm(u - v)" thenhave *: "u \ v = u' \ v' + v' \ u' - v \ u " by (simp add: norm_eq norm_eq_1 inner_add inner_diff) have"norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)" using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps) thenhave"norm(x' - y') = norm(x - y)" using H by metis
} note norm_eq = this let ?g = "\x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)" have thfg: "?g x = f x"if"norm x = 1"for x using that by auto have thd: "dist (?g x) (?g y) = dist x y"for x y proof (cases "x=0 \ y=0") case False show"dist (?g x) (?g y) = dist x y" unfolding dist_norm proof (rule norm_eq) show"x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)" "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1" using False f1 by auto qed (use False in\<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>) qed (auto simp: f1) show ?thesis unfolding orthogonal_transformation_isometry by (rule exI[where x= ?g]) (metis thfg thd) qed
subsection\<open>Induction on matrix row operations\<close>
lemma induct_matrix_row_operations: fixes P :: "real^'n^'n \ bool" assumes zero_row: "\A i. row i A = 0 \ P A" and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" and swap_cols: "\A m n. \P A; m \ n\ \ P(\ i j. A $ i $ Transposition.transpose m n j)" and row_op: "\A m n c. \P A; m \ n\ \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)" shows"P A" proof - have"P A"if"(\i j. \j \ -K; i \ j\ \ A$i$j = 0)" for A K proof - have"finite K" by simp thenshow ?thesis using that proof (induction arbitrary: A rule: finite_induct) case empty with diagonal show ?case by simp next case (insert k K) note insertK = insert have"P A"if kk: "A$k$k \ 0" and 0: "\i j. \j \ - insert k K; i \ j\ \ A$i$j = 0" "\i. \i \ -L; i \ k\ \ A$i$k = 0" for A L proof - have"finite L" by simp thenshow ?thesis using 0 kk proof (induction arbitrary: A rule: finite_induct) case (empty B) show ?case proof (rule insertK) fix i j assume"i \ - K" "j \ i" show"B $ j $ i = 0" using\<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff) qed next case (insert l L B) show ?case proof (cases "k = l") case True with insert show ?thesis by auto next case False let ?C = "\ i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B" have 1: "\j \ - insert k K; i \ j\ \ ?C $ i $ j = 0" for j i by (auto simp: insert.prems(1) row_def) have 2: "?C $ i $ k = 0" if"i \ - L" "i \ k" for i proof (cases "i=l") case True with that insert.prems show ?thesis by (simp add: row_def) next case False with that show ?thesis by (simp add: insert.prems(2) row_def) qed have 3: "?C $ k $ k \ 0" by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>) have PC: "P ?C" using insert.IH [OF 1 2 3] by auto have eqB: "(\ i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B" using\<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def) show ?thesis using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close> by (simp add: cong: if_cong) qed qed qed thenhave nonzero_hyp: "P A" if kk: "A$k$k \ 0" and zeroes: "\i j. j \ - insert k K \ i\j \ A$i$j = 0" for A by (auto simp: intro!: kk zeroes) show ?case proof (cases "row k A = 0") case True with zero_row show ?thesis by auto next case False thenobtain l where l: "A$k$l \ 0" by (auto simp: row_def zero_vec_def vec_eq_iff) show ?thesis proof (cases "k = l") case True with l nonzero_hyp insert.prems show ?thesis by blast next case False have *: "A $ i $ Transposition.transpose k l j = 0"if"j \ k" "j \ K" "i \ j" for i j using False l insert.prems that by (auto simp add: Transposition.transpose_def) have"P (\ i j. (\ i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j)" by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *) moreover have"(\ i j. (\ i j. A $ i $ Transposition.transpose k l j) $ i $ Transposition.transpose k l j) = A" by simp ultimatelyshow ?thesis by simp qed qed qed qed thenshow ?thesis by blast qed
lemma induct_matrix_elementary: fixes P :: "real^'n^'n \ bool" assumes mult: "\A B. \P A; P B\ \ P(A ** B)" and zero_row: "\A i. row i A = 0 \ P A" and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" and swap1: "\m n. m \ n \ P(\ i j. mat 1 $ i $ Transposition.transpose m n j)" and idplus: "\m n c. m \ n \ P(\ i j. if i = m \ j = n then c else of_bool (i = j))" shows"P A" proof - have swap: "P (\ i j. A $ i $ Transposition.transpose m n j)" (is "P ?C") if"P A""m \ n" for A m n proof - have"A ** (\ i j. mat 1 $ i $ Transposition.transpose m n j) = ?C" by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove) thenshow ?thesis using mult swap1 that by metis qed have row: "P (\ i. if i = m then row m A + c *\<^sub>R row n A else row i A)" (is "P ?C") if"P A""m \ n" for A m n c proof - let ?B = "\ i j. if i = m \ j = n then c else of_bool (i = j)" have"?B ** A = ?C" using\<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def by (auto simp: vec_eq_iff if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) thenshow ?thesis by (rule subst) (auto simp: that mult idplus) qed show ?thesis by (rule induct_matrix_row_operations [OF zero_row diagonal swap row]) qed
lemma induct_matrix_elementary_alt: fixes P :: "real^'n^'n \ bool" assumes mult: "\A B. \P A; P B\ \ P(A ** B)" and zero_row: "\A i. row i A = 0 \ P A" and diagonal: "\A. (\i j. i \ j \ A$i$j = 0) \ P A" and swap1: "\m n. m \ n \ P(\ i j. mat 1 $ i $ Transposition.transpose m n j)" and idplus: "\m n. m \ n \ P(\ i j. of_bool (i = m \ j = n \ i = j))" shows"P A" proof - have *: "P (\ i j. if i = m \ j = n then c else of_bool (i = j))" if"m \ n" for m n c proof (cases "c = 0") case True with diagonal show ?thesis by auto next case False thenhave eq: "(\ i j. if i = m \ j = n then c else of_bool (i = j)) =
(\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
(\<chi> i j. if i = j then if j = n then c else 1 else 0)" using\<open>m \<noteq> n\<close> apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\x. y * x" for y] cong: if_cong) apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong) done show ?thesis unfolding eq by (intro mult idplus that) (auto intro: diagonal) qed show ?thesis by (rule induct_matrix_elementary) (auto intro: assms *) qed
lemma matrix_vector_mult_matrix_matrix_mult_compose: "(*v) (A ** B) = (*v) A \ (*v) B" by (auto simp: matrix_vector_mul_assoc)
lemma induct_linear_elementary: fixes f :: "real^'n \ real^'n" assumes"linear f" and comp: "\f g. \linear f; linear g; P f; P g\ \ P(f \ g)" and zeroes: "\f i. \linear f; \x. (f x) $ i = 0\ \ P f" and const: "\c. P(\x. \ i. c i * x$i)" and swap: "\m n::'n. m \ n \ P(\x. \ i. x $ Transposition.transpose m n i)" and idplus: "\m n::'n. m \ n \ P(\x. \ i. if i = m then x$m + x$n else x$i)" shows"P f" proof - have"P ((*v) A)" for A proof (rule induct_matrix_elementary_alt) fix A B assume"P ((*v) A)" and "P ((*v) B)" thenshow"P ((*v) (A ** B))" by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose intro!: comp) next fix A :: "real^'n^'n"and i assume"row i A = 0" with matrix_vector_mul_linear show"P ((*v) A)" by (metis matrix_vector_mul_component matrix_vector_mult_0 row_def
vec_lambda_eta zero_index zeroes) next fix A :: "real^'n^'n" assume 0: "\i j. i \ j \ A $ i $ j = 0" have"A $ i $ i * x $ i = (\j\UNIV. A $ i $ j * x $ j)" for x and i :: "'n" by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i]) thenhave"(\x. \ i. A $ i $ i * x $ i) = ((*v) A)" by (auto simp: 0 matrix_vector_mult_def) thenshow"P ((*v) A)" using const [of "\i. A $ i $ i"] by simp next fix m n :: "'n" assume"m \ n" have eq: "(\j\UNIV. if i = Transposition.transpose m n j then x $ j else 0) =
(\<Sum>j\<in>UNIV. if j = Transposition.transpose m n i then x $ j else 0)" for i and x :: "real^'n" by (rule sum.cong) (auto simp add: swap_id_eq) have"(\x::real^'n. \ i. x $ Transposition.transpose m n i) = ((*v) (\ i j. if i = Transposition.transpose m n j then 1 else 0))" by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\x. x * y" for y] cong: if_cong) with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 $ i $ Transposition.transpose m n j))" by (simp add: mat_def matrix_vector_mult_def) next fix m n :: "'n" assume"m \ n" thenhave"x $ m + x $ n = (\j\UNIV. of_bool (j = n \ m = j) * x $ j)" for x :: "real^'n" by (auto simp: of_bool_def if_distrib [of "\x. x * y" for y] sum.remove cong: if_cong) thenhave"(\x::real^'n. \ i. if i = m then x $ m + x $ n else x $ i) =
((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))" unfolding matrix_vector_mult_def of_bool_def by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong) then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))" using idplus [OF \<open>m \<noteq> n\<close>] by simp qed then show ?thesis by (metis \<open>linear f\<close> matrix_vector_mul(2)) qed
end
¤ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
