2 header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} |
2 header {*Instanciates the finite cartesian product of euclidean spaces as a euclidean space.*} |
3 |
3 |
4 theory Cartesian_Euclidean_Space |
4 theory Cartesian_Euclidean_Space |
5 imports Finite_Cartesian_Product Integration |
5 imports Finite_Cartesian_Product Integration |
6 begin |
6 begin |
7 |
|
8 instantiation prod :: (real_basis, real_basis) real_basis |
|
9 begin |
|
10 |
|
11 definition "basis i = (if i < DIM('a) then (basis i, 0) else (0, basis (i - DIM('a))))" |
|
12 |
|
13 instance |
|
14 proof |
|
15 let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b" |
|
16 let ?b_a = "basis :: nat \<Rightarrow> 'a" |
|
17 let ?b_b = "basis :: nat \<Rightarrow> 'b" |
|
18 |
|
19 note image_range = |
|
20 image_add_atLeastLessThan[symmetric, of 0 "DIM('a)" "DIM('b)", simplified] |
|
21 |
|
22 have split_range: |
|
23 "{..<DIM('b) + DIM('a)} = {..<DIM('a)} \<union> {DIM('a)..<DIM('b) + DIM('a)}" |
|
24 by auto |
|
25 have *: "?b ` {DIM('a)..<DIM('b) + DIM('a)} = {0} \<times> (?b_b ` {..<DIM('b)})" |
|
26 "?b ` {..<DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0}" |
|
27 unfolding image_range image_image basis_prod_def_raw range_basis |
|
28 by (auto simp: zero_prod_def basis_eq_0_iff) |
|
29 hence b_split: |
|
30 "?b ` {..<DIM('b) + DIM('a)} = (?b_a ` {..<DIM('a)}) \<times> {0} \<union> {0} \<times> (?b_b ` {..<DIM('b)})" (is "_ = ?prod") |
|
31 by (subst split_range) (simp add: image_Un) |
|
32 |
|
33 have b_0: "?b ` {DIM('b) + DIM('a)..} = {0}" unfolding basis_prod_def_raw |
|
34 by (auto simp: zero_prod_def image_iff basis_eq_0_iff elim!: ballE[of _ _ "DIM('a) + DIM('b)"]) |
|
35 |
|
36 have split_UNIV: |
|
37 "UNIV = {..<DIM('b) + DIM('a)} \<union> {DIM('b)+DIM('a)..}" |
|
38 by auto |
|
39 |
|
40 have range_b: "range ?b = ?prod \<union> {0}" |
|
41 by (subst split_UNIV) (simp add: image_Un b_split b_0) |
|
42 |
|
43 have prod: "\<And>f A B. setsum f (A \<times> B) = (\<Sum>a\<in>A. \<Sum>b\<in>B. f (a, b))" |
|
44 by (simp add: setsum_cartesian_product) |
|
45 |
|
46 show "span (range ?b) = UNIV" |
|
47 unfolding span_explicit range_b |
|
48 proof safe |
|
49 fix a::'a and b::'b |
|
50 from in_span_basis[of a] in_span_basis[of b] |
|
51 obtain Sa ua Sb ub where span: |
|
52 "finite Sa" "Sa \<subseteq> basis ` {..<DIM('a)}" "a = (\<Sum>v\<in>Sa. ua v *\<^sub>R v)" |
|
53 "finite Sb" "Sb \<subseteq> basis ` {..<DIM('b)}" "b = (\<Sum>v\<in>Sb. ub v *\<^sub>R v)" |
|
54 unfolding span_explicit by auto |
|
55 |
|
56 let ?S = "((Sa - {0}) \<times> {0} \<union> {0} \<times> (Sb - {0}))" |
|
57 have *: |
|
58 "?S \<inter> {v. fst v = 0} \<inter> {v. snd v = 0} = {}" |
|
59 "?S \<inter> - {v. fst v = 0} \<inter> {v. snd v = 0} = (Sa - {0}) \<times> {0}" |
|
60 "?S \<inter> {v. fst v = 0} \<inter> - {v. snd v = 0} = {0} \<times> (Sb - {0})" |
|
61 by (auto simp: zero_prod_def) |
|
62 show "\<exists>S u. finite S \<and> S \<subseteq> ?prod \<union> {0} \<and> (\<Sum>v\<in>S. u v *\<^sub>R v) = (a, b)" |
|
63 apply (rule exI[of _ ?S]) |
|
64 apply (rule exI[of _ "\<lambda>(v, w). (if w = 0 then ua v else 0) + (if v = 0 then ub w else 0)"]) |
|
65 using span |
|
66 apply (simp add: prod_case_unfold setsum_addf if_distrib cond_application_beta setsum_cases prod *) |
|
67 by (auto simp add: setsum_prod intro!: setsum_mono_zero_cong_left) |
|
68 qed simp |
|
69 |
|
70 show "\<exists>d>0. ?b ` {d..} = {0} \<and> independent (?b ` {..<d}) \<and> inj_on ?b {..<d}" |
|
71 apply (rule exI[of _ "DIM('b) + DIM('a)"]) unfolding b_0 |
|
72 proof (safe intro!: DIM_positive del: notI) |
|
73 show inj_on: "inj_on ?b {..<DIM('b) + DIM('a)}" unfolding split_range |
|
74 using inj_on_iff[OF basis_inj[where 'a='a]] inj_on_iff[OF basis_inj[where 'a='b]] |
|
75 by (auto intro!: inj_onI simp: basis_prod_def basis_eq_0_iff) |
|
76 |
|
77 show "independent (?b ` {..<DIM('b) + DIM('a)})" |
|
78 unfolding independent_eq_inj_on[OF inj_on] |
|
79 proof safe |
|
80 fix i u assume i_upper: "i < DIM('b) + DIM('a)" and |
|
81 "(\<Sum>j\<in>{..<DIM('b) + DIM('a)} - {i}. u (?b j) *\<^sub>R ?b j) = ?b i" (is "?SUM = _") |
|
82 let ?left = "{..<DIM('a)}" and ?right = "{DIM('a)..<DIM('b) + DIM('a)}" |
|
83 show False |
|
84 proof cases |
|
85 assume "i < DIM('a)" |
|
86 hence "(basis i, 0) = ?SUM" unfolding `?SUM = ?b i` unfolding basis_prod_def by auto |
|
87 also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b j) *\<^sub>R ?b j) + |
|
88 (\<Sum>j\<in>?right. u (?b j) *\<^sub>R ?b j)" |
|
89 using `i < DIM('a)` by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) |
|
90 also have "\<dots> = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) + |
|
91 (\<Sum>j\<in>?right. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))" |
|
92 unfolding basis_prod_def by auto |
|
93 finally have "basis i = (\<Sum>j\<in>?left - {i}. u (?b_a j, 0) *\<^sub>R ?b_a j)" |
|
94 by (simp add: setsum_prod) |
|
95 moreover |
|
96 note independent_basis[where 'a='a, unfolded independent_eq_inj_on[OF basis_inj]] |
|
97 note this[rule_format, of i "\<lambda>v. u (v, 0)"] |
|
98 ultimately show False using `i < DIM('a)` by auto |
|
99 next |
|
100 let ?i = "i - DIM('a)" |
|
101 assume not: "\<not> i < DIM('a)" hence "DIM('a) \<le> i" by auto |
|
102 hence "?i < DIM('b)" using `i < DIM('b) + DIM('a)` by auto |
|
103 |
|
104 have inj_on: "inj_on (\<lambda>j. j - DIM('a)) {DIM('a)..<DIM('b) + DIM('a)}" |
|
105 by (auto intro!: inj_onI) |
|
106 with i_upper not have *: "{..<DIM('b)} - {?i} = (\<lambda>j. j-DIM('a))`(?right - {i})" |
|
107 by (auto simp: inj_on_image_set_diff image_minus_const_atLeastLessThan_nat) |
|
108 |
|
109 have "(0, basis ?i) = ?SUM" unfolding `?SUM = ?b i` |
|
110 unfolding basis_prod_def using not `?i < DIM('b)` by auto |
|
111 also have "\<dots> = (\<Sum>j\<in>?left. u (?b j) *\<^sub>R ?b j) + |
|
112 (\<Sum>j\<in>?right - {i}. u (?b j) *\<^sub>R ?b j)" |
|
113 using not by (subst setsum_Un_disjoint[symmetric]) (auto intro!: setsum_cong) |
|
114 also have "\<dots> = (\<Sum>j\<in>?left. u (?b_a j, 0) *\<^sub>R (?b_a j, 0)) + |
|
115 (\<Sum>j\<in>?right - {i}. u (0, ?b_b (j-DIM('a))) *\<^sub>R (0, ?b_b (j-DIM('a))))" |
|
116 unfolding basis_prod_def by auto |
|
117 finally have "basis ?i = (\<Sum>j\<in>{..<DIM('b)} - {?i}. u (0, ?b_b j) *\<^sub>R ?b_b j)" |
|
118 unfolding * |
|
119 by (subst setsum_reindex[OF inj_on[THEN subset_inj_on]]) |
|
120 (auto simp: setsum_prod) |
|
121 moreover |
|
122 note independent_basis[where 'a='b, unfolded independent_eq_inj_on[OF basis_inj]] |
|
123 note this[rule_format, of ?i "\<lambda>v. u (0, v)"] |
|
124 ultimately show False using `?i < DIM('b)` by auto |
|
125 qed |
|
126 qed |
|
127 qed |
|
128 qed |
|
129 end |
|
130 |
|
131 lemma DIM_prod[simp]: "DIM('a \<times> 'b) = DIM('b::real_basis) + DIM('a::real_basis)" |
|
132 by (rule dimension_eq) (auto simp: basis_prod_def zero_prod_def basis_eq_0_iff) |
|
133 |
|
134 instance prod :: (euclidean_space, euclidean_space) euclidean_space |
|
135 proof (default, safe) |
|
136 let ?b = "basis :: nat \<Rightarrow> 'a \<times> 'b" |
|
137 fix i j assume "i < DIM('a \<times> 'b)" "j < DIM('a \<times> 'b)" |
|
138 thus "?b i \<bullet> ?b j = (if i = j then 1 else 0)" |
|
139 unfolding basis_prod_def by (auto simp: dot_basis) |
|
140 qed |
|
141 |
|
142 instantiation prod :: (ordered_euclidean_space, ordered_euclidean_space) ordered_euclidean_space |
|
143 begin |
|
144 |
|
145 definition "x \<le> (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i \<le> y $$ i)" |
|
146 definition "x < (y::('a\<times>'b)) \<longleftrightarrow> (\<forall>i<DIM('a\<times>'b). x $$ i < y $$ i)" |
|
147 |
|
148 instance proof qed (auto simp: less_prod_def less_eq_prod_def) |
|
149 end |
|
150 |
7 |
151 lemma delta_mult_idempotent: |
8 lemma delta_mult_idempotent: |
152 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) |
9 "(if k=a then 1 else (0::'a::semiring_1)) * (if k=a then 1 else 0) = (if k=a then 1 else 0)" by (cases "k=a", auto) |
153 |
10 |
154 lemma setsum_Plus: |
11 lemma setsum_Plus: |