legacy/oldlocal/XBJRPHC.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (* Section: Conclusions                                                       *)
   4 (* Chapter: Local Fan                                                         *)
   5 (* Lemma: XBJRPHC, PQCSXWG                                                    *)
   6 (* Author: John Harrison                                                      *)
   7 (* Date: 2013-07-02                                                           *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 The continuity of the functions dihV and azim.
  12
  13 Removed from project July 22, 2013.  All the necessary theorems have been duplicated in flyspeck.ml
  14 *)
  15
  16 module Xbjrphc = struct
  17
  18 (* ========================================================================= *)
  19 (* More complex analysis.                                                    *)
  20 (* ========================================================================= *)
  21
  22 needs "Multivariate/flyspeck.ml";;
  23
  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 (* ------------------------------------------------------------------------- *)
  28
  29 (*
  30  let REAL_CONTINUOUS_AT_DIHV = prove
  31    (`!v w w1 w2:real^N.
  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]]);;
  53 *)
  54
  55 (* ------------------------------------------------------------------------- *)
  56 (* A few general lemmas.                                                     *)
  57 (* ------------------------------------------------------------------------- *)
  58
  59 let COLLINEAR_3_DOT_MULTIPLES = prove
  60  (`!a b c:real^N.
  61         collinear {a,b,c} <=>
  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]);;
  70
  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]);;
  76
  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]);;
  81
  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]);;
  88
  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]);;
  94
  95 (* ------------------------------------------------------------------------- *)
  96 (* Stronger dihV continuity results.                                         *)
  97 (* ------------------------------------------------------------------------- *)
  98
  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
 108   SUBGOAL_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)`
 111   MP_TAC THENL
 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
 128     SUBGOAL_THEN
 129       `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
 130                        ~((g:real^M->real^N) y = vec 0))
 131                   (at x within s)`
 132     MP_TAC THENL
 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]]]);;
 144
 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]);;
 160
 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]);;
 169
 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]);;
 180
 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]);;
 189
 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
 198   SET_TAC[]);;
 199
 200 let AFF_GE_2_1_0_DROPOUT_3 = prove
 201  (`!w z:real^3.
 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})`,
 205   REPEAT GEN_TAC THEN
 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
 214   MATCH_MP_TAC(MESON[]
 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
 217    [STRIP_TAC THEN
 218     ASM_REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN
 219     VECTOR_ARITH_TAC;
 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;
 225              DIMINDEX_3] THEN
 226     CONV_TAC REAL_RING]);;
 227
 228 let REAL_CONTINUOUS_AT_AZIM_SHARP = prove
 229  (`!v w w1 w2.
 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
 248       MESON_TAC[]];
 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
 253   CONJ_TAC THENL
 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;
 257              ARITH];
 258     ALL_TAC] THEN
 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
 277   STRIP_TAC 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]);;
 284
 285
 286 (* ------------------------------------------------------------------------- *)
 287 (* Some general lemmas.                                                      *)
 288 (* ------------------------------------------------------------------------- *)
 289
 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]);;
 294
 295 let CONTINUOUS_LIFT_COMPONENT = prove
 296  (`!net f:A->real^N i. f continuous net ==> (\x. lift(f x$i)) continuous net`,
 297   REPEAT GEN_TAC THEN
 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]);;
 301
 302 let CONTINUOUS_CROSS = prove
 303  (`!net:(A)net f g.
 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]);;
 311
 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]);;
 317
 318 let CROSS_LSUB = prove
 319  (`!x y z. (x - y) cross z = x cross z - y cross z`,
 320   VEC3_TAC);;
 321
 322 let CROSS_RSUB = prove
 323  (`!x y z. x cross (y - z) = x cross y - x cross z`,
 324   VEC3_TAC);;
 325
 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
 335   SUBGOAL_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)`
 338   MP_TAC THENL
 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
 355     SUBGOAL_THEN
 356       `eventually (\y. ~((f:real^M->real^N) y = vec 0) /\
 357                        ~((g:real^M->real^N) y = vec 0))
 358                   (at x within s)`
 359     MP_TAC THENL
 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]]]);;
 371
 372 (* ------------------------------------------------------------------------- *)
 373 (* Additional lemmas about aff_ge {vec 0,v} {w}.                             *)
 374 (* ------------------------------------------------------------------------- *)
 375
 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
 384   SET_TAC[]);;
 385
 386 let AFF_GE_2_1_0_DROPOUT_3 = prove
 387  (`!w z:real^3.
 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})`,
 391   REPEAT GEN_TAC THEN
 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
 400   MATCH_MP_TAC(MESON[]
 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
 403    [STRIP_TAC THEN
 404     ASM_REWRITE_TAC[DROPOUT_ADD; DROPOUT_MUL; DROPOUT_BASIS_3] THEN
 405     VECTOR_ARITH_TAC;
 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;
 411              DIMINDEX_3] THEN
 412     CONV_TAC REAL_RING]);;
 413
 414 let AFF_GE_2_1_0_SEMIALGEBRAIC = prove
 415  (`!x y z:real^3.
 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))`,
 420   let lemma0 = prove
 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])
 423   and lemma1 = prove
 424    (`!x y:real^N.
 425           ~(y = vec 0)
 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
 432   REPEAT GEN_TAC THEN
 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
 436   STRIP_TAC 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]);;
 444
 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]);;
 451
 452 (* ------------------------------------------------------------------------- *)
 453 (* Single-variable continuity for azim with slightly sharper hypothesis.     *)
 454 (* ------------------------------------------------------------------------- *)
 455
 456 let REAL_CONTINUOUS_AT_AZIM_SHARP = prove
 457  (`!v w w1 w2.
 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
 476       MESON_TAC[]];
 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
 481   CONJ_TAC THENL
 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;
 485              ARITH];
 486     ALL_TAC] THEN
 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
 505   STRIP_TAC 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]);;
 512
 513 (* ------------------------------------------------------------------------- *)
 514 (* General continuity of dihV composed with other functions.                 *)
 515 (* ------------------------------------------------------------------------- *)
 516
 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]);;
 532
 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]);;
 541
 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]);;
 552
 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]);;
 561
 562 (* ------------------------------------------------------------------------- *)
 563 (* General continuity of azim composed with other functions.                 *)
 564 (* ------------------------------------------------------------------------- *)
 565
 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)`,
 573   let lemma = prove
 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
 590   SUBGOAL_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)))`
 595   SUBST1_TAC THENL
 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
 603   SUBGOAL_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))))
 609             continuous (at z)`
 610   MATCH_MP_TAC THENL
 611    [ALL_TAC;
 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;
 619                 VECTOR_SUB] THEN
 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})
 625          ==> J x)`] THEN
 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
 628   CONJ_TAC THENL
 629    [REWRITE_TAC[GSYM closed] THEN
 630     MATCH_MP_TAC(MESON[]
 631      `!t'. s UNION t = s UNION t' /\ closed(s UNION t')
 632            ==> closed(s UNION t)`) THEN
 633     EXISTS_TAC
 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
 638     CONJ_TAC THENL
 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;
 643                   DE_MORGAN_THM];
 644       ALL_TAC] THEN
 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
 659       REWRITE_TAC[SET_RULE
 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
 673     MAP_EVERY EXISTS_TAC
 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
 682     CONJ_TAC THENL
 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];
 691       ALL_TAC] THEN
 692     CONJ_TAC THENL
 693      [REWRITE_TAC[EXTENSION; IN_UNION; IN_UNIV; IN_ELIM_THM] THEN
 694       REAL_ARITH_TAC;
 695       ALL_TAC] THEN
 696     CONJ_TAC THENL
 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];
 711       ALL_TAC] THEN
 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
 714     CONJ_TAC THENL
 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]]]);;
 729
 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]);;
 739
 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]);;
 751
 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]);;
 761
 762
 763
 764
 765 end;;