15 (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))" |
15 (\<lambda>(a, b) (u, v) x. (\<Sum>i\<in>Basis. (u\<bullet>i + (x\<bullet>i - a\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (v\<bullet>i - u\<bullet>i)) *\<^sub>R i))" |
16 |
16 |
17 lemma interval_bij_affine: |
17 lemma interval_bij_affine: |
18 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) + |
18 "interval_bij (a,b) (u,v) = (\<lambda>x. (\<Sum>i\<in>Basis. ((v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (x\<bullet>i)) *\<^sub>R i) + |
19 (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))" |
19 (\<Sum>i\<in>Basis. (u\<bullet>i - (v\<bullet>i - u\<bullet>i) / (b\<bullet>i - a\<bullet>i) * (a\<bullet>i)) *\<^sub>R i))" |
20 by (auto simp add: interval_bij_def sum.distrib [symmetric] scaleR_add_left [symmetric] |
20 by (simp add: interval_bij_def algebra_simps add_divide_distrib diff_divide_distrib flip: sum.distrib scaleR_add_left) |
21 fun_eq_iff intro!: sum.cong) |
21 |
22 (simp add: algebra_simps diff_divide_distrib [symmetric]) |
|
23 |
22 |
24 lemma continuous_interval_bij: |
23 lemma continuous_interval_bij: |
25 fixes a b :: "'a::euclidean_space" |
24 fixes a b :: "'a::euclidean_space" |
26 shows "continuous (at x) (interval_bij (a, b) (u, v))" |
25 shows "continuous (at x) (interval_bij (a, b) (u, v))" |
27 by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros) |
26 by (auto simp add: divide_inverse interval_bij_def intro!: continuous_sum continuous_intros) |
28 |
27 |
29 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))" |
28 lemma continuous_on_interval_bij: "continuous_on s (interval_bij (a, b) (u, v))" |
30 apply(rule continuous_at_imp_continuous_on) |
29 by (metis continuous_at_imp_continuous_on continuous_interval_bij) |
31 apply (rule, rule continuous_interval_bij) |
|
32 done |
|
33 |
30 |
34 lemma in_interval_interval_bij: |
31 lemma in_interval_interval_bij: |
35 fixes a b u v x :: "'a::euclidean_space" |
32 fixes a b u v x :: "'a::euclidean_space" |
36 assumes "x \<in> cbox a b" |
33 assumes "x \<in> cbox a b" |
37 and "cbox u v \<noteq> {}" |
34 and "cbox u v \<noteq> {}" |
38 shows "interval_bij (a, b) (u, v) x \<in> cbox u v" |
35 shows "interval_bij (a, b) (u, v) x \<in> cbox u v" |
39 apply (simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis cong: ball_cong) |
|
40 apply safe |
|
41 proof - |
36 proof - |
42 fix i :: 'a |
37 have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)" |
43 assume i: "i \<in> Basis" |
38 by (smt (verit) assms box_ne_empty(1) divide_nonneg_nonneg mem_box(2) mult_nonneg_nonneg) |
44 have "cbox a b \<noteq> {}" |
39 moreover |
45 using assms by auto |
40 have "\<And>i. i \<in> Basis \<Longrightarrow> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i" |
46 with i have *: "a\<bullet>i \<le> b\<bullet>i" "u\<bullet>i \<le> v\<bullet>i" |
41 apply (simp add: divide_simps algebra_simps) |
47 using assms(2) by (auto simp add: box_eq_empty) |
42 by (smt (verit, best) assms box_ne_empty(1) left_diff_distrib mem_box(2) mult.commute mult_left_mono) |
48 have x: "a\<bullet>i\<le>x\<bullet>i" "x\<bullet>i\<le>b\<bullet>i" |
43 ultimately show ?thesis |
49 using assms(1)[unfolded mem_box] using i by auto |
44 by (force simp only: interval_bij_def split_conv mem_box inner_sum_left_Basis) |
50 have "0 \<le> (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)" |
|
51 using * x by auto |
|
52 then show "u \<bullet> i \<le> u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i)" |
|
53 using * by auto |
|
54 have "((x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i)) * (v \<bullet> i - u \<bullet> i) \<le> 1 * (v \<bullet> i - u \<bullet> i)" |
|
55 apply (rule mult_right_mono) |
|
56 unfolding divide_le_eq_1 |
|
57 using * x |
|
58 apply auto |
|
59 done |
|
60 then show "u \<bullet> i + (x \<bullet> i - a \<bullet> i) / (b \<bullet> i - a \<bullet> i) * (v \<bullet> i - u \<bullet> i) \<le> v \<bullet> i" |
|
61 using * by auto |
|
62 qed |
45 qed |
63 |
46 |
64 lemma interval_bij_bij: |
47 lemma interval_bij_bij: |
65 "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow> |
48 "\<forall>(i::'a::euclidean_space)\<in>Basis. a\<bullet>i < b\<bullet>i \<and> u\<bullet>i < v\<bullet>i \<Longrightarrow> |
66 interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x" |
49 interval_bij (a, b) (u, v) (interval_bij (u, v) (a, b) x) = x" |
126 then obtain w :: "real^2" where w: |
109 then obtain w :: "real^2" where w: |
127 "w \<in> cbox (- 1) 1" |
110 "w \<in> cbox (- 1) 1" |
128 "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w" |
111 "x = (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w" |
129 unfolding image_iff .. |
112 unfolding image_iff .. |
130 then have "x \<noteq> 0" |
113 then have "x \<noteq> 0" |
131 using as[of "w$1" "w$2"] |
114 using as[of "w$1" "w$2"] by (auto simp: mem_box_cart atLeastAtMost_iff) |
132 unfolding mem_box_cart atLeastAtMost_iff |
|
133 by auto |
|
134 } note x0 = this |
115 } note x0 = this |
135 have 1: "box (- 1) (1::real^2) \<noteq> {}" |
116 let ?CB11 = "cbox (- 1) (1::real^2)" |
136 unfolding interval_eq_empty_cart by auto |
|
137 have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
|
138 for i x y c |
|
139 using exhaust_2 [of i] by (auto simp: negatex_def) |
|
140 then have "bounded_linear negatex" |
|
141 by (simp add: bounded_linearI' vec_eq_iff) |
|
142 then have 2: "continuous_on (cbox (- 1) 1) (negatex \<circ> sqprojection \<circ> ?F)" |
|
143 apply (intro continuous_intros continuous_on_component) |
|
144 unfolding * sqprojection_def |
|
145 apply (intro assms continuous_intros)+ |
|
146 apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on) |
|
147 done |
|
148 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` cbox (-1) 1 \<subseteq> cbox (-1) 1" |
|
149 unfolding subset_eq |
|
150 proof (rule, goal_cases) |
|
151 case (1 x) |
|
152 then obtain y :: "real^2" where y: |
|
153 "y \<in> cbox (- 1) 1" |
|
154 "x = (negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) y" |
|
155 unfolding image_iff .. |
|
156 have "?F y \<noteq> 0" |
|
157 by (rule x0) (use y in auto) |
|
158 then have *: "infnorm (sqprojection (?F y)) = 1" |
|
159 unfolding y o_def |
|
160 by - (rule lem2[rule_format]) |
|
161 have inf1: "infnorm x = 1" |
|
162 unfolding *[symmetric] y o_def |
|
163 by (rule lem1[rule_format]) |
|
164 show "x \<in> cbox (-1) 1" |
|
165 unfolding mem_box_cart interval_cbox_cart infnorm_2 |
|
166 proof |
|
167 fix i |
|
168 show "(- 1) $ i \<le> x $ i \<and> x $ i \<le> 1 $ i" |
|
169 using exhaust_2 [of i] inf1 by (auto simp: infnorm_2) |
|
170 qed |
|
171 qed |
|
172 obtain x :: "real^2" where x: |
117 obtain x :: "real^2" where x: |
173 "x \<in> cbox (- 1) 1" |
118 "x \<in> cbox (- 1) 1" |
174 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
119 "(negatex \<circ> sqprojection \<circ> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w)) x = x" |
175 apply (rule brouwer_weak[of "cbox (- 1) (1::real^2)" "negatex \<circ> sqprojection \<circ> ?F"]) |
120 proof (rule brouwer_weak[of ?CB11 "negatex \<circ> sqprojection \<circ> ?F"]) |
176 apply (rule compact_cbox convex_box)+ |
121 show "compact ?CB11" "convex ?CB11" |
177 unfolding interior_cbox image_subset_iff_funcset [symmetric] |
122 by (rule compact_cbox convex_box)+ |
178 apply (rule 1 2 3)+ |
123 have "box (- 1) (1::real^2) \<noteq> {}" |
179 apply blast |
124 unfolding interval_eq_empty_cart by auto |
180 done |
125 then show "interior ?CB11 \<noteq> {}" |
|
126 by simp |
|
127 have "negatex (x + y) $ i = (negatex x + negatex y) $ i \<and> negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
|
128 for i x y c |
|
129 using exhaust_2 [of i] by (auto simp: negatex_def) |
|
130 then have "bounded_linear negatex" |
|
131 by (simp add: bounded_linearI' vec_eq_iff) |
|
132 then show "continuous_on ?CB11 (negatex \<circ> sqprojection \<circ> ?F)" |
|
133 unfolding sqprojection_def |
|
134 apply (intro continuous_intros continuous_on_component | use * assms in presburger)+ |
|
135 apply (simp_all add: infnorm_eq_0 x0 linear_continuous_on) |
|
136 done |
|
137 have "(negatex \<circ> sqprojection \<circ> ?F) ` ?CB11 \<subseteq> ?CB11" |
|
138 proof clarsimp |
|
139 fix y :: "real^2" |
|
140 assume y: "y \<in> ?CB11" |
|
141 have "?F y \<noteq> 0" |
|
142 by (rule x0) (use y in auto) |
|
143 then have *: "infnorm (sqprojection (?F y)) = 1" |
|
144 using inf_eq1 by blast |
|
145 show "negatex (sqprojection (f (y $ 1) - g (y $ 2))) \<in> cbox (-1) 1" |
|
146 unfolding mem_box_cart interval_cbox_cart infnorm_2 |
|
147 by (smt (verit, del_insts) "*" component_le_infnorm_cart inf_nega neg_one_index o_apply one_index) |
|
148 qed |
|
149 then show "negatex \<circ> sqprojection \<circ> ?F \<in> ?CB11 \<rightarrow> ?CB11" |
|
150 by blast |
|
151 qed |
181 have "?F x \<noteq> 0" |
152 have "?F x \<noteq> 0" |
182 by (rule x0) (use x in auto) |
153 by (rule x0) (use x in auto) |
183 then have *: "infnorm (sqprojection (?F x)) = 1" |
154 then have *: "infnorm (sqprojection (?F x)) = 1" |
184 unfolding o_def |
155 using inf_eq1 by blast |
185 by (rule lem2[rule_format]) |
|
186 have nx: "infnorm x = 1" |
156 have nx: "infnorm x = 1" |
187 apply (subst x(2)[symmetric]) |
157 by (metis (no_types, lifting) "*" inf_nega o_apply x(2)) |
188 unfolding *[symmetric] o_def |
|
189 apply (rule lem1[rule_format]) |
|
190 done |
|
191 have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i |
158 have iff: "0 < sqprojection x$i \<longleftrightarrow> 0 < x$i" "sqprojection x$i < 0 \<longleftrightarrow> x$i < 0" if "x \<noteq> 0" for x i |
192 proof - |
159 proof - |
193 have "inverse (infnorm x) > 0" |
160 have *: "inverse (infnorm x) > 0" |
194 by (simp add: infnorm_pos_lt that) |
161 by (simp add: infnorm_pos_lt that) |
195 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
162 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
196 and "(sqprojection x $ i < 0) = (x $ i < 0)" |
163 by (simp add: sqprojection_def zero_less_mult_iff) |
197 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
164 show "(sqprojection x $ i < 0) = (x $ i < 0)" |
198 unfolding zero_less_mult_iff mult_less_0_iff |
165 unfolding sqprojection_def |
199 by (auto simp add: field_simps) |
166 by (metis * pos_less_divideR_eq scaleR_zero_right vector_scaleR_component) |
200 qed |
167 qed |
201 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
168 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
202 using x(1) unfolding mem_box_cart by auto |
169 using x(1) unfolding mem_box_cart by auto |
203 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
170 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
204 using as by auto |
171 using as by auto |
221 next |
187 next |
222 case 2 |
188 case 2 |
223 then have *: "f (x $ 1) $ 1 = 1" |
189 then have *: "f (x $ 1) $ 1 = 1" |
224 using assms(6) by auto |
190 using assms(6) by auto |
225 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
191 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
226 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] 2 |
192 by (smt (verit) "2" negatex_def o_apply vector_2(1) x(2) zero_less_one) |
227 by (auto simp: negatex_def) |
|
228 moreover have "g (x $ 2) \<in> cbox (-1) 1" |
193 moreover have "g (x $ 2) \<in> cbox (-1) 1" |
229 using assms(2) x1 by blast |
194 using assms(2) x1 by blast |
230 ultimately show False |
195 ultimately show False |
231 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
196 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
232 using not_le by auto |
197 using not_le by auto |
233 next |
198 next |
234 case 3 |
199 case 3 |
235 then have *: "g (x $ 2) $ 2 = - 1" |
200 then have *: "g (x $ 2) $ 2 = - 1" |
236 using assms(7) by auto |
201 using assms(7) by auto |
237 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
202 moreover have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
238 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 3 by (auto simp: negatex_def) |
203 by (smt (verit, ccfv_SIG) "3" negatex_def o_apply vector_2(2) x(2)) |
239 moreover |
204 moreover from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
240 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
|
241 using assms(1) by blast |
205 using assms(1) by blast |
242 ultimately show False |
206 ultimately show False |
243 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
207 by (smt (verit, del_insts) iff(2) mem_box_cart(2) neg_one_index nz vector_minus_component) |
244 by (erule_tac x=2 in allE) auto |
|
245 next |
208 next |
246 case 4 |
209 case 4 |
247 then have *: "g (x $ 2) $ 2 = 1" |
210 then have *: "g (x $ 2) $ 2 = 1" |
248 using assms(8) by auto |
211 using assms(8) by auto |
249 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
212 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
250 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] 4 by (auto simp: negatex_def) |
213 by (smt (verit, best) "4" negatex_def o_apply vector_2(2) x(2)) |
251 moreover |
214 moreover |
252 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
215 from x1 have "f (x $ 1) \<in> cbox (-1) 1" |
253 using assms(1) by blast |
216 using assms(1) by blast |
254 ultimately show False |
217 ultimately show False |
255 unfolding iff[OF nz] vector_component_simps * mem_box_cart |
218 by (smt (verit) "*" iff(1) mem_box_cart(2) nz one_index vector_minus_component) |
256 by (erule_tac x=2 in allE) auto |
|
257 qed |
219 qed |
258 qed |
220 qed |
259 |
221 |
260 proposition fashoda_unit_path: |
222 proposition fashoda_unit_path: |
261 fixes f g :: "real \<Rightarrow> real^2" |
223 fixes f g :: "real \<Rightarrow> real^2" |
267 and "(pathfinish f)$1 = 1" |
229 and "(pathfinish f)$1 = 1" |
268 and "(pathstart g)$2 = -1" |
230 and "(pathstart g)$2 = -1" |
269 and "(pathfinish g)$2 = 1" |
231 and "(pathfinish g)$2 = 1" |
270 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
232 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
271 proof - |
233 proof - |
272 note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
234 note assms = assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
273 define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real |
235 define iscale where [abs_def]: "iscale z = inverse 2 *\<^sub>R (z + 1)" for z :: real |
274 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
236 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
275 unfolding iscale_def by auto |
237 unfolding iscale_def by auto |
276 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
238 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
277 proof (rule fashoda_unit) |
239 proof (rule fashoda_unit) |
278 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" |
240 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" "(g \<circ> iscale) ` {- 1..1} \<subseteq> cbox (- 1) 1" |
279 using isc and assms(3-4) by (auto simp add: image_comp [symmetric]) |
241 using isc and assms(3-4) by (auto simp add: image_comp [symmetric]) |
280 have *: "continuous_on {- 1..1} iscale" |
242 have *: "continuous_on {- 1..1} iscale" |
281 unfolding iscale_def by (rule continuous_intros)+ |
243 unfolding iscale_def by (rule continuous_intros)+ |
282 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
244 show "continuous_on {- 1..1} (f \<circ> iscale)" |
283 apply - |
245 using "*" assms(1) continuous_on_compose continuous_on_subset isc by blast |
284 apply (rule_tac[!] continuous_on_compose[OF *]) |
246 show "continuous_on {- 1..1} (g \<circ> iscale)" |
285 apply (rule_tac[!] continuous_on_subset[OF _ isc]) |
247 by (meson "*" assms(2) continuous_on_compose continuous_on_subset isc) |
286 apply (rule assms)+ |
|
287 done |
|
288 have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" |
248 have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" |
289 unfolding vec_eq_iff by auto |
249 unfolding vec_eq_iff by auto |
290 show "(f \<circ> iscale) (- 1) $ 1 = - 1" |
250 show "(f \<circ> iscale) (- 1) $ 1 = - 1" |
291 and "(f \<circ> iscale) 1 $ 1 = 1" |
251 and "(f \<circ> iscale) 1 $ 1 = 1" |
292 and "(g \<circ> iscale) (- 1) $ 2 = -1" |
252 and "(g \<circ> iscale) (- 1) $ 2 = -1" |
293 and "(g \<circ> iscale) 1 $ 2 = 1" |
253 and "(g \<circ> iscale) 1 $ 2 = 1" |
294 unfolding o_def iscale_def |
254 unfolding o_def iscale_def using assms by (auto simp add: *) |
295 using assms |
255 qed |
296 by (auto simp add: *) |
256 then obtain s t where st: "s \<in> {- 1..1}" "t \<in> {- 1..1}" "(f \<circ> iscale) s = (g \<circ> iscale) t" |
297 qed |
|
298 then obtain s t where st: |
|
299 "s \<in> {- 1..1}" |
|
300 "t \<in> {- 1..1}" |
|
301 "(f \<circ> iscale) s = (g \<circ> iscale) t" |
|
302 by auto |
257 by auto |
303 show thesis |
258 show thesis |
304 apply (rule_tac z = "f (iscale s)" in that) |
259 proof |
305 using st |
260 show "f (iscale s) \<in> path_image f" |
306 unfolding o_def path_image_def image_iff |
261 by (metis image_eqI image_subset_iff isc path_image_def st(1)) |
307 apply - |
262 show "f (iscale s) \<in> path_image g" |
308 apply (rule_tac x="iscale s" in bexI) |
263 by (metis comp_def image_eqI image_subset_iff isc path_image_def st(2) st(3)) |
309 prefer 3 |
264 qed |
310 apply (rule_tac x="iscale t" in bexI) |
|
311 using isc[unfolded subset_eq, rule_format] |
|
312 apply auto |
|
313 done |
|
314 qed |
265 qed |
315 |
266 |
316 theorem fashoda: |
267 theorem fashoda: |
317 fixes b :: "real^2" |
268 fixes b :: "real^2" |
318 assumes "path f" |
269 assumes "path f" |
337 then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" |
288 then show "a$1 = b$1 \<or> a$2 = b$2 \<or> (a$1 < b$1 \<and> a$2 < b$2)" |
338 unfolding less_eq_vec_def forall_2 by auto |
289 unfolding less_eq_vec_def forall_2 by auto |
339 next |
290 next |
340 assume as: "a$1 = b$1" |
291 assume as: "a$1 = b$1" |
341 have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" |
292 have "\<exists>z\<in>path_image g. z$2 = (pathstart f)$2" |
342 apply (rule connected_ivt_component_cart) |
293 proof (rule connected_ivt_component_cart) |
343 apply (rule connected_path_image assms)+ |
294 show "pathstart g $ 2 \<le> pathstart f $ 2" |
344 apply (rule pathstart_in_path_image) |
295 by (metis assms(3) assms(7) mem_box_cart(2) pathstart_in_path_image subset_iff) |
345 apply (rule pathfinish_in_path_image) |
296 show "pathstart f $ 2 \<le> pathfinish g $ 2" |
346 unfolding assms using assms(3)[unfolded path_image_def subset_eq,rule_format,of "f 0"] |
297 by (metis assms(3) assms(8) in_mono mem_box_cart(2) pathstart_in_path_image) |
347 unfolding pathstart_def |
298 show "connected (path_image g)" |
348 apply (auto simp add: less_eq_vec_def mem_box_cart) |
299 using assms(2) by blast |
349 done |
300 qed (auto simp: path_defs) |
350 then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" .. |
301 then obtain z :: "real^2" where z: "z \<in> path_image g" "z $ 2 = pathstart f $ 2" .. |
351 have "z \<in> cbox a b" |
302 have "z \<in> cbox a b" |
352 using z(1) assms(4) |
303 using assms(4) z(1) by blast |
353 unfolding path_image_def |
|
354 by blast |
|
355 then have "z = f 0" |
304 then have "z = f 0" |
356 unfolding vec_eq_iff forall_2 |
305 by (smt (verit) as assms(5) exhaust_2 mem_box_cart(2) nle_le pathstart_def vec_eq_iff z(2)) |
357 unfolding z(2) pathstart_def |
|
358 using assms(3)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "f 0" 1] |
|
359 unfolding mem_box_cart |
|
360 apply (erule_tac x=1 in allE) |
|
361 using as |
|
362 apply auto |
|
363 done |
|
364 then show thesis |
306 then show thesis |
365 apply - |
307 by (metis path_defs(2) pathstart_in_path_image that z(1)) |
366 apply (rule that[OF _ z(1)]) |
|
367 unfolding path_image_def |
|
368 apply auto |
|
369 done |
|
370 next |
308 next |
371 assume as: "a$2 = b$2" |
309 assume as: "a$2 = b$2" |
372 have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" |
310 have "\<exists>z\<in>path_image f. z$1 = (pathstart g)$1" |
373 apply (rule connected_ivt_component_cart) |
311 proof (rule connected_ivt_component_cart) |
374 apply (rule connected_path_image assms)+ |
312 show "pathstart f $ 1 \<le> pathstart g $ 1" |
375 apply (rule pathstart_in_path_image) |
313 using assms(4) assms(5) mem_box_cart(2) by fastforce |
376 apply (rule pathfinish_in_path_image) |
314 show "pathstart g $ 1 \<le> pathfinish f $ 1" |
377 unfolding assms |
315 using assms(4) assms(6) mem_box_cart(2) pathstart_in_path_image by fastforce |
378 using assms(4)[unfolded path_image_def subset_eq,rule_format,of "g 0"] |
316 show "connected (path_image f)" |
379 unfolding pathstart_def |
317 by (simp add: assms(1) connected_path_image) |
380 apply (auto simp add: less_eq_vec_def mem_box_cart) |
318 qed (auto simp: path_defs) |
381 done |
|
382 then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" .. |
319 then obtain z where z: "z \<in> path_image f" "z $ 1 = pathstart g $ 1" .. |
383 have "z \<in> cbox a b" |
320 have "z \<in> cbox a b" |
384 using z(1) assms(3) |
321 using assms(3) z(1) by auto |
385 unfolding path_image_def |
|
386 by blast |
|
387 then have "z = g 0" |
322 then have "z = g 0" |
388 unfolding vec_eq_iff forall_2 |
323 by (smt (verit) as assms(7) exhaust_2 mem_box_cart(2) pathstart_def vec_eq_iff z(2)) |
389 unfolding z(2) pathstart_def |
|
390 using assms(4)[unfolded path_image_def subset_eq mem_box_cart,rule_format,of "g 0" 2] |
|
391 unfolding mem_box_cart |
|
392 apply (erule_tac x=2 in allE) |
|
393 using as |
|
394 apply auto |
|
395 done |
|
396 then show thesis |
324 then show thesis |
397 apply - |
325 by (metis path_defs(2) pathstart_in_path_image that z(1)) |
398 apply (rule that[OF z(1)]) |
|
399 unfolding path_image_def |
|
400 apply auto |
|
401 done |
|
402 next |
326 next |
403 assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2" |
327 assume as: "a $ 1 < b $ 1 \<and> a $ 2 < b $ 2" |
404 have int_nem: "cbox (-1) (1::real^2) \<noteq> {}" |
328 have int_nem: "cbox (-1) (1::real^2) \<noteq> {}" |
405 unfolding interval_eq_empty_cart by auto |
329 unfolding interval_eq_empty_cart by auto |
406 obtain z :: "real^2" where z: |
330 obtain z :: "real^2" where z: |
407 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
331 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
408 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
332 "z \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
409 apply (rule fashoda_unit_path[of "interval_bij (a,b) (- 1,1) \<circ> f" "interval_bij (a,b) (- 1,1) \<circ> g"]) |
333 proof (rule fashoda_unit_path) |
410 unfolding path_def path_image_def pathstart_def pathfinish_def |
334 show "path (interval_bij (a, b) (- 1, 1) \<circ> f)" |
411 apply (rule_tac[1-2] continuous_on_compose) |
335 by (meson assms(1) continuous_on_interval_bij path_continuous_image) |
412 apply (rule assms[unfolded path_def] continuous_on_interval_bij)+ |
336 show "path (interval_bij (a, b) (- 1, 1) \<circ> g)" |
413 unfolding subset_eq |
337 by (meson assms(2) continuous_on_interval_bij path_continuous_image) |
414 apply(rule_tac[1-2] ballI) |
338 show "path_image (interval_bij (a, b) (- 1, 1) \<circ> f) \<subseteq> cbox (- 1) 1" |
415 proof - |
339 using assms(3) |
416 fix x |
340 by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq) |
417 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> f) ` {0..1}" |
341 show "path_image (interval_bij (a, b) (- 1, 1) \<circ> g) \<subseteq> cbox (- 1) 1" |
418 then obtain y where y: |
342 using assms(4) |
419 "y \<in> {0..1}" |
343 by (simp add: path_image_def in_interval_interval_bij int_nem subset_eq) |
420 "x = (interval_bij (a, b) (- 1, 1) \<circ> f) y" |
344 show "pathstart (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = - 1" |
421 unfolding image_iff .. |
345 "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> f) $ 1 = 1" |
422 show "x \<in> cbox (- 1) 1" |
346 "pathstart (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = - 1" |
423 unfolding y o_def |
347 "pathfinish (interval_bij (a, b) (- 1, 1) \<circ> g) $ 2 = 1" |
424 apply (rule in_interval_interval_bij) |
|
425 using y(1) |
|
426 using assms(3)[unfolded path_image_def subset_eq] int_nem |
|
427 apply auto |
|
428 done |
|
429 next |
|
430 fix x |
|
431 assume "x \<in> (interval_bij (a, b) (- 1, 1) \<circ> g) ` {0..1}" |
|
432 then obtain y where y: |
|
433 "y \<in> {0..1}" |
|
434 "x = (interval_bij (a, b) (- 1, 1) \<circ> g) y" |
|
435 unfolding image_iff .. |
|
436 show "x \<in> cbox (- 1) 1" |
|
437 unfolding y o_def |
|
438 apply (rule in_interval_interval_bij) |
|
439 using y(1) |
|
440 using assms(4)[unfolded path_image_def subset_eq] int_nem |
|
441 apply auto |
|
442 done |
|
443 next |
|
444 show "(interval_bij (a, b) (- 1, 1) \<circ> f) 0 $ 1 = -1" |
|
445 and "(interval_bij (a, b) (- 1, 1) \<circ> f) 1 $ 1 = 1" |
|
446 and "(interval_bij (a, b) (- 1, 1) \<circ> g) 0 $ 2 = -1" |
|
447 and "(interval_bij (a, b) (- 1, 1) \<circ> g) 1 $ 2 = 1" |
|
448 using assms as |
348 using assms as |
449 by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def) |
349 by (simp_all add: cart_eq_inner_axis pathstart_def pathfinish_def interval_bij_def) |
450 (simp_all add: inner_axis) |
350 (simp_all add: inner_axis) |
451 qed |
351 qed (auto simp: path_defs) |
452 from z(1) obtain zf where zf: |
352 then obtain zf zg where zf: "zf \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf" |
453 "zf \<in> {0..1}" |
353 and zg: "zg \<in> {0..1}" "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg" |
454 "z = (interval_bij (a, b) (- 1, 1) \<circ> f) zf" |
354 by blast |
455 unfolding image_iff .. |
|
456 from z(2) obtain zg where zg: |
|
457 "zg \<in> {0..1}" |
|
458 "z = (interval_bij (a, b) (- 1, 1) \<circ> g) zg" |
|
459 unfolding image_iff .. |
|
460 have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" |
355 have *: "\<forall>i. (- 1) $ i < (1::real^2) $ i \<and> a $ i < b $ i" |
461 unfolding forall_2 |
356 unfolding forall_2 using as by auto |
462 using as |
|
463 by auto |
|
464 show thesis |
357 show thesis |
465 proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |
358 proof (rule_tac z="interval_bij (- 1,1) (a,b) z" in that) |
466 show "interval_bij (- 1, 1) (a, b) z \<in> path_image f" |
359 show "interval_bij (- 1, 1) (a, b) z \<in> path_image f" |
467 using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def) |
360 using zf by (simp add: interval_bij_bij_cart[OF *] path_image_def) |
468 show "interval_bij (- 1, 1) (a, b) z \<in> path_image g" |
361 show "interval_bij (- 1, 1) (a, b) z \<in> path_image g" |
491 { |
384 { |
492 assume ?L |
385 assume ?L |
493 then obtain u where u: |
386 then obtain u where u: |
494 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
387 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
495 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
388 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
496 "0 \<le> u" |
389 "0 \<le> u" "u \<le> 1" |
497 "u \<le> 1" |
|
498 by blast |
390 by blast |
499 { fix b a |
391 { fix b a |
500 assume "b + u * a > a + u * b" |
392 assume "b + u * a > a + u * b" |
501 then have "(1 - u) * b > (1 - u) * a" |
393 then have "(1 - u) * b > (1 - u) * a" |
502 by (auto simp add:field_simps) |
394 by (auto simp add:field_simps) |
503 then have "b \<ge> a" |
395 then have "b \<ge> a" |
504 apply (drule_tac mult_left_less_imp_less) |
396 using not_less_iff_gr_or_eq u(4) by fastforce |
505 using u |
|
506 apply auto |
|
507 done |
|
508 then have "u * a \<le> u * b" |
397 then have "u * a \<le> u * b" |
509 apply - |
398 by (simp add: mult_left_mono u(3)) |
510 apply (rule mult_left_mono[OF _ u(3)]) |
399 } |
511 using u(3-4) |
400 moreover |
512 apply (auto simp add: field_simps) |
401 { fix a b |
513 done |
|
514 } note * = this |
|
515 { |
|
516 fix a b |
|
517 assume "u * b > u * a" |
402 assume "u * b > u * a" |
518 then have "(1 - u) * a \<le> (1 - u) * b" |
403 then have "(1 - u) * a \<le> (1 - u) * b" |
519 apply - |
404 using less_eq_real_def u(3) u(4) by force |
520 apply (rule mult_left_mono) |
|
521 apply (drule mult_left_less_imp_less) |
|
522 using u |
|
523 apply auto |
|
524 done |
|
525 then have "a + u * b \<le> b + u * a" |
405 then have "a + u * b \<le> b + u * a" |
526 by (auto simp add: field_simps) |
406 by (auto simp add: field_simps) |
527 } note ** = this |
407 } ultimately show ?R |
528 then show ?R |
408 by (force simp add: u assms field_simps not_le) |
529 unfolding u assms |
|
530 using u |
|
531 by (auto simp add:field_simps not_le intro: * **) |
|
532 } |
409 } |
533 { |
410 { |
534 assume ?R |
411 assume ?R |
535 then show ?L |
412 then show ?L |
536 proof (cases "x$2 = b$2") |
413 proof (cases "x$2 = b$2") |
537 case True |
414 case True |
538 then show ?L |
415 with \<open>?R\<close> show ?L |
539 apply (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) |
416 by (rule_tac x="(x$2 - a$2) / (b$2 - a$2)" in exI) (auto simp add: field_simps) |
540 unfolding assms True using \<open>?R\<close> apply (auto simp add: field_simps) |
|
541 done |
|
542 next |
417 next |
543 case False |
418 case False |
544 then show ?L |
419 with \<open>?R\<close> show ?L |
545 apply (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) |
420 by (rule_tac x="1 - (x$2 - b$2) / (a$2 - b$2)" in exI) (auto simp add: field_simps) |
546 unfolding assms using \<open>?R\<close> apply (auto simp add: field_simps) |
|
547 done |
|
548 qed |
421 qed |
549 } |
422 } |
550 qed |
423 qed |
551 |
424 |
|
425 text \<open>Essentially duplicate proof that could be done by swapping co-ordinates\<close> |
552 lemma segment_horizontal: |
426 lemma segment_horizontal: |
553 fixes a :: "real^2" |
427 fixes a :: "real^2" |
554 assumes "a$2 = b$2" |
428 assumes "a$2 = b$2" |
555 shows "x \<in> closed_segment a b \<longleftrightarrow> |
429 shows "x \<in> closed_segment a b \<longleftrightarrow> |
556 x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)" |
430 x$2 = a$2 \<and> x$2 = b$2 \<and> (a$1 \<le> x$1 \<and> x$1 \<le> b$1 \<or> b$1 \<le> x$1 \<and> x$1 \<le> a$1)" |
567 { |
441 { |
568 assume ?L |
442 assume ?L |
569 then obtain u where u: |
443 then obtain u where u: |
570 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
444 "x $ 1 = (1 - u) * a $ 1 + u * b $ 1" |
571 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
445 "x $ 2 = (1 - u) * a $ 2 + u * b $ 2" |
572 "0 \<le> u" |
446 "0 \<le> u" "u \<le> 1" |
573 "u \<le> 1" |
|
574 by blast |
447 by blast |
575 { |
448 { fix b a |
576 fix b a |
|
577 assume "b + u * a > a + u * b" |
449 assume "b + u * a > a + u * b" |
578 then have "(1 - u) * b > (1 - u) * a" |
450 then have "(1 - u) * b > (1 - u) * a" |
579 by (auto simp add: field_simps) |
451 by (auto simp add: field_simps) |
580 then have "b \<ge> a" |
452 then have "b \<ge> a" |
581 apply (drule_tac mult_left_less_imp_less) |
453 by (smt (verit, best) mult_left_mono u(4)) |
582 using u |
|
583 apply auto |
|
584 done |
|
585 then have "u * a \<le> u * b" |
454 then have "u * a \<le> u * b" |
586 apply - |
455 by (simp add: mult_left_mono u(3)) |
587 apply (rule mult_left_mono[OF _ u(3)]) |
456 } |
588 using u(3-4) |
457 moreover |
589 apply (auto simp add: field_simps) |
458 { fix a b |
590 done |
|
591 } note * = this |
|
592 { |
|
593 fix a b |
|
594 assume "u * b > u * a" |
459 assume "u * b > u * a" |
595 then have "(1 - u) * a \<le> (1 - u) * b" |
460 then have "(1 - u) * a \<le> (1 - u) * b" |
596 apply - |
461 using less_eq_real_def u(3) u(4) by force |
597 apply (rule mult_left_mono) |
|
598 apply (drule mult_left_less_imp_less) |
|
599 using u |
|
600 apply auto |
|
601 done |
|
602 then have "a + u * b \<le> b + u * a" |
462 then have "a + u * b \<le> b + u * a" |
603 by (auto simp add: field_simps) |
463 by (auto simp add: field_simps) |
604 } note ** = this |
464 } |
605 then show ?R |
465 ultimately show ?R |
606 unfolding u assms |
466 by (force simp add: u assms field_simps not_le intro: ) |
607 using u |
|
608 by (auto simp add: field_simps not_le intro: * **) |
|
609 } |
467 } |
610 { |
468 { assume ?R |
611 assume ?R |
|
612 then show ?L |
469 then show ?L |
613 proof (cases "x$1 = b$1") |
470 proof (cases "x$1 = b$1") |
614 case True |
471 case True |
615 then show ?L |
472 with \<open>?R\<close> show ?L |
616 apply (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) |
473 by (rule_tac x="(x$1 - a$1) / (b$1 - a$1)" in exI) (auto simp add: field_simps) |
617 unfolding assms True |
|
618 using \<open>?R\<close> |
|
619 apply (auto simp add: field_simps) |
|
620 done |
|
621 next |
474 next |
622 case False |
475 case False |
623 then show ?L |
476 with \<open>?R\<close> show ?L |
624 apply (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) |
477 by (rule_tac x="1 - (x$1 - b$1) / (a$1 - b$1)" in exI) (auto simp add: field_simps) |
625 unfolding assms |
|
626 using \<open>?R\<close> |
|
627 apply (auto simp add: field_simps) |
|
628 done |
|
629 qed |
478 qed |
630 } |
479 } |
631 qed |
480 qed |
632 |
481 |
633 |
482 |