new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
authorpaulson <lp15@cam.ac.uk>
Wed Apr 25 15:36:29 2018 +0100 (15 months ago)
changeset 6803820b713cff87a
parent 68032 412fe0623c5d
child 68039 67b39890158c
new material on matricies by Tim Makarios (from Tarskis_Geometry in the AFP)
src/HOL/Analysis/Cartesian_Euclidean_Space.thy
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Tue Apr 24 22:22:25 2018 +0100
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed Apr 25 15:36:29 2018 +0100
     1.3 @@ -1,3 +1,7 @@
     1.4 +(* Title:      HOL/Analysis/Cartesian_Euclidean_Space.thy
     1.5 +   Some material by Tim Makarios and L C Paulson
     1.6 +*)
     1.7 +
     1.8  section \<open>Instantiates the finite Cartesian product of Euclidean spaces as a Euclidean space\<close>
     1.9  
    1.10  theory Cartesian_Euclidean_Space
    1.11 @@ -526,6 +530,12 @@
    1.12  definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))"
    1.13  definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}"
    1.14  definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}"
    1.15 +   
    1.16 +lemma times0_left [simp]: "(0::'a::semiring_1^'n^'m) ** (A::'a ^'p^'n) = 0" 
    1.17 +  by (simp add: matrix_matrix_mult_def zero_vec_def)
    1.18 +
    1.19 +lemma times0_right [simp]: "(A::'a::semiring_1^'n^'m) ** (0::'a ^'p^'n) = 0" 
    1.20 +  by (simp add: matrix_matrix_mult_def zero_vec_def)
    1.21  
    1.22  lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def)
    1.23  lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)"
    1.24 @@ -562,6 +572,16 @@
    1.25    apply simp
    1.26    done
    1.27  
    1.28 +lemma scalar_matrix_assoc:
    1.29 +  fixes A :: "real^'m^'n"
    1.30 +  shows "k *\<^sub>R (A ** B) = (k *\<^sub>R A) ** B"
    1.31 +  by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
    1.32 +
    1.33 +lemma matrix_scalar_ac:
    1.34 +  fixes A :: "real^'m^'n"
    1.35 +  shows "A ** (k *\<^sub>R B) = k *\<^sub>R A ** B"
    1.36 +  by (simp add: matrix_matrix_mult_def sum_distrib_left mult_ac vec_eq_iff)
    1.37 +
    1.38  lemma matrix_vector_mul_lid [simp]: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)"
    1.39    apply (vector matrix_vector_mult_def mat_def)
    1.40    apply (simp add: if_distrib cond_application_beta sum.delta' cong del: if_weak_cong)
    1.41 @@ -615,6 +635,13 @@
    1.42  lemma columns_transpose [simp]: "columns(transpose (A::'a::semiring_1^_^_)) = rows A"
    1.43    by (metis transpose_transpose rows_transpose)
    1.44  
    1.45 +lemma transpose_scalar: "transpose (k *\<^sub>R A) = k *\<^sub>R transpose A"
    1.46 +  unfolding transpose_def
    1.47 +  by (simp add: vec_eq_iff)
    1.48 +
    1.49 +lemma transpose_iff [iff]: "transpose A = transpose B \<longleftrightarrow> A = B"
    1.50 +  by (metis transpose_transpose)
    1.51 +
    1.52  lemma matrix_mult_transpose_dot_column:
    1.53    fixes A :: "real^'n^'n"
    1.54    shows "transpose A ** A = (\<chi> i j. (column i A) \<bullet> (column j A))"
    1.55 @@ -762,6 +789,62 @@
    1.56    shows "inj (( *v) A)"
    1.57    by (metis assms inj_on_inverseI invertible_def matrix_vector_mul_assoc matrix_vector_mul_lid)
    1.58  
    1.59 +lemma scalar_invertible:
    1.60 +  fixes A :: "real^'m^'n"
    1.61 +  assumes "k \<noteq> 0" and "invertible A"
    1.62 +  shows "invertible (k *\<^sub>R A)"
    1.63 +proof -
    1.64 +  obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
    1.65 +    using assms unfolding invertible_def by auto
    1.66 +  with `k \<noteq> 0`
    1.67 +  have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
    1.68 +    by (simp_all add: assms matrix_scalar_ac)
    1.69 +  thus "invertible (k *\<^sub>R A)"
    1.70 +    unfolding invertible_def by auto
    1.71 +qed
    1.72 +
    1.73 +lemma scalar_invertible_iff:
    1.74 +  fixes A :: "real^'m^'n"
    1.75 +  assumes "k \<noteq> 0" and "invertible A"
    1.76 +  shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
    1.77 +  by (simp add: assms scalar_invertible)
    1.78 +
    1.79 +lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
    1.80 +  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
    1.81 +  by simp
    1.82 +
    1.83 +lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
    1.84 +  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
    1.85 +  by simp
    1.86 +
    1.87 +lemma vector_matrix_mul_rid:
    1.88 +  fixes v :: "('a::semiring_1)^'n"
    1.89 +  shows "v v* mat 1 = v"
    1.90 +  by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
    1.91 +
    1.92 +lemma scalar_vector_matrix_assoc:
    1.93 +  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
    1.94 +  shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
    1.95 +  by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
    1.96 +
    1.97 +lemma vector_scalar_matrix_ac:
    1.98 +  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
    1.99 +  shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
   1.100 +proof -
   1.101 +  have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
   1.102 +    unfolding vector_matrix_mult_def
   1.103 +    by (simp add: algebra_simps)
   1.104 +  with scalar_vector_matrix_assoc
   1.105 +  show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
   1.106 +    by auto
   1.107 +qed
   1.108 +
   1.109 +lemma vector_matrix_left_distrib:
   1.110 +  fixes x y :: "real^'n" and A :: "real^'m^'n"
   1.111 +  shows "(x + y) v* A = x v* A + y v* A"
   1.112 +  unfolding vector_matrix_mult_def
   1.113 +  by (simp add: algebra_simps sum.distrib vec_eq_iff)
   1.114 +
   1.115  
   1.116  subsection\<open>Some bounds on components etc. relative to operator norm\<close>
   1.117  
   1.118 @@ -1075,11 +1158,7 @@
   1.119    { fix A A' :: "real ^'n^'n"
   1.120      assume AA': "A ** A' = mat 1"
   1.121      have sA: "surj (( *v) A)"
   1.122 -      unfolding surj_def
   1.123 -      apply clarify
   1.124 -      apply (rule_tac x="(A' *v y)" in exI)
   1.125 -      apply (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid)
   1.126 -      done
   1.127 +      using AA' matrix_right_invertible_surjective by auto
   1.128      from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA]
   1.129      obtain f' :: "real ^'n \<Rightarrow> real ^'n"
   1.130        where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
   1.131 @@ -1095,6 +1174,18 @@
   1.132    then show ?thesis by blast
   1.133  qed
   1.134  
   1.135 +lemma invertible_mult:
   1.136 +  fixes A B :: "real^'n^'n"
   1.137 +  assumes "invertible A" and "invertible B"
   1.138 +  shows "invertible (A ** B)"
   1.139 +  by (metis (no_types, hide_lams) assms invertible_def matrix_left_right_inverse matrix_mul_assoc matrix_mul_lid)
   1.140 +
   1.141 +lemma transpose_invertible:
   1.142 +  fixes A :: "real^'n^'n"
   1.143 +  assumes "invertible A"
   1.144 +  shows "invertible (transpose A)"
   1.145 +  by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
   1.146 +
   1.147  text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
   1.148  
   1.149  definition "rowvector v = (\<chi> i j. (v$j))"