src/HOL/Analysis/Cartesian_Space.thy
 author wenzelm Mon Mar 25 17:21:26 2019 +0100 (3 months ago) changeset 69981 3dced198b9ec parent 69918 eddcc7c726f3 child 70136 f03a01a18c6e permissions -rw-r--r--
more strict AFP properties;
```     1 (*  Title:      HOL/Analysis/Cartesian_Space.thy
```
```     2     Author:     Amine Chaieb, University of Cambridge
```
```     3     Author:     Jose Divasón <jose.divasonm at unirioja.es>
```
```     4     Author:     Jesús Aransay <jesus-maria.aransay at unirioja.es>
```
```     5     Author:     Johannes Hölzl, VU Amsterdam
```
```     6     Author:     Fabian Immler, TUM
```
```     7 *)
```
```     8
```
```     9 section "Linear Algebra on Finite Cartesian Products"
```
```    10
```
```    11 theory Cartesian_Space
```
```    12   imports
```
```    13     Finite_Cartesian_Product Linear_Algebra
```
```    14 begin
```
```    15
```
```    16 subsection%unimportant \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> (*much of the following
```
```    17 is really basic linear algebra, check for overlap? rename subsection?  *)
```
```    18
```
```    19 definition "cart_basis = {axis i 1 | i. i\<in>UNIV}"
```
```    20
```
```    21 lemma finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def
```
```    22   using finite_Atleast_Atmost_nat by fastforce
```
```    23
```
```    24 lemma card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)"
```
```    25   unfolding cart_basis_def Setcompr_eq_image
```
```    26   by (rule card_image) (auto simp: inj_on_def axis_eq_axis)
```
```    27
```
```    28 interpretation vec: vector_space "(*s) "
```
```    29   by unfold_locales (vector algebra_simps)+
```
```    30
```
```    31 lemma independent_cart_basis:
```
```    32   "vec.independent (cart_basis)"
```
```    33 proof (rule vec.independent_if_scalars_zero)
```
```    34   show "finite (cart_basis)" using finite_cart_basis .
```
```    35   fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec"
```
```    36   assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis"
```
```    37   obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto
```
```    38   have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x \$ i)) = 0"
```
```    39   proof (rule sum.neutral, rule ballI)
```
```    40     fix xa assume xa: "xa \<in> cart_basis - {x}"
```
```    41     obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i"
```
```    42       using xa x unfolding cart_basis_def by auto
```
```    43     have "xa \$ i = 0" unfolding a axis_def using a_not_i by auto
```
```    44     thus "f xa * xa \$ i = 0" by simp
```
```    45   qed
```
```    46   have "0 = (\<Sum>x\<in>cart_basis. f x *s x) \$ i" using eq_0 by simp
```
```    47   also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) \$ i)" unfolding sum_component ..
```
```    48   also have "... = (\<Sum>x\<in>cart_basis. f x * (x \$ i))" unfolding vector_smult_component ..
```
```    49   also have "... = f x * (x \$ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x \$ i))"
```
```    50     by (rule sum.remove[OF finite_cart_basis x_in])
```
```    51   also have "... =  f x * (x \$ i)" unfolding sum_eq_0 by simp
```
```    52   also have "... = f x" unfolding x axis_def by auto
```
```    53   finally show "f x = 0" ..
```
```    54 qed
```
```    55
```
```    56 lemma span_cart_basis:
```
```    57   "vec.span (cart_basis) = UNIV"
```
```    58 proof (auto)
```
```    59   fix x::"('a, 'b) vec"
```
```    60   let ?f="\<lambda>v. x \$ (THE i. v = axis i 1)"
```
```    61   show "x \<in> vec.span (cart_basis)"
```
```    62     apply (unfold vec.span_finite[OF finite_cart_basis])
```
```    63     apply (rule image_eqI[of _ _ ?f])
```
```    64      apply (subst  vec_eq_iff)
```
```    65      apply clarify
```
```    66   proof -
```
```    67     fix i::'b
```
```    68     let ?w = "axis i (1::'a)"
```
```    69     have the_eq_i: "(THE a. ?w = axis a 1) = i"
```
```    70       by (rule the_equality, auto simp: axis_eq_axis)
```
```    71     have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x \$ (THE i. v = axis i 1) * v \$ i) = 0"
```
```    72     proof (rule sum.neutral, rule ballI)
```
```    73       fix xa::"('a, 'b) vec"
```
```    74       assume xa: "xa \<in> cart_basis - {?w}"
```
```    75       obtain j where j: "xa = axis j 1" and i_not_j: "i \<noteq> j" using xa unfolding cart_basis_def by auto
```
```    76       have the_eq_j: "(THE i. xa = axis i 1) = j"
```
```    77       proof (rule the_equality)
```
```    78         show "xa = axis j 1" using j .
```
```    79         show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one)
```
```    80       qed
```
```    81       show "x \$ (THE i. xa = axis i 1) * xa \$ i = 0"
```
```    82         apply (subst (2) j)
```
```    83         unfolding the_eq_j unfolding axis_def using i_not_j by simp
```
```    84     qed
```
```    85     have "(\<Sum>v\<in>cart_basis. x \$ (THE i. v = axis i 1) *s v) \$ i =
```
```    86   (\<Sum>v\<in>cart_basis. (x \$ (THE i. v = axis i 1) *s v) \$ i)" unfolding sum_component ..
```
```    87     also have "... = (\<Sum>v\<in>cart_basis. x \$ (THE i. v = axis i 1) * v \$ i)"
```
```    88       unfolding vector_smult_component ..
```
```    89     also have "... = x \$ (THE a. ?w = axis a 1) * ?w \$ i + (\<Sum>v\<in>(cart_basis) - {?w}. x \$ (THE i. v = axis i 1) * v \$ i)"
```
```    90       by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def)
```
```    91     also have "... = x \$ (THE a. ?w = axis a 1) * ?w \$ i" unfolding sum_eq_0 by simp
```
```    92     also have "... = x \$ i" unfolding the_eq_i unfolding axis_def by auto
```
```    93     finally show "x \$ i = (\<Sum>v\<in>cart_basis. x \$ (THE i. v = axis i 1) *s v) \$ i" by simp
```
```    94   qed simp
```
```    95 qed
```
```    96
```
```    97 (*Some interpretations:*)
```
```    98 interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis"
```
```    99   by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis)
```
```   100
```
```   101 lemma matrix_vector_mul_linear_gen[intro, simp]:
```
```   102   "Vector_Spaces.linear (*s) (*s) ((*v) A)"
```
```   103   by unfold_locales
```
```   104     (vector matrix_vector_mult_def sum.distrib algebra_simps)+
```
```   105
```
```   106 lemma span_vec_eq: "vec.span X = span X"
```
```   107   and dim_vec_eq: "vec.dim X = dim X"
```
```   108   and dependent_vec_eq: "vec.dependent X = dependent X"
```
```   109   and subspace_vec_eq: "vec.subspace X = subspace X"
```
```   110   for X::"(real^'n) set"
```
```   111   unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def
```
```   112   by (auto simp: scalar_mult_eq_scaleR)
```
```   113
```
```   114 lemma linear_componentwise:
```
```   115   fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n"
```
```   116   assumes lf: "Vector_Spaces.linear (*s) (*s) f"
```
```   117   shows "(f x)\$j = sum (\<lambda>i. (x\$i) * (f (axis i 1)\$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs")
```
```   118 proof -
```
```   119   interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f
```
```   120     using lf .
```
```   121   let ?M = "(UNIV :: 'm set)"
```
```   122   let ?N = "(UNIV :: 'n set)"
```
```   123   have fM: "finite ?M" by simp
```
```   124   have "?rhs = (sum (\<lambda>i. (x\$i) *s (f (axis i 1))) ?M)\$j"
```
```   125     unfolding sum_component by simp
```
```   126   then show ?thesis
```
```   127     unfolding lf.sum[symmetric] lf.scale[symmetric]
```
```   128     unfolding basis_expansion by auto
```
```   129 qed
```
```   130
```
```   131 interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A"
```
```   132   using matrix_vector_mul_linear_gen.
```
```   133
```
```   134 interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis ..
```
```   135
```
```   136 lemma matrix_works:
```
```   137   assumes lf: "Vector_Spaces.linear (*s) (*s) f"
```
```   138   shows "matrix f *v x = f (x::'a::field ^ 'n)"
```
```   139   apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute)
```
```   140   apply clarify
```
```   141   apply (rule linear_componentwise[OF lf, symmetric])
```
```   142   done
```
```   143
```
```   144 lemma matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A"
```
```   145   by (simp add: matrix_eq matrix_works)
```
```   146
```
```   147 lemma matrix_compose_gen:
```
```   148   assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)"
```
```   149     and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)"
```
```   150   shows "matrix (g o f) = matrix g ** matrix f"
```
```   151   using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]]
```
```   152   by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def)
```
```   153
```
```   154 lemma matrix_compose:
```
```   155   assumes "linear (f::real^'n \<Rightarrow> real^'m)" "linear (g::real^'m \<Rightarrow> real^_)"
```
```   156   shows "matrix (g o f) = matrix g ** matrix f"
```
```   157   using matrix_compose_gen[of f g] assms
```
```   158   by (simp add: linear_def scalar_mult_eq_scaleR)
```
```   159
```
```   160 lemma left_invertible_transpose:
```
```   161   "(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)"
```
```   162   by (metis matrix_transpose_mul transpose_mat transpose_transpose)
```
```   163
```
```   164 lemma right_invertible_transpose:
```
```   165   "(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)"
```
```   166   by (metis matrix_transpose_mul transpose_mat transpose_transpose)
```
```   167
```
```   168 lemma linear_matrix_vector_mul_eq:
```
```   169   "Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)"
```
```   170   by (simp add: scalar_mult_eq_scaleR linear_def)
```
```   171
```
```   172 lemma matrix_vector_mul[simp]:
```
```   173   "Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g"
```
```   174   "linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
```
```   175   "bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f"
```
```   176   for f :: "real^'n \<Rightarrow> real ^'m"
```
```   177   by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear)
```
```   178
```
```   179 lemma matrix_left_invertible_injective:
```
```   180   fixes A :: "'a::field^'n^'m"
```
```   181   shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)"
```
```   182 proof safe
```
```   183   fix B
```
```   184   assume B: "B ** A = mat 1"
```
```   185   show "inj ((*v) A)"
```
```   186     unfolding inj_on_def
```
```   187       by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid)
```
```   188 next
```
```   189   assume "inj ((*v) A)"
```
```   190   from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this]
```
```   191   obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id"
```
```   192     by blast
```
```   193   have "matrix g ** A = mat 1"
```
```   194     by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen
```
```   195         matrix_eq matrix_id_mat_1 matrix_vector_mul(1))
```
```   196   then show "\<exists>B. B ** A = mat 1"
```
```   197     by metis
```
```   198 qed
```
```   199
```
```   200 lemma matrix_left_invertible_ker:
```
```   201   "(\<exists>B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)"
```
```   202   unfolding matrix_left_invertible_injective
```
```   203   using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A]
```
```   204   by (simp add: inj_on_def)
```
```   205
```
```   206 lemma matrix_right_invertible_surjective:
```
```   207   "(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)"
```
```   208 proof -
```
```   209   { fix B :: "'a ^'m^'n"
```
```   210     assume AB: "A ** B = mat 1"
```
```   211     { fix x :: "'a ^ 'm"
```
```   212       have "A *v (B *v x) = x"
```
```   213         by (simp add: matrix_vector_mul_assoc AB) }
```
```   214     hence "surj ((*v) A)" unfolding surj_def by metis }
```
```   215   moreover
```
```   216   { assume sf: "surj ((*v) A)"
```
```   217     from vec.linear_surjective_right_inverse[OF _ this]
```
```   218     obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id"
```
```   219       by blast
```
```   220
```
```   221     have "A ** (matrix g) = mat 1"
```
```   222       unfolding matrix_eq  matrix_vector_mul_lid
```
```   223         matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)]
```
```   224       using g(2) unfolding o_def fun_eq_iff id_def
```
```   225       .
```
```   226     hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast
```
```   227   }
```
```   228   ultimately show ?thesis unfolding surj_def by blast
```
```   229 qed
```
```   230
```
```   231 lemma matrix_left_invertible_independent_columns:
```
```   232   fixes A :: "'a::{field}^'n^'m"
```
```   233   shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow>
```
```   234       (\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
```
```   235     (is "?lhs \<longleftrightarrow> ?rhs")
```
```   236 proof -
```
```   237   let ?U = "UNIV :: 'n set"
```
```   238   { assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0"
```
```   239     { fix c i
```
```   240       assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U"
```
```   241       let ?x = "\<chi> i. c i"
```
```   242       have th0:"A *v ?x = 0"
```
```   243         using c
```
```   244         by (vector matrix_mult_sum)
```
```   245       from k[rule_format, OF th0] i
```
```   246       have "c i = 0" by (vector vec_eq_iff)}
```
```   247     hence ?rhs by blast }
```
```   248   moreover
```
```   249   { assume H: ?rhs
```
```   250     { fix x assume x: "A *v x = 0"
```
```   251       let ?c = "\<lambda>i. ((x\$i ):: 'a)"
```
```   252       from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x]
```
```   253       have "x = 0" by vector }
```
```   254   }
```
```   255   ultimately show ?thesis unfolding matrix_left_invertible_ker by auto
```
```   256 qed
```
```   257
```
```   258 lemma matrix_right_invertible_independent_rows:
```
```   259   fixes A :: "'a::{field}^'n^'m"
```
```   260   shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow>
```
```   261     (\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))"
```
```   262   unfolding left_invertible_transpose[symmetric]
```
```   263     matrix_left_invertible_independent_columns
```
```   264   by (simp add:)
```
```   265
```
```   266 lemma matrix_right_invertible_span_columns:
```
```   267   "(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow>
```
```   268     vec.span (columns A) = UNIV" (is "?lhs = ?rhs")
```
```   269 proof -
```
```   270   let ?U = "UNIV :: 'm set"
```
```   271   have fU: "finite ?U" by simp
```
```   272   have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x\$i) *s column i A) ?U = y)"
```
```   273     unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def
```
```   274     by (simp add: eq_commute)
```
```   275   have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast
```
```   276   { assume h: ?lhs
```
```   277     { fix x:: "'a ^'n"
```
```   278       from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m"
```
```   279         where y: "sum (\<lambda>i. (y\$i) *s column i A) ?U = x" by blast
```
```   280       have "x \<in> vec.span (columns A)"
```
```   281         unfolding y[symmetric] scalar_mult_eq_scaleR
```
```   282       proof (rule vec.span_sum [OF vec.span_scale])
```
```   283         show "column i A \<in> vec.span (columns A)" for i
```
```   284           using columns_def vec.span_superset by auto
```
```   285       qed
```
```   286     }
```
```   287     then have ?rhs unfolding rhseq by blast }
```
```   288   moreover
```
```   289   { assume h:?rhs
```
```   290     let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x\$i) *s column i A) ?U = y"
```
```   291     { fix y
```
```   292       have "y \<in> vec.span (columns A)"
```
```   293         unfolding h by blast
```
```   294       then have "?P y"
```
```   295       proof (induction rule: vec.span_induct_alt)
```
```   296         case base
```
```   297         then show ?case
```
```   298           by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right)
```
```   299       next
```
```   300         case (step c y1 y2)
```
```   301         from step obtain i where i: "i \<in> ?U" "y1 = column i A"
```
```   302           unfolding columns_def by blast
```
```   303         obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x\$i) *s column i A) ?U = y2"
```
```   304           using step by blast
```
```   305         let ?x = "(\<chi> j. if j = i then c + (x\$i) else (x\$j))::'a^'m"
```
```   306         show ?case
```
```   307         proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong)
```
```   308           fix j
```
```   309           have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   310               else (x\$xa) * ((column xa A\$j))) = (if xa = i then c * ((column i A)\$j) else 0) + ((x\$xa) * ((column xa A)\$j))"
```
```   311             using i(1) by (simp add: field_simps)
```
```   312           have "sum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   313               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"
```
```   314             by (rule sum.cong[OF refl]) (use th in blast)
```
```   315           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"
```
```   316             by (simp add: sum.distrib)
```
```   317           also have "\<dots> = c * ((column i A)\$j) + sum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U"
```
```   318             unfolding sum.delta[OF fU]
```
```   319             using i(1) by simp
```
```   320           finally show "sum (\<lambda>xa. if xa = i then (c + (x\$i)) * ((column xa A)\$j)
```
```   321             else (x\$xa) * ((column xa A\$j))) ?U = c * ((column i A)\$j) + sum (\<lambda>xa. ((x\$xa) * ((column xa A)\$j))) ?U" .
```
```   322         qed
```
```   323       qed
```
```   324     }
```
```   325     then have ?lhs unfolding lhseq ..
```
```   326   }
```
```   327   ultimately show ?thesis by blast
```
```   328 qed
```
```   329
```
```   330 lemma matrix_left_invertible_span_rows_gen:
```
```   331   "(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV"
```
```   332   unfolding right_invertible_transpose[symmetric]
```
```   333   unfolding columns_transpose[symmetric]
```
```   334   unfolding matrix_right_invertible_span_columns
```
```   335   ..
```
```   336
```
```   337 lemma matrix_left_invertible_span_rows:
```
```   338   "(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV"
```
```   339   using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq)
```
```   340
```
```   341 lemma matrix_left_right_inverse:
```
```   342   fixes A A' :: "'a::{field}^'n^'n"
```
```   343   shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1"
```
```   344 proof -
```
```   345   { fix A A' :: "'a ^'n^'n"
```
```   346     assume AA': "A ** A' = mat 1"
```
```   347     have sA: "surj ((*v) A)"
```
```   348       using AA' matrix_right_invertible_surjective by auto
```
```   349     from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA]
```
```   350     obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n"
```
```   351       where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast
```
```   352     have th: "matrix f' ** A = mat 1"
```
```   353       by (simp add: matrix_eq matrix_works[OF f'(1)]
```
```   354           matrix_vector_mul_assoc[symmetric] f'(2)[rule_format])
```
```   355     hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp
```
```   356     hence "matrix f' = A'"
```
```   357       by (simp add: matrix_mul_assoc[symmetric] AA')
```
```   358     hence "matrix f' ** A = A' ** A" by simp
```
```   359     hence "A' ** A = mat 1" by (simp add: th)
```
```   360   }
```
```   361   then show ?thesis by blast
```
```   362 qed
```
```   363
```
```   364 lemma invertible_left_inverse:
```
```   365   fixes A :: "'a::{field}^'n^'n"
```
```   366   shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). B ** A = mat 1)"
```
```   367   by (metis invertible_def matrix_left_right_inverse)
```
```   368
```
```   369 lemma invertible_right_inverse:
```
```   370   fixes A :: "'a::{field}^'n^'n"
```
```   371   shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). A** B = mat 1)"
```
```   372   by (metis invertible_def matrix_left_right_inverse)
```
```   373
```
```   374 lemma invertible_mult:
```
```   375   assumes inv_A: "invertible A"
```
```   376   and inv_B: "invertible B"
```
```   377   shows "invertible (A**B)"
```
```   378 proof -
```
```   379   obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1"
```
```   380     using inv_A unfolding invertible_def by blast
```
```   381   obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1"
```
```   382     using inv_B unfolding invertible_def by blast
```
```   383   show ?thesis
```
```   384   proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI)
```
```   385     have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))"
```
```   386       using matrix_mul_assoc[of A B "(B' ** A')", symmetric] .
```
```   387     also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] ..
```
```   388     also have "... = A ** (mat 1 ** A')" unfolding BB' ..
```
```   389     also have "... = A ** A'" unfolding matrix_mul_lid ..
```
```   390     also have "... = mat 1" unfolding AA' ..
```
```   391     finally show "A ** B ** (B' ** A') = mat (1::'a)" .
```
```   392     have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] .
```
```   393     also have "... =  B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] ..
```
```   394     also have "... =  B' ** (mat 1 ** B)" unfolding A'A ..
```
```   395     also have "... = B' ** B"  unfolding matrix_mul_lid ..
```
```   396     also have "... = mat 1" unfolding B'B ..
```
```   397     finally show "B' ** A' ** (A ** B) = mat 1" .
```
```   398   qed
```
```   399 qed
```
```   400
```
```   401 lemma transpose_invertible:
```
```   402   fixes A :: "real^'n^'n"
```
```   403   assumes "invertible A"
```
```   404   shows "invertible (transpose A)"
```
```   405   by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose)
```
```   406
```
```   407 lemma vector_matrix_mul_assoc:
```
```   408   fixes v :: "('a::comm_semiring_1)^'n"
```
```   409   shows "(v v* M) v* N = v v* (M ** N)"
```
```   410 proof -
```
```   411   from matrix_vector_mul_assoc
```
```   412   have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast
```
```   413   thus "(v v* M) v* N = v v* (M ** N)"
```
```   414     by (simp add: matrix_transpose_mul [symmetric])
```
```   415 qed
```
```   416
```
```   417 lemma matrix_scaleR_vector_ac:
```
```   418   fixes A :: "real^('m::finite)^'n"
```
```   419   shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v"
```
```   420   by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix)
```
```   421
```
```   422 lemma scaleR_matrix_vector_assoc:
```
```   423   fixes A :: "real^('m::finite)^'n"
```
```   424   shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v"
```
```   425   by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR)
```
```   426
```
```   427 (*Finally, some interesting theorems and interpretations that don't appear in any file of the
```
```   428   library.*)
```
```   429
```
```   430 locale linear_first_finite_dimensional_vector_space =
```
```   431   l?: Vector_Spaces.linear scaleB scaleC f +
```
```   432   B?: finite_dimensional_vector_space scaleB BasisB
```
```   433   for scaleB :: "('a::field => 'b::ab_group_add => 'b)" (infixr "*b" 75)
```
```   434   and scaleC :: "('a => 'c::ab_group_add => 'c)" (infixr "*c" 75)
```
```   435   and BasisB :: "('b set)"
```
```   436   and f :: "('b=>'c)"
```
```   437
```
```   438 lemma vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)"
```
```   439 proof -
```
```   440   let ?f="\<lambda>i::'n. axis i (1::'a)"
```
```   441   have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)"
```
```   442     unfolding vec.dim_UNIV ..
```
```   443   also have "... = card ({i. i\<in> UNIV}::('n) set)"
```
```   444     proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto)
```
```   445       show "inj (\<lambda>i::'n. axis i (1::'a))"  by (simp add: inj_on_def axis_eq_axis)
```
```   446       fix i::'n
```
```   447       show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto
```
```   448       fix x::"'a^'n"
```
```   449       assume "x \<in> cart_basis"
```
```   450       thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto
```
```   451     qed
```
```   452   also have "... = CARD('n)" by auto
```
```   453   finally show ?thesis .
```
```   454 qed
```
```   455
```
```   456 interpretation vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a"
```
```   457 by unfold_locales (simp_all add: algebra_simps)
```
```   458
```
```   459 lemmas [simp del] = vector_space_over_itself.scale_scale
```
```   460
```
```   461 interpretation vector_space_over_itself: finite_dimensional_vector_space
```
```   462   "(*) :: 'a::field => 'a => 'a" "{1}"
```
```   463   by unfold_locales (auto simp: vector_space_over_itself.span_singleton)
```
```   464
```
```   465 lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1"
```
```   466   unfolding vector_space_over_itself.dimension_def by simp
```
```   467
```
```   468
```
```   469 lemma dim_subset_UNIV_cart_gen:
```
```   470   fixes S :: "('a::field^'n) set"
```
```   471   shows "vec.dim S \<le> CARD('n)"
```
```   472   by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card)
```
```   473
```
```   474 lemma dim_subset_UNIV_cart:
```
```   475   fixes S :: "(real^'n) set"
```
```   476   shows "dim S \<le> CARD('n)"
```
```   477   using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq)
```
```   478
```
```   479 text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close>
```
```   480
```
```   481 lemma matrix_mult_dot: "A *v x = (\<chi> i. inner (A\$i) x)"
```
```   482   by (simp add: matrix_vector_mult_def inner_vec_def)
```
```   483
```
```   484 lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)"
```
```   485   apply (rule adjoint_unique)
```
```   486   apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def
```
```   487     sum_distrib_right sum_distrib_left)
```
```   488   apply (subst sum.swap)
```
```   489   apply (simp add:  ac_simps)
```
```   490   done
```
```   491
```
```   492 lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)"
```
```   493   shows "matrix(adjoint f) = transpose(matrix f)"
```
```   494 proof -
```
```   495   have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))"
```
```   496     by (simp add: lf)
```
```   497   also have "\<dots> = transpose(matrix f)"
```
```   498     unfolding adjoint_matrix matrix_of_matrix_vector_mul
```
```   499     apply rule
```
```   500     done
```
```   501   finally show ?thesis .
```
```   502 qed
```
```   503
```
```   504
```
```   505 subsection\<open> Rank of a matrix\<close>
```
```   506
```
```   507 text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close>
```
```   508
```
```   509 lemma matrix_vector_mult_in_columnspace_gen:
```
```   510   fixes A :: "'a::field^'n^'m"
```
```   511   shows "(A *v x) \<in> vec.span(columns A)"
```
```   512   apply (simp add: matrix_vector_column columns_def transpose_def column_def)
```
```   513   apply (intro vec.span_sum vec.span_scale)
```
```   514   apply (force intro: vec.span_base)
```
```   515   done
```
```   516
```
```   517 lemma matrix_vector_mult_in_columnspace:
```
```   518   fixes A :: "real^'n^'m"
```
```   519   shows "(A *v x) \<in> span(columns A)"
```
```   520   using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq)
```
```   521
```
```   522 lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}"
```
```   523   by (simp add: subspace_def orthogonal_clauses)
```
```   524
```
```   525 lemma orthogonal_nullspace_rowspace:
```
```   526   fixes A :: "real^'n^'m"
```
```   527   assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)"
```
```   528   shows "orthogonal x y"
```
```   529   using y
```
```   530 proof (induction rule: span_induct)
```
```   531   case base
```
```   532   then show ?case
```
```   533     by (simp add: subspace_orthogonal_to_vector)
```
```   534 next
```
```   535   case (step v)
```
```   536   then obtain i where "v = row i A"
```
```   537     by (auto simp: rows_def)
```
```   538   with 0 show ?case
```
```   539     unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def
```
```   540     by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index)
```
```   541 qed
```
```   542
```
```   543 lemma nullspace_inter_rowspace:
```
```   544   fixes A :: "real^'n^'m"
```
```   545   shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0"
```
```   546   using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right
```
```   547   by blast
```
```   548
```
```   549 lemma matrix_vector_mul_injective_on_rowspace:
```
```   550   fixes A :: "real^'n^'m"
```
```   551   shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y"
```
```   552   using nullspace_inter_rowspace [of A "x-y"]
```
```   553   by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff)
```
```   554
```
```   555 definition%important rank :: "'a::field^'n^'m=>nat"
```
```   556   where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)"
```
```   557
```
```   558 lemma row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m"
```
```   559   by (auto simp: row_rank_def_gen dim_vec_eq)
```
```   560
```
```   561 lemma dim_rows_le_dim_columns:
```
```   562   fixes A :: "real^'n^'m"
```
```   563   shows "dim(rows A) \<le> dim(columns A)"
```
```   564 proof -
```
```   565   have "dim (span (rows A)) \<le> dim (span (columns A))"
```
```   566   proof -
```
```   567     obtain B where "independent B" "span(rows A) \<subseteq> span B"
```
```   568               and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))"
```
```   569       using basis_exists [of "span(rows A)"] by metis
```
```   570     with span_subspace have eq: "span B = span(rows A)"
```
```   571       by auto
```
```   572     then have inj: "inj_on ((*v) A) (span B)"
```
```   573       by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace)
```
```   574     then have ind: "independent ((*v) A ` B)"
```
```   575       by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>])
```
```   576     have "dim (span (rows A)) \<le> card ((*v) A ` B)"
```
```   577       unfolding B(2)[symmetric]
```
```   578       using inj
```
```   579       by (auto simp: card_image inj_on_subset span_superset)
```
```   580     also have "\<dots> \<le> dim (span (columns A))"
```
```   581       using _ ind
```
```   582       by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace)
```
```   583     finally show ?thesis .
```
```   584   qed
```
```   585   then show ?thesis
```
```   586     by (simp add: dim_span)
```
```   587 qed
```
```   588
```
```   589 lemma column_rank_def:
```
```   590   fixes A :: "real^'n^'m"
```
```   591   shows "rank A = dim(columns A)"
```
```   592   unfolding row_rank_def
```
```   593   by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose)
```
```   594
```
```   595 lemma rank_transpose:
```
```   596   fixes A :: "real^'n^'m"
```
```   597   shows "rank(transpose A) = rank A"
```
```   598   by (metis column_rank_def row_rank_def rows_transpose)
```
```   599
```
```   600 lemma matrix_vector_mult_basis:
```
```   601   fixes A :: "real^'n^'m"
```
```   602   shows "A *v (axis k 1) = column k A"
```
```   603   by (simp add: cart_eq_inner_axis column_def matrix_mult_dot)
```
```   604
```
```   605 lemma columns_image_basis:
```
```   606   fixes A :: "real^'n^'m"
```
```   607   shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))"
```
```   608   by (force simp: columns_def matrix_vector_mult_basis [symmetric])
```
```   609
```
```   610 lemma rank_dim_range:
```
```   611   fixes A :: "real^'n^'m"
```
```   612   shows "rank A = dim(range (\<lambda>x. A *v x))"
```
```   613   unfolding column_rank_def
```
```   614 proof (rule span_eq_dim)
```
```   615   have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r")
```
```   616     by (simp add: columns_image_basis image_subsetI span_mono)
```
```   617   then show "?l = ?r"
```
```   618     by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace
```
```   619         span_eq span_span)
```
```   620 qed
```
```   621
```
```   622 lemma rank_bound:
```
```   623   fixes A :: "real^'n^'m"
```
```   624   shows "rank A \<le> min CARD('m) (CARD('n))"
```
```   625   by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff
```
```   626       column_rank_def row_rank_def)
```
```   627
```
```   628 lemma full_rank_injective:
```
```   629   fixes A :: "real^'n^'m"
```
```   630   shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)"
```
```   631   by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def
```
```   632       dim_eq_full [symmetric] card_cart_basis vec.dimension_def)
```
```   633
```
```   634 lemma full_rank_surjective:
```
```   635   fixes A :: "real^'n^'m"
```
```   636   shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)"
```
```   637   by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric]
```
```   638                 matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose)
```
```   639
```
```   640 lemma rank_I: "rank(mat 1::real^'n^'n) = CARD('n)"
```
```   641   by (simp add: full_rank_injective inj_on_def)
```
```   642
```
```   643 lemma less_rank_noninjective:
```
```   644   fixes A :: "real^'n^'m"
```
```   645   shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)"
```
```   646 using less_le rank_bound by (auto simp: full_rank_injective [symmetric])
```
```   647
```
```   648 lemma matrix_nonfull_linear_equations_eq:
```
```   649   fixes A :: "real^'n^'m"
```
```   650   shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)"
```
```   651   by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker)
```
```   652
```
```   653 lemma rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0"
```
```   654   for A :: "real^'n^'m"
```
```   655   by (auto simp: rank_dim_range matrix_eq)
```
```   656
```
```   657 lemma rank_mul_le_right:
```
```   658   fixes A :: "real^'n^'m" and B :: "real^'p^'n"
```
```   659   shows "rank(A ** B) \<le> rank B"
```
```   660 proof -
```
```   661   have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))"
```
```   662     by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc)
```
```   663   also have "\<dots> \<le> rank B"
```
```   664     by (simp add: rank_dim_range dim_image_le)
```
```   665   finally show ?thesis .
```
```   666 qed
```
```   667
```
```   668 lemma rank_mul_le_left:
```
```   669   fixes A :: "real^'n^'m" and B :: "real^'p^'n"
```
```   670   shows "rank(A ** B) \<le> rank A"
```
```   671   by (metis matrix_transpose_mul rank_mul_le_right rank_transpose)
```
```   672
```
```   673
```
```   674 subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3/4\<close>\<close>
```
```   675
```
```   676 lemma exhaust_2:
```
```   677   fixes x :: 2
```
```   678   shows "x = 1 \<or> x = 2"
```
```   679 proof (induct x)
```
```   680   case (of_int z)
```
```   681   then have "0 \<le> z" and "z < 2" by simp_all
```
```   682   then have "z = 0 | z = 1" by arith
```
```   683   then show ?case by auto
```
```   684 qed
```
```   685
```
```   686 lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2"
```
```   687   by (metis exhaust_2)
```
```   688
```
```   689 lemma exhaust_3:
```
```   690   fixes x :: 3
```
```   691   shows "x = 1 \<or> x = 2 \<or> x = 3"
```
```   692 proof (induct x)
```
```   693   case (of_int z)
```
```   694   then have "0 \<le> z" and "z < 3" by simp_all
```
```   695   then have "z = 0 \<or> z = 1 \<or> z = 2" by arith
```
```   696   then show ?case by auto
```
```   697 qed
```
```   698
```
```   699 lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3"
```
```   700   by (metis exhaust_3)
```
```   701
```
```   702 lemma exhaust_4:
```
```   703   fixes x :: 4
```
```   704   shows "x = 1 \<or> x = 2 \<or> x = 3 \<or> x = 4"
```
```   705 proof (induct x)
```
```   706   case (of_int z)
```
```   707   then have "0 \<le> z" and "z < 4" by simp_all
```
```   708   then have "z = 0 \<or> z = 1 \<or> z = 2 \<or> z = 3" by arith
```
```   709   then show ?case by auto
```
```   710 qed
```
```   711
```
```   712 lemma forall_4: "(\<forall>i::4. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3 \<and> P 4"
```
```   713   by (metis exhaust_4)
```
```   714
```
```   715 lemma UNIV_1 [simp]: "UNIV = {1::1}"
```
```   716   by (auto simp add: num1_eq_iff)
```
```   717
```
```   718 lemma UNIV_2: "UNIV = {1::2, 2::2}"
```
```   719   using exhaust_2 by auto
```
```   720
```
```   721 lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}"
```
```   722   using exhaust_3 by auto
```
```   723
```
```   724 lemma UNIV_4: "UNIV = {1::4, 2::4, 3::4, 4::4}"
```
```   725   using exhaust_4 by auto
```
```   726
```
```   727 lemma sum_1: "sum f (UNIV::1 set) = f 1"
```
```   728   unfolding UNIV_1 by simp
```
```   729
```
```   730 lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2"
```
```   731   unfolding UNIV_2 by simp
```
```   732
```
```   733 lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3"
```
```   734   unfolding UNIV_3 by (simp add: ac_simps)
```
```   735
```
```   736 lemma sum_4: "sum f (UNIV::4 set) = f 1 + f 2 + f 3 + f 4"
```
```   737   unfolding UNIV_4 by (simp add: ac_simps)
```
```   738
```
```   739 subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close>
```
```   740
```
```   741 lemma vector_one: "(x::'a ^1) = (\<chi> i. (x\$1))"
```
```   742   by (simp add: vec_eq_iff)
```
```   743
```
```   744 lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))"
```
```   745   apply auto
```
```   746   apply (erule_tac x= "x\$1" in allE)
```
```   747   apply (simp only: vector_one[symmetric])
```
```   748   done
```
```   749
```
```   750 lemma norm_vector_1: "norm (x :: _^1) = norm (x\$1)"
```
```   751   by (simp add: norm_vec_def)
```
```   752
```
```   753 lemma dist_vector_1:
```
```   754   fixes x :: "'a::real_normed_vector^1"
```
```   755   shows "dist x y = dist (x\$1) (y\$1)"
```
```   756   by (simp add: dist_norm norm_vector_1)
```
```   757
```
```   758 lemma norm_real: "norm(x::real ^ 1) = \<bar>x\$1\<bar>"
```
```   759   by (simp add: norm_vector_1)
```
```   760
```
```   761 lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x\$1) - (y\$1)\<bar>"
```
```   762   by (auto simp add: norm_real dist_norm)
```
```   763
```
```   764
```
```   765 subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close>
```
```   766
```
```   767 lemma vector_one_nth [simp]:
```
```   768   fixes x :: "'a^1" shows "vec (x \$ 1) = x"
```
```   769   by (metis vec_def vector_one)
```
```   770
```
```   771 lemma tendsto_at_within_vector_1:
```
```   772   fixes S :: "'a :: metric_space set"
```
```   773   assumes "(f \<longlongrightarrow> fx) (at x within S)"
```
```   774   shows "((\<lambda>y::'a^1. \<chi> i. f (y \$ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)"
```
```   775 proof (rule topological_tendstoI)
```
```   776   fix T :: "('a^1) set"
```
```   777   assume "open T" "vec fx \<in> T"
```
```   778   have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x \$ 1) ` T"
```
```   779     using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce
```
```   780   then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x \$ 1)) \<in> T"
```
```   781     unfolding eventually_at dist_norm [symmetric]
```
```   782     by (rule ex_forward)
```
```   783        (use \<open>open T\<close> in
```
```   784          \<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>)
```
```   785 qed
```
```   786
```
```   787 lemma has_derivative_vector_1:
```
```   788   assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)"
```
```   789   shows "((\<lambda>x. vec (g (x \$ 1))) has_derivative (*\<^sub>R) (g' a))
```
```   790          (at ((vec a)::real^1) within vec ` S)"
```
```   791     using der_g
```
```   792     apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1)
```
```   793     apply (drule tendsto_at_within_vector_1, vector)
```
```   794     apply (auto simp: algebra_simps eventually_at tendsto_def)
```
```   795     done
```
```   796
```
```   797
```
```   798 subsection%unimportant\<open>Explicit vector construction from lists\<close>
```
```   799
```
```   800 definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)"
```
```   801
```
```   802 lemma vector_1 [simp]: "(vector[x]) \$1 = x"
```
```   803   unfolding vector_def by simp
```
```   804
```
```   805 lemma vector_2 [simp]: "(vector[x,y]) \$1 = x" "(vector[x,y] :: 'a^2)\$2 = (y::'a::zero)"
```
```   806   unfolding vector_def by simp_all
```
```   807
```
```   808 lemma vector_3 [simp]:
```
```   809  "(vector [x,y,z] ::('a::zero)^3)\$1 = x"
```
```   810  "(vector [x,y,z] ::('a::zero)^3)\$2 = y"
```
```   811  "(vector [x,y,z] ::('a::zero)^3)\$3 = z"
```
```   812   unfolding vector_def by simp_all
```
```   813
```
```   814 lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))"
```
```   815   by (metis vector_1 vector_one)
```
```   816
```
```   817 lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))"
```
```   818   apply auto
```
```   819   apply (erule_tac x="v\$1" in allE)
```
```   820   apply (erule_tac x="v\$2" in allE)
```
```   821   apply (subgoal_tac "vector [v\$1, v\$2] = v")
```
```   822   apply simp
```
```   823   apply (vector vector_def)
```
```   824   apply (simp add: forall_2)
```
```   825   done
```
```   826
```
```   827 lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))"
```
```   828   apply auto
```
```   829   apply (erule_tac x="v\$1" in allE)
```
```   830   apply (erule_tac x="v\$2" in allE)
```
```   831   apply (erule_tac x="v\$3" in allE)
```
```   832   apply (subgoal_tac "vector [v\$1, v\$2, v\$3] = v")
```
```   833   apply simp
```
```   834   apply (vector vector_def)
```
```   835   apply (simp add: forall_3)
```
```   836   done
```
```   837
```
```   838 subsection%unimportant \<open>lambda skolemization on cartesian products\<close>
```
```   839
```
```   840 lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow>
```
```   841    (\<exists>x::'a ^ 'n. \<forall>i. P i (x \$ i))" (is "?lhs \<longleftrightarrow> ?rhs")
```
```   842 proof -
```
```   843   let ?S = "(UNIV :: 'n set)"
```
```   844   { assume H: "?rhs"
```
```   845     then have ?lhs by auto }
```
```   846   moreover
```
```   847   { assume H: "?lhs"
```
```   848     then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis
```
```   849     let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n"
```
```   850     { fix i
```
```   851       from f have "P i (f i)" by metis
```
```   852       then have "P i (?x \$ i)" by auto
```
```   853     }
```
```   854     hence "\<forall>i. P i (?x\$i)" by metis
```
```   855     hence ?rhs by metis }
```
```   856   ultimately show ?thesis by metis
```
```   857 qed
```
```   858
```
```   859
```
```   860 text \<open>The same result in terms of square matrices.\<close>
```
```   861
```
```   862
```
```   863 text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close>
```
```   864
```
```   865 definition "rowvector v = (\<chi> i j. (v\$j))"
```
```   866
```
```   867 definition "columnvector v = (\<chi> i j. (v\$i))"
```
```   868
```
```   869 lemma transpose_columnvector: "transpose(columnvector v) = rowvector v"
```
```   870   by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff)
```
```   871
```
```   872 lemma transpose_rowvector: "transpose(rowvector v) = columnvector v"
```
```   873   by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff)
```
```   874
```
```   875 lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v"
```
```   876   by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def)
```
```   877
```
```   878 lemma dot_matrix_product:
```
```   879   "(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))\$1)\$1"
```
```   880   by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def)
```
```   881
```
```   882 lemma dot_matrix_vector_mul:
```
```   883   fixes A B :: "real ^'n ^'n" and x y :: "real ^'n"
```
```   884   shows "(A *v x) \<bullet> (B *v y) =
```
```   885       (((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))\$1)\$1"
```
```   886   unfolding dot_matrix_product transpose_columnvector[symmetric]
```
```   887     dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc ..
```
```   888
```
```   889
```
```   890 lemma dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x\$i = 0} = card d"
```
```   891   (is "vec.dim ?A = _")
```
```   892 proof (rule vec.dim_unique)
```
```   893   let ?B = "((\<lambda>x. axis x 1) ` d)"
```
```   894   have subset_basis: "?B \<subseteq> cart_basis"
```
```   895     by (auto simp: cart_basis_def)
```
```   896   show "?B \<subseteq> ?A"
```
```   897     by (auto simp: axis_def)
```
```   898   show "vec.independent ((\<lambda>x. axis x 1) ` d)"
```
```   899     using subset_basis
```
```   900     by (rule vec.independent_mono[OF vec.independent_Basis])
```
```   901   have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x \$ i = 0" for x::"'a^'n"
```
```   902   proof -
```
```   903     have "finite ?B"
```
```   904       using subset_basis finite_cart_basis
```
```   905       by (rule finite_subset)
```
```   906     have "x = (\<Sum>i\<in>UNIV. x \$ i *s axis i 1)"
```
```   907       by (rule basis_expansion[symmetric])
```
```   908     also have "\<dots> = (\<Sum>i\<in>d. (x \$ i) *s axis i 1)"
```
```   909       by (rule sum.mono_neutral_cong_right) (auto simp: that)
```
```   910     also have "\<dots> \<in> vec.span ?B"
```
```   911       by (simp add: vec.span_sum vec.span_clauses)
```
```   912     finally show "x \<in> vec.span ?B" .
```
```   913   qed
```
```   914   then show "?A \<subseteq> vec.span ?B" by auto
```
```   915 qed (simp add: card_image inj_on_def axis_eq_axis)
```
```   916
```
```   917 lemma affinity_inverses:
```
```   918   assumes m0: "m \<noteq> (0::'a::field)"
```
```   919   shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id"
```
```   920   "(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id"
```
```   921   using m0
```
```   922   by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff)
```
```   923
```
```   924 lemma vector_affinity_eq:
```
```   925   assumes m0: "(m::'a::field) \<noteq> 0"
```
```   926   shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)"
```
```   927 proof
```
```   928   assume h: "m *s x + c = y"
```
```   929   hence "m *s x = y - c" by (simp add: field_simps)
```
```   930   hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp
```
```   931   then show "x = inverse m *s y + - (inverse m *s c)"
```
```   932     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
```
```   933 next
```
```   934   assume h: "x = inverse m *s y + - (inverse m *s c)"
```
```   935   show "m *s x + c = y" unfolding h
```
```   936     using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib)
```
```   937 qed
```
```   938
```
```   939 lemma vector_eq_affinity:
```
```   940     "(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)"
```
```   941   using vector_affinity_eq[where m=m and x=x and y=y and c=c]
```
```   942   by metis
```
```   943
```
```   944 lemma vector_cart:
```
```   945   fixes f :: "real^'n \<Rightarrow> real"
```
```   946   shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)"
```
```   947   unfolding euclidean_eq_iff[where 'a="real^'n"]
```
```   948   by simp (simp add: Basis_vec_def inner_axis)
```
```   949
```
```   950 lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)"
```
```   951   by (rule vector_cart)
```
```   952
```
```   953 subsection%unimportant \<open>Explicit formulas for low dimensions\<close>
```
```   954
```
```   955 lemma  prod_neutral_const: "prod f {(1::nat)..1} = f 1"
```
```   956   by simp
```
```   957
```
```   958 lemma  prod_2: "prod f {(1::nat)..2} = f 1 * f 2"
```
```   959   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
```
```   960
```
```   961 lemma  prod_3: "prod f {(1::nat)..3} = f 1 * f 2 * f 3"
```
```   962   by (simp add: eval_nat_numeral atLeastAtMostSuc_conv mult.commute)
```
```   963
```
```   964
```
```   965 subsection  \<open>Orthogonality of a matrix\<close>
```
```   966
```
```   967 definition%important  "orthogonal_matrix (Q::'a::semiring_1^'n^'n) \<longleftrightarrow>
```
```   968   transpose Q ** Q = mat 1 \<and> Q ** transpose Q = mat 1"
```
```   969
```
```   970 lemma  orthogonal_matrix: "orthogonal_matrix (Q:: real ^'n^'n) \<longleftrightarrow> transpose Q ** Q = mat 1"
```
```   971   by (metis matrix_left_right_inverse orthogonal_matrix_def)
```
```   972
```
```   973 lemma  orthogonal_matrix_id: "orthogonal_matrix (mat 1 :: _^'n^'n)"
```
```   974   by (simp add: orthogonal_matrix_def)
```
```   975
```
```   976 proposition  orthogonal_matrix_mul:
```
```   977   fixes A :: "real ^'n^'n"
```
```   978   assumes  "orthogonal_matrix A" "orthogonal_matrix B"
```
```   979   shows "orthogonal_matrix(A ** B)"
```
```   980   using assms
```
```   981   by (simp add: orthogonal_matrix matrix_transpose_mul matrix_left_right_inverse matrix_mul_assoc)
```
```   982
```
```   983 proposition  orthogonal_transformation_matrix:
```
```   984   fixes f:: "real^'n \<Rightarrow> real^'n"
```
```   985   shows "orthogonal_transformation f \<longleftrightarrow> linear f \<and> orthogonal_matrix(matrix f)"
```
```   986   (is "?lhs \<longleftrightarrow> ?rhs")
```
```   987 proof -
```
```   988   let ?mf = "matrix f"
```
```   989   let ?ot = "orthogonal_transformation f"
```
```   990   let ?U = "UNIV :: 'n set"
```
```   991   have fU: "finite ?U" by simp
```
```   992   let ?m1 = "mat 1 :: real ^'n^'n"
```
```   993   {
```
```   994     assume ot: ?ot
```
```   995     from ot have lf: "Vector_Spaces.linear (*s) (*s) f" and fd: "\<And>v w. f v \<bullet> f w = v \<bullet> w"
```
```   996       unfolding orthogonal_transformation_def orthogonal_matrix linear_def scalar_mult_eq_scaleR
```
```   997       by blast+
```
```   998     {
```
```   999       fix i j
```
```  1000       let ?A = "transpose ?mf ** ?mf"
```
```  1001       have th0: "\<And>b (x::'a::comm_ring_1). (if b then 1 else 0)*x = (if b then x else 0)"
```
```  1002         "\<And>b (x::'a::comm_ring_1). x*(if b then 1 else 0) = (if b then x else 0)"
```
```  1003         by simp_all
```
```  1004       from fd[of "axis i 1" "axis j 1",
```
```  1005         simplified matrix_works[OF lf, symmetric] dot_matrix_vector_mul]
```
```  1006       have "?A\$i\$j = ?m1 \$ i \$ j"
```
```  1007         by (simp add: inner_vec_def matrix_matrix_mult_def columnvector_def rowvector_def
```
```  1008             th0 sum.delta[OF fU] mat_def axis_def)
```
```  1009     }
```
```  1010     then have "orthogonal_matrix ?mf"
```
```  1011       unfolding orthogonal_matrix
```
```  1012       by vector
```
```  1013     with lf have ?rhs
```
```  1014       unfolding linear_def scalar_mult_eq_scaleR
```
```  1015       by blast
```
```  1016   }
```
```  1017   moreover
```
```  1018   {
```
```  1019     assume lf: "Vector_Spaces.linear (*s) (*s) f" and om: "orthogonal_matrix ?mf"
```
```  1020     from lf om have ?lhs
```
```  1021       unfolding orthogonal_matrix_def norm_eq orthogonal_transformation
```
```  1022       apply (simp only: matrix_works[OF lf, symmetric] dot_matrix_vector_mul)
```
```  1023       apply (simp add: dot_matrix_product linear_def scalar_mult_eq_scaleR)
```
```  1024       done
```
```  1025   }
```
```  1026   ultimately show ?thesis
```
```  1027     by (auto simp: linear_def scalar_mult_eq_scaleR)
```
```  1028 qed
```
```  1029
```
```  1030
```
```  1031 subsection \<open> We can find an orthogonal matrix taking any unit vector to any other\<close>
```
```  1032
```
```  1033 lemma  orthogonal_matrix_transpose [simp]:
```
```  1034      "orthogonal_matrix(transpose A) \<longleftrightarrow> orthogonal_matrix A"
```
```  1035   by (auto simp: orthogonal_matrix_def)
```
```  1036
```
```  1037 lemma  orthogonal_matrix_orthonormal_columns:
```
```  1038   fixes A :: "real^'n^'n"
```
```  1039   shows "orthogonal_matrix A \<longleftrightarrow>
```
```  1040           (\<forall>i. norm(column i A) = 1) \<and>
```
```  1041           (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (column i A) (column j A))"
```
```  1042   by (auto simp: orthogonal_matrix matrix_mult_transpose_dot_column vec_eq_iff mat_def norm_eq_1 orthogonal_def)
```
```  1043
```
```  1044 lemma  orthogonal_matrix_orthonormal_rows:
```
```  1045   fixes A :: "real^'n^'n"
```
```  1046   shows "orthogonal_matrix A \<longleftrightarrow>
```
```  1047           (\<forall>i. norm(row i A) = 1) \<and>
```
```  1048           (\<forall>i j. i \<noteq> j \<longrightarrow> orthogonal (row i A) (row j A))"
```
```  1049   using orthogonal_matrix_orthonormal_columns [of "transpose A"] by simp
```
```  1050
```
```  1051 proposition  orthogonal_matrix_exists_basis:
```
```  1052   fixes a :: "real^'n"
```
```  1053   assumes "norm a = 1"
```
```  1054   obtains A where "orthogonal_matrix A" "A *v (axis k 1) = a"
```
```  1055 proof -
```
```  1056   obtain S where "a \<in> S" "pairwise orthogonal S" and noS: "\<And>x. x \<in> S \<Longrightarrow> norm x = 1"
```
```  1057    and "independent S" "card S = CARD('n)" "span S = UNIV"
```
```  1058     using vector_in_orthonormal_basis assms by force
```
```  1059   then obtain f0 where "bij_betw f0 (UNIV::'n set) S"
```
```  1060     by (metis finite_class.finite_UNIV finite_same_card_bij finiteI_independent)
```
```  1061   then obtain f where f: "bij_betw f (UNIV::'n set) S" and a: "a = f k"
```
```  1062     using bij_swap_iff [of k "inv f0 a" f0]
```
```  1063     by (metis UNIV_I \<open>a \<in> S\<close> bij_betw_inv_into_right bij_betw_swap_iff swap_apply(1))
```
```  1064   show thesis
```
```  1065   proof
```
```  1066     have [simp]: "\<And>i. norm (f i) = 1"
```
```  1067       using bij_betwE [OF \<open>bij_betw f UNIV S\<close>] by (blast intro: noS)
```
```  1068     have [simp]: "\<And>i j. i \<noteq> j \<Longrightarrow> orthogonal (f i) (f j)"
```
```  1069       using \<open>pairwise orthogonal S\<close> \<open>bij_betw f UNIV S\<close>
```
```  1070       by (auto simp: pairwise_def bij_betw_def inj_on_def)
```
```  1071     show "orthogonal_matrix (\<chi> i j. f j \$ i)"
```
```  1072       by (simp add: orthogonal_matrix_orthonormal_columns column_def)
```
```  1073     show "(\<chi> i j. f j \$ i) *v axis k 1 = a"
```
```  1074       by (simp add: matrix_vector_mult_def axis_def a if_distrib cong: if_cong)
```
```  1075   qed
```
```  1076 qed
```
```  1077
```
```  1078 lemma  orthogonal_transformation_exists_1:
```
```  1079   fixes a b :: "real^'n"
```
```  1080   assumes "norm a = 1" "norm b = 1"
```
```  1081   obtains f where "orthogonal_transformation f" "f a = b"
```
```  1082 proof -
```
```  1083   obtain k::'n where True
```
```  1084     by simp
```
```  1085   obtain A B where AB: "orthogonal_matrix A" "orthogonal_matrix B" and eq: "A *v (axis k 1) = a" "B *v (axis k 1) = b"
```
```  1086     using orthogonal_matrix_exists_basis assms by metis
```
```  1087   let ?f = "\<lambda>x. (B ** transpose A) *v x"
```
```  1088   show thesis
```
```  1089   proof
```
```  1090     show "orthogonal_transformation ?f"
```
```  1091       by (subst orthogonal_transformation_matrix)
```
```  1092         (auto simp: AB orthogonal_matrix_mul)
```
```  1093   next
```
```  1094     show "?f a = b"
```
```  1095       using \<open>orthogonal_matrix A\<close> unfolding orthogonal_matrix_def
```
```  1096       by (metis eq matrix_mul_rid matrix_vector_mul_assoc)
```
```  1097   qed
```
```  1098 qed
```
```  1099
```
```  1100 proposition  orthogonal_transformation_exists:
```
```  1101   fixes a b :: "real^'n"
```
```  1102   assumes "norm a = norm b"
```
```  1103   obtains f where "orthogonal_transformation f" "f a = b"
```
```  1104 proof (cases "a = 0 \<or> b = 0")
```
```  1105   case True
```
```  1106   with assms show ?thesis
```
```  1107     using that by force
```
```  1108 next
```
```  1109   case False
```
```  1110   then obtain f where f: "orthogonal_transformation f" and eq: "f (a /\<^sub>R norm a) = (b /\<^sub>R norm b)"
```
```  1111     by (auto intro: orthogonal_transformation_exists_1 [of "a /\<^sub>R norm a" "b /\<^sub>R norm b"])
```
```  1112   show ?thesis
```
```  1113   proof
```
```  1114     interpret linear f
```
```  1115       using f by (simp add: orthogonal_transformation_linear)
```
```  1116     have "f a /\<^sub>R norm a = f (a /\<^sub>R norm a)"
```
```  1117       by (simp add: scale)
```
```  1118     also have "\<dots> = b /\<^sub>R norm a"
```
```  1119       by (simp add: eq assms [symmetric])
```
```  1120     finally show "f a = b"
```
```  1121       using False by auto
```
```  1122   qed (use f in auto)
```
```  1123 qed
```
```  1124
```
```  1125
```
```  1126 subsection  \<open>Linearity of scaling, and hence isometry, that preserves origin\<close>
```
```  1127
```
```  1128 lemma  scaling_linear:
```
```  1129   fixes f :: "'a::real_inner \<Rightarrow> 'a::real_inner"
```
```  1130   assumes f0: "f 0 = 0"
```
```  1131     and fd: "\<forall>x y. dist (f x) (f y) = c * dist x y"
```
```  1132   shows "linear f"
```
```  1133 proof -
```
```  1134   {
```
```  1135     fix v w
```
```  1136     have "norm (f x) = c * norm x" for x
```
```  1137       by (metis dist_0_norm f0 fd)
```
```  1138     then have "f v \<bullet> f w = c\<^sup>2 * (v \<bullet> w)"
```
```  1139       unfolding dot_norm_neg dist_norm[symmetric]
```
```  1140       by (simp add: fd power2_eq_square field_simps)
```
```  1141   }
```
```  1142   then show ?thesis
```
```  1143     unfolding linear_iff vector_eq[where 'a="'a"] scalar_mult_eq_scaleR
```
```  1144     by (simp add: inner_add field_simps)
```
```  1145 qed
```
```  1146
```
```  1147 lemma  isometry_linear:
```
```  1148   "f (0::'a::real_inner) = (0::'a) \<Longrightarrow> \<forall>x y. dist(f x) (f y) = dist x y \<Longrightarrow> linear f"
```
```  1149   by (rule scaling_linear[where c=1]) simp_all
```
```  1150
```
```  1151 text \<open>Hence another formulation of orthogonal transformation\<close>
```
```  1152
```
```  1153 proposition  orthogonal_transformation_isometry:
```
```  1154   "orthogonal_transformation f \<longleftrightarrow> f(0::'a::real_inner) = (0::'a) \<and> (\<forall>x y. dist(f x) (f y) = dist x y)"
```
```  1155   unfolding orthogonal_transformation
```
```  1156   apply (auto simp: linear_0 isometry_linear)
```
```  1157    apply (metis (no_types, hide_lams) dist_norm linear_diff)
```
```  1158   by (metis dist_0_norm)
```
```  1159
```
```  1160
```
```  1161 subsection  \<open>Can extend an isometry from unit sphere\<close>
```
```  1162
```
```  1163 lemma  isometry_sphere_extend:
```
```  1164   fixes f:: "'a::real_inner \<Rightarrow> 'a"
```
```  1165   assumes f1: "\<And>x. norm x = 1 \<Longrightarrow> norm (f x) = 1"
```
```  1166     and fd1: "\<And>x y. \<lbrakk>norm x = 1; norm y = 1\<rbrakk> \<Longrightarrow> dist (f x) (f y) = dist x y"
```
```  1167   shows "\<exists>g. orthogonal_transformation g \<and> (\<forall>x. norm x = 1 \<longrightarrow> g x = f x)"
```
```  1168 proof -
```
```  1169   {
```
```  1170     fix x y x' y' u v u' v' :: "'a"
```
```  1171     assume H: "x = norm x *\<^sub>R u" "y = norm y *\<^sub>R v"
```
```  1172               "x' = norm x *\<^sub>R u'" "y' = norm y *\<^sub>R v'"
```
```  1173       and J: "norm u = 1" "norm u' = 1" "norm v = 1" "norm v' = 1" "norm(u' - v') = norm(u - v)"
```
```  1174     then have *: "u \<bullet> v = u' \<bullet> v' + v' \<bullet> u' - v \<bullet> u "
```
```  1175       by (simp add: norm_eq norm_eq_1 inner_add inner_diff)
```
```  1176     have "norm (norm x *\<^sub>R u' - norm y *\<^sub>R v') = norm (norm x *\<^sub>R u - norm y *\<^sub>R v)"
```
```  1177       using J by (simp add: norm_eq norm_eq_1 inner_diff * field_simps)
```
```  1178     then have "norm(x' - y') = norm(x - y)"
```
```  1179       using H by metis
```
```  1180   }
```
```  1181   note norm_eq = this
```
```  1182   let ?g = "\<lambda>x. if x = 0 then 0 else norm x *\<^sub>R f (x /\<^sub>R norm x)"
```
```  1183   have thfg: "?g x = f x" if "norm x = 1" for x
```
```  1184     using that by auto
```
```  1185   have thd: "dist (?g x) (?g y) = dist x y" for x y
```
```  1186   proof (cases "x=0 \<or> y=0")
```
```  1187     case False
```
```  1188     show "dist (?g x) (?g y) = dist x y"
```
```  1189       unfolding dist_norm
```
```  1190     proof (rule norm_eq)
```
```  1191       show "x = norm x *\<^sub>R (x /\<^sub>R norm x)" "y = norm y *\<^sub>R (y /\<^sub>R norm y)"
```
```  1192            "norm (f (x /\<^sub>R norm x)) = 1" "norm (f (y /\<^sub>R norm y)) = 1"
```
```  1193         using False f1 by auto
```
```  1194     qed (use False in \<open>auto simp: field_simps intro: f1 fd1[unfolded dist_norm]\<close>)
```
```  1195   qed (auto simp: f1)
```
```  1196   show ?thesis
```
```  1197     unfolding orthogonal_transformation_isometry
```
```  1198     by (rule exI[where x= ?g]) (metis thfg thd)
```
```  1199 qed
```
```  1200
```
```  1201 subsection\<open>Induction on matrix row operations\<close>
```
```  1202
```
```  1203 lemma induct_matrix_row_operations:
```
```  1204   fixes P :: "real^'n^'n \<Rightarrow> bool"
```
```  1205   assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
```
```  1206     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A\$i\$j = 0) \<Longrightarrow> P A"
```
```  1207     and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A \$ i \$ Fun.swap m n id j)"
```
```  1208     and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
```
```  1209                    \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
```
```  1210   shows "P A"
```
```  1211 proof -
```
```  1212   have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K;  i \<noteq> j\<rbrakk> \<Longrightarrow> A\$i\$j = 0)" for A K
```
```  1213   proof -
```
```  1214     have "finite K"
```
```  1215       by simp
```
```  1216     then show ?thesis using that
```
```  1217     proof (induction arbitrary: A rule: finite_induct)
```
```  1218       case empty
```
```  1219       with diagonal show ?case
```
```  1220         by simp
```
```  1221     next
```
```  1222       case (insert k K)
```
```  1223       note insertK = insert
```
```  1224       have "P A" if kk: "A\$k\$k \<noteq> 0"
```
```  1225         and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A\$i\$j = 0"
```
```  1226                "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A\$i\$k = 0" for A L
```
```  1227       proof -
```
```  1228         have "finite L"
```
```  1229           by simp
```
```  1230         then show ?thesis using 0 kk
```
```  1231         proof (induction arbitrary: A rule: finite_induct)
```
```  1232           case (empty B)
```
```  1233           show ?case
```
```  1234           proof (rule insertK)
```
```  1235             fix i j
```
```  1236             assume "i \<in> - K" "j \<noteq> i"
```
```  1237             show "B \$ j \$ i = 0"
```
```  1238               using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty
```
```  1239               by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff)
```
```  1240           qed
```
```  1241         next
```
```  1242           case (insert l L B)
```
```  1243           show ?case
```
```  1244           proof (cases "k = l")
```
```  1245             case True
```
```  1246             with insert show ?thesis
```
```  1247               by auto
```
```  1248           next
```
```  1249             case False
```
```  1250             let ?C = "\<chi> i. if i = l then row l B - (B \$ l \$ k / B \$ k \$ k) *\<^sub>R row k B else row i B"
```
```  1251             have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C \$ i \$ j = 0" for j i
```
```  1252               by (auto simp: insert.prems(1) row_def)
```
```  1253             have 2: "?C \$ i \$ k = 0"
```
```  1254               if "i \<in> - L" "i \<noteq> k" for i
```
```  1255             proof (cases "i=l")
```
```  1256               case True
```
```  1257               with that insert.prems show ?thesis
```
```  1258                 by (simp add: row_def)
```
```  1259             next
```
```  1260               case False
```
```  1261               with that show ?thesis
```
```  1262                 by (simp add: insert.prems(2) row_def)
```
```  1263             qed
```
```  1264             have 3: "?C \$ k \$ k \<noteq> 0"
```
```  1265               by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>)
```
```  1266             have PC: "P ?C"
```
```  1267               using insert.IH [OF 1 2 3] by auto
```
```  1268             have eqB: "(\<chi> i. if i = l then row l ?C + (B \$ l \$ k / B \$ k \$ k) *\<^sub>R row k ?C else row i ?C) = B"
```
```  1269               using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def)
```
```  1270             show ?thesis
```
```  1271               using row_op [OF PC, of l k, where c = "B\$l\$k / B\$k\$k"] eqB \<open>k \<noteq> l\<close>
```
```  1272               by (simp add: cong: if_cong)
```
```  1273           qed
```
```  1274         qed
```
```  1275       qed
```
```  1276       then have nonzero_hyp: "P A"
```
```  1277         if kk: "A\$k\$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A\$i\$j = 0" for A
```
```  1278         by (auto simp: intro!: kk zeroes)
```
```  1279       show ?case
```
```  1280       proof (cases "row k A = 0")
```
```  1281         case True
```
```  1282         with zero_row show ?thesis by auto
```
```  1283       next
```
```  1284         case False
```
```  1285         then obtain l where l: "A\$k\$l \<noteq> 0"
```
```  1286           by (auto simp: row_def zero_vec_def vec_eq_iff)
```
```  1287         show ?thesis
```
```  1288         proof (cases "k = l")
```
```  1289           case True
```
```  1290           with l nonzero_hyp insert.prems show ?thesis
```
```  1291             by blast
```
```  1292         next
```
```  1293           case False
```
```  1294           have *: "A \$ i \$ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
```
```  1295             using False l insert.prems that
```
```  1296             by (auto simp: swap_def insert split: if_split_asm)
```
```  1297           have "P (\<chi> i j. (\<chi> i j. A \$ i \$ Fun.swap k l id j) \$ i \$ Fun.swap k l id j)"
```
```  1298             by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
```
```  1299           moreover
```
```  1300           have "(\<chi> i j. (\<chi> i j. A \$ i \$ Fun.swap k l id j) \$ i \$ Fun.swap k l id j) = A"
```
```  1301             by (vector Fun.swap_def)
```
```  1302           ultimately show ?thesis
```
```  1303             by simp
```
```  1304         qed
```
```  1305       qed
```
```  1306     qed
```
```  1307   qed
```
```  1308   then show ?thesis
```
```  1309     by blast
```
```  1310 qed
```
```  1311
```
```  1312 lemma induct_matrix_elementary:
```
```  1313   fixes P :: "real^'n^'n \<Rightarrow> bool"
```
```  1314   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
```
```  1315     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
```
```  1316     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A\$i\$j = 0) \<Longrightarrow> P A"
```
```  1317     and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 \$ i \$ Fun.swap m n id j)"
```
```  1318     and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
```
```  1319   shows "P A"
```
```  1320 proof -
```
```  1321   have swap: "P (\<chi> i j. A \$ i \$ Fun.swap m n id j)"  (is "P ?C")
```
```  1322     if "P A" "m \<noteq> n" for A m n
```
```  1323   proof -
```
```  1324     have "A ** (\<chi> i j. mat 1 \$ i \$ Fun.swap m n id j) = ?C"
```
```  1325       by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
```
```  1326     then show ?thesis
```
```  1327       using mult swap1 that by metis
```
```  1328   qed
```
```  1329   have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"  (is "P ?C")
```
```  1330     if "P A" "m \<noteq> n" for A m n c
```
```  1331   proof -
```
```  1332     let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)"
```
```  1333     have "?B ** A = ?C"
```
```  1334       using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def
```
```  1335       by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
```
```  1336     then show ?thesis
```
```  1337       by (rule subst) (auto simp: that mult idplus)
```
```  1338   qed
```
```  1339   show ?thesis
```
```  1340     by (rule induct_matrix_row_operations [OF zero_row diagonal swap row])
```
```  1341 qed
```
```  1342
```
```  1343 lemma induct_matrix_elementary_alt:
```
```  1344   fixes P :: "real^'n^'n \<Rightarrow> bool"
```
```  1345   assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
```
```  1346     and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
```
```  1347     and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A\$i\$j = 0) \<Longrightarrow> P A"
```
```  1348     and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 \$ i \$ Fun.swap m n id j)"
```
```  1349     and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
```
```  1350   shows "P A"
```
```  1351 proof -
```
```  1352   have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
```
```  1353     if "m \<noteq> n" for m n c
```
```  1354   proof (cases "c = 0")
```
```  1355     case True
```
```  1356     with diagonal show ?thesis by auto
```
```  1357   next
```
```  1358     case False
```
```  1359     then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) =
```
```  1360                       (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
```
```  1361                       (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
```
```  1362                       (\<chi> i j. if i = j then if j = n then c else 1 else 0)"
```
```  1363       using \<open>m \<noteq> n\<close>
```
```  1364       apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong)
```
```  1365       apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
```
```  1366       done
```
```  1367     show ?thesis
```
```  1368       apply (subst eq)
```
```  1369       apply (intro mult idplus that)
```
```  1370        apply (auto intro: diagonal)
```
```  1371       done
```
```  1372   qed
```
```  1373   show ?thesis
```
```  1374     by (rule induct_matrix_elementary) (auto intro: assms *)
```
```  1375 qed
```
```  1376
```
```  1377 lemma matrix_vector_mult_matrix_matrix_mult_compose:
```
```  1378   "(*v) (A ** B) = (*v) A \<circ> (*v) B"
```
```  1379   by (auto simp: matrix_vector_mul_assoc)
```
```  1380
```
```  1381 lemma induct_linear_elementary:
```
```  1382   fixes f :: "real^'n \<Rightarrow> real^'n"
```
```  1383   assumes "linear f"
```
```  1384     and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
```
```  1385     and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) \$ i = 0\<rbrakk> \<Longrightarrow> P f"
```
```  1386     and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x\$i)"
```
```  1387     and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x \$ Fun.swap m n id i)"
```
```  1388     and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x\$m + x\$n else x\$i)"
```
```  1389   shows "P f"
```
```  1390 proof -
```
```  1391   have "P ((*v) A)" for A
```
```  1392   proof (rule induct_matrix_elementary_alt)
```
```  1393     fix A B
```
```  1394     assume "P ((*v) A)" and "P ((*v) B)"
```
```  1395     then show "P ((*v) (A ** B))"
```
```  1396       by (auto simp add: matrix_vector_mult_matrix_matrix_mult_compose matrix_vector_mul_linear
```
```  1397           intro!: comp)
```
```  1398   next
```
```  1399     fix A :: "real^'n^'n" and i
```
```  1400     assume "row i A = 0"
```
```  1401     show "P ((*v) A)"
```
```  1402       using matrix_vector_mul_linear
```
```  1403       by (rule zeroes[where i=i])
```
```  1404         (metis \<open>row i A = 0\<close> inner_zero_left matrix_vector_mul_component row_def vec_lambda_eta)
```
```  1405   next
```
```  1406     fix A :: "real^'n^'n"
```
```  1407     assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A \$ i \$ j = 0"
```
```  1408     have "A \$ i \$ i * x \$ i = (\<Sum>j\<in>UNIV. A \$ i \$ j * x \$ j)" for x and i :: "'n"
```
```  1409       by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
```
```  1410     then have "(\<lambda>x. \<chi> i. A \$ i \$ i * x \$ i) = ((*v) A)"
```
```  1411       by (auto simp: 0 matrix_vector_mult_def)
```
```  1412     then show "P ((*v) A)"
```
```  1413       using const [of "\<lambda>i. A \$ i \$ i"] by simp
```
```  1414   next
```
```  1415     fix m n :: "'n"
```
```  1416     assume "m \<noteq> n"
```
```  1417     have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x \$ j else 0) =
```
```  1418               (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x \$ j else 0)"
```
```  1419       for i and x :: "real^'n"
```
```  1420       unfolding swap_def by (rule sum.cong) auto
```
```  1421     have "(\<lambda>x::real^'n. \<chi> i. x \$ Fun.swap m n id i) = ((*v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
```
```  1422       by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
```
```  1423     with swap [OF \<open>m \<noteq> n\<close>] show "P ((*v) (\<chi> i j. mat 1 \$ i \$ Fun.swap m n id j))"
```
```  1424       by (simp add: mat_def matrix_vector_mult_def)
```
```  1425   next
```
```  1426     fix m n :: "'n"
```
```  1427     assume "m \<noteq> n"
```
```  1428     then have "x \$ m + x \$ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x \$ j)" for x :: "real^'n"
```
```  1429       by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
```
```  1430     then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x \$ m + x \$ n else x \$ i) =
```
```  1431                ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
```
```  1432       unfolding matrix_vector_mult_def of_bool_def
```
```  1433       by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
```
```  1434     then show "P ((*v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
```
```  1435       using idplus [OF \<open>m \<noteq> n\<close>] by simp
```
```  1436   qed
```
```  1437   then show ?thesis
```
```  1438     by (metis \<open>linear f\<close> matrix_vector_mul)
```
```  1439 qed
```
```  1440
```
`  1441 end`