src/HOL/Analysis/Cartesian_Euclidean_Space.thy
changeset 68073 fad29d2a17a5
parent 68072 493b818e8e10
parent 68069 36209dfb981e
child 68074 8d50467f7555
     1.1 --- a/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Wed May 02 13:49:38 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Cartesian_Euclidean_Space.thy	Thu May 03 15:07:14 2018 +0200
     1.3 @@ -1,3 +1,7 @@
     1.4 +(* Title:      HOL/Analysis/Cartesian_Euclidean_Space.thy
     1.5 +   Some material by Jose Divasón, 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 @@ -176,12 +180,10 @@
    1.12  qed
    1.13  
    1.14  lemma matrix_mult_transpose_dot_column:
    1.15 -  fixes A :: "real^'n^'n"
    1.16    shows "transpose A ** A = (\<chi> i j. inner (column i A) (column j A))"
    1.17    by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def column_def inner_vec_def)
    1.18  
    1.19  lemma matrix_mult_transpose_dot_row:
    1.20 -  fixes A :: "real^'n^'n"
    1.21    shows "A ** transpose A = (\<chi> i j. inner (row i A) (row j A))"
    1.22    by (simp add: matrix_matrix_mult_def vec_eq_iff transpose_def row_def inner_vec_def)
    1.23  
    1.24 @@ -215,11 +217,77 @@
    1.25    by (simp add: linear_conv_bounded_linear linear_matrix_vector_mul_eq)
    1.26  
    1.27  lemma
    1.28 -  fixes A :: "real^'n^'m"
    1.29 +  fixes A :: "'a::{euclidean_space,real_algebra_1}^'n^'m"
    1.30    shows matrix_vector_mult_linear_continuous_at [continuous_intros]: "isCont (( *v) A) z"
    1.31      and matrix_vector_mult_linear_continuous_on [continuous_intros]: "continuous_on S (( *v) A)"
    1.32    by (simp_all add: linear_continuous_at linear_continuous_on)
    1.33  
    1.34 +lemma scalar_invertible:
    1.35 +  fixes A :: "('a::real_algebra_1)^'m^'n"
    1.36 +  assumes "k \<noteq> 0" and "invertible A"
    1.37 +  shows "invertible (k *\<^sub>R A)"
    1.38 +proof -
    1.39 +  obtain A' where "A ** A' = mat 1" and "A' ** A = mat 1"
    1.40 +    using assms unfolding invertible_def by auto
    1.41 +  with `k \<noteq> 0`
    1.42 +  have "(k *\<^sub>R A) ** ((1/k) *\<^sub>R A') = mat 1" "((1/k) *\<^sub>R A') ** (k *\<^sub>R A) = mat 1"
    1.43 +    by (simp_all add: assms matrix_scalar_ac)
    1.44 +  thus "invertible (k *\<^sub>R A)"
    1.45 +    unfolding invertible_def by auto
    1.46 +qed
    1.47 +
    1.48 +lemma scalar_invertible_iff:
    1.49 +  fixes A :: "('a::real_algebra_1)^'m^'n"
    1.50 +  assumes "k \<noteq> 0" and "invertible A"
    1.51 +  shows "invertible (k *\<^sub>R A) \<longleftrightarrow> k \<noteq> 0 \<and> invertible A"
    1.52 +  by (simp add: assms scalar_invertible)
    1.53 +
    1.54 +lemma vector_transpose_matrix [simp]: "x v* transpose A = A *v x"
    1.55 +  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
    1.56 +  by simp
    1.57 +
    1.58 +lemma transpose_matrix_vector [simp]: "transpose A *v x = x v* A"
    1.59 +  unfolding transpose_def vector_matrix_mult_def matrix_vector_mult_def
    1.60 +  by simp
    1.61 +
    1.62 +lemma vector_scalar_commute:
    1.63 +  fixes A :: "'a::{field}^'m^'n"
    1.64 +  shows "A *v (c *s x) = c *s (A *v x)"
    1.65 +  by (simp add: vector_scalar_mult_def matrix_vector_mult_def mult_ac sum_distrib_left)
    1.66 +
    1.67 +lemma scalar_vector_matrix_assoc:
    1.68 +  fixes k :: "'a::{field}" and x :: "'a::{field}^'n" and A :: "'a^'m^'n"
    1.69 +  shows "(k *s x) v* A = k *s (x v* A)"
    1.70 +  by (metis transpose_matrix_vector vector_scalar_commute)
    1.71 + 
    1.72 +lemma vector_matrix_mult_0 [simp]: "0 v* A = 0"
    1.73 +  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
    1.74 +
    1.75 +lemma vector_matrix_mult_0_right [simp]: "x v* 0 = 0"
    1.76 +  unfolding vector_matrix_mult_def by (simp add: zero_vec_def)
    1.77 +
    1.78 +lemma vector_matrix_mul_rid [simp]:
    1.79 +  fixes v :: "('a::semiring_1)^'n"
    1.80 +  shows "v v* mat 1 = v"
    1.81 +  by (metis matrix_vector_mul_lid transpose_mat vector_transpose_matrix)
    1.82 +
    1.83 +lemma scaleR_vector_matrix_assoc:
    1.84 +  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
    1.85 +  shows "(k *\<^sub>R x) v* A = k *\<^sub>R (x v* A)"
    1.86 +  by (metis matrix_vector_mult_scaleR transpose_matrix_vector)
    1.87 +
    1.88 +lemma vector_scaleR_matrix_ac:
    1.89 +  fixes k :: real and x :: "real^'n" and A :: "real^'m^'n"
    1.90 +  shows "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
    1.91 +proof -
    1.92 +  have "x v* (k *\<^sub>R A) = (k *\<^sub>R x) v* A"
    1.93 +    unfolding vector_matrix_mult_def
    1.94 +    by (simp add: algebra_simps)
    1.95 +  with scaleR_vector_matrix_assoc
    1.96 +  show "x v* (k *\<^sub>R A) = k *\<^sub>R (x v* A)"
    1.97 +    by auto
    1.98 +qed
    1.99 +
   1.100  
   1.101  subsection\<open>Some bounds on components etc. relative to operator norm\<close>
   1.102  
   1.103 @@ -402,22 +470,18 @@
   1.104    have fU: "finite ?U" by simp
   1.105    have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)"
   1.106      unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
   1.107 -    apply (subst eq_commute)
   1.108 -    apply rule
   1.109 -    done
   1.110 +    by (simp add: eq_commute)
   1.111    have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
   1.112    { assume h: ?lhs
   1.113      { fix x:: "'a ^'n"
   1.114        from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
   1.115          where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast
   1.116        have "x \<in> vec.span (columns A)"
   1.117 -        unfolding y[symmetric]
   1.118 -        apply (rule vec.span_sum)
   1.119 -        apply (rule vec.span_scale)
   1.120 -        apply (rule vec.span_base)
   1.121 -        unfolding columns_def
   1.122 -        apply blast
   1.123 -        done
   1.124 +        unfolding y[symmetric] scalar_mult_eq_scaleR
   1.125 +      proof (rule span_sum [OF span_mul])
   1.126 +        show "column i A \<in> span (columns A)" for i
   1.127 +          using columns_def span_inc by auto
   1.128 +      qed
   1.129      }
   1.130      then have ?rhs unfolding rhseq by blast }
   1.131    moreover
   1.132 @@ -428,17 +492,18 @@
   1.133          unfolding h by blast
   1.134        then have "?P y"
   1.135        proof (induction rule: vec.span_induct_alt)
   1.136 -        show "\<exists>x::'a ^ 'm. sum (\<lambda>i. (x$i) *s column i A) ?U = 0"
   1.137 -          by (rule exI[where x=0], simp)
   1.138 +        case base
   1.139 +        then show ?case
   1.140 +          by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
   1.141        next
   1.142 -        fix c y1 y2
   1.143 -        assume y1: "y1 \<in> columns A" and y2: "?P y2"
   1.144 +        case (step c y1 y2)
   1.145 +        then obtain i where i: "i \<in> ?U" "y1 = column i A"
   1.146          from y1 obtain i where i: "i \<in> ?U" "y1 = column i A"
   1.147            unfolding columns_def by blast
   1.148 -        from y2 obtain x:: "'a ^'m" where
   1.149 -          x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast
   1.150 +        obtain x:: "real ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2"
   1.151 +          using step by blast
   1.152          let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m"
   1.153 -        show "?P (c*s y1 + y2)"
   1.154 +        show ?case
   1.155          proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
   1.156            fix j
   1.157            have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.158 @@ -446,9 +511,7 @@
   1.159              using i(1) by (simp add: field_simps)
   1.160            have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j)
   1.161                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"
   1.162 -            apply (rule sum.cong[OF refl])
   1.163 -            using th apply blast
   1.164 -            done
   1.165 +            by (rule sum.cong[OF refl]) (use th in blast)
   1.166            also have "\<dots> = sum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.167              by (simp add: sum.distrib)
   1.168            also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U"
   1.169 @@ -1038,8 +1101,8 @@
   1.170      obtain B where "independent B" "span(rows A) \<subseteq> span B"
   1.171                and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
   1.172        using basis_exists [of "span(rows A)"] by blast
   1.173 -    then have eq: "span B = span(rows A)"
   1.174 -      using span_subspace subspace_span by blast
   1.175 +    with span_subspace have eq: "span B = span(rows A)"
   1.176 +      by auto
   1.177      then have inj: "inj_on (( *v) A) (span B)"
   1.178        by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
   1.179      then have ind: "independent (( *v) A ` B)"
   1.180 @@ -1208,15 +1271,13 @@
   1.181  
   1.182  definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
   1.183  
   1.184 -lemma vector_1: "(vector[x]) $1 = x"
   1.185 +lemma vector_1 [simp]: "(vector[x]) $1 = x"
   1.186    unfolding vector_def by simp
   1.187  
   1.188 -lemma vector_2:
   1.189 - "(vector[x,y]) $1 = x"
   1.190 - "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
   1.191 +lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)"
   1.192    unfolding vector_def by simp_all
   1.193  
   1.194 -lemma vector_3:
   1.195 +lemma vector_3 [simp]:
   1.196   "(vector [x,y,z] ::('a::zero)^3)$1 = x"
   1.197   "(vector [x,y,z] ::('a::zero)^3)$2 = y"
   1.198   "(vector [x,y,z] ::('a::zero)^3)$3 = z"
   1.199 @@ -1247,7 +1308,7 @@
   1.200    done
   1.201  
   1.202  lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)"
   1.203 -  apply (rule bounded_linearI[where K=1])
   1.204 +  apply (rule bounded_linear_intro[where K=1])
   1.205    using component_le_norm_cart[of _ k] unfolding real_norm_def by auto
   1.206  
   1.207  lemma interval_split_cart:
   1.208 @@ -1263,4 +1324,4 @@
   1.209    bounded_linear.uniform_limit[OF bounded_linear_vec_nth]
   1.210    bounded_linear.uniform_limit[OF bounded_linear_component_cart]
   1.211  
   1.212 -end
   1.213 \ No newline at end of file
   1.214 +end