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.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
```