author | nipkow |
Wed, 16 Jan 2019 17:03:31 +0100 | |
changeset 69669 | de2f0a24b0f0 |
parent 69667 | 82bb6225588b |
child 69675 | 880ab0f27ddf |
child 69678 | 0f4d4a13dc16 |
permissions | -rw-r--r-- |
68189 | 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 |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
7 |
*) |
68189 | 8 |
|
69665 | 9 |
section "Linear Algebra on Finite Cartesian Products" |
10 |
||
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
11 |
theory Cartesian_Space |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
12 |
imports |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
13 |
Finite_Cartesian_Product Linear_Algebra |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
14 |
begin |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
15 |
|
69667 | 16 |
subsection \<open>Type @{typ \<open>'a ^ 'n\<close>} and fields as vector spaces\<close> |
17 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
18 |
definition%unimportant "cart_basis = {axis i 1 | i. i\<in>UNIV}" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
19 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
20 |
lemma%unimportant finite_cart_basis: "finite (cart_basis)" unfolding cart_basis_def |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
21 |
using finite_Atleast_Atmost_nat by fastforce |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
22 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
23 |
lemma%unimportant card_cart_basis: "card (cart_basis::('a::zero_neq_one^'i) set) = CARD('i)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
24 |
unfolding cart_basis_def Setcompr_eq_image |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
25 |
by (rule card_image) (auto simp: inj_on_def axis_eq_axis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
26 |
|
69667 | 27 |
interpretation%important vec: vector_space "(*s) " |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
28 |
by unfold_locales (vector algebra_simps)+ |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
29 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
30 |
lemma%unimportant independent_cart_basis: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
31 |
"vec.independent (cart_basis)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
32 |
proof (rule vec.independent_if_scalars_zero) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
33 |
show "finite (cart_basis)" using finite_cart_basis . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
34 |
fix f::"('a, 'b) vec \<Rightarrow> 'a" and x::"('a, 'b) vec" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
35 |
assume eq_0: "(\<Sum>x\<in>cart_basis. f x *s x) = 0" and x_in: "x \<in> cart_basis" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
36 |
obtain i where x: "x = axis i 1" using x_in unfolding cart_basis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
37 |
have sum_eq_0: "(\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i)) = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
38 |
proof (rule sum.neutral, rule ballI) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
39 |
fix xa assume xa: "xa \<in> cart_basis - {x}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
40 |
obtain a where a: "xa = axis a 1" and a_not_i: "a \<noteq> i" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
41 |
using xa x unfolding cart_basis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
42 |
have "xa $ i = 0" unfolding a axis_def using a_not_i by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
43 |
thus "f xa * xa $ i = 0" by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
44 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
45 |
have "0 = (\<Sum>x\<in>cart_basis. f x *s x) $ i" using eq_0 by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
46 |
also have "... = (\<Sum>x\<in>cart_basis. (f x *s x) $ i)" unfolding sum_component .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
47 |
also have "... = (\<Sum>x\<in>cart_basis. f x * (x $ i))" unfolding vector_smult_component .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
48 |
also have "... = f x * (x $ i) + (\<Sum>x\<in>(cart_basis) - {x}. f x * (x $ i))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
49 |
by (rule sum.remove[OF finite_cart_basis x_in]) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
50 |
also have "... = f x * (x $ i)" unfolding sum_eq_0 by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
51 |
also have "... = f x" unfolding x axis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
52 |
finally show "f x = 0" .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
53 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
54 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
55 |
lemma%unimportant span_cart_basis: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
56 |
"vec.span (cart_basis) = UNIV" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
57 |
proof (auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
58 |
fix x::"('a, 'b) vec" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
59 |
let ?f="\<lambda>v. x $ (THE i. v = axis i 1)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
60 |
show "x \<in> vec.span (cart_basis)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
61 |
apply (unfold vec.span_finite[OF finite_cart_basis]) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
62 |
apply (rule image_eqI[of _ _ ?f]) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
63 |
apply (subst vec_eq_iff) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
64 |
apply clarify |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
65 |
proof - |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
66 |
fix i::'b |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
67 |
let ?w = "axis i (1::'a)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
68 |
have the_eq_i: "(THE a. ?w = axis a 1) = i" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
69 |
by (rule the_equality, auto simp: axis_eq_axis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
70 |
have sum_eq_0: "(\<Sum>v\<in>(cart_basis) - {?w}. x $ (THE i. v = axis i 1) * v $ i) = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
71 |
proof (rule sum.neutral, rule ballI) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
72 |
fix xa::"('a, 'b) vec" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
73 |
assume xa: "xa \<in> cart_basis - {?w}" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
74 |
obtain j where j: "xa = axis j 1" and i_not_j: "i \<noteq> j" using xa unfolding cart_basis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
75 |
have the_eq_j: "(THE i. xa = axis i 1) = j" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
76 |
proof (rule the_equality) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
77 |
show "xa = axis j 1" using j . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
78 |
show "\<And>i. xa = axis i 1 \<Longrightarrow> i = j" by (metis axis_eq_axis j zero_neq_one) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
79 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
80 |
show "x $ (THE i. xa = axis i 1) * xa $ i = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
81 |
apply (subst (2) j) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
82 |
unfolding the_eq_j unfolding axis_def using i_not_j by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
83 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
84 |
have "(\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i = |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
85 |
(\<Sum>v\<in>cart_basis. (x $ (THE i. v = axis i 1) *s v) $ i)" unfolding sum_component .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
86 |
also have "... = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) * v $ i)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
87 |
unfolding vector_smult_component .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
88 |
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)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
89 |
by (rule sum.remove[OF finite_cart_basis], auto simp add: cart_basis_def) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
90 |
also have "... = x $ (THE a. ?w = axis a 1) * ?w $ i" unfolding sum_eq_0 by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
91 |
also have "... = x $ i" unfolding the_eq_i unfolding axis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
92 |
finally show "x $ i = (\<Sum>v\<in>cart_basis. x $ (THE i. v = axis i 1) *s v) $ i" by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
93 |
qed simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
94 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
95 |
|
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
96 |
(*Some interpretations:*) |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
97 |
interpretation vec: finite_dimensional_vector_space "(*s)" "cart_basis" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
98 |
by (unfold_locales, auto simp add: finite_cart_basis independent_cart_basis span_cart_basis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
99 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
100 |
lemma%unimportant matrix_vector_mul_linear_gen[intro, simp]: |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
101 |
"Vector_Spaces.linear (*s) (*s) ((*v) A)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
102 |
by unfold_locales |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
103 |
(vector matrix_vector_mult_def sum.distrib algebra_simps)+ |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
104 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
105 |
lemma%important span_vec_eq: "vec.span X = span X" |
68074 | 106 |
and dim_vec_eq: "vec.dim X = dim X" |
107 |
and dependent_vec_eq: "vec.dependent X = dependent X" |
|
108 |
and subspace_vec_eq: "vec.subspace X = subspace X" |
|
109 |
for X::"(real^'n) set" |
|
110 |
unfolding span_raw_def dim_raw_def dependent_raw_def subspace_raw_def |
|
111 |
by (auto simp: scalar_mult_eq_scaleR) |
|
112 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
113 |
lemma%important linear_componentwise: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
114 |
fixes f:: "'a::field ^'m \<Rightarrow> 'a ^ 'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
115 |
assumes lf: "Vector_Spaces.linear (*s) (*s) f" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
116 |
shows "(f x)$j = sum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
117 |
proof%unimportant - |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
118 |
interpret lf: Vector_Spaces.linear "(*s)" "(*s)" f |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
119 |
using lf . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
120 |
let ?M = "(UNIV :: 'm set)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
121 |
let ?N = "(UNIV :: 'n set)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
122 |
have fM: "finite ?M" by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
123 |
have "?rhs = (sum (\<lambda>i. (x$i) *s (f (axis i 1))) ?M)$j" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
124 |
unfolding sum_component by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
125 |
then show ?thesis |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
126 |
unfolding lf.sum[symmetric] lf.scale[symmetric] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
127 |
unfolding basis_expansion by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
128 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
129 |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
130 |
interpretation vec: Vector_Spaces.linear "(*s)" "(*s)" "(*v) A" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
131 |
using matrix_vector_mul_linear_gen. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
132 |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
133 |
interpretation vec: finite_dimensional_vector_space_pair "(*s)" cart_basis "(*s)" cart_basis .. |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
134 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
135 |
lemma%unimportant matrix_works: |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
136 |
assumes lf: "Vector_Spaces.linear (*s) (*s) f" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
137 |
shows "matrix f *v x = f (x::'a::field ^ 'n)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
138 |
apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult.commute) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
139 |
apply clarify |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
140 |
apply (rule linear_componentwise[OF lf, symmetric]) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
141 |
done |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
142 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
143 |
lemma%unimportant matrix_of_matrix_vector_mul[simp]: "matrix(\<lambda>x. A *v (x :: 'a::field ^ 'n)) = A" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
144 |
by (simp add: matrix_eq matrix_works) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
145 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
146 |
lemma%unimportant matrix_compose_gen: |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
147 |
assumes lf: "Vector_Spaces.linear (*s) (*s) (f::'a::{field}^'n \<Rightarrow> 'a^'m)" |
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
148 |
and lg: "Vector_Spaces.linear (*s) (*s) (g::'a^'m \<Rightarrow> 'a^_)" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
149 |
shows "matrix (g o f) = matrix g ** matrix f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
150 |
using lf lg Vector_Spaces.linear_compose[OF lf lg] matrix_works[OF Vector_Spaces.linear_compose[OF lf lg]] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
151 |
by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
152 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
153 |
lemma%unimportant matrix_compose: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
154 |
assumes "linear (f::real^'n \<Rightarrow> real^'m)" "linear (g::real^'m \<Rightarrow> real^_)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
155 |
shows "matrix (g o f) = matrix g ** matrix f" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
156 |
using matrix_compose_gen[of f g] assms |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
157 |
by (simp add: linear_def scalar_mult_eq_scaleR) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
158 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
159 |
lemma%unimportant left_invertible_transpose: |
68074 | 160 |
"(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)" |
161 |
by (metis matrix_transpose_mul transpose_mat transpose_transpose) |
|
162 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
163 |
lemma%unimportant right_invertible_transpose: |
68074 | 164 |
"(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)" |
165 |
by (metis matrix_transpose_mul transpose_mat transpose_transpose) |
|
166 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
167 |
lemma%unimportant linear_matrix_vector_mul_eq: |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
168 |
"Vector_Spaces.linear (*s) (*s) f \<longleftrightarrow> linear (f :: real^'n \<Rightarrow> real ^'m)" |
68074 | 169 |
by (simp add: scalar_mult_eq_scaleR linear_def) |
170 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
171 |
lemma%unimportant matrix_vector_mul[simp]: |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
172 |
"Vector_Spaces.linear (*s) (*s) g \<Longrightarrow> (\<lambda>y. matrix g *v y) = g" |
68074 | 173 |
"linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f" |
174 |
"bounded_linear f \<Longrightarrow> (\<lambda>x. matrix f *v x) = f" |
|
175 |
for f :: "real^'n \<Rightarrow> real ^'m" |
|
176 |
by (simp_all add: ext matrix_works linear_matrix_vector_mul_eq linear_linear) |
|
177 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
178 |
lemma%important matrix_left_invertible_injective: |
68074 | 179 |
fixes A :: "'a::field^'n^'m" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
180 |
shows "(\<exists>B. B ** A = mat 1) \<longleftrightarrow> inj ((*v) A)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
181 |
proof%unimportant safe |
68074 | 182 |
fix B |
183 |
assume B: "B ** A = mat 1" |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
184 |
show "inj ((*v) A)" |
68074 | 185 |
unfolding inj_on_def |
186 |
by (metis B matrix_vector_mul_assoc matrix_vector_mul_lid) |
|
187 |
next |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
188 |
assume "inj ((*v) A)" |
68074 | 189 |
from vec.linear_injective_left_inverse[OF matrix_vector_mul_linear_gen this] |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
190 |
obtain g where "Vector_Spaces.linear (*s) (*s) g" and g: "g \<circ> (*v) A = id" |
68074 | 191 |
by blast |
192 |
have "matrix g ** A = mat 1" |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
193 |
by (metis matrix_vector_mul_linear_gen \<open>Vector_Spaces.linear (*s) (*s) g\<close> g matrix_compose_gen |
68074 | 194 |
matrix_eq matrix_id_mat_1 matrix_vector_mul(1)) |
195 |
then show "\<exists>B. B ** A = mat 1" |
|
196 |
by metis |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
197 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
198 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
199 |
lemma%unimportant matrix_left_invertible_ker: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
200 |
"(\<exists>B. (B::'a::{field} ^'m^'n) ** (A::'a::{field}^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
201 |
unfolding matrix_left_invertible_injective |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
202 |
using vec.inj_on_iff_eq_0[OF vec.subspace_UNIV, of A] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
203 |
by (simp add: inj_on_def) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
204 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
205 |
lemma%important matrix_right_invertible_surjective: |
68074 | 206 |
"(\<exists>B. (A::'a::field^'n^'m) ** (B::'a::field^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
207 |
proof%unimportant - |
68074 | 208 |
{ fix B :: "'a ^'m^'n" |
209 |
assume AB: "A ** B = mat 1" |
|
210 |
{ fix x :: "'a ^ 'm" |
|
211 |
have "A *v (B *v x) = x" |
|
212 |
by (simp add: matrix_vector_mul_assoc AB) } |
|
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
213 |
hence "surj ((*v) A)" unfolding surj_def by metis } |
68074 | 214 |
moreover |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
215 |
{ assume sf: "surj ((*v) A)" |
68074 | 216 |
from vec.linear_surjective_right_inverse[OF _ this] |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
217 |
obtain g:: "'a ^'m \<Rightarrow> 'a ^'n" where g: "Vector_Spaces.linear (*s) (*s) g" "(*v) A \<circ> g = id" |
68074 | 218 |
by blast |
219 |
||
220 |
have "A ** (matrix g) = mat 1" |
|
221 |
unfolding matrix_eq matrix_vector_mul_lid |
|
222 |
matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] |
|
223 |
using g(2) unfolding o_def fun_eq_iff id_def |
|
224 |
. |
|
225 |
hence "\<exists>B. A ** (B::'a^'m^'n) = mat 1" by blast |
|
226 |
} |
|
227 |
ultimately show ?thesis unfolding surj_def by blast |
|
228 |
qed |
|
229 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
230 |
lemma%important matrix_left_invertible_independent_columns: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
231 |
fixes A :: "'a::{field}^'n^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
232 |
shows "(\<exists>(B::'a ^'m^'n). B ** A = mat 1) \<longleftrightarrow> |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
233 |
(\<forall>c. sum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
234 |
(is "?lhs \<longleftrightarrow> ?rhs") |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
235 |
proof%unimportant - |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
236 |
let ?U = "UNIV :: 'n set" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
237 |
{ assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
238 |
{ fix c i |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
239 |
assume c: "sum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
240 |
let ?x = "\<chi> i. c i" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
241 |
have th0:"A *v ?x = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
242 |
using c |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
243 |
by (vector matrix_mult_sum) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
244 |
from k[rule_format, OF th0] i |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
245 |
have "c i = 0" by (vector vec_eq_iff)} |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
246 |
hence ?rhs by blast } |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
247 |
moreover |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
248 |
{ assume H: ?rhs |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
249 |
{ fix x assume x: "A *v x = 0" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
250 |
let ?c = "\<lambda>i. ((x$i ):: 'a)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
251 |
from H[rule_format, of ?c, unfolded matrix_mult_sum[symmetric], OF x] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
252 |
have "x = 0" by vector } |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
253 |
} |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
254 |
ultimately show ?thesis unfolding matrix_left_invertible_ker by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
255 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
256 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
257 |
lemma%unimportant matrix_right_invertible_independent_rows: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
258 |
fixes A :: "'a::{field}^'n^'m" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
259 |
shows "(\<exists>(B::'a^'m^'n). A ** B = mat 1) \<longleftrightarrow> |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
260 |
(\<forall>c. sum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
261 |
unfolding left_invertible_transpose[symmetric] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
262 |
matrix_left_invertible_independent_columns |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
263 |
by (simp add:) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
264 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
265 |
lemma%important matrix_right_invertible_span_columns: |
68074 | 266 |
"(\<exists>(B::'a::field ^'n^'m). (A::'a ^'m^'n) ** B = mat 1) \<longleftrightarrow> |
267 |
vec.span (columns A) = UNIV" (is "?lhs = ?rhs") |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
268 |
proof%unimportant - |
68074 | 269 |
let ?U = "UNIV :: 'm set" |
270 |
have fU: "finite ?U" by simp |
|
271 |
have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y)" |
|
272 |
unfolding matrix_right_invertible_surjective matrix_mult_sum surj_def |
|
273 |
by (simp add: eq_commute) |
|
274 |
have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> vec.span (columns A))" by blast |
|
275 |
{ assume h: ?lhs |
|
276 |
{ fix x:: "'a ^'n" |
|
277 |
from h[unfolded lhseq, rule_format, of x] obtain y :: "'a ^'m" |
|
278 |
where y: "sum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast |
|
279 |
have "x \<in> vec.span (columns A)" |
|
280 |
unfolding y[symmetric] scalar_mult_eq_scaleR |
|
281 |
proof (rule vec.span_sum [OF vec.span_scale]) |
|
282 |
show "column i A \<in> vec.span (columns A)" for i |
|
283 |
using columns_def vec.span_superset by auto |
|
284 |
qed |
|
285 |
} |
|
286 |
then have ?rhs unfolding rhseq by blast } |
|
287 |
moreover |
|
288 |
{ assume h:?rhs |
|
289 |
let ?P = "\<lambda>(y::'a ^'n). \<exists>(x::'a^'m). sum (\<lambda>i. (x$i) *s column i A) ?U = y" |
|
290 |
{ fix y |
|
291 |
have "y \<in> vec.span (columns A)" |
|
292 |
unfolding h by blast |
|
293 |
then have "?P y" |
|
294 |
proof (induction rule: vec.span_induct_alt) |
|
295 |
case base |
|
296 |
then show ?case |
|
297 |
by (metis (full_types) matrix_mult_sum matrix_vector_mult_0_right) |
|
298 |
next |
|
299 |
case (step c y1 y2) |
|
300 |
from step obtain i where i: "i \<in> ?U" "y1 = column i A" |
|
301 |
unfolding columns_def by blast |
|
302 |
obtain x:: "'a ^'m" where x: "sum (\<lambda>i. (x$i) *s column i A) ?U = y2" |
|
303 |
using step by blast |
|
304 |
let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::'a^'m" |
|
305 |
show ?case |
|
306 |
proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left if_distribR cong del: if_weak_cong) |
|
307 |
fix j |
|
308 |
have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
309 |
else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" |
|
310 |
using i(1) by (simp add: field_simps) |
|
311 |
have "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
312 |
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" |
|
313 |
by (rule sum.cong[OF refl]) (use th in blast) |
|
314 |
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" |
|
315 |
by (simp add: sum.distrib) |
|
316 |
also have "\<dots> = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" |
|
317 |
unfolding sum.delta[OF fU] |
|
318 |
using i(1) by simp |
|
319 |
finally show "sum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
320 |
else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + sum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" . |
|
321 |
qed |
|
322 |
qed |
|
323 |
} |
|
324 |
then have ?lhs unfolding lhseq .. |
|
325 |
} |
|
326 |
ultimately show ?thesis by blast |
|
327 |
qed |
|
328 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
329 |
lemma%unimportant matrix_left_invertible_span_rows_gen: |
68074 | 330 |
"(\<exists>(B::'a^'m^'n). B ** (A::'a::field^'n^'m) = mat 1) \<longleftrightarrow> vec.span (rows A) = UNIV" |
331 |
unfolding right_invertible_transpose[symmetric] |
|
332 |
unfolding columns_transpose[symmetric] |
|
333 |
unfolding matrix_right_invertible_span_columns |
|
334 |
.. |
|
335 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
336 |
lemma%unimportant matrix_left_invertible_span_rows: |
68074 | 337 |
"(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV" |
338 |
using matrix_left_invertible_span_rows_gen[of A] by (simp add: span_vec_eq) |
|
339 |
||
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
340 |
lemma%important matrix_left_right_inverse: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
341 |
fixes A A' :: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
342 |
shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
343 |
proof%unimportant - |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
344 |
{ fix A A' :: "'a ^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
345 |
assume AA': "A ** A' = mat 1" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
346 |
have sA: "surj ((*v) A)" |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
347 |
using AA' matrix_right_invertible_surjective by auto |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
348 |
from vec.linear_surjective_isomorphism[OF matrix_vector_mul_linear_gen sA] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
349 |
obtain f' :: "'a ^'n \<Rightarrow> 'a ^'n" |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
350 |
where f': "Vector_Spaces.linear (*s) (*s) f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
351 |
have th: "matrix f' ** A = mat 1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
352 |
by (simp add: matrix_eq matrix_works[OF f'(1)] |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
353 |
matrix_vector_mul_assoc[symmetric] f'(2)[rule_format]) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
354 |
hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
355 |
hence "matrix f' = A'" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
356 |
by (simp add: matrix_mul_assoc[symmetric] AA') |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
357 |
hence "matrix f' ** A = A' ** A" by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
358 |
hence "A' ** A = mat 1" by (simp add: th) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
359 |
} |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
360 |
then show ?thesis by blast |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
361 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
362 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
363 |
lemma%unimportant invertible_left_inverse: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
364 |
fixes A :: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
365 |
shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). B ** A = mat 1)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
366 |
by (metis invertible_def matrix_left_right_inverse) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
367 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
368 |
lemma%unimportant invertible_right_inverse: |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
369 |
fixes A :: "'a::{field}^'n^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
370 |
shows "invertible A \<longleftrightarrow> (\<exists>(B::'a^'n^'n). A** B = mat 1)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
371 |
by (metis invertible_def matrix_left_right_inverse) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
372 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
373 |
lemma%important invertible_mult: |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
374 |
assumes inv_A: "invertible A" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
375 |
and inv_B: "invertible B" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
376 |
shows "invertible (A**B)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
377 |
proof%unimportant - |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
378 |
obtain A' where AA': "A ** A' = mat 1" and A'A: "A' ** A = mat 1" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
379 |
using inv_A unfolding invertible_def by blast |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
380 |
obtain B' where BB': "B ** B' = mat 1" and B'B: "B' ** B = mat 1" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
381 |
using inv_B unfolding invertible_def by blast |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
382 |
show ?thesis |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
383 |
proof (unfold invertible_def, rule exI[of _ "B'**A'"], rule conjI) |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
384 |
have "A ** B ** (B' ** A') = A ** (B ** (B' ** A'))" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
385 |
using matrix_mul_assoc[of A B "(B' ** A')", symmetric] . |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
386 |
also have "... = A ** (B ** B' ** A')" unfolding matrix_mul_assoc[of B "B'" "A'"] .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
387 |
also have "... = A ** (mat 1 ** A')" unfolding BB' .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
388 |
also have "... = A ** A'" unfolding matrix_mul_lid .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
389 |
also have "... = mat 1" unfolding AA' .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
390 |
finally show "A ** B ** (B' ** A') = mat (1::'a)" . |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
391 |
have "B' ** A' ** (A ** B) = B' ** (A' ** (A ** B))" using matrix_mul_assoc[of B' A' "(A ** B)", symmetric] . |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
392 |
also have "... = B' ** (A' ** A ** B)" unfolding matrix_mul_assoc[of A' A B] .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
393 |
also have "... = B' ** (mat 1 ** B)" unfolding A'A .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
394 |
also have "... = B' ** B" unfolding matrix_mul_lid .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
395 |
also have "... = mat 1" unfolding B'B .. |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
396 |
finally show "B' ** A' ** (A ** B) = mat 1" . |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
397 |
qed |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
398 |
qed |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
399 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
400 |
lemma%unimportant transpose_invertible: |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
401 |
fixes A :: "real^'n^'n" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
402 |
assumes "invertible A" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
403 |
shows "invertible (transpose A)" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
404 |
by (meson assms invertible_def matrix_left_right_inverse right_invertible_transpose) |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
405 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
406 |
lemma%important vector_matrix_mul_assoc: |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
407 |
fixes v :: "('a::comm_semiring_1)^'n" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
408 |
shows "(v v* M) v* N = v v* (M ** N)" |
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
409 |
proof%unimportant - |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
410 |
from matrix_vector_mul_assoc |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
411 |
have "transpose N *v (transpose M *v v) = (transpose N ** transpose M) *v v" by fast |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
412 |
thus "(v v* M) v* N = v v* (M ** N)" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
413 |
by (simp add: matrix_transpose_mul [symmetric]) |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
414 |
qed |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
415 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
416 |
lemma%unimportant matrix_scaleR_vector_ac: |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
417 |
fixes A :: "real^('m::finite)^'n" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
418 |
shows "A *v (k *\<^sub>R v) = k *\<^sub>R A *v v" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
419 |
by (metis matrix_vector_mult_scaleR transpose_scalar vector_scaleR_matrix_ac vector_transpose_matrix) |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
420 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
421 |
lemma%unimportant scaleR_matrix_vector_assoc: |
68073
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
422 |
fixes A :: "real^('m::finite)^'n" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
423 |
shows "k *\<^sub>R (A *v v) = k *\<^sub>R A *v v" |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
424 |
by (metis matrix_scaleR_vector_ac matrix_vector_mult_scaleR) |
fad29d2a17a5
merged; resolved conflicts manually (esp. lemmas that have been moved from Linear_Algebra and Cartesian_Euclidean_Space)
immler
parents:
68072
diff
changeset
|
425 |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
426 |
(*Finally, some interesting theorems and interpretations that don't appear in any file of the |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
427 |
library.*) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
428 |
|
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
429 |
locale linear_first_finite_dimensional_vector_space = |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
430 |
l?: Vector_Spaces.linear scaleB scaleC f + |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
431 |
B?: finite_dimensional_vector_space scaleB BasisB |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
432 |
for scaleB :: "('a::field => 'b::ab_group_add => 'b)" (infixr "*b" 75) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
433 |
and scaleC :: "('a => 'c::ab_group_add => 'c)" (infixr "*c" 75) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
434 |
and BasisB :: "('b set)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
435 |
and f :: "('b=>'c)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
436 |
|
68833
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
437 |
lemma%important vec_dim_card: "vec.dim (UNIV::('a::{field}^'n) set) = CARD ('n)" |
fde093888c16
tagged 21 theories in the Analysis library for the manual
Angeliki KoutsoukouArgyraki <ak2110@cam.ac.uk>
parents:
68189
diff
changeset
|
438 |
proof%unimportant - |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
439 |
let ?f="\<lambda>i::'n. axis i (1::'a)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
440 |
have "vec.dim (UNIV::('a::{field}^'n) set) = card (cart_basis::('a^'n) set)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
441 |
unfolding vec.dim_UNIV .. |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
442 |
also have "... = card ({i. i\<in> UNIV}::('n) set)" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
443 |
proof (rule bij_betw_same_card[of ?f, symmetric], unfold bij_betw_def, auto) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
444 |
show "inj (\<lambda>i::'n. axis i (1::'a))" by (simp add: inj_on_def axis_eq_axis) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
445 |
fix i::'n |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
446 |
show "axis i 1 \<in> cart_basis" unfolding cart_basis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
447 |
fix x::"'a^'n" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
448 |
assume "x \<in> cart_basis" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
449 |
thus "x \<in> range (\<lambda>i. axis i 1)" unfolding cart_basis_def by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
450 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
451 |
also have "... = CARD('n)" by auto |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
452 |
finally show ?thesis . |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
453 |
qed |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
454 |
|
69667 | 455 |
interpretation%important vector_space_over_itself: vector_space "(*) :: 'a::field \<Rightarrow> 'a \<Rightarrow> 'a" |
456 |
by unfold_locales (simp_all add: algebra_simps) |
|
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
457 |
|
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
458 |
lemmas [simp del] = vector_space_over_itself.scale_scale |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
459 |
|
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
460 |
interpretation vector_space_over_itself: finite_dimensional_vector_space |
69064
5840724b1d71
Prefix form of infix with * on either side no longer needs special treatment
nipkow
parents:
68833
diff
changeset
|
461 |
"(*) :: 'a::field => 'a => 'a" "{1}" |
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
462 |
by unfold_locales (auto simp: vector_space_over_itself.span_singleton) |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
463 |
|
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
464 |
lemma dimension_eq_1[code_unfold]: "vector_space_over_itself.dimension TYPE('a::field)= 1" |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
465 |
unfolding vector_space_over_itself.dimension_def by simp |
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
466 |
|
69666 | 467 |
|
468 |
lemma%unimportant dim_subset_UNIV_cart_gen: |
|
469 |
fixes S :: "('a::field^'n) set" |
|
470 |
shows "vec.dim S \<le> CARD('n)" |
|
471 |
by (metis vec.dim_eq_full vec.dim_subset_UNIV vec.span_UNIV vec_dim_card) |
|
472 |
||
473 |
lemma%unimportant dim_subset_UNIV_cart: |
|
474 |
fixes S :: "(real^'n) set" |
|
475 |
shows "dim S \<le> CARD('n)" |
|
476 |
using dim_subset_UNIV_cart_gen[of S] by (simp add: dim_vec_eq) |
|
477 |
||
478 |
text\<open>Two sometimes fruitful ways of looking at matrix-vector multiplication.\<close> |
|
479 |
||
480 |
lemma%important matrix_mult_dot: "A *v x = (\<chi> i. inner (A$i) x)" |
|
481 |
by (simp add: matrix_vector_mult_def inner_vec_def) |
|
482 |
||
483 |
lemma%unimportant adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
|
484 |
apply (rule adjoint_unique) |
|
485 |
apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def |
|
486 |
sum_distrib_right sum_distrib_left) |
|
487 |
apply (subst sum.swap) |
|
488 |
apply (simp add: ac_simps) |
|
489 |
done |
|
490 |
||
491 |
lemma%important matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)" |
|
492 |
shows "matrix(adjoint f) = transpose(matrix f)" |
|
493 |
proof%unimportant - |
|
494 |
have "matrix(adjoint f) = matrix(adjoint ((*v) (matrix f)))" |
|
495 |
by (simp add: lf) |
|
496 |
also have "\<dots> = transpose(matrix f)" |
|
497 |
unfolding adjoint_matrix matrix_of_matrix_vector_mul |
|
498 |
apply rule |
|
499 |
done |
|
500 |
finally show ?thesis . |
|
501 |
qed |
|
502 |
||
503 |
||
504 |
subsection%important\<open> Rank of a matrix\<close> |
|
505 |
||
506 |
text\<open>Equivalence of row and column rank is taken from George Mackiw's paper, Mathematics Magazine 1995, p. 285.\<close> |
|
507 |
||
508 |
lemma%unimportant matrix_vector_mult_in_columnspace_gen: |
|
509 |
fixes A :: "'a::field^'n^'m" |
|
510 |
shows "(A *v x) \<in> vec.span(columns A)" |
|
511 |
apply (simp add: matrix_vector_column columns_def transpose_def column_def) |
|
512 |
apply (intro vec.span_sum vec.span_scale) |
|
513 |
apply (force intro: vec.span_base) |
|
514 |
done |
|
515 |
||
516 |
lemma%unimportant matrix_vector_mult_in_columnspace: |
|
517 |
fixes A :: "real^'n^'m" |
|
518 |
shows "(A *v x) \<in> span(columns A)" |
|
519 |
using matrix_vector_mult_in_columnspace_gen[of A x] by (simp add: span_vec_eq) |
|
520 |
||
521 |
lemma subspace_orthogonal_to_vector: "subspace {y. orthogonal x y}" |
|
522 |
by (simp add: subspace_def orthogonal_clauses) |
|
523 |
||
524 |
lemma%important orthogonal_nullspace_rowspace: |
|
525 |
fixes A :: "real^'n^'m" |
|
526 |
assumes 0: "A *v x = 0" and y: "y \<in> span(rows A)" |
|
527 |
shows "orthogonal x y" |
|
528 |
using y |
|
529 |
proof%unimportant (induction rule: span_induct) |
|
530 |
case base |
|
531 |
then show ?case |
|
532 |
by (simp add: subspace_orthogonal_to_vector) |
|
533 |
next |
|
534 |
case (step v) |
|
535 |
then obtain i where "v = row i A" |
|
536 |
by (auto simp: rows_def) |
|
537 |
with 0 show ?case |
|
538 |
unfolding orthogonal_def inner_vec_def matrix_vector_mult_def row_def |
|
539 |
by (simp add: mult.commute) (metis (no_types) vec_lambda_beta zero_index) |
|
540 |
qed |
|
541 |
||
542 |
lemma%unimportant nullspace_inter_rowspace: |
|
543 |
fixes A :: "real^'n^'m" |
|
544 |
shows "A *v x = 0 \<and> x \<in> span(rows A) \<longleftrightarrow> x = 0" |
|
545 |
using orthogonal_nullspace_rowspace orthogonal_self span_zero matrix_vector_mult_0_right |
|
546 |
by blast |
|
547 |
||
548 |
lemma%unimportant matrix_vector_mul_injective_on_rowspace: |
|
549 |
fixes A :: "real^'n^'m" |
|
550 |
shows "\<lbrakk>A *v x = A *v y; x \<in> span(rows A); y \<in> span(rows A)\<rbrakk> \<Longrightarrow> x = y" |
|
551 |
using nullspace_inter_rowspace [of A "x-y"] |
|
552 |
by (metis diff_eq_diff_eq diff_self matrix_vector_mult_diff_distrib span_diff) |
|
553 |
||
554 |
definition%important rank :: "'a::field^'n^'m=>nat" |
|
555 |
where row_rank_def_gen: "rank A \<equiv> vec.dim(rows A)" |
|
556 |
||
557 |
lemma%important row_rank_def: "rank A = dim (rows A)" for A::"real^'n^'m" |
|
558 |
by%unimportant (auto simp: row_rank_def_gen dim_vec_eq) |
|
559 |
||
560 |
lemma%important dim_rows_le_dim_columns: |
|
561 |
fixes A :: "real^'n^'m" |
|
562 |
shows "dim(rows A) \<le> dim(columns A)" |
|
563 |
proof%unimportant - |
|
564 |
have "dim (span (rows A)) \<le> dim (span (columns A))" |
|
565 |
proof - |
|
566 |
obtain B where "independent B" "span(rows A) \<subseteq> span B" |
|
567 |
and B: "B \<subseteq> span(rows A)""card B = dim (span(rows A))" |
|
568 |
using basis_exists [of "span(rows A)"] by metis |
|
569 |
with span_subspace have eq: "span B = span(rows A)" |
|
570 |
by auto |
|
571 |
then have inj: "inj_on ((*v) A) (span B)" |
|
572 |
by (simp add: inj_on_def matrix_vector_mul_injective_on_rowspace) |
|
573 |
then have ind: "independent ((*v) A ` B)" |
|
574 |
by (rule linear_independent_injective_image [OF Finite_Cartesian_Product.matrix_vector_mul_linear \<open>independent B\<close>]) |
|
575 |
have "dim (span (rows A)) \<le> card ((*v) A ` B)" |
|
576 |
unfolding B(2)[symmetric] |
|
577 |
using inj |
|
578 |
by (auto simp: card_image inj_on_subset span_superset) |
|
579 |
also have "\<dots> \<le> dim (span (columns A))" |
|
580 |
using _ ind |
|
581 |
by (rule independent_card_le_dim) (auto intro!: matrix_vector_mult_in_columnspace) |
|
582 |
finally show ?thesis . |
|
583 |
qed |
|
584 |
then show ?thesis |
|
585 |
by (simp add: dim_span) |
|
586 |
qed |
|
587 |
||
588 |
lemma%unimportant column_rank_def: |
|
589 |
fixes A :: "real^'n^'m" |
|
590 |
shows "rank A = dim(columns A)" |
|
591 |
unfolding row_rank_def |
|
592 |
by (metis columns_transpose dim_rows_le_dim_columns le_antisym rows_transpose) |
|
593 |
||
594 |
lemma%unimportant rank_transpose: |
|
595 |
fixes A :: "real^'n^'m" |
|
596 |
shows "rank(transpose A) = rank A" |
|
597 |
by (metis column_rank_def row_rank_def rows_transpose) |
|
598 |
||
599 |
lemma%unimportant matrix_vector_mult_basis: |
|
600 |
fixes A :: "real^'n^'m" |
|
601 |
shows "A *v (axis k 1) = column k A" |
|
602 |
by (simp add: cart_eq_inner_axis column_def matrix_mult_dot) |
|
603 |
||
604 |
lemma%unimportant columns_image_basis: |
|
605 |
fixes A :: "real^'n^'m" |
|
606 |
shows "columns A = (*v) A ` (range (\<lambda>i. axis i 1))" |
|
607 |
by (force simp: columns_def matrix_vector_mult_basis [symmetric]) |
|
608 |
||
609 |
lemma%important rank_dim_range: |
|
610 |
fixes A :: "real^'n^'m" |
|
611 |
shows "rank A = dim(range (\<lambda>x. A *v x))" |
|
612 |
unfolding column_rank_def |
|
613 |
proof%unimportant (rule span_eq_dim) |
|
614 |
have "span (columns A) \<subseteq> span (range ((*v) A))" (is "?l \<subseteq> ?r") |
|
615 |
by (simp add: columns_image_basis image_subsetI span_mono) |
|
616 |
then show "?l = ?r" |
|
617 |
by (metis (no_types, lifting) image_subset_iff matrix_vector_mult_in_columnspace |
|
618 |
span_eq span_span) |
|
619 |
qed |
|
620 |
||
621 |
lemma%unimportant rank_bound: |
|
622 |
fixes A :: "real^'n^'m" |
|
623 |
shows "rank A \<le> min CARD('m) (CARD('n))" |
|
624 |
by (metis (mono_tags, lifting) dim_subset_UNIV_cart min.bounded_iff |
|
625 |
column_rank_def row_rank_def) |
|
626 |
||
627 |
lemma%unimportant full_rank_injective: |
|
628 |
fixes A :: "real^'n^'m" |
|
629 |
shows "rank A = CARD('n) \<longleftrightarrow> inj ((*v) A)" |
|
630 |
by (simp add: matrix_left_invertible_injective [symmetric] matrix_left_invertible_span_rows row_rank_def |
|
631 |
dim_eq_full [symmetric] card_cart_basis vec.dimension_def) |
|
632 |
||
633 |
lemma%unimportant full_rank_surjective: |
|
634 |
fixes A :: "real^'n^'m" |
|
635 |
shows "rank A = CARD('m) \<longleftrightarrow> surj ((*v) A)" |
|
636 |
by (simp add: matrix_right_invertible_surjective [symmetric] left_invertible_transpose [symmetric] |
|
637 |
matrix_left_invertible_injective full_rank_injective [symmetric] rank_transpose) |
|
638 |
||
639 |
lemma%unimportant rank_I: "rank(mat 1::real^'n^'n) = CARD('n)" |
|
640 |
by (simp add: full_rank_injective inj_on_def) |
|
641 |
||
642 |
lemma%unimportant less_rank_noninjective: |
|
643 |
fixes A :: "real^'n^'m" |
|
644 |
shows "rank A < CARD('n) \<longleftrightarrow> \<not> inj ((*v) A)" |
|
645 |
using less_le rank_bound by (auto simp: full_rank_injective [symmetric]) |
|
646 |
||
647 |
lemma%unimportant matrix_nonfull_linear_equations_eq: |
|
648 |
fixes A :: "real^'n^'m" |
|
649 |
shows "(\<exists>x. (x \<noteq> 0) \<and> A *v x = 0) \<longleftrightarrow> rank A \<noteq> CARD('n)" |
|
650 |
by (meson matrix_left_invertible_injective full_rank_injective matrix_left_invertible_ker) |
|
651 |
||
652 |
lemma%unimportant rank_eq_0: "rank A = 0 \<longleftrightarrow> A = 0" and rank_0 [simp]: "rank (0::real^'n^'m) = 0" |
|
653 |
for A :: "real^'n^'m" |
|
654 |
by (auto simp: rank_dim_range matrix_eq) |
|
655 |
||
656 |
lemma%important rank_mul_le_right: |
|
657 |
fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
658 |
shows "rank(A ** B) \<le> rank B" |
|
659 |
proof%unimportant - |
|
660 |
have "rank(A ** B) \<le> dim ((*v) A ` range ((*v) B))" |
|
661 |
by (auto simp: rank_dim_range image_comp o_def matrix_vector_mul_assoc) |
|
662 |
also have "\<dots> \<le> rank B" |
|
663 |
by (simp add: rank_dim_range dim_image_le) |
|
664 |
finally show ?thesis . |
|
665 |
qed |
|
666 |
||
667 |
lemma%unimportant rank_mul_le_left: |
|
668 |
fixes A :: "real^'n^'m" and B :: "real^'p^'n" |
|
669 |
shows "rank(A ** B) \<le> rank A" |
|
670 |
by (metis matrix_transpose_mul rank_mul_le_right rank_transpose) |
|
671 |
||
69669 | 672 |
|
673 |
subsection%unimportant \<open>Lemmas for working on \<open>real^1/2/3\<close>\<close> |
|
674 |
||
675 |
lemma exhaust_2: |
|
676 |
fixes x :: 2 |
|
677 |
shows "x = 1 \<or> x = 2" |
|
678 |
proof (induct x) |
|
679 |
case (of_int z) |
|
680 |
then have "0 \<le> z" and "z < 2" by simp_all |
|
681 |
then have "z = 0 | z = 1" by arith |
|
682 |
then show ?case by auto |
|
683 |
qed |
|
684 |
||
685 |
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2" |
|
686 |
by (metis exhaust_2) |
|
687 |
||
688 |
lemma exhaust_3: |
|
689 |
fixes x :: 3 |
|
690 |
shows "x = 1 \<or> x = 2 \<or> x = 3" |
|
691 |
proof (induct x) |
|
692 |
case (of_int z) |
|
693 |
then have "0 \<le> z" and "z < 3" by simp_all |
|
694 |
then have "z = 0 \<or> z = 1 \<or> z = 2" by arith |
|
695 |
then show ?case by auto |
|
696 |
qed |
|
697 |
||
698 |
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" |
|
699 |
by (metis exhaust_3) |
|
700 |
||
701 |
lemma UNIV_1 [simp]: "UNIV = {1::1}" |
|
702 |
by (auto simp add: num1_eq_iff) |
|
703 |
||
704 |
lemma UNIV_2: "UNIV = {1::2, 2::2}" |
|
705 |
using exhaust_2 by auto |
|
706 |
||
707 |
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" |
|
708 |
using exhaust_3 by auto |
|
709 |
||
710 |
lemma sum_1: "sum f (UNIV::1 set) = f 1" |
|
711 |
unfolding UNIV_1 by simp |
|
712 |
||
713 |
lemma sum_2: "sum f (UNIV::2 set) = f 1 + f 2" |
|
714 |
unfolding UNIV_2 by simp |
|
715 |
||
716 |
lemma sum_3: "sum f (UNIV::3 set) = f 1 + f 2 + f 3" |
|
717 |
unfolding UNIV_3 by (simp add: ac_simps) |
|
718 |
||
719 |
subsection%unimportant\<open>The collapse of the general concepts to dimension one\<close> |
|
720 |
||
721 |
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" |
|
722 |
by (simp add: vec_eq_iff) |
|
723 |
||
724 |
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" |
|
725 |
apply auto |
|
726 |
apply (erule_tac x= "x$1" in allE) |
|
727 |
apply (simp only: vector_one[symmetric]) |
|
728 |
done |
|
729 |
||
730 |
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" |
|
731 |
by (simp add: norm_vec_def) |
|
732 |
||
733 |
lemma dist_vector_1: |
|
734 |
fixes x :: "'a::real_normed_vector^1" |
|
735 |
shows "dist x y = dist (x$1) (y$1)" |
|
736 |
by (simp add: dist_norm norm_vector_1) |
|
737 |
||
738 |
lemma norm_real: "norm(x::real ^ 1) = \<bar>x$1\<bar>" |
|
739 |
by (simp add: norm_vector_1) |
|
740 |
||
741 |
lemma dist_real: "dist(x::real ^ 1) y = \<bar>(x$1) - (y$1)\<bar>" |
|
742 |
by (auto simp add: norm_real dist_norm) |
|
743 |
||
744 |
||
745 |
subsection%unimportant\<open>Routine results connecting the types \<^typ>\<open>real^1\<close> and \<^typ>\<open>real\<close>\<close> |
|
746 |
||
747 |
lemma vector_one_nth [simp]: |
|
748 |
fixes x :: "'a^1" shows "vec (x $ 1) = x" |
|
749 |
by (metis vec_def vector_one) |
|
750 |
||
751 |
lemma tendsto_at_within_vector_1: |
|
752 |
fixes S :: "'a :: metric_space set" |
|
753 |
assumes "(f \<longlongrightarrow> fx) (at x within S)" |
|
754 |
shows "((\<lambda>y::'a^1. \<chi> i. f (y $ 1)) \<longlongrightarrow> (vec fx::'a^1)) (at (vec x) within vec ` S)" |
|
755 |
proof (rule topological_tendstoI) |
|
756 |
fix T :: "('a^1) set" |
|
757 |
assume "open T" "vec fx \<in> T" |
|
758 |
have "\<forall>\<^sub>F x in at x within S. f x \<in> (\<lambda>x. x $ 1) ` T" |
|
759 |
using \<open>open T\<close> \<open>vec fx \<in> T\<close> assms open_image_vec_nth tendsto_def by fastforce |
|
760 |
then show "\<forall>\<^sub>F x::'a^1 in at (vec x) within vec ` S. (\<chi> i. f (x $ 1)) \<in> T" |
|
761 |
unfolding eventually_at dist_norm [symmetric] |
|
762 |
by (rule ex_forward) |
|
763 |
(use \<open>open T\<close> in |
|
764 |
\<open>fastforce simp: dist_norm dist_vec_def L2_set_def image_iff vector_one open_vec_def\<close>) |
|
765 |
qed |
|
766 |
||
767 |
lemma has_derivative_vector_1: |
|
768 |
assumes der_g: "(g has_derivative (\<lambda>x. x * g' a)) (at a within S)" |
|
769 |
shows "((\<lambda>x. vec (g (x $ 1))) has_derivative (*\<^sub>R) (g' a)) |
|
770 |
(at ((vec a)::real^1) within vec ` S)" |
|
771 |
using der_g |
|
772 |
apply (auto simp: Deriv.has_derivative_within bounded_linear_scaleR_right norm_vector_1) |
|
773 |
apply (drule tendsto_at_within_vector_1, vector) |
|
774 |
apply (auto simp: algebra_simps eventually_at tendsto_def) |
|
775 |
done |
|
776 |
||
777 |
||
778 |
subsection%unimportant\<open>Explicit vector construction from lists\<close> |
|
779 |
||
780 |
definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)" |
|
781 |
||
782 |
lemma vector_1 [simp]: "(vector[x]) $1 = x" |
|
783 |
unfolding vector_def by simp |
|
784 |
||
785 |
lemma vector_2 [simp]: "(vector[x,y]) $1 = x" "(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" |
|
786 |
unfolding vector_def by simp_all |
|
787 |
||
788 |
lemma vector_3 [simp]: |
|
789 |
"(vector [x,y,z] ::('a::zero)^3)$1 = x" |
|
790 |
"(vector [x,y,z] ::('a::zero)^3)$2 = y" |
|
791 |
"(vector [x,y,z] ::('a::zero)^3)$3 = z" |
|
792 |
unfolding vector_def by simp_all |
|
793 |
||
794 |
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))" |
|
795 |
by (metis vector_1 vector_one) |
|
796 |
||
797 |
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))" |
|
798 |
apply auto |
|
799 |
apply (erule_tac x="v$1" in allE) |
|
800 |
apply (erule_tac x="v$2" in allE) |
|
801 |
apply (subgoal_tac "vector [v$1, v$2] = v") |
|
802 |
apply simp |
|
803 |
apply (vector vector_def) |
|
804 |
apply (simp add: forall_2) |
|
805 |
done |
|
806 |
||
807 |
lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))" |
|
808 |
apply auto |
|
809 |
apply (erule_tac x="v$1" in allE) |
|
810 |
apply (erule_tac x="v$2" in allE) |
|
811 |
apply (erule_tac x="v$3" in allE) |
|
812 |
apply (subgoal_tac "vector [v$1, v$2, v$3] = v") |
|
813 |
apply simp |
|
814 |
apply (vector vector_def) |
|
815 |
apply (simp add: forall_3) |
|
816 |
done |
|
817 |
||
818 |
subsection%unimportant \<open>lambda skolemization on cartesian products\<close> |
|
819 |
||
820 |
lemma%important lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow> |
|
821 |
(\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs") |
|
822 |
proof%unimportant - |
|
823 |
let ?S = "(UNIV :: 'n set)" |
|
824 |
{ assume H: "?rhs" |
|
825 |
then have ?lhs by auto } |
|
826 |
moreover |
|
827 |
{ assume H: "?lhs" |
|
828 |
then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis |
|
829 |
let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n" |
|
830 |
{ fix i |
|
831 |
from f have "P i (f i)" by metis |
|
832 |
then have "P i (?x $ i)" by auto |
|
833 |
} |
|
834 |
hence "\<forall>i. P i (?x$i)" by metis |
|
835 |
hence ?rhs by metis } |
|
836 |
ultimately show ?thesis by metis |
|
837 |
qed |
|
838 |
||
839 |
||
840 |
text \<open>The same result in terms of square matrices.\<close> |
|
841 |
||
842 |
||
843 |
text \<open>Considering an n-element vector as an n-by-1 or 1-by-n matrix.\<close> |
|
844 |
||
845 |
definition%unimportant "rowvector v = (\<chi> i j. (v$j))" |
|
846 |
||
847 |
definition%unimportant "columnvector v = (\<chi> i j. (v$i))" |
|
848 |
||
849 |
lemma%unimportant transpose_columnvector: "transpose(columnvector v) = rowvector v" |
|
850 |
by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) |
|
851 |
||
852 |
lemma%unimportant transpose_rowvector: "transpose(rowvector v) = columnvector v" |
|
853 |
by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) |
|
854 |
||
855 |
lemma%unimportant dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" |
|
856 |
by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) |
|
857 |
||
858 |
lemma%unimportant dot_matrix_product: |
|
859 |
"(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" |
|
860 |
by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) |
|
861 |
||
862 |
lemma%unimportant dot_matrix_vector_mul: |
|
863 |
fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" |
|
864 |
shows "(A *v x) \<bullet> (B *v y) = |
|
865 |
(((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" |
|
866 |
unfolding dot_matrix_product transpose_columnvector[symmetric] |
|
867 |
dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. |
|
868 |
||
869 |
||
870 |
lemma%important dim_substandard_cart: "vec.dim {x::'a::field^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" |
|
871 |
(is "vec.dim ?A = _") |
|
872 |
proof%unimportant (rule vec.dim_unique) |
|
873 |
let ?B = "((\<lambda>x. axis x 1) ` d)" |
|
874 |
have subset_basis: "?B \<subseteq> cart_basis" |
|
875 |
by (auto simp: cart_basis_def) |
|
876 |
show "?B \<subseteq> ?A" |
|
877 |
by (auto simp: axis_def) |
|
878 |
show "vec.independent ((\<lambda>x. axis x 1) ` d)" |
|
879 |
using subset_basis |
|
880 |
by (rule vec.independent_mono[OF vec.independent_Basis]) |
|
881 |
have "x \<in> vec.span ?B" if "\<forall>i. i \<notin> d \<longrightarrow> x $ i = 0" for x::"'a^'n" |
|
882 |
proof - |
|
883 |
have "finite ?B" |
|
884 |
using subset_basis finite_cart_basis |
|
885 |
by (rule finite_subset) |
|
886 |
have "x = (\<Sum>i\<in>UNIV. x $ i *s axis i 1)" |
|
887 |
by (rule basis_expansion[symmetric]) |
|
888 |
also have "\<dots> = (\<Sum>i\<in>d. (x $ i) *s axis i 1)" |
|
889 |
by (rule sum.mono_neutral_cong_right) (auto simp: that) |
|
890 |
also have "\<dots> \<in> vec.span ?B" |
|
891 |
by (simp add: vec.span_sum vec.span_clauses) |
|
892 |
finally show "x \<in> vec.span ?B" . |
|
893 |
qed |
|
894 |
then show "?A \<subseteq> vec.span ?B" by auto |
|
895 |
qed (simp add: card_image inj_on_def axis_eq_axis) |
|
896 |
||
897 |
lemma%unimportant affinity_inverses: |
|
898 |
assumes m0: "m \<noteq> (0::'a::field)" |
|
899 |
shows "(\<lambda>x. m *s x + c) \<circ> (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id" |
|
900 |
"(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) \<circ> (\<lambda>x. m *s x + c) = id" |
|
901 |
using m0 |
|
902 |
by (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) |
|
903 |
||
904 |
lemma%important vector_affinity_eq: |
|
905 |
assumes m0: "(m::'a::field) \<noteq> 0" |
|
906 |
shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)" |
|
907 |
proof%unimportant |
|
908 |
assume h: "m *s x + c = y" |
|
909 |
hence "m *s x = y - c" by (simp add: field_simps) |
|
910 |
hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp |
|
911 |
then show "x = inverse m *s y + - (inverse m *s c)" |
|
912 |
using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
|
913 |
next |
|
914 |
assume h: "x = inverse m *s y + - (inverse m *s c)" |
|
915 |
show "m *s x + c = y" unfolding h |
|
916 |
using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
|
917 |
qed |
|
918 |
||
919 |
lemma%unimportant vector_eq_affinity: |
|
920 |
"(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)" |
|
921 |
using vector_affinity_eq[where m=m and x=x and y=y and c=c] |
|
922 |
by metis |
|
923 |
||
924 |
lemma%unimportant vector_cart: |
|
925 |
fixes f :: "real^'n \<Rightarrow> real" |
|
926 |
shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)" |
|
927 |
unfolding euclidean_eq_iff[where 'a="real^'n"] |
|
928 |
by simp (simp add: Basis_vec_def inner_axis) |
|
929 |
||
930 |
lemma%unimportant const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)" |
|
931 |
by (rule vector_cart) |
|
932 |
||
68072
493b818e8e10
added Johannes' generalizations Modules.thy and Vector_Spaces.thy; adapted HOL and HOL-Analysis accordingly
immler
parents:
diff
changeset
|
933 |
end |