13 by (simp add: inner_axis) |
14 by (simp add: inner_axis) |
14 |
15 |
15 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis" |
16 lemma axis_in_Basis: "a \<in> Basis \<Longrightarrow> axis i a \<in> Basis" |
16 by (auto simp add: Basis_vec_def axis_eq_axis) |
17 by (auto simp add: Basis_vec_def axis_eq_axis) |
17 |
18 |
18 subsection {*Fashoda meet theorem. *} |
19 |
19 |
20 subsection {* Fashoda meet theorem *} |
20 lemma infnorm_2: "infnorm (x::real^2) = max (abs(x$1)) (abs(x$2))" |
21 |
21 unfolding infnorm_cart UNIV_2 apply(rule cSup_eq) by auto |
22 lemma infnorm_2: |
22 |
23 fixes x :: "real^2" |
23 lemma infnorm_eq_1_2: "infnorm (x::real^2) = 1 \<longleftrightarrow> |
24 shows "infnorm x = max (abs (x$1)) (abs (x$2))" |
24 (abs(x$1) \<le> 1 \<and> abs(x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1))" |
25 unfolding infnorm_cart UNIV_2 by (rule cSup_eq) auto |
|
26 |
|
27 lemma infnorm_eq_1_2: |
|
28 fixes x :: "real^2" |
|
29 shows "infnorm x = 1 \<longleftrightarrow> |
|
30 abs (x$1) \<le> 1 \<and> abs (x$2) \<le> 1 \<and> (x$1 = -1 \<or> x$1 = 1 \<or> x$2 = -1 \<or> x$2 = 1)" |
25 unfolding infnorm_2 by auto |
31 unfolding infnorm_2 by auto |
26 |
32 |
27 lemma infnorm_eq_1_imp: assumes "infnorm (x::real^2) = 1" shows "abs(x$1) \<le> 1" "abs(x$2) \<le> 1" |
33 lemma infnorm_eq_1_imp: |
|
34 fixes x :: "real^2" |
|
35 assumes "infnorm x = 1" |
|
36 shows "abs (x$1) \<le> 1" and "abs (x$2) \<le> 1" |
28 using assms unfolding infnorm_eq_1_2 by auto |
37 using assms unfolding infnorm_eq_1_2 by auto |
29 |
38 |
30 lemma fashoda_unit: fixes f g::"real \<Rightarrow> real^2" |
39 lemma fashoda_unit: |
31 assumes "f ` {- 1..1} \<subseteq> {- 1..1}" "g ` {- 1..1} \<subseteq> {- 1..1}" |
40 fixes f g :: "real \<Rightarrow> real^2" |
32 "continuous_on {- 1..1} f" "continuous_on {- 1..1} g" |
41 assumes "f ` {- 1..1} \<subseteq> {- 1..1}" |
33 "f (- 1)$1 = - 1" "f 1$1 = 1" "g (- 1) $2 = -1" "g 1 $2 = 1" |
42 and "g ` {- 1..1} \<subseteq> {- 1..1}" |
34 shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" proof(rule ccontr) |
43 and "continuous_on {- 1..1} f" |
35 case goal1 note as = this[unfolded bex_simps,rule_format] |
44 and "continuous_on {- 1..1} g" |
|
45 and "f (- 1)$1 = - 1" |
|
46 and "f 1$1 = 1" "g (- 1) $2 = -1" |
|
47 and "g 1 $2 = 1" |
|
48 shows "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. f s = g t" |
|
49 proof (rule ccontr) |
|
50 assume "\<not> ?thesis" |
|
51 note as = this[unfolded bex_simps,rule_format] |
36 def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" |
52 def sqprojection \<equiv> "\<lambda>z::real^2. (inverse (infnorm z)) *\<^sub>R z" |
37 def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" |
53 def negatex \<equiv> "\<lambda>x::real^2. (vector [-(x$1), x$2])::real^2" |
38 have lem1:"\<forall>z::real^2. infnorm(negatex z) = infnorm z" |
54 have lem1: "\<forall>z::real^2. infnorm (negatex z) = infnorm z" |
39 unfolding negatex_def infnorm_2 vector_2 by auto |
55 unfolding negatex_def infnorm_2 vector_2 by auto |
40 have lem2:"\<forall>z. z\<noteq>0 \<longrightarrow> infnorm(sqprojection z) = 1" unfolding sqprojection_def |
56 have lem2: "\<forall>z. z \<noteq> 0 \<longrightarrow> infnorm (sqprojection z) = 1" |
41 unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] unfolding abs_inverse real_abs_infnorm |
57 unfolding sqprojection_def |
42 apply(subst infnorm_eq_0[THEN sym]) by auto |
58 unfolding infnorm_mul[unfolded scalar_mult_eq_scaleR] |
43 let ?F = "(\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w)" |
59 unfolding abs_inverse real_abs_infnorm |
44 have *:"\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}" |
60 apply (subst infnorm_eq_0[THEN sym]) |
45 apply(rule set_eqI) unfolding image_iff Bex_def mem_interval_cart apply rule defer |
61 apply auto |
46 apply(rule_tac x="vec x" in exI) by auto |
62 done |
47 { fix x assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}" |
63 let ?F = "\<lambda>w::real^2. (f \<circ> (\<lambda>x. x$1)) w - (g \<circ> (\<lambda>x. x$2)) w" |
|
64 have *: "\<And>i. (\<lambda>x::real^2. x $ i) ` {- 1..1} = {- 1..1::real}" |
|
65 apply (rule set_eqI) |
|
66 unfolding image_iff Bex_def mem_interval_cart |
|
67 apply rule |
|
68 defer |
|
69 apply (rule_tac x="vec x" in exI) |
|
70 apply auto |
|
71 done |
|
72 { |
|
73 fix x |
|
74 assume "x \<in> (\<lambda>w. (f \<circ> (\<lambda>x. x $ 1)) w - (g \<circ> (\<lambda>x. x $ 2)) w) ` {- 1..1::real^2}" |
48 then guess w unfolding image_iff .. note w = this |
75 then guess w unfolding image_iff .. note w = this |
49 hence "x \<noteq> 0" using as[of "w$1" "w$2"] unfolding mem_interval_cart by auto} note x0=this |
76 then have "x \<noteq> 0" |
50 have 21:"\<And>i::2. i\<noteq>1 \<Longrightarrow> i=2" using UNIV_2 by auto |
77 using as[of "w$1" "w$2"] |
51 have 1:"{- 1<..<1::real^2} \<noteq> {}" unfolding interval_eq_empty_cart by auto |
78 unfolding mem_interval_cart |
52 have 2:"continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" |
79 by auto |
53 apply(intro continuous_on_intros continuous_on_component) |
80 } note x0 = this |
54 unfolding * apply(rule assms)+ |
81 have 21: "\<And>i::2. i \<noteq> 1 \<Longrightarrow> i = 2" |
55 apply(subst sqprojection_def) |
82 using UNIV_2 by auto |
56 apply(intro continuous_on_intros) |
83 have 1: "{- 1<..<1::real^2} \<noteq> {}" |
57 apply(simp add: infnorm_eq_0 x0) |
84 unfolding interval_eq_empty_cart by auto |
58 apply(rule linear_continuous_on) |
85 have 2: "continuous_on {- 1..1} (negatex \<circ> sqprojection \<circ> ?F)" |
59 proof- |
86 apply (intro continuous_on_intros continuous_on_component) |
60 show "bounded_linear negatex" apply(rule bounded_linearI') unfolding vec_eq_iff proof(rule_tac[!] allI) fix i::2 and x y::"real^2" and c::real |
87 unfolding * |
61 show "negatex (x + y) $ i = (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
88 apply (rule assms)+ |
62 apply-apply(case_tac[!] "i\<noteq>1") prefer 3 apply(drule_tac[1-2] 21) |
89 apply (subst sqprojection_def) |
63 unfolding negatex_def by(auto simp add:vector_2 ) qed |
90 apply (intro continuous_on_intros) |
|
91 apply (simp add: infnorm_eq_0 x0) |
|
92 apply (rule linear_continuous_on) |
|
93 proof - |
|
94 show "bounded_linear negatex" |
|
95 apply (rule bounded_linearI') |
|
96 unfolding vec_eq_iff |
|
97 proof (rule_tac[!] allI) |
|
98 fix i :: 2 |
|
99 fix x y :: "real^2" |
|
100 fix c :: real |
|
101 show "negatex (x + y) $ i = |
|
102 (negatex x + negatex y) $ i" "negatex (c *\<^sub>R x) $ i = (c *\<^sub>R negatex x) $ i" |
|
103 apply - |
|
104 apply (case_tac[!] "i\<noteq>1") |
|
105 prefer 3 |
|
106 apply (drule_tac[1-2] 21) |
|
107 unfolding negatex_def |
|
108 apply (auto simp add:vector_2) |
|
109 done |
|
110 qed |
64 qed |
111 qed |
65 have 3:"(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" unfolding subset_eq apply rule proof- |
112 have 3: "(negatex \<circ> sqprojection \<circ> ?F) ` {- 1..1} \<subseteq> {- 1..1}" |
66 case goal1 then guess y unfolding image_iff .. note y=this have "?F y \<noteq> 0" apply(rule x0) using y(1) by auto |
113 unfolding subset_eq |
67 hence *:"infnorm (sqprojection (?F y)) = 1" unfolding y o_def apply- by(rule lem2[rule_format]) |
114 apply rule |
68 have "infnorm x = 1" unfolding *[THEN sym] y o_def by(rule lem1[rule_format]) |
115 proof - |
69 thus "x\<in>{- 1..1}" unfolding mem_interval_cart infnorm_2 apply- apply rule |
116 case goal1 |
70 proof-case goal1 thus ?case apply(cases "i=1") defer apply(drule 21) by auto qed qed |
117 then guess y unfolding image_iff .. note y=this |
71 guess x apply(rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"]) |
118 have "?F y \<noteq> 0" |
72 apply(rule compact_interval convex_interval)+ unfolding interior_closed_interval |
119 apply (rule x0) |
73 apply(rule 1 2 3)+ . note x=this |
120 using y(1) |
74 have "?F x \<noteq> 0" apply(rule x0) using x(1) by auto |
121 apply auto |
75 hence *:"infnorm (sqprojection (?F x)) = 1" unfolding o_def by(rule lem2[rule_format]) |
122 done |
76 have nx:"infnorm x = 1" apply(subst x(2)[THEN sym]) unfolding *[THEN sym] o_def by(rule lem1[rule_format]) |
123 then have *: "infnorm (sqprojection (?F y)) = 1" |
77 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)" |
124 unfolding y o_def by - (rule lem2[rule_format]) |
78 apply- apply(rule_tac[!] allI impI)+ proof- fix x::"real^2" and i::2 assume x:"x\<noteq>0" |
125 have "infnorm x = 1" |
79 have "inverse (infnorm x) > 0" using x[unfolded infnorm_pos_lt[THEN sym]] by auto |
126 unfolding *[THEN sym] y o_def by (rule lem1[rule_format]) |
80 thus "(0 < sqprojection x $ i) = (0 < x $ i)" "(sqprojection x $ i < 0) = (x $ i < 0)" |
127 then show "x \<in> {- 1..1}" |
|
128 unfolding mem_interval_cart infnorm_2 |
|
129 apply - |
|
130 apply rule |
|
131 proof - |
|
132 case goal1 |
|
133 then show ?case |
|
134 apply (cases "i = 1") |
|
135 defer |
|
136 apply (drule 21) |
|
137 apply auto |
|
138 done |
|
139 qed |
|
140 qed |
|
141 guess x |
|
142 apply (rule brouwer_weak[of "{- 1..1::real^2}" "negatex \<circ> sqprojection \<circ> ?F"]) |
|
143 apply (rule compact_interval convex_interval)+ unfolding interior_closed_interval |
|
144 apply (rule 1 2 3)+ |
|
145 done |
|
146 note x=this |
|
147 have "?F x \<noteq> 0" |
|
148 apply (rule x0) |
|
149 using x(1) |
|
150 apply auto |
|
151 done |
|
152 then have *: "infnorm (sqprojection (?F x)) = 1" |
|
153 unfolding o_def by (rule lem2[rule_format]) |
|
154 have nx: "infnorm x = 1" |
|
155 apply (subst x(2)[THEN sym]) |
|
156 unfolding *[THEN sym] o_def |
|
157 apply (rule lem1[rule_format]) |
|
158 done |
|
159 have "\<forall>x i. x \<noteq> 0 \<longrightarrow> (0 < (sqprojection x)$i \<longleftrightarrow> 0 < x$i)" |
|
160 and "\<forall>x i. x \<noteq> 0 \<longrightarrow> ((sqprojection x)$i < 0 \<longleftrightarrow> x$i < 0)" |
|
161 apply - |
|
162 apply (rule_tac[!] allI impI)+ |
|
163 proof - |
|
164 fix x :: "real^2" |
|
165 fix i :: 2 |
|
166 assume x: "x \<noteq> 0" |
|
167 have "inverse (infnorm x) > 0" |
|
168 using x[unfolded infnorm_pos_lt[THEN sym]] by auto |
|
169 then show "(0 < sqprojection x $ i) = (0 < x $ i)" |
|
170 and "(sqprojection x $ i < 0) = (x $ i < 0)" |
81 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
171 unfolding sqprojection_def vector_component_simps vector_scaleR_component real_scaleR_def |
82 unfolding zero_less_mult_iff mult_less_0_iff by(auto simp add:field_simps) qed |
172 unfolding zero_less_mult_iff mult_less_0_iff |
|
173 by (auto simp add: field_simps) |
|
174 qed |
83 note lem3 = this[rule_format] |
175 note lem3 = this[rule_format] |
84 have x1:"x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" using x(1) unfolding mem_interval_cart by auto |
176 have x1: "x $ 1 \<in> {- 1..1::real}" "x $ 2 \<in> {- 1..1::real}" |
85 hence nz:"f (x $ 1) - g (x $ 2) \<noteq> 0" unfolding right_minus_eq apply-apply(rule as) by auto |
177 using x(1) unfolding mem_interval_cart by auto |
86 have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" using nx unfolding infnorm_eq_1_2 by auto |
178 then have nz: "f (x $ 1) - g (x $ 2) \<noteq> 0" |
87 thus False proof- fix P Q R S |
179 unfolding right_minus_eq |
88 presume "P \<or> Q \<or> R \<or> S" "P\<Longrightarrow>False" "Q\<Longrightarrow>False" "R\<Longrightarrow>False" "S\<Longrightarrow>False" thus False by auto |
180 apply - |
89 next assume as:"x$1 = 1" |
181 apply (rule as) |
90 hence *:"f (x $ 1) $ 1 = 1" using assms(6) by auto |
182 apply auto |
|
183 done |
|
184 have "x $ 1 = -1 \<or> x $ 1 = 1 \<or> x $ 2 = -1 \<or> x $ 2 = 1" |
|
185 using nx unfolding infnorm_eq_1_2 by auto |
|
186 then show False |
|
187 proof - |
|
188 fix P Q R S |
|
189 presume "P \<or> Q \<or> R \<or> S" |
|
190 and "P \<Longrightarrow> False" |
|
191 and "Q \<Longrightarrow> False" |
|
192 and "R \<Longrightarrow> False" |
|
193 and "S \<Longrightarrow> False" |
|
194 then show False by auto |
|
195 next |
|
196 assume as: "x$1 = 1" |
|
197 then have *: "f (x $ 1) $ 1 = 1" |
|
198 using assms(6) by auto |
91 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
199 have "sqprojection (f (x$1) - g (x$2)) $ 1 < 0" |
92 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
200 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
93 unfolding as negatex_def vector_2 by auto moreover |
201 unfolding as negatex_def vector_2 |
94 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto |
202 by auto |
95 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
203 moreover |
96 apply(erule_tac x=1 in allE) by auto |
204 from x1 have "g (x $ 2) \<in> {- 1..1}" |
97 next assume as:"x$1 = -1" |
205 apply - |
98 hence *:"f (x $ 1) $ 1 = - 1" using assms(5) by auto |
206 apply (rule assms(2)[unfolded subset_eq,rule_format]) |
|
207 apply auto |
|
208 done |
|
209 ultimately show False |
|
210 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
211 apply (erule_tac x=1 in allE) |
|
212 apply auto |
|
213 done |
|
214 next |
|
215 assume as: "x$1 = -1" |
|
216 then have *: "f (x $ 1) $ 1 = - 1" |
|
217 using assms(5) by auto |
99 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
218 have "sqprojection (f (x$1) - g (x$2)) $ 1 > 0" |
100 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
219 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=1]] |
101 unfolding as negatex_def vector_2 by auto moreover |
220 unfolding as negatex_def vector_2 |
102 from x1 have "g (x $ 2) \<in> {- 1..1}" apply-apply(rule assms(2)[unfolded subset_eq,rule_format]) by auto |
221 by auto |
103 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
222 moreover |
104 apply(erule_tac x=1 in allE) by auto |
223 from x1 have "g (x $ 2) \<in> {- 1..1}" |
105 next assume as:"x$2 = 1" |
224 apply - |
106 hence *:"g (x $ 2) $ 2 = 1" using assms(8) by auto |
225 apply (rule assms(2)[unfolded subset_eq,rule_format]) |
|
226 apply auto |
|
227 done |
|
228 ultimately show False |
|
229 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
230 apply (erule_tac x=1 in allE) |
|
231 apply auto |
|
232 done |
|
233 next |
|
234 assume as: "x$2 = 1" |
|
235 then have *: "g (x $ 2) $ 2 = 1" |
|
236 using assms(8) by auto |
107 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
237 have "sqprojection (f (x$1) - g (x$2)) $ 2 > 0" |
108 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
238 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
109 unfolding as negatex_def vector_2 by auto moreover |
239 unfolding as negatex_def vector_2 |
110 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto |
240 by auto |
111 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
241 moreover |
112 apply(erule_tac x=2 in allE) by auto |
242 from x1 have "f (x $ 1) \<in> {- 1..1}" |
113 next assume as:"x$2 = -1" |
243 apply - |
114 hence *:"g (x $ 2) $ 2 = - 1" using assms(7) by auto |
244 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
|
245 apply auto |
|
246 done |
|
247 ultimately show False |
|
248 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
249 apply (erule_tac x=2 in allE) |
|
250 apply auto |
|
251 done |
|
252 next |
|
253 assume as: "x$2 = -1" |
|
254 then have *: "g (x $ 2) $ 2 = - 1" |
|
255 using assms(7) by auto |
115 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
256 have "sqprojection (f (x$1) - g (x$2)) $ 2 < 0" |
116 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
257 using x(2)[unfolded o_def vec_eq_iff,THEN spec[where x=2]] |
117 unfolding as negatex_def vector_2 by auto moreover |
258 unfolding as negatex_def vector_2 |
118 from x1 have "f (x $ 1) \<in> {- 1..1}" apply-apply(rule assms(1)[unfolded subset_eq,rule_format]) by auto |
259 by auto |
119 ultimately show False unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
260 moreover |
120 apply(erule_tac x=2 in allE) by auto qed(auto) qed |
261 from x1 have "f (x $ 1) \<in> {- 1..1}" |
121 |
262 apply - |
122 lemma fashoda_unit_path: fixes f ::"real \<Rightarrow> real^2" and g ::"real \<Rightarrow> real^2" |
263 apply (rule assms(1)[unfolded subset_eq,rule_format]) |
123 assumes "path f" "path g" "path_image f \<subseteq> {- 1..1}" "path_image g \<subseteq> {- 1..1}" |
264 apply auto |
124 "(pathstart f)$1 = -1" "(pathfinish f)$1 = 1" "(pathstart g)$2 = -1" "(pathfinish g)$2 = 1" |
265 done |
125 obtains z where "z \<in> path_image f" "z \<in> path_image g" proof- |
266 ultimately show False |
|
267 unfolding lem3[OF nz] vector_component_simps * mem_interval_cart |
|
268 apply (erule_tac x=2 in allE) |
|
269 apply auto |
|
270 done |
|
271 qed auto |
|
272 qed |
|
273 |
|
274 lemma fashoda_unit_path: |
|
275 fixes f g :: "real \<Rightarrow> real^2" |
|
276 assumes "path f" |
|
277 and "path g" |
|
278 and "path_image f \<subseteq> {- 1..1}" |
|
279 and "path_image g \<subseteq> {- 1..1}" |
|
280 and "(pathstart f)$1 = -1" |
|
281 and "(pathfinish f)$1 = 1" |
|
282 and "(pathstart g)$2 = -1" |
|
283 and "(pathfinish g)$2 = 1" |
|
284 obtains z where "z \<in> path_image f" and "z \<in> path_image g" |
|
285 proof - |
126 note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
286 note assms=assms[unfolded path_def pathstart_def pathfinish_def path_image_def] |
127 def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" |
287 def iscale \<equiv> "\<lambda>z::real. inverse 2 *\<^sub>R (z + 1)" |
128 have isc:"iscale ` {- 1..1} \<subseteq> {0..1}" unfolding iscale_def by(auto) |
288 have isc: "iscale ` {- 1..1} \<subseteq> {0..1}" |
129 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" proof(rule fashoda_unit) |
289 unfolding iscale_def by auto |
|
290 have "\<exists>s\<in>{- 1..1}. \<exists>t\<in>{- 1..1}. (f \<circ> iscale) s = (g \<circ> iscale) t" |
|
291 proof (rule fashoda_unit) |
130 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" |
292 show "(f \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" "(g \<circ> iscale) ` {- 1..1} \<subseteq> {- 1..1}" |
131 using isc and assms(3-4) unfolding image_compose by auto |
293 using isc and assms(3-4) unfolding image_compose by auto |
132 have *:"continuous_on {- 1..1} iscale" unfolding iscale_def by(rule continuous_on_intros)+ |
294 have *: "continuous_on {- 1..1} iscale" |
|
295 unfolding iscale_def by (rule continuous_on_intros)+ |
133 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
296 show "continuous_on {- 1..1} (f \<circ> iscale)" "continuous_on {- 1..1} (g \<circ> iscale)" |
134 apply-apply(rule_tac[!] continuous_on_compose[OF *]) apply(rule_tac[!] continuous_on_subset[OF _ isc]) |
297 apply - |
135 by(rule assms)+ have *:"(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" unfolding vec_eq_iff by auto |
298 apply (rule_tac[!] continuous_on_compose[OF *]) |
136 show "(f \<circ> iscale) (- 1) $ 1 = - 1" "(f \<circ> iscale) 1 $ 1 = 1" "(g \<circ> iscale) (- 1) $ 2 = -1" "(g \<circ> iscale) 1 $ 2 = 1" |
299 apply (rule_tac[!] continuous_on_subset[OF _ isc]) |
137 unfolding o_def iscale_def using assms by(auto simp add:*) qed |
300 apply (rule assms)+ |
|
301 done |
|
302 have *: "(1 / 2) *\<^sub>R (1 + (1::real^1)) = 1" |
|
303 unfolding vec_eq_iff by auto |
|
304 show "(f \<circ> iscale) (- 1) $ 1 = - 1" |
|
305 and "(f \<circ> iscale) 1 $ 1 = 1" |
|
306 and "(g \<circ> iscale) (- 1) $ 2 = -1" |
|
307 and "(g \<circ> iscale) 1 $ 2 = 1" |
|
308 unfolding o_def iscale_def |
|
309 using assms |
|
310 by (auto simp add: *) |
|
311 qed |
138 then guess s .. from this(2) guess t .. note st=this |
312 then guess s .. from this(2) guess t .. note st=this |
139 show thesis apply(rule_tac z="f (iscale s)" in that) |
313 show thesis |
140 using st `s\<in>{- 1..1}` unfolding o_def path_image_def image_iff apply- |
314 apply (rule_tac z="f (iscale s)" in that) |
141 apply(rule_tac x="iscale s" in bexI) prefer 3 apply(rule_tac x="iscale t" in bexI) |
315 using st `s\<in>{- 1..1}` |
142 using isc[unfolded subset_eq, rule_format] by auto qed |
316 unfolding o_def path_image_def image_iff |
|
317 apply - |
|
318 apply (rule_tac x="iscale s" in bexI) |
|
319 prefer 3 |
|
320 apply (rule_tac x="iscale t" in bexI) |
|
321 using isc[unfolded subset_eq, rule_format] |
|
322 apply auto |
|
323 done |
|
324 qed |
143 |
325 |
144 lemma fashoda: fixes b::"real^2" |
326 lemma fashoda: fixes b::"real^2" |
145 assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" |
327 assumes "path f" "path g" "path_image f \<subseteq> {a..b}" "path_image g \<subseteq> {a..b}" |
146 "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1" |
328 "(pathstart f)$1 = a$1" "(pathfinish f)$1 = b$1" |
147 "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2" |
329 "(pathstart g)$2 = a$2" "(pathfinish g)$2 = b$2" |