1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
3 (* Section: Conclusions *)
4 (* Chapter: Local Fan *)
5 (* Lemma: XBJRPHC, PQCSXWG *)
6 (* Author: John Harrison *)
8 (* ========================================================================== *)
11 The continuity of the functions dihV and azim.
13 Removed from project July 22, 2013. All the necessary theorems have been duplicated in flyspeck.ml
16 module Xbjrphc = struct
18 (* ========================================================================= *)
19 (* More complex analysis. *)
20 (* ========================================================================= *)
22 needs "Multivariate/flyspeck.ml";;
24 (* ------------------------------------------------------------------------- *)
25 (* Some of the material at the top of the file may be repetitive.
26 It was patched together from various email messages from J.H. to T.H. *)
27 (* ------------------------------------------------------------------------- *)
30 let REAL_CONTINUOUS_AT_DIHV = prove
32 ~collinear {v, w, w2} ==> dihV v w w1 real_continuous at w2`,
33 REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
34 REWRITE_TAC[dihV] THEN CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
35 GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
36 MATCH_MP_TAC REAL_CONTINUOUS_CONTINUOUS_AT_COMPOSE THEN CONJ_TAC THENL
37 [MATCH_MP_TAC CONTINUOUS_SUB THEN CONJ_TAC THEN
38 MATCH_MP_TAC CONTINUOUS_MUL THEN
39 SIMP_TAC[CONTINUOUS_CONST; o_DEF; CONTINUOUS_SUB; CONTINUOUS_AT_ID;
40 CONTINUOUS_AT_LIFT_DOT2];
41 GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN
42 REWRITE_TAC[ARCV_ANGLE; angle] THEN
43 REWRITE_TAC[VECTOR_SUB_RZERO; ETA_AX] THEN
44 MATCH_MP_TAC REAL_CONTINUOUS_WITHIN_VECTOR_ANGLE THEN
45 POP_ASSUM MP_TAC THEN GEOM_ORIGIN_TAC `v:real^N` THEN
46 REWRITE_TAC[VECTOR_SUB_RZERO; CONTRAPOS_THM; VECTOR_SUB_EQ] THEN
47 MAP_EVERY X_GEN_TAC [`z:real^N`; `w:real^N`] THEN
48 ASM_CASES_TAC `w:real^N = vec 0` THEN
49 ASM_REWRITE_TAC[COLLINEAR_LEMMA_ALT] THEN DISCH_THEN(MP_TAC o AP_TERM
50 `(%) (inv((w:real^N) dot w)):real^N->real^N`) THEN
51 ASM_SIMP_TAC[VECTOR_MUL_ASSOC; REAL_MUL_LINV; DOT_EQ_0] THEN
52 MESON_TAC[VECTOR_MUL_LID]]);;
55 (* ------------------------------------------------------------------------- *)
56 (* A few general lemmas. *)
57 (* ------------------------------------------------------------------------- *)
59 let COLLINEAR_3_DOT_MULTIPLES = prove
62 ((b - a) dot (b - a)) % (c - a) = ((c - a) dot (b - a)) % (b - a)`,
63 GEOM_ORIGIN_TAC `a:real^N` THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN
64 REPEAT GEN_TAC THEN ASM_CASES_TAC `b:real^N = vec 0` THENL
65 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC; DOT_RZERO; VECTOR_MUL_LZERO];
66 ONCE_REWRITE_TAC[GSYM VECTOR_SUB_EQ] THEN POP_ASSUM MP_TAC THEN
67 REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL; GSYM DOT_EQ_0] THEN
68 REWRITE_TAC[GSYM DOT_EQ_0; DOT_RSUB; DOT_LSUB; DOT_RMUL; DOT_LMUL] THEN
69 REWRITE_TAC[DOT_SYM] THEN CONV_TAC REAL_RING]);;
71 let CONTINUOUS_CONTINUOUS_WITHINREAL = prove
72 (`!f x s. f continuous (atreal x within s) <=>
73 (f o drop) continuous (at (lift x) within IMAGE lift s)`,
74 REWRITE_TAC[REALLIM_WITHINREAL_WITHIN; CONTINUOUS_WITHIN;
75 CONTINUOUS_WITHINREAL; o_DEF; LIFT_DROP; LIM_WITHINREAL_WITHIN]);;
77 let CONTINUOUS_CONTINUOUS_ATREAL = prove
78 (`!f x. f continuous (atreal x) <=> (f o drop) continuous (at (lift x))`,
79 REWRITE_TAC[REALLIM_ATREAL_AT; CONTINUOUS_AT;
80 CONTINUOUS_ATREAL; o_DEF; LIFT_DROP; LIM_ATREAL_AT]);;
82 let REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL = prove
83 (`!f x s. f real_continuous (atreal x within s) <=>
84 (f o drop) real_continuous (at (lift x) within IMAGE lift s)`,
85 REWRITE_TAC[REALLIM_WITHINREAL_WITHIN; REAL_CONTINUOUS_WITHIN;
86 REAL_CONTINUOUS_WITHINREAL; o_DEF; LIFT_DROP;
87 LIM_WITHINREAL_WITHIN]);;
89 let REAL_CONTINUOUS_REAL_CONTINUOUS_ATREAL = prove
90 (`!f x. f real_continuous (atreal x) <=>
91 (f o drop) real_continuous (at (lift x))`,
92 REWRITE_TAC[REALLIM_ATREAL_AT; REAL_CONTINUOUS_AT;
93 REAL_CONTINUOUS_ATREAL; o_DEF; LIFT_DROP; LIM_ATREAL_AT]);;
95 (* ------------------------------------------------------------------------- *)
96 (* Stronger dihV continuity results. *)
97 (* ------------------------------------------------------------------------- *)
99 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE = prove
100 (`!f:real^M->real^N g x s.
101 ~(f x = vec 0) /\ ~(g x = vec 0) /\
102 f continuous (at x within s) /\
103 g continuous (at x within s)
104 ==> (\x. Cx(vector_angle (f x) (g x))) continuous (at x within s)`,
105 REPEAT STRIP_TAC THEN
106 ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THEN
107 ASM_SIMP_TAC[CONTINUOUS_TRIVIAL_LIMIT; vector_angle] THEN
109 `(cacs o (\x. Cx(((f x:real^N) dot g x) / (norm(f x) * norm(g x)))))
110 continuous (at (x:real^M) within s)`
112 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN CONJ_TAC THENL
113 [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
114 MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
115 ASM_SIMP_TAC[NETLIMIT_WITHIN; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
116 REWRITE_TAC[CONTINUOUS_CX_LIFT; GSYM CX_MUL; LIFT_CMUL] THEN
117 ASM_SIMP_TAC[CONTINUOUS_WITHIN_LIFT_DOT2] THEN
118 MATCH_MP_TAC CONTINUOUS_MUL THEN
119 ASM_SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; o_DEF];
120 MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
121 EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
122 REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
123 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
124 REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]];
125 ASM_SIMP_TAC[CONTINUOUS_WITHIN; CX_ACS; o_DEF;
126 NORM_CAUCHY_SCHWARZ_DIV] THEN
127 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
129 `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
130 ~((g:real^M->real^N) y = vec 0))
133 [REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
134 [UNDISCH_TAC `(f:real^M->real^N) continuous (at x within s)`;
135 UNDISCH_TAC `(g:real^M->real^N) continuous (at x within s)`] THEN
136 REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THENL
137 [DISCH_THEN(MP_TAC o SPEC `norm((f:real^M->real^N) x)`);
138 DISCH_THEN(MP_TAC o SPEC `norm((g:real^M->real^N) x)`)] THEN
139 ASM_REWRITE_TAC[NORM_POS_LT] THEN
140 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
141 REWRITE_TAC[] THEN CONV_TAC NORM_ARITH;
142 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
143 SIMP_TAC[CX_ACS; NORM_CAUCHY_SCHWARZ_DIV]]]);;
145 let REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE = prove
146 (`!f:real^M->real^N g h k x s.
147 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
148 f continuous (at x within s) /\ g continuous (at x within s) /\
149 h continuous (at x within s) /\ k continuous (at x within s)
150 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (at x within s)`,
151 REPEAT STRIP_TAC THEN REWRITE_TAC[dihV] THEN
152 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
153 REWRITE_TAC[ARCV_ANGLE; angle; REAL_CONTINUOUS_CONTINUOUS; o_DEF] THEN
154 REWRITE_TAC[VECTOR_SUB_RZERO] THEN
155 MATCH_MP_TAC CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE THEN
156 ASM_REWRITE_TAC[VECTOR_SUB_EQ; GSYM COLLINEAR_3_DOT_MULTIPLES] THEN
157 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_SUB THEN CONJ_TAC THEN
158 MATCH_MP_TAC CONTINUOUS_MUL THEN REWRITE_TAC[o_DEF] THEN
159 ASM_SIMP_TAC[CONTINUOUS_WITHIN_LIFT_DOT2; o_DEF; CONTINUOUS_SUB]);;
161 let REAL_CONTINUOUS_AT_DIHV_COMPOSE = prove
162 (`!f:real^M->real^N g h k x.
163 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
164 f continuous (at x) /\ g continuous (at x) /\
165 h continuous (at x) /\ k continuous (at x)
166 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (at x)`,
167 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
168 REWRITE_TAC[REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE]);;
170 let REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE = prove
171 (`!f:real->real^N g h k x s.
172 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
173 f continuous (atreal x within s) /\ g continuous (atreal x within s) /\
174 h continuous (atreal x within s) /\ k continuous (atreal x within s)
175 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous
176 (atreal x within s)`,
177 REWRITE_TAC[CONTINUOUS_CONTINUOUS_WITHINREAL;
178 REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL] THEN
179 SIMP_TAC[o_DEF; REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE; LIFT_DROP]);;
181 let REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE = prove
182 (`!f:real->real^N g h k x.
183 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
184 f continuous (atreal x) /\ g continuous (atreal x) /\
185 h continuous (atreal x) /\ k continuous (atreal x)
186 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (atreal x)`,
187 ONCE_REWRITE_TAC[GSYM WITHINREAL_UNIV] THEN
188 REWRITE_TAC[REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE]);;
190 let AFF_GE_2_1_0 = prove
191 (`!v w. DISJOINT {vec 0, v} {w}
192 ==> aff_ge {vec 0, v} {w} = {s % v + t % w |s,t| &0 <= t}`,
193 SIMP_TAC[AFF_GE_2_1; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
194 REPEAT STRIP_TAC THEN
195 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> q /\ p /\ r`] THEN
196 ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
197 REWRITE_TAC[REAL_ARITH `t + u = &1 <=> t = &1 - u`; UNWIND_THM2] THEN
200 let AFF_GE_2_1_0_DROPOUT_3 = prove
202 ~collinear{vec 0,basis 3,z}
203 ==> (w IN aff_ge {vec 0,basis 3} {z} <=>
204 (dropout 3 w) IN aff_ge {vec 0:real^2} {dropout 3 z})`,
206 ASM_CASES_TAC `z:real^3 = vec 0` THENL
207 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
208 ASM_CASES_TAC `z:real^3 = basis 3` THENL
209 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
210 REWRITE_TAC[COLLINEAR_BASIS_3] THEN DISCH_TAC THEN
211 ASM_SIMP_TAC[AFF_GE_2_1_0; SET_RULE `DISJOINT s {a} <=> ~(a IN s)`;
212 IN_INSERT; NOT_IN_EMPTY; AFF_GE_1_1_0] THEN
213 REWRITE_TAC[IN_ELIM_THM] THEN
215 `(!t. ((?s. P s t) <=> Q t)) ==> ((?s t. P s t) <=> (?t. Q t))`) THEN
216 X_GEN_TAC `t:real` THEN EQ_TAC THENL
218 ASM_REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN
220 STRIP_TAC THEN EXISTS_TAC `(w:real^3)$3 - t * (z:real^3)$3` THEN
221 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CART_EQ]) THEN
222 ASM_REWRITE_TAC[CART_EQ; FORALL_2; FORALL_3; DIMINDEX_2; DIMINDEX_3] THEN
223 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
224 SIMP_TAC[dropout; LAMBDA_BETA; DIMINDEX_2; ARITH; BASIS_COMPONENT;
226 CONV_TAC REAL_RING]);;
228 let REAL_CONTINUOUS_AT_AZIM_SHARP = prove
230 ~collinear{v,w,w1} /\ ~collinear{v,w,w2} /\ ~(w2 IN aff_ge {v,w} {w1})
231 ==> (azim v w w1) real_continuous at w2`,
232 GEOM_ORIGIN_TAC `v:real^3` THEN
233 GEOM_BASIS_MULTIPLE_TAC 3 `w:real^3` THEN
234 X_GEN_TAC `w:real` THEN ASM_CASES_TAC `w = &0` THENL
235 [ASM_REWRITE_TAC[VECTOR_MUL_LZERO; INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
236 ASM_SIMP_TAC[REAL_LE_LT; COLLINEAR_SPECIAL_SCALE] THEN
237 DISCH_TAC THEN REPEAT GEN_TAC THEN
238 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
239 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_SPECIAL_SCALE o
240 rand o rand o lhand o goal_concl) THEN
241 ASM_REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY; IN_SING] THEN ANTS_TAC THENL
242 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
243 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
244 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THENL
245 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
246 ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
247 ASM_SIMP_TAC[COLLINEAR_LEMMA_ALT; BASIS_NONZERO; DIMINDEX_3; ARITH] THEN
249 DISCH_THEN SUBST1_TAC THEN DISCH_TAC] THEN
250 ASM_SIMP_TAC[AZIM_SPECIAL_SCALE; AZIM_ARG] THEN
251 MATCH_MP_TAC(REWRITE_RULE[o_DEF]
252 REAL_CONTINUOUS_CONTINUOUS_AT_COMPOSE) THEN
254 [REWRITE_TAC[complex_div] THEN MATCH_MP_TAC CONTINUOUS_COMPLEX_MUL THEN
255 REWRITE_TAC[CONTINUOUS_CONST; ETA_AX] THEN
256 SIMP_TAC[LINEAR_CONTINUOUS_AT; LINEAR_DROPOUT; DIMINDEX_3; DIMINDEX_2;
259 MATCH_MP_TAC REAL_CONTINUOUS_AT_WITHIN THEN
260 MATCH_MP_TAC REAL_CONTINUOUS_AT_ARG THEN
261 MP_TAC(ISPECL [`w2:real^3`; `w1:real^3`] AFF_GE_2_1_0_DROPOUT_3) THEN
262 ASM_REWRITE_TAC[] THEN
263 REPEAT(FIRST_X_ASSUM(MP_TAC o
264 GEN_REWRITE_RULE RAND_CONV [COLLINEAR_BASIS_3])) THEN
265 SPEC_TAC(`(dropout 3:real^3->real^2) w2`,`v2:real^2`) THEN
266 SPEC_TAC(`(dropout 3:real^3->real^2) w1`,`v1:real^2`) THEN
267 POP_ASSUM_LIST(K ALL_TAC) THEN
268 GEOM_BASIS_MULTIPLE_TAC 1 `v1:complex` THEN
269 X_GEN_TAC `w:real` THEN ASM_CASES_TAC `w = &0` THEN
270 ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
271 GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN ASM_REWRITE_TAC[] THEN
272 DISCH_TAC THEN X_GEN_TAC `z:complex` THEN
273 DISCH_THEN(K ALL_TAC) THEN DISCH_THEN(K ALL_TAC) THEN
274 REWRITE_TAC[CONTRAPOS_THM; COMPLEX_BASIS; COMPLEX_CMUL] THEN
275 REWRITE_TAC[COMPLEX_MUL_RID; RE_DIV_CX; IM_DIV_CX; real] THEN
276 ASM_SIMP_TAC[REAL_DIV_EQ_0; REAL_LE_RDIV_EQ; REAL_MUL_LZERO] THEN
278 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_1_1_0 o rand o goal_concl) THEN
279 ASM_REWRITE_TAC[COMPLEX_VEC_0; CX_INJ] THEN DISCH_THEN SUBST1_TAC THEN
280 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `Re z / w` THEN
281 ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE; COMPLEX_EQ] THEN
282 ASM_SIMP_TAC[COMPLEX_CMUL; CX_DIV; COMPLEX_DIV_RMUL; CX_INJ] THEN
283 REWRITE_TAC[RE_CX; IM_CX]);;
286 (* ------------------------------------------------------------------------- *)
287 (* Some general lemmas. *)
288 (* ------------------------------------------------------------------------- *)
290 let LINEAR_CONTINUOUS_COMPOSE = prove
291 (`!net f:A->real^N g:real^N->real^P.
292 f continuous net /\ linear g ==> (\x. g(f x)) continuous net`,
293 REWRITE_TAC[continuous; LIM_LINEAR]);;
295 let CONTINUOUS_LIFT_COMPONENT = prove
296 (`!net f:A->real^N i. f continuous net ==> (\x. lift(f x$i)) continuous net`,
298 SUBGOAL_THEN `linear(\x:real^N. lift (x$i))` MP_TAC THENL
299 [REWRITE_TAC[LINEAR_LIFT_COMPONENT]; REWRITE_TAC[GSYM IMP_CONJ_ALT]] THEN
300 REWRITE_TAC[LINEAR_CONTINUOUS_COMPOSE]);;
302 let CONTINUOUS_CROSS = prove
304 f continuous net /\ g continuous net
305 ==> (\x. (f x) cross (g x)) continuous net`,
306 REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[CONTINUOUS_COMPONENTWISE_LIFT] THEN
307 REWRITE_TAC[cross; VECTOR_3; DIMINDEX_3; FORALL_3; LIFT_SUB] THEN
308 REPEAT CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_SUB THEN
309 REWRITE_TAC[LIFT_CMUL] THEN CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_MUL THEN
310 ASM_SIMP_TAC[o_DEF; CONTINUOUS_LIFT_COMPONENT]);;
312 let CONTINUOUS_ON_CROSS = prove
313 (`!f:real^N->real^3 g s.
314 f continuous_on s /\ g continuous_on s
315 ==> (\x. (f x) cross (g x)) continuous_on s`,
316 SIMP_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN; CONTINUOUS_CROSS]);;
318 let CROSS_LSUB = prove
319 (`!x y z. (x - y) cross z = x cross z - y cross z`,
322 let CROSS_RSUB = prove
323 (`!x y z. x cross (y - z) = x cross y - x cross z`,
326 let CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE = prove
327 (`!f:real^M->real^N g x s.
328 ~(f x = vec 0) /\ ~(g x = vec 0) /\
329 f continuous (at x within s) /\
330 g continuous (at x within s)
331 ==> (\x. Cx(vector_angle (f x) (g x))) continuous (at x within s)`,
332 REPEAT STRIP_TAC THEN
333 ASM_CASES_TAC `trivial_limit(at (x:real^M) within s)` THEN
334 ASM_SIMP_TAC[CONTINUOUS_TRIVIAL_LIMIT; vector_angle] THEN
336 `(cacs o (\x. Cx(((f x:real^N) dot g x) / (norm(f x) * norm(g x)))))
337 continuous (at (x:real^M) within s)`
339 [MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN CONJ_TAC THENL
340 [REWRITE_TAC[CX_DIV; CX_MUL] THEN REWRITE_TAC[WITHIN_UNIV] THEN
341 MATCH_MP_TAC CONTINUOUS_COMPLEX_DIV THEN
342 ASM_SIMP_TAC[NETLIMIT_WITHIN; COMPLEX_ENTIRE; CX_INJ; NORM_EQ_0] THEN
343 REWRITE_TAC[CONTINUOUS_CX_LIFT; GSYM CX_MUL; LIFT_CMUL] THEN
344 ASM_SIMP_TAC[CONTINUOUS_WITHIN_LIFT_DOT2] THEN
345 MATCH_MP_TAC CONTINUOUS_MUL THEN
346 ASM_SIMP_TAC[CONTINUOUS_LIFT_NORM_COMPOSE; o_DEF];
347 MATCH_MP_TAC CONTINUOUS_WITHIN_SUBSET THEN
348 EXISTS_TAC `{z | real z /\ abs(Re z) <= &1}` THEN
349 REWRITE_TAC[CONTINUOUS_WITHIN_CACS_REAL] THEN
350 REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; IN_ELIM_THM] THEN
351 REWRITE_TAC[REAL_CX; RE_CX; NORM_CAUCHY_SCHWARZ_DIV]];
352 ASM_SIMP_TAC[CONTINUOUS_WITHIN; CX_ACS; o_DEF;
353 NORM_CAUCHY_SCHWARZ_DIV] THEN
354 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] LIM_TRANSFORM_EVENTUALLY) THEN
356 `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
357 ~((g:real^M->real^N) y = vec 0))
360 [REWRITE_TAC[EVENTUALLY_AND] THEN CONJ_TAC THENL
361 [UNDISCH_TAC `(f:real^M->real^N) continuous (at x within s)`;
362 UNDISCH_TAC `(g:real^M->real^N) continuous (at x within s)`] THEN
363 REWRITE_TAC[CONTINUOUS_WITHIN; tendsto] THENL
364 [DISCH_THEN(MP_TAC o SPEC `norm((f:real^M->real^N) x)`);
365 DISCH_THEN(MP_TAC o SPEC `norm((g:real^M->real^N) x)`)] THEN
366 ASM_REWRITE_TAC[NORM_POS_LT] THEN
367 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
368 REWRITE_TAC[] THEN CONV_TAC NORM_ARITH;
369 MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] EVENTUALLY_MONO) THEN
370 SIMP_TAC[CX_ACS; NORM_CAUCHY_SCHWARZ_DIV]]]);;
372 (* ------------------------------------------------------------------------- *)
373 (* Additional lemmas about aff_ge {vec 0,v} {w}. *)
374 (* ------------------------------------------------------------------------- *)
376 let AFF_GE_2_1_0 = prove
377 (`!v w. DISJOINT {vec 0, v} {w}
378 ==> aff_ge {vec 0, v} {w} = {s % v + t % w |s,t| &0 <= t}`,
379 SIMP_TAC[AFF_GE_2_1; VECTOR_MUL_RZERO; VECTOR_ADD_LID] THEN
380 REPEAT STRIP_TAC THEN
381 ONCE_REWRITE_TAC[TAUT `p /\ q /\ r <=> q /\ p /\ r`] THEN
382 ONCE_REWRITE_TAC[MESON[] `(?a b c. P a b c) <=> (?c b a. P a b c)`] THEN
383 REWRITE_TAC[REAL_ARITH `t + u = &1 <=> t = &1 - u`; UNWIND_THM2] THEN
386 let AFF_GE_2_1_0_DROPOUT_3 = prove
388 ~collinear{vec 0,basis 3,z}
389 ==> (w IN aff_ge {vec 0,basis 3} {z} <=>
390 (dropout 3 w) IN aff_ge {vec 0:real^2} {dropout 3 z})`,
392 ASM_CASES_TAC `z:real^3 = vec 0` THENL
393 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
394 ASM_CASES_TAC `z:real^3 = basis 3` THENL
395 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC] THEN
396 REWRITE_TAC[COLLINEAR_BASIS_3] THEN DISCH_TAC THEN
397 ASM_SIMP_TAC[AFF_GE_2_1_0; SET_RULE `DISJOINT s {a} <=> ~(a IN s)`;
398 IN_INSERT; NOT_IN_EMPTY; AFF_GE_1_1_0] THEN
399 REWRITE_TAC[IN_ELIM_THM] THEN
401 `(!t. ((?s. P s t) <=> Q t)) ==> ((?s t. P s t) <=> (?t. Q t))`) THEN
402 X_GEN_TAC `t:real` THEN EQ_TAC THENL
404 ASM_REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN
406 STRIP_TAC THEN EXISTS_TAC `(w:real^3)$3 - t * (z:real^3)$3` THEN
407 FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [CART_EQ]) THEN
408 ASM_REWRITE_TAC[CART_EQ; FORALL_2; FORALL_3; DIMINDEX_2; DIMINDEX_3] THEN
409 REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
410 SIMP_TAC[dropout; LAMBDA_BETA; DIMINDEX_2; ARITH; BASIS_COMPONENT;
412 CONV_TAC REAL_RING]);;
414 let AFF_GE_2_1_0_SEMIALGEBRAIC = prove
416 ~collinear {vec 0,x,y} /\ ~collinear {vec 0,x,z}
417 ==> (z IN aff_ge {vec 0,x} {y} <=>
418 (x cross y) cross x cross z = vec 0 /\
419 &0 <= (x cross z) dot (x cross y))`,
421 (`~(y = vec 0) ==> ((?s. x = s % y) <=> y cross x = vec 0)`,
422 REWRITE_TAC[CROSS_EQ_0] THEN SIMP_TAC[COLLINEAR_LEMMA_ALT])
426 ==> ((?t. &0 <= t /\ x = t % y) <=>
427 (?t. x = t % y) /\ &0 <= x dot y)`,
428 REPEAT STRIP_TAC THEN REWRITE_TAC[LEFT_AND_EXISTS_THM] THEN
429 AP_TERM_TAC THEN REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `t:real` THEN
430 ASM_CASES_TAC `x:real^N = t % y` THEN
431 ASM_SIMP_TAC[DOT_LMUL; REAL_LE_MUL_EQ; DOT_POS_LT]) in
433 MAP_EVERY (fun t -> ASM_CASES_TAC t THENL
434 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC]; ALL_TAC])
435 [`x:real^3 = vec 0`; `y:real^3 = vec 0`; `y:real^3 = x`] THEN
437 ASM_SIMP_TAC[AFF_GE_2_1_0; IN_ELIM_THM; SET_RULE
438 `DISJOINT {a,b} {c} <=> ~(a = c) /\ ~(b = c)`] THEN
439 ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN
440 REWRITE_TAC[RIGHT_EXISTS_AND_THM; VECTOR_ARITH
441 `a:real^N = b + c <=> a - c = b`] THEN
442 RULE_ASSUM_TAC(REWRITE_RULE[GSYM CROSS_EQ_0]) THEN
443 ASM_SIMP_TAC[lemma0; lemma1; CROSS_RMUL; CROSS_RSUB; VECTOR_SUB_EQ]);;
445 let AZIM_IN_UPPER_HALFSPACE = prove
446 (`!v w x y. azim v w x y <= pi <=>
447 &0 <= ((w - v) cross (x - v)) dot (y - v)`,
448 GEOM_ORIGIN_TAC `v:real^3` THEN REWRITE_TAC[VECTOR_SUB_RZERO] THEN
449 REWRITE_TAC[GSYM Local_lemmas.SIN_AZIM_POS_PI_LT;
450 Polar_fan.SIN_AZIM_MUTUAL_CROSS]);;
452 (* ------------------------------------------------------------------------- *)
453 (* Single-variable continuity for azim with slightly sharper hypothesis. *)
454 (* ------------------------------------------------------------------------- *)
456 let REAL_CONTINUOUS_AT_AZIM_SHARP = prove
458 ~collinear{v,w,w1} /\ ~(w2 IN aff_ge {v,w} {w1})
459 ==> (\w2. azim v w w1 w2) real_continuous at w2`,
460 GEOM_ORIGIN_TAC `v:real^3` THEN
461 GEOM_BASIS_MULTIPLE_TAC 3 `w:real^3` THEN
462 X_GEN_TAC `w:real` THEN ASM_CASES_TAC `w = &0` THENL
463 [ASM_REWRITE_TAC[VECTOR_MUL_LZERO; INSERT_AC; COLLINEAR_2]; ALL_TAC] THEN
464 ASM_SIMP_TAC[REAL_LE_LT; COLLINEAR_SPECIAL_SCALE] THEN
465 DISCH_TAC THEN REPEAT GEN_TAC THEN
466 REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
467 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_SPECIAL_SCALE o
468 rand o rand o lhand o goal_concl) THEN
469 ASM_REWRITE_TAC[FINITE_INSERT; FINITE_EMPTY; IN_SING] THEN ANTS_TAC THENL
470 [POP_ASSUM_LIST(MP_TAC o end_itlist CONJ) THEN
471 ONCE_REWRITE_TAC[GSYM CONTRAPOS_THM] THEN REWRITE_TAC[DE_MORGAN_THM] THEN
472 DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THENL
473 [ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
474 ASM_REWRITE_TAC[COLLINEAR_2; INSERT_AC];
475 ASM_SIMP_TAC[COLLINEAR_LEMMA_ALT; BASIS_NONZERO; DIMINDEX_3; ARITH] THEN
477 DISCH_THEN SUBST1_TAC THEN DISCH_TAC] THEN
478 ASM_SIMP_TAC[AZIM_SPECIAL_SCALE; AZIM_ARG] THEN
479 MATCH_MP_TAC(REWRITE_RULE[o_DEF]
480 REAL_CONTINUOUS_CONTINUOUS_AT_COMPOSE) THEN
482 [REWRITE_TAC[complex_div] THEN MATCH_MP_TAC CONTINUOUS_COMPLEX_MUL THEN
483 REWRITE_TAC[CONTINUOUS_CONST; ETA_AX] THEN
484 SIMP_TAC[LINEAR_CONTINUOUS_AT; LINEAR_DROPOUT; DIMINDEX_3; DIMINDEX_2;
487 MATCH_MP_TAC REAL_CONTINUOUS_AT_WITHIN THEN
488 MATCH_MP_TAC REAL_CONTINUOUS_AT_ARG THEN
489 MP_TAC(ISPECL [`w2:real^3`; `w1:real^3`] AFF_GE_2_1_0_DROPOUT_3) THEN
490 ASM_REWRITE_TAC[] THEN
491 REPEAT(FIRST_X_ASSUM(MP_TAC o
492 GEN_REWRITE_RULE RAND_CONV [COLLINEAR_BASIS_3])) THEN
493 SPEC_TAC(`(dropout 3:real^3->real^2) w2`,`v2:real^2`) THEN
494 SPEC_TAC(`(dropout 3:real^3->real^2) w1`,`v1:real^2`) THEN
495 POP_ASSUM_LIST(K ALL_TAC) THEN
496 GEOM_BASIS_MULTIPLE_TAC 1 `v1:complex` THEN
497 X_GEN_TAC `w:real` THEN ASM_CASES_TAC `w = &0` THEN
498 ASM_REWRITE_TAC[VECTOR_MUL_LZERO] THEN
499 GEN_REWRITE_TAC LAND_CONV [REAL_LE_LT] THEN ASM_REWRITE_TAC[] THEN
500 DISCH_TAC THEN X_GEN_TAC `z:complex` THEN
501 DISCH_THEN(K ALL_TAC) THEN
502 REWRITE_TAC[CONTRAPOS_THM; COMPLEX_BASIS; COMPLEX_CMUL] THEN
503 REWRITE_TAC[COMPLEX_MUL_RID; RE_DIV_CX; IM_DIV_CX; real] THEN
504 ASM_SIMP_TAC[REAL_DIV_EQ_0; REAL_LE_RDIV_EQ; REAL_MUL_LZERO] THEN
506 W(MP_TAC o PART_MATCH (lhs o rand) AFF_GE_1_1_0 o rand o goal_concl) THEN
507 ASM_REWRITE_TAC[COMPLEX_VEC_0; CX_INJ] THEN DISCH_THEN SUBST1_TAC THEN
508 REWRITE_TAC[IN_ELIM_THM] THEN EXISTS_TAC `Re z / w` THEN
509 ASM_SIMP_TAC[REAL_LE_DIV; REAL_LT_IMP_LE; COMPLEX_EQ] THEN
510 ASM_SIMP_TAC[COMPLEX_CMUL; CX_DIV; COMPLEX_DIV_RMUL; CX_INJ] THEN
511 REWRITE_TAC[RE_CX; IM_CX]);;
513 (* ------------------------------------------------------------------------- *)
514 (* General continuity of dihV composed with other functions. *)
515 (* ------------------------------------------------------------------------- *)
517 let REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE = prove
518 (`!f:real^M->real^N g h k x s.
519 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
520 f continuous (at x within s) /\ g continuous (at x within s) /\
521 h continuous (at x within s) /\ k continuous (at x within s)
522 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (at x within s)`,
523 REPEAT STRIP_TAC THEN REWRITE_TAC[dihV] THEN
524 CONV_TAC(TOP_DEPTH_CONV let_CONV) THEN
525 REWRITE_TAC[ARCV_ANGLE; angle; REAL_CONTINUOUS_CONTINUOUS; o_DEF] THEN
526 REWRITE_TAC[VECTOR_SUB_RZERO] THEN
527 MATCH_MP_TAC CONTINUOUS_WITHIN_CX_VECTOR_ANGLE_COMPOSE THEN
528 ASM_REWRITE_TAC[VECTOR_SUB_EQ; GSYM COLLINEAR_3_DOT_MULTIPLES] THEN
529 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_SUB THEN CONJ_TAC THEN
530 MATCH_MP_TAC CONTINUOUS_MUL THEN REWRITE_TAC[o_DEF] THEN
531 ASM_SIMP_TAC[CONTINUOUS_WITHIN_LIFT_DOT2; o_DEF; CONTINUOUS_SUB]);;
533 let REAL_CONTINUOUS_AT_DIHV_COMPOSE = prove
534 (`!f:real^M->real^N g h k x.
535 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
536 f continuous (at x) /\ g continuous (at x) /\
537 h continuous (at x) /\ k continuous (at x)
538 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (at x)`,
539 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
540 REWRITE_TAC[REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE]);;
542 let REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE = prove
543 (`!f:real->real^N g h k x s.
544 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
545 f continuous (atreal x within s) /\ g continuous (atreal x within s) /\
546 h continuous (atreal x within s) /\ k continuous (atreal x within s)
547 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous
548 (atreal x within s)`,
549 REWRITE_TAC[CONTINUOUS_CONTINUOUS_WITHINREAL;
550 REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL] THEN
551 SIMP_TAC[o_DEF; REAL_CONTINUOUS_WITHIN_DIHV_COMPOSE; LIFT_DROP]);;
553 let REAL_CONTINUOUS_ATREAL_DIHV_COMPOSE = prove
554 (`!f:real->real^N g h k x.
555 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
556 f continuous (atreal x) /\ g continuous (atreal x) /\
557 h continuous (atreal x) /\ k continuous (atreal x)
558 ==> (\x. dihV (f x) (g x) (h x) (k x)) real_continuous (atreal x)`,
559 ONCE_REWRITE_TAC[GSYM WITHINREAL_UNIV] THEN
560 REWRITE_TAC[REAL_CONTINUOUS_WITHINREAL_DIHV_COMPOSE]);;
562 (* ------------------------------------------------------------------------- *)
563 (* General continuity of azim composed with other functions. *)
564 (* ------------------------------------------------------------------------- *)
566 let REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE = prove
567 (`!f:real^M->real^3 g h k x s.
568 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
569 ~(k x IN aff_ge {f x,g x} {h x}) /\
570 f continuous (at x within s) /\ g continuous (at x within s) /\
571 h continuous (at x within s) /\ k continuous (at x within s)
572 ==> (\x. azim (f x) (g x) (h x) (k x)) real_continuous (at x within s)`,
574 (`!s t u f:real^M->real^N g h.
575 (closed s /\ closed t) /\ s UNION t = UNIV /\
576 (g continuous_on (u INTER s) /\ h continuous_on (u INTER t)) /\
577 (!x. x IN u INTER s ==> g x = f x) /\
578 (!x. x IN u INTER t ==> h x = f x)
579 ==> f continuous_on u`,
580 REPEAT STRIP_TAC THEN
581 SUBGOAL_THEN `u:real^M->bool = (u INTER s) UNION (u INTER t)`
582 SUBST1_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN
583 MATCH_MP_TAC CONTINUOUS_ON_UNION_LOCAL THEN
584 REWRITE_TAC[CLOSED_IN_CLOSED] THEN REPEAT CONJ_TAC THENL
585 [EXISTS_TAC `s:real^M->bool` THEN ASM SET_TAC[];
586 EXISTS_TAC `t:real^M->bool` THEN ASM SET_TAC[];
587 ASM_MESON_TAC[CONTINUOUS_ON_EQ];
588 ASM_MESON_TAC[CONTINUOUS_ON_EQ]]) in
589 REPEAT STRIP_TAC THEN REWRITE_TAC[REAL_CONTINUOUS_CONTINUOUS; o_DEF] THEN
591 `(\x:real^M. Cx(azim (f x) (g x) (h x) (k x))) =
592 (\z. Cx(azim (vec 0) (fstcart z)
593 (fstcart(sndcart z)) (sndcart(sndcart z)))) o
594 (\x. pastecart (g x - f x) (pastecart (h x - f x) (k x - f x)))`
596 [REWRITE_TAC[FUN_EQ_THM; o_THM; FSTCART_PASTECART; SNDCART_PASTECART] THEN
597 X_GEN_TAC `y:real^M` THEN
598 SUBST1_TAC(VECTOR_ARITH `vec 0 = (f:real^M->real^3) y - f y`) THEN
599 SIMP_TAC[ONCE_REWRITE_RULE[VECTOR_ADD_SYM] AZIM_TRANSLATION; VECTOR_SUB];
600 MATCH_MP_TAC CONTINUOUS_WITHIN_COMPOSE THEN
601 ASM_SIMP_TAC[CONTINUOUS_PASTECART; CONTINUOUS_SUB]] THEN
602 MATCH_MP_TAC CONTINUOUS_AT_WITHIN THEN
604 `!z. ~collinear {vec 0,fstcart z,fstcart(sndcart z)} /\
605 ~collinear {vec 0,fstcart z,sndcart(sndcart z)} /\
606 ~(sndcart(sndcart z) IN aff_ge {vec 0,fstcart z} {fstcart(sndcart z)})
607 ==> (\z. Cx(azim (vec 0) (fstcart z) (fstcart(sndcart z))
608 (sndcart(sndcart z))))
612 ASM_SIMP_TAC[FSTCART_PASTECART; SNDCART_PASTECART; GSYM COLLINEAR_3] THEN
613 REPEAT(CONJ_TAC THENL [ASM_MESON_TAC[INSERT_AC]; ALL_TAC]) THEN
614 SUBST1_TAC(VECTOR_ARITH `vec 0 = (f:real^M->real^3) x - f x`) THEN
615 ONCE_REWRITE_TAC[SET_RULE `{a,b} = {a} UNION {b}`] THEN
616 REWRITE_TAC[GSYM IMAGE_UNION; SET_RULE
617 `{a - b:real^3} = IMAGE (\x. x - b) {a}`] THEN
618 REWRITE_TAC[ONCE_REWRITE_RULE[VECTOR_ADD_SYM] AFF_GE_TRANSLATION;
620 ASM_REWRITE_TAC[IN_IMAGE; VECTOR_ARITH `a + x:real^3 = b + x <=> a = b`;
621 UNWIND_THM1; SET_RULE `{a} UNION {b} = {a,b}`]] THEN
622 ONCE_REWRITE_TAC[SET_RULE
623 `(!x. ~P x /\ ~Q x /\ ~R x ==> J x) <=>
624 (!x. x IN UNIV DIFF (({x | P x} UNION {x | Q x}) UNION {x | R x})
626 MATCH_MP_TAC(MESON[CONTINUOUS_ON_EQ_CONTINUOUS_AT]
627 `open s /\ f continuous_on s ==> !z. z IN s ==> f continuous at z`) THEN
629 [REWRITE_TAC[GSYM closed] THEN
631 `!t'. s UNION t = s UNION t' /\ closed(s UNION t')
632 ==> closed(s UNION t)`) THEN
634 `{z | (fstcart z cross fstcart(sndcart z)) cross
635 fstcart z cross sndcart(sndcart z) = vec 0 /\
636 &0 <= (fstcart z cross sndcart(sndcart z)) dot
637 (fstcart z cross fstcart(sndcart z))}` THEN
639 [MATCH_MP_TAC(SET_RULE
640 `(!x. ~(x IN s) ==> (x IN t <=> x IN t'))
641 ==> s UNION t = s UNION t'`) THEN
642 REWRITE_TAC[AFF_GE_2_1_0_SEMIALGEBRAIC; IN_UNION; IN_ELIM_THM;
645 MATCH_MP_TAC CLOSED_UNION THEN CONJ_TAC THENL
646 [MATCH_MP_TAC CLOSED_UNION THEN CONJ_TAC THEN
647 REWRITE_TAC[GSYM DOT_CAUCHY_SCHWARZ_EQUAL] THEN
648 ONCE_REWRITE_TAC[GSYM REAL_SUB_0] THEN
649 REWRITE_TAC[GSYM LIFT_EQ; LIFT_NUM] THEN
650 SIMP_TAC[SET_RULE `{x | f x = a} = {x | x IN UNIV /\ f x IN {a}}`] THEN
651 MATCH_MP_TAC CONTINUOUS_CLOSED_PREIMAGE THEN
652 SIMP_TAC[CLOSED_UNIV; CLOSED_SING; LIFT_SUB; REAL_POW_2; LIFT_CMUL] THEN
653 MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
654 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_ON_MUL THEN
655 REWRITE_TAC[o_DEF] THEN REPEAT CONJ_TAC THEN
656 MATCH_MP_TAC CONTINUOUS_ON_LIFT_DOT2 THEN CONJ_TAC;
657 ONCE_REWRITE_TAC[MESON[LIFT_DROP; real_ge]
658 `&0 <= x <=> drop(lift x) >= &0`] THEN
660 `{z | f z = vec 0 /\ drop(g z) >= &0} =
661 {z | z IN UNIV /\ f z IN {vec 0}} INTER
662 {z | z IN UNIV /\ g z IN {k | drop(k) >= &0}}`] THEN
663 MATCH_MP_TAC CLOSED_INTER THEN
664 CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_CLOSED_PREIMAGE THEN
665 REWRITE_TAC[CLOSED_SING; drop; CLOSED_UNIV;
666 CLOSED_HALFSPACE_COMPONENT_GE] THEN
667 REPEAT((MATCH_MP_TAC CONTINUOUS_ON_CROSS ORELSE
668 MATCH_MP_TAC CONTINUOUS_ON_LIFT_DOT2) THEN CONJ_TAC)] THEN
669 TRY(GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF]) THEN
670 SIMP_TAC[CONTINUOUS_ON_COMPOSE; LINEAR_CONTINUOUS_ON;
671 LINEAR_FSTCART; LINEAR_SNDCART];
672 MATCH_MP_TAC lemma THEN
674 [`{z | z IN UNIV /\ lift((fstcart z cross (fstcart(sndcart z))) dot
675 (sndcart(sndcart z))) IN {x | x$1 >= &0}}`;
676 `{z | z IN UNIV /\ lift((fstcart z cross (fstcart(sndcart z))) dot
677 (sndcart(sndcart z))) IN {x | x$1 <= &0}}`;
678 `\z. Cx(dihV (vec 0:real^3) (fstcart z)
679 (fstcart(sndcart z)) (sndcart(sndcart z)))`;
680 `\z. Cx(&2 * pi - dihV (vec 0:real^3) (fstcart z)
681 (fstcart(sndcart z)) (sndcart(sndcart z)))`] THEN
683 [CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_CLOSED_PREIMAGE THEN
684 REWRITE_TAC[CLOSED_UNIV; CLOSED_HALFSPACE_COMPONENT_GE;
685 CLOSED_HALFSPACE_COMPONENT_LE] THEN
686 MATCH_MP_TAC CONTINUOUS_ON_LIFT_DOT2 THEN
687 (CONJ_TAC THENL [MATCH_MP_TAC CONTINUOUS_ON_CROSS; ALL_TAC]) THEN
688 ONCE_REWRITE_TAC[GSYM o_DEF] THEN
689 SIMP_TAC[CONTINUOUS_ON_COMPOSE; LINEAR_CONTINUOUS_ON;
690 LINEAR_FSTCART; LINEAR_SNDCART];
693 [REWRITE_TAC[EXTENSION; IN_UNION; IN_UNIV; IN_ELIM_THM] THEN
697 [CONJ_TAC THEN MATCH_MP_TAC CONTINUOUS_AT_IMP_CONTINUOUS_ON THEN
698 REWRITE_TAC[FORALL_PASTECART; IN_DIFF; IN_UNIV; IN_UNION; IN_INTER;
699 FSTCART_PASTECART; SNDCART_PASTECART; IN_ELIM_THM; DE_MORGAN_THM] THEN
700 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`; `z:real^3`] THEN
701 REPEAT STRIP_TAC THEN REWRITE_TAC[CX_SUB] THEN
702 TRY(MATCH_MP_TAC CONTINUOUS_SUB THEN REWRITE_TAC[CONTINUOUS_CONST]) THEN
703 GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
704 REWRITE_TAC[GSYM REAL_CONTINUOUS_CONTINUOUS] THEN
705 MATCH_MP_TAC REAL_CONTINUOUS_AT_DIHV_COMPOSE THEN
706 ASM_REWRITE_TAC[FSTCART_PASTECART; SNDCART_PASTECART;
707 CONTINUOUS_CONST] THEN
708 ONCE_REWRITE_TAC[GSYM o_DEF] THEN
709 SIMP_TAC[CONTINUOUS_AT_COMPOSE; LINEAR_CONTINUOUS_AT;
710 LINEAR_FSTCART; LINEAR_SNDCART];
712 REWRITE_TAC[FORALL_PASTECART; IN_DIFF; IN_UNIV; IN_UNION; IN_INTER; CX_INJ;
713 FSTCART_PASTECART; SNDCART_PASTECART; IN_ELIM_THM; DE_MORGAN_THM] THEN
715 [REWRITE_TAC[GSYM drop; LIFT_DROP; real_ge] THEN
716 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`; `z:real^3`] THEN
717 REPEAT STRIP_TAC THEN MATCH_MP_TAC(GSYM AZIM_DIHV_SAME_STRONG) THEN
718 ASM_REWRITE_TAC[AZIM_IN_UPPER_HALFSPACE; VECTOR_SUB_RZERO];
719 REWRITE_TAC[GSYM drop; LIFT_DROP] THEN
720 MAP_EVERY X_GEN_TAC [`x:real^3`; `y:real^3`; `z:real^3`] THEN
721 REPEAT STRIP_TAC THEN MATCH_MP_TAC(GSYM AZIM_DIHV_COMPL) THEN
722 ASM_REWRITE_TAC[] THEN
723 MATCH_MP_TAC(REAL_ARITH
724 `(x <= pi ==> x = pi) ==> pi <= x`) THEN
725 ASM_REWRITE_TAC[AZIM_IN_UPPER_HALFSPACE; VECTOR_SUB_RZERO] THEN
726 ASM_SIMP_TAC[REAL_ARITH `x <= &0 ==> (&0 <= x <=> x = &0)`] THEN
727 REWRITE_TAC[Local_lemmas.CROSS_DOT_COPLANAR] THEN
728 ASM_SIMP_TAC[GSYM AZIM_EQ_0_PI_EQ_COPLANAR; AZIM_EQ_0_GE_ALT]]]);;
730 let REAL_CONTINUOUS_AT_AZIM_COMPOSE = prove
731 (`!f:real^M->real^3 g h k x.
732 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
733 ~(k x IN aff_ge {f x,g x} {h x}) /\
734 f continuous (at x) /\ g continuous (at x) /\
735 h continuous (at x) /\ k continuous (at x)
736 ==> (\x. azim (f x) (g x) (h x) (k x)) real_continuous (at x)`,
737 ONCE_REWRITE_TAC[GSYM WITHIN_UNIV] THEN
738 REWRITE_TAC[REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE]);;
740 let REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE = prove
741 (`!f:real->real^3 g h k x s.
742 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
743 ~(k x IN aff_ge {f x,g x} {h x}) /\
744 f continuous (atreal x within s) /\ g continuous (atreal x within s) /\
745 h continuous (atreal x within s) /\ k continuous (atreal x within s)
746 ==> (\x. azim (f x) (g x) (h x) (k x)) real_continuous
747 (atreal x within s)`,
748 REWRITE_TAC[CONTINUOUS_CONTINUOUS_WITHINREAL;
749 REAL_CONTINUOUS_REAL_CONTINUOUS_WITHINREAL] THEN
750 SIMP_TAC[o_DEF; REAL_CONTINUOUS_WITHIN_AZIM_COMPOSE; LIFT_DROP]);;
752 let REAL_CONTINUOUS_ATREAL_AZIM_COMPOSE = prove
753 (`!f:real->real^3 g h k x.
754 ~collinear {f x,g x,h x} /\ ~collinear {f x,g x,k x} /\
755 ~(k x IN aff_ge {f x,g x} {h x}) /\
756 f continuous (atreal x) /\ g continuous (atreal x) /\
757 h continuous (atreal x) /\ k continuous (atreal x)
758 ==> (\x. azim (f x) (g x) (h x) (k x)) real_continuous (atreal x)`,
759 ONCE_REWRITE_TAC[GSYM WITHINREAL_UNIV] THEN
760 REWRITE_TAC[REAL_CONTINUOUS_WITHINREAL_AZIM_COMPOSE]);;