author | immler |
Mon, 16 Dec 2013 17:08:22 +0100 | |
changeset 54776 | db890d9fc5c2 |
parent 54775 | 2d3df8633dad |
child 55522 | 23d2cbac6dce |
permissions | -rw-r--r-- |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1 |
header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
2 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
3 |
theory Cartesian_Euclidean_Space |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
4 |
imports Finite_Cartesian_Product Integration |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
5 |
begin |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
6 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
7 |
lemma delta_mult_idempotent: |
49644 | 8 |
"(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" |
9 |
by (cases "k=a") auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
10 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
11 |
lemma setsum_Plus: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
12 |
"\<lbrakk>finite A; finite B\<rbrakk> \<Longrightarrow> |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
13 |
(\<Sum>x\<in>A <+> B. g x) = (\<Sum>x\<in>A. g (Inl x)) + (\<Sum>x\<in>B. g (Inr x))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
14 |
unfolding Plus_def |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
15 |
by (subst setsum_Un_disjoint, auto simp add: setsum_reindex) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
16 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
17 |
lemma setsum_UNIV_sum: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
18 |
fixes g :: "'a::finite + 'b::finite \<Rightarrow> _" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
19 |
shows "(\<Sum>x\<in>UNIV. g x) = (\<Sum>x\<in>UNIV. g (Inl x)) + (\<Sum>x\<in>UNIV. g (Inr x))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
20 |
apply (subst UNIV_Plus_UNIV [symmetric]) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
21 |
apply (rule setsum_Plus [OF finite finite]) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
22 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
23 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
24 |
lemma setsum_mult_product: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
25 |
"setsum h {..<A * B :: nat} = (\<Sum>i\<in>{..<A}. \<Sum>j\<in>{..<B}. h (j + i * B))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
26 |
unfolding sumr_group[of h B A, unfolded atLeast0LessThan, symmetric] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
27 |
proof (rule setsum_cong, simp, rule setsum_reindex_cong) |
49644 | 28 |
fix i |
29 |
show "inj_on (\<lambda>j. j + i * B) {..<B}" by (auto intro!: inj_onI) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
30 |
show "{i * B..<i * B + B} = (\<lambda>j. j + i * B) ` {..<B}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
31 |
proof safe |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
32 |
fix j assume "j \<in> {i * B..<i * B + B}" |
49644 | 33 |
then show "j \<in> (\<lambda>j. j + i * B) ` {..<B}" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
34 |
by (auto intro!: image_eqI[of _ _ "j - i * B"]) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
35 |
qed simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
36 |
qed simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
37 |
|
49644 | 38 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
39 |
subsection{* Basic componentwise operations on vectors. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
40 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
41 |
instantiation vec :: (times, finite) times |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
42 |
begin |
49644 | 43 |
|
44 |
definition "op * \<equiv> (\<lambda> x y. (\<chi> i. (x$i) * (y$i)))" |
|
45 |
instance .. |
|
46 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
47 |
end |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
48 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
49 |
instantiation vec :: (one, finite) one |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
50 |
begin |
49644 | 51 |
|
52 |
definition "1 \<equiv> (\<chi> i. 1)" |
|
53 |
instance .. |
|
54 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
55 |
end |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
56 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
57 |
instantiation vec :: (ord, finite) ord |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
58 |
begin |
49644 | 59 |
|
60 |
definition "x \<le> y \<longleftrightarrow> (\<forall>i. x$i \<le> y$i)" |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
61 |
definition "x < (y::'a^'b) \<longleftrightarrow> x \<le> y \<and> \<not> y \<le> x" |
49644 | 62 |
instance .. |
63 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
64 |
end |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
65 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
66 |
text{* The ordering on one-dimensional vectors is linear. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
67 |
|
49197 | 68 |
class cart_one = |
69 |
assumes UNIV_one: "card (UNIV \<Colon> 'a set) = Suc 0" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
70 |
begin |
49197 | 71 |
|
72 |
subclass finite |
|
73 |
proof |
|
74 |
from UNIV_one show "finite (UNIV :: 'a set)" |
|
75 |
by (auto intro!: card_ge_0_finite) |
|
76 |
qed |
|
77 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
78 |
end |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
79 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
80 |
instance vec:: (order, finite) order |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
81 |
by default (auto simp: less_eq_vec_def less_vec_def vec_eq_iff |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
82 |
intro: order.trans order.antisym order.strict_implies_order) |
49197 | 83 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
84 |
instance vec :: (linorder, cart_one) linorder |
49197 | 85 |
proof |
86 |
obtain a :: 'b where all: "\<And>P. (\<forall>i. P i) \<longleftrightarrow> P a" |
|
87 |
proof - |
|
88 |
have "card (UNIV :: 'b set) = Suc 0" by (rule UNIV_one) |
|
89 |
then obtain b :: 'b where "UNIV = {b}" by (auto iff: card_Suc_eq) |
|
90 |
then have "\<And>P. (\<forall>i\<in>UNIV. P i) \<longleftrightarrow> P b" by auto |
|
91 |
then show thesis by (auto intro: that) |
|
92 |
qed |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
93 |
fix x y :: "'a^'b::cart_one" |
49197 | 94 |
note [simp] = less_eq_vec_def less_vec_def all vec_eq_iff field_simps |
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
95 |
show "x \<le> y \<or> y \<le> x" by auto |
49197 | 96 |
qed |
97 |
||
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
98 |
text{* Constant Vectors *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
99 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
100 |
definition "vec x = (\<chi> i. x)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
101 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
102 |
text{* Also the scalar-vector multiplication. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
103 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
104 |
definition vector_scalar_mult:: "'a::times \<Rightarrow> 'a ^ 'n \<Rightarrow> 'a ^ 'n" (infixl "*s" 70) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
105 |
where "c *s x = (\<chi> i. c * (x$i))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
106 |
|
49644 | 107 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
108 |
subsection {* A naive proof procedure to lift really trivial arithmetic stuff from the basis of the vector space. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
109 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
110 |
method_setup vector = {* |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
111 |
let |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
112 |
val ss1 = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
113 |
simpset_of (put_simpset HOL_basic_ss @{context} |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
114 |
addsimps [@{thm setsum_addf} RS sym, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
115 |
@{thm setsum_subtractf} RS sym, @{thm setsum_right_distrib}, |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
116 |
@{thm setsum_left_distrib}, @{thm setsum_negf} RS sym]) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
117 |
val ss2 = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
118 |
simpset_of (@{context} addsimps |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
119 |
[@{thm plus_vec_def}, @{thm times_vec_def}, |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
120 |
@{thm minus_vec_def}, @{thm uminus_vec_def}, |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
121 |
@{thm one_vec_def}, @{thm zero_vec_def}, @{thm vec_def}, |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
122 |
@{thm scaleR_vec_def}, |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
123 |
@{thm vec_lambda_beta}, @{thm vector_scalar_mult_def}]) |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
124 |
fun vector_arith_tac ctxt ths = |
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
125 |
simp_tac (put_simpset ss1 ctxt) |
49644 | 126 |
THEN' (fn i => rtac @{thm setsum_cong2} i |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
127 |
ORELSE rtac @{thm setsum_0'} i |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
128 |
ORELSE simp_tac (put_simpset HOL_basic_ss ctxt addsimps [@{thm vec_eq_iff}]) i) |
49644 | 129 |
(* THEN' TRY o clarify_tac HOL_cs THEN' (TRY o rtac @{thm iffI}) *) |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
130 |
THEN' asm_full_simp_tac (put_simpset ss2 ctxt addsimps ths) |
49644 | 131 |
in |
51717
9e7d1c139569
simplifier uses proper Proof.context instead of historic type simpset;
wenzelm
parents:
51641
diff
changeset
|
132 |
Attrib.thms >> (fn ths => fn ctxt => SIMPLE_METHOD' (vector_arith_tac ctxt ths)) |
49644 | 133 |
end |
42814 | 134 |
*} "lift trivial vector statements to real arith statements" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
135 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
136 |
lemma vec_0[simp]: "vec 0 = 0" by (vector zero_vec_def) |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
137 |
lemma vec_1[simp]: "vec 1 = 1" by (vector one_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
138 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
139 |
lemma vec_inj[simp]: "vec x = vec y \<longleftrightarrow> x = y" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
140 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
141 |
lemma vec_in_image_vec: "vec x \<in> (vec ` S) \<longleftrightarrow> x \<in> S" by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
142 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
143 |
lemma vec_add: "vec(x + y) = vec x + vec y" by (vector vec_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
144 |
lemma vec_sub: "vec(x - y) = vec x - vec y" by (vector vec_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
145 |
lemma vec_cmul: "vec(c * x) = c *s vec x " by (vector vec_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
146 |
lemma vec_neg: "vec(- x) = - vec x " by (vector vec_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
147 |
|
49644 | 148 |
lemma vec_setsum: |
149 |
assumes "finite S" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
150 |
shows "vec(setsum f S) = setsum (vec o f) S" |
49644 | 151 |
using assms |
152 |
proof induct |
|
153 |
case empty |
|
154 |
then show ?case by simp |
|
155 |
next |
|
156 |
case insert |
|
157 |
then show ?case by (auto simp add: vec_add) |
|
158 |
qed |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
159 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
160 |
text{* Obvious "component-pushing". *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
161 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
162 |
lemma vec_component [simp]: "vec x $ i = x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
163 |
by (vector vec_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
164 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
165 |
lemma vector_mult_component [simp]: "(x * y)$i = x$i * y$i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
166 |
by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
167 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
168 |
lemma vector_smult_component [simp]: "(c *s y)$i = c * (y$i)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
169 |
by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
170 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
171 |
lemma cond_component: "(if b then x else y)$i = (if b then x$i else y$i)" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
172 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
173 |
lemmas vector_component = |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
174 |
vec_component vector_add_component vector_mult_component |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
175 |
vector_smult_component vector_minus_component vector_uminus_component |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
176 |
vector_scaleR_component cond_component |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
177 |
|
49644 | 178 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
179 |
subsection {* Some frequently useful arithmetic lemmas over vectors. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
180 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
181 |
instance vec :: (semigroup_mult, finite) semigroup_mult |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
182 |
by default (vector mult_assoc) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
183 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
184 |
instance vec :: (monoid_mult, finite) monoid_mult |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
185 |
by default vector+ |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
186 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
187 |
instance vec :: (ab_semigroup_mult, finite) ab_semigroup_mult |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
188 |
by default (vector mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
189 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
190 |
instance vec :: (comm_monoid_mult, finite) comm_monoid_mult |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
191 |
by default vector |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
192 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
193 |
instance vec :: (semiring, finite) semiring |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
194 |
by default (vector field_simps)+ |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
195 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
196 |
instance vec :: (semiring_0, finite) semiring_0 |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
197 |
by default (vector field_simps)+ |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
198 |
instance vec :: (semiring_1, finite) semiring_1 |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
199 |
by default vector |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
200 |
instance vec :: (comm_semiring, finite) comm_semiring |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
201 |
by default (vector field_simps)+ |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
202 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
203 |
instance vec :: (comm_semiring_0, finite) comm_semiring_0 .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
204 |
instance vec :: (cancel_comm_monoid_add, finite) cancel_comm_monoid_add .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
205 |
instance vec :: (semiring_0_cancel, finite) semiring_0_cancel .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
206 |
instance vec :: (comm_semiring_0_cancel, finite) comm_semiring_0_cancel .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
207 |
instance vec :: (ring, finite) ring .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
208 |
instance vec :: (semiring_1_cancel, finite) semiring_1_cancel .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
209 |
instance vec :: (comm_semiring_1, finite) comm_semiring_1 .. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
210 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
211 |
instance vec :: (ring_1, finite) ring_1 .. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
212 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
213 |
instance vec :: (real_algebra, finite) real_algebra |
49644 | 214 |
by default (simp_all add: vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
215 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
216 |
instance vec :: (real_algebra_1, finite) real_algebra_1 .. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
217 |
|
49644 | 218 |
lemma of_nat_index: "(of_nat n :: 'a::semiring_1 ^'n)$i = of_nat n" |
219 |
proof (induct n) |
|
220 |
case 0 |
|
221 |
then show ?case by vector |
|
222 |
next |
|
223 |
case Suc |
|
224 |
then show ?case by vector |
|
225 |
qed |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
226 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
227 |
lemma one_index [simp]: "(1 :: 'a :: one ^ 'n) $ i = 1" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
228 |
by vector |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
229 |
|
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
230 |
lemma neg_one_index [simp]: "(- 1 :: 'a :: {one, uminus} ^ 'n) $ i = - 1" |
49644 | 231 |
by vector |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
232 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
233 |
instance vec :: (semiring_char_0, finite) semiring_char_0 |
38621
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37678
diff
changeset
|
234 |
proof |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37678
diff
changeset
|
235 |
fix m n :: nat |
d6cb7e625d75
more concise characterization of of_nat operation and class semiring_char_0
haftmann
parents:
37678
diff
changeset
|
236 |
show "inj (of_nat :: nat \<Rightarrow> 'a ^ 'b)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
237 |
by (auto intro!: injI simp add: vec_eq_iff of_nat_index) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
238 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
239 |
|
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
240 |
instance vec :: (numeral, finite) numeral .. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
241 |
instance vec :: (semiring_numeral, finite) semiring_numeral .. |
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
242 |
|
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
243 |
lemma numeral_index [simp]: "numeral w $ i = numeral w" |
49644 | 244 |
by (induct w) (simp_all only: numeral.simps vector_add_component one_index) |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
245 |
|
54489
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
246 |
lemma neg_numeral_index [simp]: "- numeral w $ i = - numeral w" |
03ff4d1e6784
eliminiated neg_numeral in favour of - (numeral _)
haftmann
parents:
54230
diff
changeset
|
247 |
by (simp only: vector_uminus_component numeral_index) |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
248 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
249 |
instance vec :: (comm_ring_1, finite) comm_ring_1 .. |
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
250 |
instance vec :: (ring_char_0, finite) ring_char_0 .. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
251 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
252 |
lemma vector_smult_assoc: "a *s (b *s x) = ((a::'a::semigroup_mult) * b) *s x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
253 |
by (vector mult_assoc) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
254 |
lemma vector_sadd_rdistrib: "((a::'a::semiring) + b) *s x = a *s x + b *s x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
255 |
by (vector field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
256 |
lemma vector_add_ldistrib: "(c::'a::semiring) *s (x + y) = c *s x + c *s y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
257 |
by (vector field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
258 |
lemma vector_smult_lzero[simp]: "(0::'a::mult_zero) *s x = 0" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
259 |
lemma vector_smult_lid[simp]: "(1::'a::monoid_mult) *s x = x" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
260 |
lemma vector_ssub_ldistrib: "(c::'a::ring) *s (x - y) = c *s x - c *s y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
261 |
by (vector field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
262 |
lemma vector_smult_rneg: "(c::'a::ring) *s -x = -(c *s x)" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
263 |
lemma vector_smult_lneg: "- (c::'a::ring) *s x = -(c *s x)" by vector |
47108
2a1953f0d20d
merged fork with new numeral representation (see NEWS)
huffman
parents:
45031
diff
changeset
|
264 |
lemma vector_sneg_minus1: "-x = (-1::'a::ring_1) *s x" by vector |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
265 |
lemma vector_smult_rzero[simp]: "c *s 0 = (0::'a::mult_zero ^ 'n)" by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
266 |
lemma vector_sub_rdistrib: "((a::'a::ring) - b) *s x = a *s x - b *s x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
267 |
by (vector field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
268 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
269 |
lemma vec_eq[simp]: "(vec m = vec n) \<longleftrightarrow> (m = n)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
270 |
by (simp add: vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
271 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
272 |
lemma norm_eq_0_imp: "norm x = 0 ==> x = (0::real ^'n)" by (metis norm_eq_zero) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
273 |
lemma vector_mul_eq_0[simp]: "(a *s x = 0) \<longleftrightarrow> a = (0::'a::idom) \<or> x = 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
274 |
by vector |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
275 |
lemma vector_mul_lcancel[simp]: "a *s x = a *s y \<longleftrightarrow> a = (0::real) \<or> x = y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
276 |
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_ssub_ldistrib) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
277 |
lemma vector_mul_rcancel[simp]: "a *s x = b *s x \<longleftrightarrow> (a::real) = b \<or> x = 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
278 |
by (metis eq_iff_diff_eq_0 vector_mul_eq_0 vector_sub_rdistrib) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
279 |
lemma vector_mul_lcancel_imp: "a \<noteq> (0::real) ==> a *s x = a *s y ==> (x = y)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
280 |
by (metis vector_mul_lcancel) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
281 |
lemma vector_mul_rcancel_imp: "x \<noteq> 0 \<Longrightarrow> (a::real) *s x = b *s x ==> a = b" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
282 |
by (metis vector_mul_rcancel) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
283 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
284 |
lemma component_le_norm_cart: "\<bar>x$i\<bar> <= norm x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
285 |
apply (simp add: norm_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
286 |
apply (rule member_le_setL2, simp_all) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
287 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
288 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
289 |
lemma norm_bound_component_le_cart: "norm x <= e ==> \<bar>x$i\<bar> <= e" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
290 |
by (metis component_le_norm_cart order_trans) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
291 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
292 |
lemma norm_bound_component_lt_cart: "norm x < e ==> \<bar>x$i\<bar> < e" |
53595 | 293 |
by (metis component_le_norm_cart le_less_trans) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
294 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
295 |
lemma norm_le_l1_cart: "norm x <= setsum(\<lambda>i. \<bar>x$i\<bar>) UNIV" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
296 |
by (simp add: norm_vec_def setL2_le_setsum) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
297 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
298 |
lemma scalar_mult_eq_scaleR: "c *s x = c *\<^sub>R x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
299 |
unfolding scaleR_vec_def vector_scalar_mult_def by simp |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
300 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
301 |
lemma dist_mul[simp]: "dist (c *s x) (c *s y) = \<bar>c\<bar> * dist x y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
302 |
unfolding dist_norm scalar_mult_eq_scaleR |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
303 |
unfolding scaleR_right_diff_distrib[symmetric] by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
304 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
305 |
lemma setsum_component [simp]: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
306 |
fixes f:: " 'a \<Rightarrow> ('b::comm_monoid_add) ^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
307 |
shows "(setsum f S)$i = setsum (\<lambda>x. (f x)$i) S" |
49644 | 308 |
proof (cases "finite S") |
309 |
case True |
|
310 |
then show ?thesis by induct simp_all |
|
311 |
next |
|
312 |
case False |
|
313 |
then show ?thesis by simp |
|
314 |
qed |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
315 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
316 |
lemma setsum_eq: "setsum f S = (\<chi> i. setsum (\<lambda>x. (f x)$i ) S)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
317 |
by (simp add: vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
318 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
319 |
lemma setsum_cmul: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
320 |
fixes f:: "'c \<Rightarrow> ('a::semiring_1)^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
321 |
shows "setsum (\<lambda>x. c *s f x) S = c *s setsum f S" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
322 |
by (simp add: vec_eq_iff setsum_right_distrib) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
323 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
324 |
lemma setsum_norm_allsubsets_bound_cart: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
325 |
fixes f:: "'a \<Rightarrow> real ^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
326 |
assumes fP: "finite P" and fPs: "\<And>Q. Q \<subseteq> P \<Longrightarrow> norm (setsum f Q) \<le> e" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
327 |
shows "setsum (\<lambda>x. norm (f x)) P \<le> 2 * real CARD('n) * e" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
328 |
using setsum_norm_allsubsets_bound[OF assms] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
329 |
by (simp add: DIM_cart Basis_real_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
330 |
|
54776
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
331 |
instantiation vec :: (ordered_euclidean_space, finite) ordered_euclidean_space |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
332 |
begin |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
333 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
334 |
definition "inf x y = (\<chi> i. inf (x $ i) (y $ i))" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
335 |
definition "sup x y = (\<chi> i. sup (x $ i) (y $ i))" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
336 |
definition "Inf X = (\<chi> i. (INF x:X. x $ i))" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
337 |
definition "Sup X = (\<chi> i. (SUP x:X. x $ i))" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
338 |
definition "abs x = (\<chi> i. abs (x $ i))" |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
339 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
340 |
instance |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
341 |
apply default |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
342 |
unfolding euclidean_representation_setsum' |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
343 |
apply (auto simp: less_eq_vec_def inf_vec_def sup_vec_def Inf_vec_def Sup_vec_def inner_axis |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
344 |
Basis_vec_def inner_Basis_inf_left inner_Basis_sup_left inner_Basis_INF_left |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
345 |
inner_Basis_SUP_left eucl_le[where 'a='a] less_le_not_le abs_vec_def abs_inner) |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
346 |
done |
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
347 |
|
db890d9fc5c2
ordered_euclidean_space compatible with more standard pointwise ordering on products; conditionally complete lattice with product order
immler
parents:
54775
diff
changeset
|
348 |
end |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
349 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
350 |
subsection {* Matrix operations *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
351 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
352 |
text{* Matrix notation. NB: an MxN matrix is of type @{typ "'a^'n^'m"}, not @{typ "'a^'m^'n"} *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
353 |
|
49644 | 354 |
definition matrix_matrix_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'p^'n \<Rightarrow> 'a ^ 'p ^'m" |
355 |
(infixl "**" 70) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
356 |
where "m ** m' == (\<chi> i j. setsum (\<lambda>k. ((m$i)$k) * ((m'$k)$j)) (UNIV :: 'n set)) ::'a ^ 'p ^'m" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
357 |
|
49644 | 358 |
definition matrix_vector_mult :: "('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n \<Rightarrow> 'a ^ 'm" |
359 |
(infixl "*v" 70) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
360 |
where "m *v x \<equiv> (\<chi> i. setsum (\<lambda>j. ((m$i)$j) * (x$j)) (UNIV ::'n set)) :: 'a^'m" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
361 |
|
49644 | 362 |
definition vector_matrix_mult :: "'a ^ 'm \<Rightarrow> ('a::semiring_1) ^'n^'m \<Rightarrow> 'a ^'n " |
363 |
(infixl "v*" 70) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
364 |
where "v v* m == (\<chi> j. setsum (\<lambda>i. ((m$i)$j) * (v$i)) (UNIV :: 'm set)) :: 'a^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
365 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
366 |
definition "(mat::'a::zero => 'a ^'n^'n) k = (\<chi> i j. if i = j then k else 0)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
367 |
definition transpose where |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
368 |
"(transpose::'a^'n^'m \<Rightarrow> 'a^'m^'n) A = (\<chi> i j. ((A$j)$i))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
369 |
definition "(row::'m => 'a ^'n^'m \<Rightarrow> 'a ^'n) i A = (\<chi> j. ((A$i)$j))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
370 |
definition "(column::'n =>'a^'n^'m =>'a^'m) j A = (\<chi> i. ((A$i)$j))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
371 |
definition "rows(A::'a^'n^'m) = { row i A | i. i \<in> (UNIV :: 'm set)}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
372 |
definition "columns(A::'a^'n^'m) = { column i A | i. i \<in> (UNIV :: 'n set)}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
373 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
374 |
lemma mat_0[simp]: "mat 0 = 0" by (vector mat_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
375 |
lemma matrix_add_ldistrib: "(A ** (B + C)) = (A ** B) + (A ** C)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
376 |
by (vector matrix_matrix_mult_def setsum_addf[symmetric] field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
377 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
378 |
lemma matrix_mul_lid: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
379 |
fixes A :: "'a::semiring_1 ^ 'm ^ 'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
380 |
shows "mat 1 ** A = A" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
381 |
apply (simp add: matrix_matrix_mult_def mat_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
382 |
apply vector |
49644 | 383 |
apply (auto simp only: if_distrib cond_application_beta setsum_delta'[OF finite] |
384 |
mult_1_left mult_zero_left if_True UNIV_I) |
|
385 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
386 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
387 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
388 |
lemma matrix_mul_rid: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
389 |
fixes A :: "'a::semiring_1 ^ 'm ^ 'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
390 |
shows "A ** mat 1 = A" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
391 |
apply (simp add: matrix_matrix_mult_def mat_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
392 |
apply vector |
49644 | 393 |
apply (auto simp only: if_distrib cond_application_beta setsum_delta[OF finite] |
394 |
mult_1_right mult_zero_right if_True UNIV_I cong: if_cong) |
|
395 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
396 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
397 |
lemma matrix_mul_assoc: "A ** (B ** C) = (A ** B) ** C" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
398 |
apply (vector matrix_matrix_mult_def setsum_right_distrib setsum_left_distrib mult_assoc) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
399 |
apply (subst setsum_commute) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
400 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
401 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
402 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
403 |
lemma matrix_vector_mul_assoc: "A *v (B *v x) = (A ** B) *v x" |
49644 | 404 |
apply (vector matrix_matrix_mult_def matrix_vector_mult_def |
405 |
setsum_right_distrib setsum_left_distrib mult_assoc) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
406 |
apply (subst setsum_commute) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
407 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
408 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
409 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
410 |
lemma matrix_vector_mul_lid: "mat 1 *v x = (x::'a::semiring_1 ^ 'n)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
411 |
apply (vector matrix_vector_mult_def mat_def) |
49644 | 412 |
apply (simp add: if_distrib cond_application_beta setsum_delta' cong del: if_weak_cong) |
413 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
414 |
|
49644 | 415 |
lemma matrix_transpose_mul: |
416 |
"transpose(A ** B) = transpose B ** transpose (A::'a::comm_semiring_1^_^_)" |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
417 |
by (simp add: matrix_matrix_mult_def transpose_def vec_eq_iff mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
418 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
419 |
lemma matrix_eq: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
420 |
fixes A B :: "'a::semiring_1 ^ 'n ^ 'm" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
421 |
shows "A = B \<longleftrightarrow> (\<forall>x. A *v x = B *v x)" (is "?lhs \<longleftrightarrow> ?rhs") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
422 |
apply auto |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
423 |
apply (subst vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
424 |
apply clarify |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
425 |
apply (clarsimp simp add: matrix_vector_mult_def if_distrib cond_application_beta vec_eq_iff cong del: if_weak_cong) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
426 |
apply (erule_tac x="axis ia 1" in allE) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
427 |
apply (erule_tac x="i" in allE) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
428 |
apply (auto simp add: if_distrib cond_application_beta axis_def |
49644 | 429 |
setsum_delta[OF finite] cong del: if_weak_cong) |
430 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
431 |
|
49644 | 432 |
lemma matrix_vector_mul_component: "((A::real^_^_) *v x)$k = (A$k) \<bullet> x" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
433 |
by (simp add: matrix_vector_mult_def inner_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
434 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
435 |
lemma dot_lmul_matrix: "((x::real ^_) v* A) \<bullet> y = x \<bullet> (A *v y)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
436 |
apply (simp add: inner_vec_def matrix_vector_mult_def vector_matrix_mult_def setsum_left_distrib setsum_right_distrib mult_ac) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
437 |
apply (subst setsum_commute) |
49644 | 438 |
apply simp |
439 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
440 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
441 |
lemma transpose_mat: "transpose (mat n) = mat n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
442 |
by (vector transpose_def mat_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
443 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
444 |
lemma transpose_transpose: "transpose(transpose A) = A" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
445 |
by (vector transpose_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
446 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
447 |
lemma row_transpose: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
448 |
fixes A:: "'a::semiring_1^_^_" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
449 |
shows "row i (transpose A) = column i A" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
450 |
by (simp add: row_def column_def transpose_def vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
451 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
452 |
lemma column_transpose: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
453 |
fixes A:: "'a::semiring_1^_^_" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
454 |
shows "column i (transpose A) = row i A" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
455 |
by (simp add: row_def column_def transpose_def vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
456 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
457 |
lemma rows_transpose: "rows(transpose (A::'a::semiring_1^_^_)) = columns A" |
49644 | 458 |
by (auto simp add: rows_def columns_def row_transpose intro: set_eqI) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
459 |
|
49644 | 460 |
lemma columns_transpose: "columns(transpose (A::'a::semiring_1^_^_)) = rows A" |
461 |
by (metis transpose_transpose rows_transpose) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
462 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
463 |
text{* Two sometimes fruitful ways of looking at matrix-vector multiplication. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
464 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
465 |
lemma matrix_mult_dot: "A *v x = (\<chi> i. A$i \<bullet> x)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
466 |
by (simp add: matrix_vector_mult_def inner_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
467 |
|
49644 | 468 |
lemma matrix_mult_vsum: |
469 |
"(A::'a::comm_semiring_1^'n^'m) *v x = setsum (\<lambda>i. (x$i) *s column i A) (UNIV:: 'n set)" |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
470 |
by (simp add: matrix_vector_mult_def vec_eq_iff column_def mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
471 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
472 |
lemma vector_componentwise: |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
473 |
"(x::'a::ring_1^'n) = (\<chi> j. \<Sum>i\<in>UNIV. (x$i) * (axis i 1 :: 'a^'n) $ j)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
474 |
by (simp add: axis_def if_distrib setsum_cases vec_eq_iff) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
475 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
476 |
lemma basis_expansion: "setsum (\<lambda>i. (x$i) *s axis i 1) UNIV = (x::('a::ring_1) ^'n)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
477 |
by (auto simp add: axis_def vec_eq_iff if_distrib setsum_cases cong del: if_weak_cong) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
478 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
479 |
lemma linear_componentwise: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
480 |
fixes f:: "real ^'m \<Rightarrow> real ^ _" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
481 |
assumes lf: "linear f" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
482 |
shows "(f x)$j = setsum (\<lambda>i. (x$i) * (f (axis i 1)$j)) (UNIV :: 'm set)" (is "?lhs = ?rhs") |
49644 | 483 |
proof - |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
484 |
let ?M = "(UNIV :: 'm set)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
485 |
let ?N = "(UNIV :: 'n set)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
486 |
have fM: "finite ?M" by simp |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
487 |
have "?rhs = (setsum (\<lambda>i.(x$i) *\<^sub>R f (axis i 1) ) ?M)$j" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
488 |
unfolding setsum_component by simp |
49644 | 489 |
then show ?thesis |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
490 |
unfolding linear_setsum_mul[OF lf fM, symmetric] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
491 |
unfolding scalar_mult_eq_scaleR[symmetric] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
492 |
unfolding basis_expansion |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
493 |
by simp |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
494 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
495 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
496 |
text{* Inverse matrices (not necessarily square) *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
497 |
|
49644 | 498 |
definition |
499 |
"invertible(A::'a::semiring_1^'n^'m) \<longleftrightarrow> (\<exists>A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
500 |
|
49644 | 501 |
definition |
502 |
"matrix_inv(A:: 'a::semiring_1^'n^'m) = |
|
503 |
(SOME A'::'a^'m^'n. A ** A' = mat 1 \<and> A' ** A = mat 1)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
504 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
505 |
text{* Correspondence between matrices and linear operators. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
506 |
|
49644 | 507 |
definition matrix :: "('a::{plus,times, one, zero}^'m \<Rightarrow> 'a ^ 'n) \<Rightarrow> 'a^'m^'n" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
508 |
where "matrix f = (\<chi> i j. (f(axis j 1))$i)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
509 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
510 |
lemma matrix_vector_mul_linear: "linear(\<lambda>x. A *v (x::real ^ _))" |
53600
8fda7ad57466
make 'linear' into a sublocale of 'bounded_linear';
huffman
parents:
53595
diff
changeset
|
511 |
by (simp add: linear_iff matrix_vector_mult_def vec_eq_iff |
49644 | 512 |
field_simps setsum_right_distrib setsum_addf) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
513 |
|
49644 | 514 |
lemma matrix_works: |
515 |
assumes lf: "linear f" |
|
516 |
shows "matrix f *v x = f (x::real ^ 'n)" |
|
517 |
apply (simp add: matrix_def matrix_vector_mult_def vec_eq_iff mult_commute) |
|
518 |
apply clarify |
|
519 |
apply (rule linear_componentwise[OF lf, symmetric]) |
|
520 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
521 |
|
49644 | 522 |
lemma matrix_vector_mul: "linear f ==> f = (\<lambda>x. matrix f *v (x::real ^ 'n))" |
523 |
by (simp add: ext matrix_works) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
524 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
525 |
lemma matrix_of_matrix_vector_mul: "matrix(\<lambda>x. A *v (x :: real ^ 'n)) = A" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
526 |
by (simp add: matrix_eq matrix_vector_mul_linear matrix_works) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
527 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
528 |
lemma matrix_compose: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
529 |
assumes lf: "linear (f::real^'n \<Rightarrow> real^'m)" |
49644 | 530 |
and lg: "linear (g::real^'m \<Rightarrow> real^_)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
531 |
shows "matrix (g o f) = matrix g ** matrix f" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
532 |
using lf lg linear_compose[OF lf lg] matrix_works[OF linear_compose[OF lf lg]] |
49644 | 533 |
by (simp add: matrix_eq matrix_works matrix_vector_mul_assoc[symmetric] o_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
534 |
|
49644 | 535 |
lemma matrix_vector_column: |
536 |
"(A::'a::comm_semiring_1^'n^_) *v x = setsum (\<lambda>i. (x$i) *s ((transpose A)$i)) (UNIV:: 'n set)" |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
537 |
by (simp add: matrix_vector_mult_def transpose_def vec_eq_iff mult_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
538 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
539 |
lemma adjoint_matrix: "adjoint(\<lambda>x. (A::real^'n^'m) *v x) = (\<lambda>x. transpose A *v x)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
540 |
apply (rule adjoint_unique) |
49644 | 541 |
apply (simp add: transpose_def inner_vec_def matrix_vector_mult_def |
542 |
setsum_left_distrib setsum_right_distrib) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
543 |
apply (subst setsum_commute) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
544 |
apply (auto simp add: mult_ac) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
545 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
546 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
547 |
lemma matrix_adjoint: assumes lf: "linear (f :: real^'n \<Rightarrow> real ^'m)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
548 |
shows "matrix(adjoint f) = transpose(matrix f)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
549 |
apply (subst matrix_vector_mul[OF lf]) |
49644 | 550 |
unfolding adjoint_matrix matrix_of_matrix_vector_mul |
551 |
apply rule |
|
552 |
done |
|
553 |
||
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
554 |
|
44360 | 555 |
subsection {* lambda skolemization on cartesian products *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
556 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
557 |
(* FIXME: rename do choice_cart *) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
558 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
559 |
lemma lambda_skolem: "(\<forall>i. \<exists>x. P i x) \<longleftrightarrow> |
37494 | 560 |
(\<exists>x::'a ^ 'n. \<forall>i. P i (x $ i))" (is "?lhs \<longleftrightarrow> ?rhs") |
49644 | 561 |
proof - |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
562 |
let ?S = "(UNIV :: 'n set)" |
49644 | 563 |
{ assume H: "?rhs" |
564 |
then have ?lhs by auto } |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
565 |
moreover |
49644 | 566 |
{ assume H: "?lhs" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
567 |
then obtain f where f:"\<forall>i. P i (f i)" unfolding choice_iff by metis |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
568 |
let ?x = "(\<chi> i. (f i)) :: 'a ^ 'n" |
49644 | 569 |
{ fix i |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
570 |
from f have "P i (f i)" by metis |
37494 | 571 |
then have "P i (?x $ i)" by auto |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
572 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
573 |
hence "\<forall>i. P i (?x$i)" by metis |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
574 |
hence ?rhs by metis } |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
575 |
ultimately show ?thesis by metis |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
576 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
577 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
578 |
lemma vector_sub_project_orthogonal_cart: "(b::real^'n) \<bullet> (x - ((b \<bullet> x) / (b \<bullet> b)) *s b) = 0" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
579 |
unfolding inner_simps scalar_mult_eq_scaleR by auto |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
580 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
581 |
lemma left_invertible_transpose: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
582 |
"(\<exists>(B). B ** transpose (A) = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). A ** B = mat 1)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
583 |
by (metis matrix_transpose_mul transpose_mat transpose_transpose) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
584 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
585 |
lemma right_invertible_transpose: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
586 |
"(\<exists>(B). transpose (A) ** B = mat (1::'a::comm_semiring_1)) \<longleftrightarrow> (\<exists>(B). B ** A = mat 1)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
587 |
by (metis matrix_transpose_mul transpose_mat transpose_transpose) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
588 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
589 |
lemma matrix_left_invertible_injective: |
49644 | 590 |
"(\<exists>B. (B::real^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x y. A *v x = A *v y \<longrightarrow> x = y)" |
591 |
proof - |
|
592 |
{ fix B:: "real^'m^'n" and x y assume B: "B ** A = mat 1" and xy: "A *v x = A*v y" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
593 |
from xy have "B*v (A *v x) = B *v (A*v y)" by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
594 |
hence "x = y" |
49644 | 595 |
unfolding matrix_vector_mul_assoc B matrix_vector_mul_lid . } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
596 |
moreover |
49644 | 597 |
{ assume A: "\<forall>x y. A *v x = A *v y \<longrightarrow> x = y" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
598 |
hence i: "inj (op *v A)" unfolding inj_on_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
599 |
from linear_injective_left_inverse[OF matrix_vector_mul_linear i] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
600 |
obtain g where g: "linear g" "g o op *v A = id" by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
601 |
have "matrix g ** A = mat 1" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
602 |
unfolding matrix_eq matrix_vector_mul_lid matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] |
44165 | 603 |
using g(2) by (simp add: fun_eq_iff) |
49644 | 604 |
then have "\<exists>B. (B::real ^'m^'n) ** A = mat 1" by blast } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
605 |
ultimately show ?thesis by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
606 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
607 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
608 |
lemma matrix_left_invertible_ker: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
609 |
"(\<exists>B. (B::real ^'m^'n) ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> (\<forall>x. A *v x = 0 \<longrightarrow> x = 0)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
610 |
unfolding matrix_left_invertible_injective |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
611 |
using linear_injective_0[OF matrix_vector_mul_linear, of A] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
612 |
by (simp add: inj_on_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
613 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
614 |
lemma matrix_right_invertible_surjective: |
49644 | 615 |
"(\<exists>B. (A::real^'n^'m) ** (B::real^'m^'n) = mat 1) \<longleftrightarrow> surj (\<lambda>x. A *v x)" |
616 |
proof - |
|
617 |
{ fix B :: "real ^'m^'n" |
|
618 |
assume AB: "A ** B = mat 1" |
|
619 |
{ fix x :: "real ^ 'm" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
620 |
have "A *v (B *v x) = x" |
49644 | 621 |
by (simp add: matrix_vector_mul_lid matrix_vector_mul_assoc AB) } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
622 |
hence "surj (op *v A)" unfolding surj_def by metis } |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
623 |
moreover |
49644 | 624 |
{ assume sf: "surj (op *v A)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
625 |
from linear_surjective_right_inverse[OF matrix_vector_mul_linear sf] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
626 |
obtain g:: "real ^'m \<Rightarrow> real ^'n" where g: "linear g" "op *v A o g = id" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
627 |
by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
628 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
629 |
have "A ** (matrix g) = mat 1" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
630 |
unfolding matrix_eq matrix_vector_mul_lid |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
631 |
matrix_vector_mul_assoc[symmetric] matrix_works[OF g(1)] |
44165 | 632 |
using g(2) unfolding o_def fun_eq_iff id_def |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
633 |
. |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
634 |
hence "\<exists>B. A ** (B::real^'m^'n) = mat 1" by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
635 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
636 |
ultimately show ?thesis unfolding surj_def by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
637 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
638 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
639 |
lemma matrix_left_invertible_independent_columns: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
640 |
fixes A :: "real^'n^'m" |
49644 | 641 |
shows "(\<exists>(B::real ^'m^'n). B ** A = mat 1) \<longleftrightarrow> |
642 |
(\<forall>c. setsum (\<lambda>i. c i *s column i A) (UNIV :: 'n set) = 0 \<longrightarrow> (\<forall>i. c i = 0))" |
|
643 |
(is "?lhs \<longleftrightarrow> ?rhs") |
|
644 |
proof - |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
645 |
let ?U = "UNIV :: 'n set" |
49644 | 646 |
{ assume k: "\<forall>x. A *v x = 0 \<longrightarrow> x = 0" |
647 |
{ fix c i |
|
648 |
assume c: "setsum (\<lambda>i. c i *s column i A) ?U = 0" and i: "i \<in> ?U" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
649 |
let ?x = "\<chi> i. c i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
650 |
have th0:"A *v ?x = 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
651 |
using c |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
652 |
unfolding matrix_mult_vsum vec_eq_iff |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
653 |
by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
654 |
from k[rule_format, OF th0] i |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
655 |
have "c i = 0" by (vector vec_eq_iff)} |
49644 | 656 |
hence ?rhs by blast } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
657 |
moreover |
49644 | 658 |
{ assume H: ?rhs |
659 |
{ fix x assume x: "A *v x = 0" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
660 |
let ?c = "\<lambda>i. ((x$i ):: real)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
661 |
from H[rule_format, of ?c, unfolded matrix_mult_vsum[symmetric], OF x] |
49644 | 662 |
have "x = 0" by vector } |
663 |
} |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
664 |
ultimately show ?thesis unfolding matrix_left_invertible_ker by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
665 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
666 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
667 |
lemma matrix_right_invertible_independent_rows: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
668 |
fixes A :: "real^'n^'m" |
49644 | 669 |
shows "(\<exists>(B::real^'m^'n). A ** B = mat 1) \<longleftrightarrow> |
670 |
(\<forall>c. setsum (\<lambda>i. c i *s row i A) (UNIV :: 'm set) = 0 \<longrightarrow> (\<forall>i. c i = 0))" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
671 |
unfolding left_invertible_transpose[symmetric] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
672 |
matrix_left_invertible_independent_columns |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
673 |
by (simp add: column_transpose) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
674 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
675 |
lemma matrix_right_invertible_span_columns: |
49644 | 676 |
"(\<exists>(B::real ^'n^'m). (A::real ^'m^'n) ** B = mat 1) \<longleftrightarrow> |
677 |
span (columns A) = UNIV" (is "?lhs = ?rhs") |
|
678 |
proof - |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
679 |
let ?U = "UNIV :: 'm set" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
680 |
have fU: "finite ?U" by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
681 |
have lhseq: "?lhs \<longleftrightarrow> (\<forall>y. \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
682 |
unfolding matrix_right_invertible_surjective matrix_mult_vsum surj_def |
49644 | 683 |
apply (subst eq_commute) |
684 |
apply rule |
|
685 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
686 |
have rhseq: "?rhs \<longleftrightarrow> (\<forall>x. x \<in> span (columns A))" by blast |
49644 | 687 |
{ assume h: ?lhs |
688 |
{ fix x:: "real ^'n" |
|
689 |
from h[unfolded lhseq, rule_format, of x] obtain y :: "real ^'m" |
|
690 |
where y: "setsum (\<lambda>i. (y$i) *s column i A) ?U = x" by blast |
|
691 |
have "x \<in> span (columns A)" |
|
692 |
unfolding y[symmetric] |
|
693 |
apply (rule span_setsum[OF fU]) |
|
694 |
apply clarify |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
695 |
unfolding scalar_mult_eq_scaleR |
49644 | 696 |
apply (rule span_mul) |
697 |
apply (rule span_superset) |
|
698 |
unfolding columns_def |
|
699 |
apply blast |
|
700 |
done |
|
701 |
} |
|
702 |
then have ?rhs unfolding rhseq by blast } |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
703 |
moreover |
49644 | 704 |
{ assume h:?rhs |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
705 |
let ?P = "\<lambda>(y::real ^'n). \<exists>(x::real^'m). setsum (\<lambda>i. (x$i) *s column i A) ?U = y" |
49644 | 706 |
{ fix y |
707 |
have "?P y" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
708 |
proof (rule span_induct_alt[of ?P "columns A", folded scalar_mult_eq_scaleR]) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
709 |
show "\<exists>x\<Colon>real ^ 'm. setsum (\<lambda>i. (x$i) *s column i A) ?U = 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
710 |
by (rule exI[where x=0], simp) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
711 |
next |
49644 | 712 |
fix c y1 y2 |
713 |
assume y1: "y1 \<in> columns A" and y2: "?P y2" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
714 |
from y1 obtain i where i: "i \<in> ?U" "y1 = column i A" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
715 |
unfolding columns_def by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
716 |
from y2 obtain x:: "real ^'m" where |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
717 |
x: "setsum (\<lambda>i. (x$i) *s column i A) ?U = y2" by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
718 |
let ?x = "(\<chi> j. if j = i then c + (x$i) else (x$j))::real^'m" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
719 |
show "?P (c*s y1 + y2)" |
49962
a8cc904a6820
Renamed {left,right}_distrib to distrib_{right,left}.
webertj
parents:
49644
diff
changeset
|
720 |
proof (rule exI[where x= "?x"], vector, auto simp add: i x[symmetric] if_distrib distrib_left cond_application_beta cong del: if_weak_cong) |
49644 | 721 |
fix j |
722 |
have th: "\<forall>xa \<in> ?U. (if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
723 |
else (x$xa) * ((column xa A$j))) = (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))" |
|
724 |
using i(1) by (simp add: field_simps) |
|
725 |
have "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
726 |
else (x$xa) * ((column xa A$j))) ?U = setsum (\<lambda>xa. (if xa = i then c * ((column i A)$j) else 0) + ((x$xa) * ((column xa A)$j))) ?U" |
|
727 |
apply (rule setsum_cong[OF refl]) |
|
728 |
using th apply blast |
|
729 |
done |
|
730 |
also have "\<dots> = setsum (\<lambda>xa. if xa = i then c * ((column i A)$j) else 0) ?U + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" |
|
731 |
by (simp add: setsum_addf) |
|
732 |
also have "\<dots> = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" |
|
733 |
unfolding setsum_delta[OF fU] |
|
734 |
using i(1) by simp |
|
735 |
finally show "setsum (\<lambda>xa. if xa = i then (c + (x$i)) * ((column xa A)$j) |
|
736 |
else (x$xa) * ((column xa A$j))) ?U = c * ((column i A)$j) + setsum (\<lambda>xa. ((x$xa) * ((column xa A)$j))) ?U" . |
|
737 |
qed |
|
738 |
next |
|
739 |
show "y \<in> span (columns A)" |
|
740 |
unfolding h by blast |
|
741 |
qed |
|
742 |
} |
|
743 |
then have ?lhs unfolding lhseq .. |
|
744 |
} |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
745 |
ultimately show ?thesis by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
746 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
747 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
748 |
lemma matrix_left_invertible_span_rows: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
749 |
"(\<exists>(B::real^'m^'n). B ** (A::real^'n^'m) = mat 1) \<longleftrightarrow> span (rows A) = UNIV" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
750 |
unfolding right_invertible_transpose[symmetric] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
751 |
unfolding columns_transpose[symmetric] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
752 |
unfolding matrix_right_invertible_span_columns |
49644 | 753 |
.. |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
754 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
755 |
text {* The same result in terms of square matrices. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
756 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
757 |
lemma matrix_left_right_inverse: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
758 |
fixes A A' :: "real ^'n^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
759 |
shows "A ** A' = mat 1 \<longleftrightarrow> A' ** A = mat 1" |
49644 | 760 |
proof - |
761 |
{ fix A A' :: "real ^'n^'n" |
|
762 |
assume AA': "A ** A' = mat 1" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
763 |
have sA: "surj (op *v A)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
764 |
unfolding surj_def |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
765 |
apply clarify |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
766 |
apply (rule_tac x="(A' *v y)" in exI) |
49644 | 767 |
apply (simp add: matrix_vector_mul_assoc AA' matrix_vector_mul_lid) |
768 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
769 |
from linear_surjective_isomorphism[OF matrix_vector_mul_linear sA] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
770 |
obtain f' :: "real ^'n \<Rightarrow> real ^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
771 |
where f': "linear f'" "\<forall>x. f' (A *v x) = x" "\<forall>x. A *v f' x = x" by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
772 |
have th: "matrix f' ** A = mat 1" |
49644 | 773 |
by (simp add: matrix_eq matrix_works[OF f'(1)] |
774 |
matrix_vector_mul_assoc[symmetric] matrix_vector_mul_lid f'(2)[rule_format]) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
775 |
hence "(matrix f' ** A) ** A' = mat 1 ** A'" by simp |
49644 | 776 |
hence "matrix f' = A'" |
777 |
by (simp add: matrix_mul_assoc[symmetric] AA' matrix_mul_rid matrix_mul_lid) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
778 |
hence "matrix f' ** A = A' ** A" by simp |
49644 | 779 |
hence "A' ** A = mat 1" by (simp add: th) |
780 |
} |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
781 |
then show ?thesis by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
782 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
783 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
784 |
text {* Considering an n-element vector as an n-by-1 or 1-by-n matrix. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
785 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
786 |
definition "rowvector v = (\<chi> i j. (v$j))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
787 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
788 |
definition "columnvector v = (\<chi> i j. (v$i))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
789 |
|
49644 | 790 |
lemma transpose_columnvector: "transpose(columnvector v) = rowvector v" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
791 |
by (simp add: transpose_def rowvector_def columnvector_def vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
792 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
793 |
lemma transpose_rowvector: "transpose(rowvector v) = columnvector v" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
794 |
by (simp add: transpose_def columnvector_def rowvector_def vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
795 |
|
49644 | 796 |
lemma dot_rowvector_columnvector: "columnvector (A *v v) = A ** columnvector v" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
797 |
by (vector columnvector_def matrix_matrix_mult_def matrix_vector_mult_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
798 |
|
49644 | 799 |
lemma dot_matrix_product: |
800 |
"(x::real^'n) \<bullet> y = (((rowvector x ::real^'n^1) ** (columnvector y :: real^1^'n))$1)$1" |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
801 |
by (vector matrix_matrix_mult_def rowvector_def columnvector_def inner_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
802 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
803 |
lemma dot_matrix_vector_mul: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
804 |
fixes A B :: "real ^'n ^'n" and x y :: "real ^'n" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
805 |
shows "(A *v x) \<bullet> (B *v y) = |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
806 |
(((rowvector x :: real^'n^1) ** ((transpose A ** B) ** (columnvector y :: real ^1^'n)))$1)$1" |
49644 | 807 |
unfolding dot_matrix_product transpose_columnvector[symmetric] |
808 |
dot_rowvector_columnvector matrix_transpose_mul matrix_mul_assoc .. |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
809 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
810 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
811 |
lemma infnorm_cart:"infnorm (x::real^'n) = Sup {abs(x$i) |i. i\<in>UNIV}" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
812 |
by (simp add: infnorm_def inner_axis Basis_vec_def) (metis (lifting) inner_axis real_inner_1_right) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
813 |
|
49644 | 814 |
lemma component_le_infnorm_cart: "\<bar>x$i\<bar> \<le> infnorm (x::real^'n)" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
815 |
using Basis_le_infnorm[of "axis i 1" x] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
816 |
by (simp add: Basis_vec_def axis_eq_axis inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
817 |
|
49644 | 818 |
lemma continuous_component: "continuous F f \<Longrightarrow> continuous F (\<lambda>x. f x $ i)" |
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44571
diff
changeset
|
819 |
unfolding continuous_def by (rule tendsto_vec_nth) |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
820 |
|
49644 | 821 |
lemma continuous_on_component: "continuous_on s f \<Longrightarrow> continuous_on s (\<lambda>x. f x $ i)" |
44647
e4de7750cdeb
modernize lemmas about 'continuous' and 'continuous_on';
huffman
parents:
44571
diff
changeset
|
822 |
unfolding continuous_on_def by (fast intro: tendsto_vec_nth) |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
823 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
824 |
lemma closed_positive_orthant: "closed {x::real^'n. \<forall>i. 0 \<le>x$i}" |
44233 | 825 |
by (simp add: Collect_all_eq closed_INT closed_Collect_le) |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
826 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
827 |
lemma bounded_component_cart: "bounded s \<Longrightarrow> bounded ((\<lambda>x. x $ i) ` s)" |
49644 | 828 |
unfolding bounded_def |
829 |
apply clarify |
|
830 |
apply (rule_tac x="x $ i" in exI) |
|
831 |
apply (rule_tac x="e" in exI) |
|
832 |
apply clarify |
|
833 |
apply (rule order_trans [OF dist_vec_nth_le], simp) |
|
834 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
835 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
836 |
lemma compact_lemma_cart: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
837 |
fixes f :: "nat \<Rightarrow> 'a::heine_borel ^ 'n" |
50998 | 838 |
assumes f: "bounded (range f)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
839 |
shows "\<forall>d. |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
840 |
\<exists>l r. subseq r \<and> |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
841 |
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
842 |
proof |
49644 | 843 |
fix d :: "'n set" |
844 |
have "finite d" by simp |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
845 |
thus "\<exists>l::'a ^ 'n. \<exists>r. subseq r \<and> |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
846 |
(\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r n) $ i) (l $ i) < e) sequentially)" |
49644 | 847 |
proof (induct d) |
848 |
case empty |
|
849 |
thus ?case unfolding subseq_def by auto |
|
850 |
next |
|
851 |
case (insert k d) |
|
852 |
obtain l1::"'a^'n" and r1 where r1:"subseq r1" |
|
853 |
and lr1:"\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
854 |
using insert(3) by auto |
50998 | 855 |
have s': "bounded ((\<lambda>x. x $ k) ` range f)" using `bounded (range f)` |
856 |
by (auto intro!: bounded_component_cart) |
|
857 |
have f': "\<forall>n. f (r1 n) $ k \<in> (\<lambda>x. x $ k) ` range f" by simp |
|
858 |
have "bounded (range (\<lambda>i. f (r1 i) $ k))" |
|
859 |
by (metis (lifting) bounded_subset image_subsetI f' s') |
|
860 |
then obtain l2 r2 where r2: "subseq r2" |
|
49644 | 861 |
and lr2: "((\<lambda>i. f (r1 (r2 i)) $ k) ---> l2) sequentially" |
50998 | 862 |
using bounded_imp_convergent_subsequence[of "\<lambda>i. f (r1 i) $ k"] by (auto simp: o_def) |
49644 | 863 |
def r \<equiv> "r1 \<circ> r2" |
864 |
have r: "subseq r" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
865 |
using r1 and r2 unfolding r_def o_def subseq_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
866 |
moreover |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
867 |
def l \<equiv> "(\<chi> i. if i = k then l2 else l1$i)::'a^'n" |
49644 | 868 |
{ fix e :: real assume "e > 0" |
869 |
from lr1 `e>0` have N1:"eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 n) $ i) (l1 $ i) < e) sequentially" |
|
870 |
by blast |
|
871 |
from lr2 `e>0` have N2:"eventually (\<lambda>n. dist (f (r1 (r2 n)) $ k) l2 < e) sequentially" |
|
872 |
by (rule tendstoD) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
873 |
from r2 N1 have N1': "eventually (\<lambda>n. \<forall>i\<in>d. dist (f (r1 (r2 n)) $ i) (l1 $ i) < e) sequentially" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
874 |
by (rule eventually_subseq) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
875 |
have "eventually (\<lambda>n. \<forall>i\<in>(insert k d). dist (f (r n) $ i) (l $ i) < e) sequentially" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
876 |
using N1' N2 by (rule eventually_elim2, simp add: l_def r_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
877 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
878 |
ultimately show ?case by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
879 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
880 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
881 |
|
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
882 |
instance vec :: (heine_borel, finite) heine_borel |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
883 |
proof |
50998 | 884 |
fix f :: "nat \<Rightarrow> 'a ^ 'b" |
885 |
assume f: "bounded (range f)" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
886 |
then obtain l r where r: "subseq r" |
49644 | 887 |
and l: "\<forall>e>0. eventually (\<lambda>n. \<forall>i\<in>UNIV. dist (f (r n) $ i) (l $ i) < e) sequentially" |
50998 | 888 |
using compact_lemma_cart [OF f] by blast |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
889 |
let ?d = "UNIV::'b set" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
890 |
{ fix e::real assume "e>0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
891 |
hence "0 < e / (real_of_nat (card ?d))" |
49644 | 892 |
using zero_less_card_finite divide_pos_pos[of e, of "real_of_nat (card ?d)"] by auto |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
893 |
with l have "eventually (\<lambda>n. \<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))) sequentially" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
894 |
by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
895 |
moreover |
49644 | 896 |
{ fix n |
897 |
assume n: "\<forall>i. dist (f (r n) $ i) (l $ i) < e / (real_of_nat (card ?d))" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
898 |
have "dist (f (r n)) l \<le> (\<Sum>i\<in>?d. dist (f (r n) $ i) (l $ i))" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
899 |
unfolding dist_vec_def using zero_le_dist by (rule setL2_le_setsum) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
900 |
also have "\<dots> < (\<Sum>i\<in>?d. e / (real_of_nat (card ?d)))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
901 |
by (rule setsum_strict_mono) (simp_all add: n) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
902 |
finally have "dist (f (r n)) l < e" by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
903 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
904 |
ultimately have "eventually (\<lambda>n. dist (f (r n)) l < e) sequentially" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
905 |
by (rule eventually_elim1) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
906 |
} |
49644 | 907 |
hence "((f \<circ> r) ---> l) sequentially" unfolding o_def tendsto_iff by simp |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
908 |
with r show "\<exists>l r. subseq r \<and> ((f \<circ> r) ---> l) sequentially" by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
909 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
910 |
|
49644 | 911 |
lemma interval_cart: |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
912 |
fixes a :: "real^'n" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
913 |
shows "box a b = {x::real^'n. \<forall>i. a$i < x$i \<and> x$i < b$i}" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
914 |
and "{a .. b} = {x::real^'n. \<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i}" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
915 |
by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def mem_interval Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
916 |
|
49644 | 917 |
lemma mem_interval_cart: |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
918 |
fixes a :: "real^'n" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
919 |
shows "x \<in> box a b \<longleftrightarrow> (\<forall>i. a$i < x$i \<and> x$i < b$i)" |
49644 | 920 |
and "x \<in> {a .. b} \<longleftrightarrow> (\<forall>i. a$i \<le> x$i \<and> x$i \<le> b$i)" |
921 |
using interval_cart[of a b] by (auto simp add: set_eq_iff less_vec_def less_eq_vec_def) |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
922 |
|
49644 | 923 |
lemma interval_eq_empty_cart: |
924 |
fixes a :: "real^'n" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
925 |
shows "(box a b = {} \<longleftrightarrow> (\<exists>i. b$i \<le> a$i))" (is ?th1) |
49644 | 926 |
and "({a .. b} = {} \<longleftrightarrow> (\<exists>i. b$i < a$i))" (is ?th2) |
927 |
proof - |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
928 |
{ fix i x assume as:"b$i \<le> a$i" and x:"x\<in>box a b" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
929 |
hence "a $ i < x $ i \<and> x $ i < b $ i" unfolding mem_interval_cart by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
930 |
hence "a$i < b$i" by auto |
49644 | 931 |
hence False using as by auto } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
932 |
moreover |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
933 |
{ assume as:"\<forall>i. \<not> (b$i \<le> a$i)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
934 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
935 |
{ fix i |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
936 |
have "a$i < b$i" using as[THEN spec[where x=i]] by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
937 |
hence "a$i < ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i < b$i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
938 |
unfolding vector_smult_component and vector_add_component |
49644 | 939 |
by auto } |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
940 |
hence "box a b \<noteq> {}" using mem_interval_cart(1)[of "?x" a b] by auto } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
941 |
ultimately show ?th1 by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
942 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
943 |
{ fix i x assume as:"b$i < a$i" and x:"x\<in>{a .. b}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
944 |
hence "a $ i \<le> x $ i \<and> x $ i \<le> b $ i" unfolding mem_interval_cart by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
945 |
hence "a$i \<le> b$i" by auto |
49644 | 946 |
hence False using as by auto } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
947 |
moreover |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
948 |
{ assume as:"\<forall>i. \<not> (b$i < a$i)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
949 |
let ?x = "(1/2) *\<^sub>R (a + b)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
950 |
{ fix i |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
951 |
have "a$i \<le> b$i" using as[THEN spec[where x=i]] by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
952 |
hence "a$i \<le> ((1/2) *\<^sub>R (a+b)) $ i" "((1/2) *\<^sub>R (a+b)) $ i \<le> b$i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
953 |
unfolding vector_smult_component and vector_add_component |
49644 | 954 |
by auto } |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
955 |
hence "{a .. b} \<noteq> {}" using mem_interval_cart(2)[of "?x" a b] by auto } |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
956 |
ultimately show ?th2 by blast |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
957 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
958 |
|
49644 | 959 |
lemma interval_ne_empty_cart: |
960 |
fixes a :: "real^'n" |
|
961 |
shows "{a .. b} \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i \<le> b$i)" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
962 |
and "box a b \<noteq> {} \<longleftrightarrow> (\<forall>i. a$i < b$i)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
963 |
unfolding interval_eq_empty_cart[of a b] by (auto simp add: not_less not_le) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
964 |
(* BH: Why doesn't just "auto" work here? *) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
965 |
|
49644 | 966 |
lemma subset_interval_imp_cart: |
967 |
fixes a :: "real^'n" |
|
968 |
shows "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> {c .. d} \<subseteq> {a .. b}" |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
969 |
and "(\<forall>i. a$i < c$i \<and> d$i < b$i) \<Longrightarrow> {c .. d} \<subseteq> box a b" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
970 |
and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> {a .. b}" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
971 |
and "(\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i) \<Longrightarrow> box c d \<subseteq> box a b" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
972 |
unfolding subset_eq[unfolded Ball_def] unfolding mem_interval_cart |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
973 |
by (auto intro: order_trans less_le_trans le_less_trans less_imp_le) (* BH: Why doesn't just "auto" work here? *) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
974 |
|
49644 | 975 |
lemma interval_sing: |
976 |
fixes a :: "'a::linorder^'n" |
|
977 |
shows "{a .. a} = {a} \<and> {a<..<a} = {}" |
|
978 |
apply (auto simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) |
|
979 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
980 |
|
49644 | 981 |
lemma interval_open_subset_closed_cart: |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
982 |
fixes a :: "real^'n" |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
983 |
shows "box a b \<subseteq> {a .. b}" |
49644 | 984 |
proof (simp add: subset_eq, rule) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
985 |
fix x |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
986 |
assume x: "x \<in>box a b" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
987 |
{ fix i |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
988 |
have "a $ i \<le> x $ i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
989 |
using x order_less_imp_le[of "a$i" "x$i"] |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
990 |
by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
991 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
992 |
moreover |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
993 |
{ fix i |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
994 |
have "x $ i \<le> b $ i" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
995 |
using x order_less_imp_le[of "x$i" "b$i"] |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
996 |
by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff mem_interval Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
997 |
} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
998 |
ultimately |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
999 |
show "a \<le> x \<and> x \<le> b" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
1000 |
by(simp add: set_eq_iff less_vec_def less_eq_vec_def vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1001 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1002 |
|
49644 | 1003 |
lemma subset_interval_cart: |
1004 |
fixes a :: "real^'n" |
|
1005 |
shows "{c .. d} \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th1) |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1006 |
and "{c .. d} \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i \<le> d$i) --> (\<forall>i. a$i < c$i \<and> d$i < b$i)" (is ?th2) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1007 |
and "box c d \<subseteq> {a .. b} \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th3) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1008 |
and "box c d \<subseteq> box a b \<longleftrightarrow> (\<forall>i. c$i < d$i) --> (\<forall>i. a$i \<le> c$i \<and> d$i \<le> b$i)" (is ?th4) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1009 |
using subset_interval[of c d a b] by (simp_all add: Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1010 |
|
49644 | 1011 |
lemma disjoint_interval_cart: |
1012 |
fixes a::"real^'n" |
|
1013 |
shows "{a .. b} \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i < c$i \<or> b$i < c$i \<or> d$i < a$i))" (is ?th1) |
|
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1014 |
and "{a .. b} \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i < a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th2) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1015 |
and "box a b \<inter> {c .. d} = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i < c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th3) |
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1016 |
and "box a b \<inter> box c d = {} \<longleftrightarrow> (\<exists>i. (b$i \<le> a$i \<or> d$i \<le> c$i \<or> b$i \<le> c$i \<or> d$i \<le> a$i))" (is ?th4) |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1017 |
using disjoint_interval[of a b c d] by (simp_all add: Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1018 |
|
49644 | 1019 |
lemma inter_interval_cart: |
54775
2d3df8633dad
prefer box over greaterThanLessThan on euclidean_space
immler
parents:
54489
diff
changeset
|
1020 |
fixes a :: "real^'n" |
49644 | 1021 |
shows "{a .. b} \<inter> {c .. d} = {(\<chi> i. max (a$i) (c$i)) .. (\<chi> i. min (b$i) (d$i))}" |
39302
d7728f65b353
renamed lemmas: ext_iff -> fun_eq_iff, set_ext_iff -> set_eq_iff, set_ext -> set_eqI
nipkow
parents:
39198
diff
changeset
|
1022 |
unfolding set_eq_iff and Int_iff and mem_interval_cart |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1023 |
by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1024 |
|
49644 | 1025 |
lemma closed_interval_left_cart: |
1026 |
fixes b :: "real^'n" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1027 |
shows "closed {x::real^'n. \<forall>i. x$i \<le> b$i}" |
44233 | 1028 |
by (simp add: Collect_all_eq closed_INT closed_Collect_le) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1029 |
|
49644 | 1030 |
lemma closed_interval_right_cart: |
1031 |
fixes a::"real^'n" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1032 |
shows "closed {x::real^'n. \<forall>i. a$i \<le> x$i}" |
44233 | 1033 |
by (simp add: Collect_all_eq closed_INT closed_Collect_le) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1034 |
|
49644 | 1035 |
lemma is_interval_cart: |
1036 |
"is_interval (s::(real^'n) set) \<longleftrightarrow> |
|
1037 |
(\<forall>a\<in>s. \<forall>b\<in>s. \<forall>x. (\<forall>i. ((a$i \<le> x$i \<and> x$i \<le> b$i) \<or> (b$i \<le> x$i \<and> x$i \<le> a$i))) \<longrightarrow> x \<in> s)" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1038 |
by (simp add: is_interval_def Ball_def Basis_vec_def inner_axis imp_ex) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1039 |
|
49644 | 1040 |
lemma closed_halfspace_component_le_cart: "closed {x::real^'n. x$i \<le> a}" |
44233 | 1041 |
by (simp add: closed_Collect_le) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1042 |
|
49644 | 1043 |
lemma closed_halfspace_component_ge_cart: "closed {x::real^'n. x$i \<ge> a}" |
44233 | 1044 |
by (simp add: closed_Collect_le) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1045 |
|
49644 | 1046 |
lemma open_halfspace_component_lt_cart: "open {x::real^'n. x$i < a}" |
1047 |
by (simp add: open_Collect_less) |
|
1048 |
||
1049 |
lemma open_halfspace_component_gt_cart: "open {x::real^'n. x$i > a}" |
|
44233 | 1050 |
by (simp add: open_Collect_less) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1051 |
|
49644 | 1052 |
lemma Lim_component_le_cart: |
1053 |
fixes f :: "'a \<Rightarrow> real^'n" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1054 |
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. f x $i \<le> b) net" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1055 |
shows "l$i \<le> b" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1056 |
by (rule tendsto_le[OF assms(2) tendsto_const tendsto_vec_nth, OF assms(1, 3)]) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1057 |
|
49644 | 1058 |
lemma Lim_component_ge_cart: |
1059 |
fixes f :: "'a \<Rightarrow> real^'n" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1060 |
assumes "(f ---> l) net" "\<not> (trivial_limit net)" "eventually (\<lambda>x. b \<le> (f x)$i) net" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1061 |
shows "b \<le> l$i" |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1062 |
by (rule tendsto_le[OF assms(2) tendsto_vec_nth tendsto_const, OF assms(1, 3)]) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1063 |
|
49644 | 1064 |
lemma Lim_component_eq_cart: |
1065 |
fixes f :: "'a \<Rightarrow> real^'n" |
|
1066 |
assumes net: "(f ---> l) net" "~(trivial_limit net)" and ev:"eventually (\<lambda>x. f(x)$i = b) net" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1067 |
shows "l$i = b" |
49644 | 1068 |
using ev[unfolded order_eq_iff eventually_conj_iff] and |
1069 |
Lim_component_ge_cart[OF net, of b i] and |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1070 |
Lim_component_le_cart[OF net, of i b] by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1071 |
|
49644 | 1072 |
lemma connected_ivt_component_cart: |
1073 |
fixes x :: "real^'n" |
|
1074 |
shows "connected s \<Longrightarrow> x \<in> s \<Longrightarrow> y \<in> s \<Longrightarrow> x$k \<le> a \<Longrightarrow> a \<le> y$k \<Longrightarrow> (\<exists>z\<in>s. z$k = a)" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1075 |
using connected_ivt_hyperplane[of s x y "axis k 1" a] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1076 |
by (auto simp add: inner_axis inner_commute) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1077 |
|
49644 | 1078 |
lemma subspace_substandard_cart: "subspace {x::real^_. (\<forall>i. P i \<longrightarrow> x$i = 0)}" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1079 |
unfolding subspace_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1080 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1081 |
lemma closed_substandard_cart: |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
1082 |
"closed {x::'a::real_normed_vector ^ 'n. \<forall>i. P i \<longrightarrow> x$i = 0}" |
49644 | 1083 |
proof - |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
1084 |
{ fix i::'n |
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
1085 |
have "closed {x::'a ^ 'n. P i \<longrightarrow> x$i = 0}" |
49644 | 1086 |
by (cases "P i") (simp_all add: closed_Collect_eq) } |
44213
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
1087 |
thus ?thesis |
6fb54701a11b
add lemmas open_Collect_less, closed_Collect_le, closed_Collect_eq;
huffman
parents:
44211
diff
changeset
|
1088 |
unfolding Collect_all_eq by (simp add: closed_INT) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1089 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1090 |
|
49644 | 1091 |
lemma dim_substandard_cart: "dim {x::real^'n. \<forall>i. i \<notin> d \<longrightarrow> x$i = 0} = card d" |
1092 |
(is "dim ?A = _") |
|
1093 |
proof - |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1094 |
let ?a = "\<lambda>x. axis x 1 :: real^'n" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1095 |
have *: "{x. \<forall>i\<in>Basis. i \<notin> ?a ` d \<longrightarrow> x \<bullet> i = 0} = ?A" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1096 |
by (auto simp: image_iff Basis_vec_def axis_eq_axis inner_axis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1097 |
have "?a ` d \<subseteq> Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1098 |
by (auto simp: Basis_vec_def) |
49644 | 1099 |
thus ?thesis |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1100 |
using dim_substandard[of "?a ` d"] card_image[of ?a d] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1101 |
by (auto simp: axis_eq_axis inj_on_def *) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1102 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1103 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1104 |
lemma affinity_inverses: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1105 |
assumes m0: "m \<noteq> (0::'a::field)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1106 |
shows "(\<lambda>x. m *s x + c) o (\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) = id" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1107 |
"(\<lambda>x. inverse(m) *s x + (-(inverse(m) *s c))) o (\<lambda>x. m *s x + c) = id" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1108 |
using m0 |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset
|
1109 |
apply (auto simp add: fun_eq_iff vector_add_ldistrib diff_conv_add_uminus simp del: add_uminus_conv_diff) |
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset
|
1110 |
apply (simp_all add: vector_smult_lneg[symmetric] vector_smult_assoc vector_sneg_minus1 [symmetric]) |
49644 | 1111 |
done |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1112 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1113 |
lemma vector_affinity_eq: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1114 |
assumes m0: "(m::'a::field) \<noteq> 0" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1115 |
shows "m *s x + c = y \<longleftrightarrow> x = inverse m *s y + -(inverse m *s c)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1116 |
proof |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1117 |
assume h: "m *s x + c = y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1118 |
hence "m *s x = y - c" by (simp add: field_simps) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1119 |
hence "inverse m *s (m *s x) = inverse m *s (y - c)" by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1120 |
then show "x = inverse m *s y + - (inverse m *s c)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1121 |
using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1122 |
next |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1123 |
assume h: "x = inverse m *s y + - (inverse m *s c)" |
54230
b1d955791529
more simplification rules on unary and binary minus
haftmann
parents:
53600
diff
changeset
|
1124 |
show "m *s x + c = y" unfolding h |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1125 |
using m0 by (simp add: vector_smult_assoc vector_ssub_ldistrib) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1126 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1127 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1128 |
lemma vector_eq_affinity: |
49644 | 1129 |
"(m::'a::field) \<noteq> 0 ==> (y = m *s x + c \<longleftrightarrow> inverse(m) *s y + -(inverse(m) *s c) = x)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1130 |
using vector_affinity_eq[where m=m and x=x and y=y and c=c] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1131 |
by metis |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1132 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1133 |
lemma vector_cart: |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1134 |
fixes f :: "real^'n \<Rightarrow> real" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1135 |
shows "(\<chi> i. f (axis i 1)) = (\<Sum>i\<in>Basis. f i *\<^sub>R i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1136 |
unfolding euclidean_eq_iff[where 'a="real^'n"] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1137 |
by simp (simp add: Basis_vec_def inner_axis) |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1138 |
|
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1139 |
lemma const_vector_cart:"((\<chi> i. d)::real^'n) = (\<Sum>i\<in>Basis. d *\<^sub>R i)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1140 |
by (rule vector_cart) |
49644 | 1141 |
|
44360 | 1142 |
subsection "Convex Euclidean Space" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1143 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1144 |
lemma Cart_1:"(1::real^'n) = \<Sum>Basis" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1145 |
using const_vector_cart[of 1] by (simp add: one_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1146 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1147 |
declare vector_add_ldistrib[simp] vector_ssub_ldistrib[simp] vector_smult_assoc[simp] vector_smult_rneg[simp] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1148 |
declare vector_sadd_rdistrib[simp] vector_sub_rdistrib[simp] |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1149 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1150 |
lemmas vector_component_simps = vector_minus_component vector_smult_component vector_add_component less_eq_vec_def vec_lambda_beta vector_uminus_component |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1151 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1152 |
lemma convex_box_cart: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1153 |
assumes "\<And>i. convex {x. P i x}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1154 |
shows "convex {x. \<forall>i. P i (x$i)}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1155 |
using assms unfolding convex_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1156 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1157 |
lemma convex_positive_orthant_cart: "convex {x::real^'n. (\<forall>i. 0 \<le> x$i)}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1158 |
by (rule convex_box_cart) (simp add: atLeast_def[symmetric] convex_real_interval) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1159 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1160 |
lemma unit_interval_convex_hull_cart: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1161 |
"{0::real^'n .. 1} = convex hull {x. \<forall>i. (x$i = 0) \<or> (x$i = 1)}" (is "?int = convex hull ?points") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1162 |
unfolding Cart_1 unit_interval_convex_hull[where 'a="real^'n"] |
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1163 |
by (rule arg_cong[where f="\<lambda>x. convex hull x"]) (simp add: Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1164 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1165 |
lemma cube_convex_hull_cart: |
49644 | 1166 |
assumes "0 < d" |
1167 |
obtains s::"(real^'n) set" |
|
1168 |
where "finite s" "{x - (\<chi> i. d) .. x + (\<chi> i. d)} = convex hull s" |
|
1169 |
proof - |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1170 |
from cube_convex_hull [OF assms, of x] guess s . |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1171 |
with that[of s] show thesis by (simp add: const_vector_cart) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1172 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1173 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1174 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1175 |
subsection "Derivative" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1176 |
|
49644 | 1177 |
lemma differentiable_at_imp_differentiable_on: |
1178 |
"(\<forall>x\<in>(s::(real^'n) set). f differentiable at x) \<Longrightarrow> f differentiable_on s" |
|
51641
cd05e9fcc63d
remove the within-filter, replace "at" by "at _ within UNIV" (This allows to remove a couple of redundant lemmas)
hoelzl
parents:
51489
diff
changeset
|
1179 |
by (metis differentiable_at_withinI differentiable_on_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1180 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1181 |
definition "jacobian f net = matrix(frechet_derivative f net)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1182 |
|
49644 | 1183 |
lemma jacobian_works: |
1184 |
"(f::(real^'a) \<Rightarrow> (real^'b)) differentiable net \<longleftrightarrow> |
|
1185 |
(f has_derivative (\<lambda>h. (jacobian f net) *v h)) net" |
|
1186 |
apply rule |
|
1187 |
unfolding jacobian_def |
|
1188 |
apply (simp only: matrix_works[OF linear_frechet_derivative]) defer |
|
1189 |
apply (rule differentiableI) |
|
1190 |
apply assumption |
|
1191 |
unfolding frechet_derivative_works |
|
1192 |
apply assumption |
|
1193 |
done |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1194 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1195 |
|
49644 | 1196 |
subsection {* Component of the differential must be zero if it exists at a local |
1197 |
maximum or minimum for that corresponding component. *} |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1198 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1199 |
lemma differential_zero_maxmin_cart: |
49644 | 1200 |
fixes f::"real^'a \<Rightarrow> real^'b" |
1201 |
assumes "0 < e" "((\<forall>y \<in> ball x e. (f y)$k \<le> (f x)$k) \<or> (\<forall>y\<in>ball x e. (f x)$k \<le> (f y)$k))" |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1202 |
"f differentiable (at x)" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1203 |
shows "jacobian f (at x) $ k = 0" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1204 |
using differential_zero_maxmin_component[of "axis k 1" e x f] assms |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1205 |
vector_cart[of "\<lambda>j. frechet_derivative f (at x) j $ k"] |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1206 |
by (simp add: Basis_vec_def axis_eq_axis inner_axis jacobian_def matrix_def) |
49644 | 1207 |
|
37494 | 1208 |
subsection {* Lemmas for working on @{typ "real^1"} *} |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1209 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1210 |
lemma forall_1[simp]: "(\<forall>i::1. P i) \<longleftrightarrow> P 1" |
49644 | 1211 |
by (metis (full_types) num1_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1212 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1213 |
lemma ex_1[simp]: "(\<exists>x::1. P x) \<longleftrightarrow> P 1" |
49644 | 1214 |
by auto (metis (full_types) num1_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1215 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1216 |
lemma exhaust_2: |
49644 | 1217 |
fixes x :: 2 |
1218 |
shows "x = 1 \<or> x = 2" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1219 |
proof (induct x) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1220 |
case (of_int z) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1221 |
then have "0 <= z" and "z < 2" by simp_all |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1222 |
then have "z = 0 | z = 1" by arith |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1223 |
then show ?case by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1224 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1225 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1226 |
lemma forall_2: "(\<forall>i::2. P i) \<longleftrightarrow> P 1 \<and> P 2" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1227 |
by (metis exhaust_2) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1228 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1229 |
lemma exhaust_3: |
49644 | 1230 |
fixes x :: 3 |
1231 |
shows "x = 1 \<or> x = 2 \<or> x = 3" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1232 |
proof (induct x) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1233 |
case (of_int z) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1234 |
then have "0 <= z" and "z < 3" by simp_all |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1235 |
then have "z = 0 \<or> z = 1 \<or> z = 2" by arith |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1236 |
then show ?case by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1237 |
qed |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1238 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1239 |
lemma forall_3: "(\<forall>i::3. P i) \<longleftrightarrow> P 1 \<and> P 2 \<and> P 3" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1240 |
by (metis exhaust_3) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1241 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1242 |
lemma UNIV_1 [simp]: "UNIV = {1::1}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1243 |
by (auto simp add: num1_eq_iff) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1244 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1245 |
lemma UNIV_2: "UNIV = {1::2, 2::2}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1246 |
using exhaust_2 by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1247 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1248 |
lemma UNIV_3: "UNIV = {1::3, 2::3, 3::3}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1249 |
using exhaust_3 by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1250 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1251 |
lemma setsum_1: "setsum f (UNIV::1 set) = f 1" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1252 |
unfolding UNIV_1 by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1253 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1254 |
lemma setsum_2: "setsum f (UNIV::2 set) = f 1 + f 2" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1255 |
unfolding UNIV_2 by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1256 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1257 |
lemma setsum_3: "setsum f (UNIV::3 set) = f 1 + f 2 + f 3" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1258 |
unfolding UNIV_3 by (simp add: add_ac) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1259 |
|
49644 | 1260 |
instantiation num1 :: cart_one |
1261 |
begin |
|
1262 |
||
1263 |
instance |
|
1264 |
proof |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1265 |
show "CARD(1) = Suc 0" by auto |
49644 | 1266 |
qed |
1267 |
||
1268 |
end |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1269 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1270 |
subsection{* The collapse of the general concepts to dimension one. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1271 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1272 |
lemma vector_one: "(x::'a ^1) = (\<chi> i. (x$1))" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
1273 |
by (simp add: vec_eq_iff) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1274 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1275 |
lemma forall_one: "(\<forall>(x::'a ^1). P x) \<longleftrightarrow> (\<forall>x. P(\<chi> i. x))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1276 |
apply auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1277 |
apply (erule_tac x= "x$1" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1278 |
apply (simp only: vector_one[symmetric]) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1279 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1280 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1281 |
lemma norm_vector_1: "norm (x :: _^1) = norm (x$1)" |
44136
e63ad7d5158d
more uniform naming scheme for finite cartesian product type and related theorems
huffman
parents:
44135
diff
changeset
|
1282 |
by (simp add: norm_vec_def) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1283 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1284 |
lemma norm_real: "norm(x::real ^ 1) = abs(x$1)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1285 |
by (simp add: norm_vector_1) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1286 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1287 |
lemma dist_real: "dist(x::real ^ 1) y = abs((x$1) - (y$1))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1288 |
by (auto simp add: norm_real dist_norm) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1289 |
|
49644 | 1290 |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1291 |
subsection{* Explicit vector construction from lists. *} |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1292 |
|
43995
c479836d9048
simplified definition of vector (also removed Cartesian_Euclidean_Space.from_nat which collides with Countable.from_nat)
hoelzl
parents:
42814
diff
changeset
|
1293 |
definition "vector l = (\<chi> i. foldr (\<lambda>x f n. fun_upd (f (n+1)) n x) l (\<lambda>n x. 0) 1 i)" |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1294 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1295 |
lemma vector_1: "(vector[x]) $1 = x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1296 |
unfolding vector_def by simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1297 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1298 |
lemma vector_2: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1299 |
"(vector[x,y]) $1 = x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1300 |
"(vector[x,y] :: 'a^2)$2 = (y::'a::zero)" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1301 |
unfolding vector_def by simp_all |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1302 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1303 |
lemma vector_3: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1304 |
"(vector [x,y,z] ::('a::zero)^3)$1 = x" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1305 |
"(vector [x,y,z] ::('a::zero)^3)$2 = y" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1306 |
"(vector [x,y,z] ::('a::zero)^3)$3 = z" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1307 |
unfolding vector_def by simp_all |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1308 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1309 |
lemma forall_vector_1: "(\<forall>v::'a::zero^1. P v) \<longleftrightarrow> (\<forall>x. P(vector[x]))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1310 |
apply auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1311 |
apply (erule_tac x="v$1" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1312 |
apply (subgoal_tac "vector [v$1] = v") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1313 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1314 |
apply (vector vector_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1315 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1316 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1317 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1318 |
lemma forall_vector_2: "(\<forall>v::'a::zero^2. P v) \<longleftrightarrow> (\<forall>x y. P(vector[x, y]))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1319 |
apply auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1320 |
apply (erule_tac x="v$1" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1321 |
apply (erule_tac x="v$2" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1322 |
apply (subgoal_tac "vector [v$1, v$2] = v") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1323 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1324 |
apply (vector vector_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1325 |
apply (simp add: forall_2) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1326 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1327 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1328 |
lemma forall_vector_3: "(\<forall>v::'a::zero^3. P v) \<longleftrightarrow> (\<forall>x y z. P(vector[x, y, z]))" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1329 |
apply auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1330 |
apply (erule_tac x="v$1" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1331 |
apply (erule_tac x="v$2" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1332 |
apply (erule_tac x="v$3" in allE) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1333 |
apply (subgoal_tac "vector [v$1, v$2, v$3] = v") |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1334 |
apply simp |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1335 |
apply (vector vector_def) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1336 |
apply (simp add: forall_3) |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1337 |
done |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1338 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1339 |
lemma bounded_linear_component_cart[intro]: "bounded_linear (\<lambda>x::real^'n. x $ k)" |
49644 | 1340 |
apply (rule bounded_linearI[where K=1]) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1341 |
using component_le_norm_cart[of _ k] unfolding real_norm_def by auto |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1342 |
|
49644 | 1343 |
lemma integral_component_eq_cart[simp]: |
1344 |
fixes f :: "'n::ordered_euclidean_space \<Rightarrow> real^'m" |
|
1345 |
assumes "f integrable_on s" |
|
1346 |
shows "integral s (\<lambda>x. f x $ k) = integral s f $ k" |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1347 |
using integral_linear[OF assms(1) bounded_linear_component_cart,unfolded o_def] . |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1348 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1349 |
lemma interval_split_cart: |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1350 |
"{a..b::real^'n} \<inter> {x. x$k \<le> c} = {a .. (\<chi> i. if i = k then min (b$k) c else b$i)}" |
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1351 |
"{a..b} \<inter> {x. x$k \<ge> c} = {(\<chi> i. if i = k then max (a$k) c else a$i) .. b}" |
49644 | 1352 |
apply (rule_tac[!] set_eqI) |
1353 |
unfolding Int_iff mem_interval_cart mem_Collect_eq |
|
1354 |
unfolding vec_lambda_beta |
|
1355 |
by auto |
|
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1356 |
|
50526
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1357 |
lemma interval_bij_bij_cart: fixes x::"real^'n" assumes "\<forall>i. a$i < b$i \<and> u$i < v$i" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1358 |
shows "interval_bij (a,b) (u,v) (interval_bij (u,v) (a,b) x) = x" |
899c9c4e4a4c
Remove the indexed basis from the definition of euclidean spaces and only use the set of Basis vectors
hoelzl
parents:
49962
diff
changeset
|
1359 |
using assms by (intro interval_bij_bij) (auto simp: Basis_vec_def inner_axis) |
37489
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1360 |
|
44e42d392c6e
Introduce a type class for euclidean spaces, port most lemmas from real^'n to this type class.
hoelzl
parents:
diff
changeset
|
1361 |
end |