Examples/borsuk.ml

   1 (* ========================================================================= *)
   2 (* Borsuk-Ulam theorem for an ordinary 2-sphere in real^3.                   *)
   3 (* From Andrew Browder's article, AMM vol. 113 (2006), pp. 935-6             *)
   4 (* ========================================================================= *)
   5
   6 needs "Multivariate/moretop.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* The Borsuk-Ulam theorem for the unit sphere.                              *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 let THEOREM_1 = prove
  13  (`!f:real^3->real^2.
  14         f continuous_on {x | norm(x) = &1}
  15         ==> ?x. norm(x) = &1 /\ f(--x) = f(x)`,
  16   REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
  17   PURE_REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b) <=> a ==> ~b`] THEN
  18   DISCH_TAC THEN
  19   ABBREV_TAC `(g:real^3->real^2) = \x. f(x) - f(--x)` THEN
  20   ABBREV_TAC `k = \z. (g:real^3->real^2)
  21                       (vector[Re z; Im z; sqrt(&1 - norm z pow 2)])` THEN
  22   MP_TAC(ISPECL [`k:complex->complex`; `Cx(&0)`; `&1`]
  23         CONTINUOUS_LOGARITHM_ON_CBALL) THEN
  24   MATCH_MP_TAC(TAUT `a /\ (a /\ b ==> c) ==> (a ==> b) ==> c`) THEN
  25   CONJ_TAC THENL
  26    [CONJ_TAC THENL
  27      [EXPAND_TAC "k" THEN
  28       MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
  29       CONJ_TAC THENL
  30        [REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;
  31                     CONTINUOUS_COMPONENTWISE] THEN
  32         SIMP_TAC[DIMINDEX_3; FORALL_3; VECTOR_3; ETA_AX] THEN
  33         REWRITE_TAC[REAL_CONTINUOUS_COMPLEX_COMPONENTS_WITHIN] THEN
  34         X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
  35         MATCH_MP_TAC(REWRITE_RULE[o_DEF] REAL_CONTINUOUS_WITHIN_COMPOSE) THEN
  36         SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_POW;
  37                  REAL_CONTINUOUS_CONST; REAL_CONTINUOUS_NORM_WITHIN] THEN
  38         MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET THEN
  39         EXISTS_TAC `{t | &0 <= t}` THEN
  40         REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG] THEN
  41         SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; IN_ELIM_THM; dist;
  42                  COMPLEX_SUB_LZERO; NORM_NEG; REAL_SUB_LE] THEN
  43         REWRITE_TAC[ABS_SQUARE_LE_1; REAL_ABS_NORM];
  44         ALL_TAC] THEN
  45       EXPAND_TAC "g" THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
  46       CONJ_TAC THENL
  47        [ALL_TAC;
  48         MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
  49         CONJ_TAC THENL
  50          [MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN REWRITE_TAC[linear] THEN
  51           CONJ_TAC THEN VECTOR_ARITH_TAC;
  52           REWRITE_TAC[GSYM IMAGE_o]]] THEN
  53       MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
  54       EXISTS_TAC `{x:real^3 | norm x = &1}` THEN ASM_REWRITE_TAC[] THEN
  55       REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_ELIM_THM] THEN
  56       SIMP_TAC[NORM_EQ_1; DOT_3; VECTOR_3; VECTOR_NEG_COMPONENT; dist;
  57                DIMINDEX_3; ARITH; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG] THEN
  58       REWRITE_TAC[REAL_NEG_MUL2] THEN X_GEN_TAC `z:complex` THEN DISCH_TAC;
  59       X_GEN_TAC `z:complex` THEN
  60       REWRITE_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG] THEN
  61       DISCH_TAC THEN MAP_EVERY EXPAND_TAC ["k"; "g"] THEN
  62       REWRITE_TAC[COMPLEX_RING `x - y = Cx(&0) <=> y = x`] THEN
  63       FIRST_X_ASSUM MATCH_MP_TAC THEN
  64       REWRITE_TAC[NORM_EQ_1; DOT_3; VECTOR_3]] THEN
  65     REWRITE_TAC[GSYM REAL_POW_2; COMPLEX_SQNORM] THEN
  66     REWRITE_TAC[REAL_ARITH `r + i + s = &1 <=> s = &1 - (r + i)`] THEN
  67     MATCH_MP_TAC SQRT_POW_2 THEN REWRITE_TAC[GSYM COMPLEX_SQNORM] THEN
  68     ASM_SIMP_TAC[REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_ABS_NORM];
  69     ALL_TAC] THEN
  70   DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
  71   DISCH_THEN(X_CHOOSE_THEN `h:complex->complex` STRIP_ASSUME_TAC) THEN
  72   ABBREV_TAC `m = \z:complex. (h(z) - h(--z)) / (Cx pi * ii)` THEN
  73   SUBGOAL_THEN
  74     `!z:complex. norm(z) = &1 ==> cexp(Cx pi * ii * m z) = cexp(Cx pi * ii)`
  75   MP_TAC THENL
  76    [EXPAND_TAC "m" THEN
  77     REWRITE_TAC[COMPLEX_SUB_LDISTRIB; complex_div; COMPLEX_SUB_RDISTRIB] THEN
  78     SIMP_TAC[CX_INJ; PI_NZ; CEXP_SUB; COMPLEX_FIELD
  79      `~(p = Cx(&0)) ==> p * ii * h * inv(p * ii) = h`] THEN
  80     X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
  81     SUBGOAL_THEN `cexp(h z) = k z /\ cexp(h(--z:complex)) = k(--z)`
  82      (CONJUNCTS_THEN SUBST1_TAC)
  83     THENL
  84      [CONJ_TAC THEN CONV_TAC SYM_CONV THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
  85       ASM_SIMP_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG; REAL_LE_REFL];
  86       ALL_TAC] THEN
  87     REWRITE_TAC[EULER; RE_MUL_CX; IM_MUL_CX; RE_II; IM_II; COMPLEX_ADD_RID;
  88                 REAL_MUL_RZERO; REAL_MUL_RID; SIN_PI; COS_PI; REAL_EXP_0;
  89                 COMPLEX_MUL_RZERO; COMPLEX_MUL_LID] THEN
  90     MATCH_MP_TAC(COMPLEX_FIELD
  91      `~(y = Cx(&0)) /\ x = -- y ==> x / y = Cx(-- &1)`) THEN
  92     CONJ_TAC THENL
  93      [FIRST_X_ASSUM MATCH_MP_TAC THEN
  94       ASM_SIMP_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG; REAL_LE_REFL];
  95       MAP_EVERY EXPAND_TAC ["k"; "g"] THEN
  96       REWRITE_TAC[COMPLEX_NEG_SUB] THEN BINOP_TAC THEN AP_TERM_TAC THEN
  97       SIMP_TAC[CART_EQ; FORALL_3; VECTOR_3; VECTOR_NEG_COMPONENT;
  98                DIMINDEX_3; ARITH; RE_NEG; IM_NEG; NORM_NEG; REAL_NEG_NEG] THEN
  99       ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 100       REWRITE_TAC[SQRT_0; REAL_NEG_0]];
 101     ALL_TAC] THEN
 102   REWRITE_TAC[CEXP_EQ; CX_MUL] THEN
 103   SIMP_TAC[CX_INJ; PI_NZ; COMPLEX_FIELD
 104    `~(p = Cx(&0))
 105     ==> (p * ii * m = p * ii + (t * n * p) * ii <=> m = t * n + Cx(&1))`] THEN
 106   REWRITE_TAC[GSYM CX_ADD; GSYM CX_MUL] THEN DISCH_THEN(LABEL_TAC "*") THEN
 107   SUBGOAL_THEN
 108    `?n. !z. z IN {z | norm(z) = &1} ==> (m:complex->complex)(z) = n`
 109   MP_TAC THENL
 110    [MATCH_MP_TAC CONTINUOUS_DISCRETE_RANGE_CONSTANT THEN CONJ_TAC THENL
 111      [ONCE_REWRITE_TAC[NORM_ARITH `norm z = dist(vec 0,z)`] THEN
 112       SIMP_TAC[GSYM sphere; CONNECTED_SPHERE; DIMINDEX_2; LE_REFL];
 113       ALL_TAC] THEN
 114     CONJ_TAC THENL
 115      [EXPAND_TAC "m" THEN MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_DIV THEN
 116       SIMP_TAC[CONTINUOUS_ON_CONST; COMPLEX_ENTIRE; II_NZ; CX_INJ; PI_NZ] THEN
 117       MATCH_MP_TAC CONTINUOUS_ON_SUB THEN CONJ_TAC THENL
 118        [ALL_TAC;
 119         MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
 120         CONJ_TAC THENL
 121          [MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN REWRITE_TAC[linear] THEN
 122           CONJ_TAC THEN VECTOR_ARITH_TAC;
 123           REWRITE_TAC[GSYM IMAGE_o]]] THEN
 124       FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
 125        (REWRITE_RULE[IMP_CONJ] CONTINUOUS_ON_SUBSET)) THEN
 126       SIMP_TAC[SUBSET; FORALL_IN_IMAGE; NORM_NEG; IN_CBALL;
 127                COMPLEX_SUB_LZERO; dist; IN_ELIM_THM; REAL_LE_REFL];
 128       ALL_TAC] THEN
 129     X_GEN_TAC `z:complex` THEN REWRITE_TAC[IN_ELIM_THM] THEN
 130     DISCH_TAC THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN
 131     X_GEN_TAC `w:complex` THEN STRIP_TAC THEN
 132     REMOVE_THEN "*" (fun th -> MP_TAC(SPEC `w:complex` th) THEN
 133                                MP_TAC(SPEC `z:complex` th)) THEN
 134     ASM_REWRITE_TAC[] THEN
 135     REPEAT(DISCH_THEN(CHOOSE_THEN
 136      (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN
 137     REWRITE_TAC[GSYM CX_SUB; COMPLEX_NORM_CX] THEN
 138     MATCH_MP_TAC(REAL_ARITH
 139      `~(abs(x - y) < &1) ==> &1 <= abs((&2 * x + &1) - (&2 * y + &1))`) THEN
 140     ASM_SIMP_TAC[GSYM REAL_EQ_INTEGERS] THEN ASM_MESON_TAC[];
 141     REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `v:complex`)] THEN
 142   SUBGOAL_THEN
 143     `?n. integer n /\ !z:complex. norm z = &1 ==> m z = Cx(&2 * n + &1)`
 144   MP_TAC THENL
 145    [REMOVE_THEN "*" (MP_TAC o SPEC `Cx(&1)`) THEN
 146     ASM_SIMP_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM] THEN ASM_MESON_TAC[];
 147     ALL_TAC] THEN
 148   DISCH_THEN(X_CHOOSE_THEN `n:real` MP_TAC) THEN EXPAND_TAC "m" THEN
 149   DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
 150   DISCH_THEN(fun th -> MP_TAC(SPEC `--Cx(&1)` th) THEN
 151                         MP_TAC(SPEC `Cx(&1)` th)) THEN
 152   REWRITE_TAC[NORM_NEG; COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_NEG_NEG] THEN
 153   REWRITE_TAC[complex_div; COMPLEX_SUB_RDISTRIB] THEN
 154   MATCH_MP_TAC(COMPLEX_RING
 155    `~(z = Cx(&0)) ==> a - b = z ==> ~(b - a = z)`) THEN
 156   REWRITE_TAC[CX_INJ; REAL_ARITH `&2 * n + &1 = &0 <=> n = --(&1 / &2)`] THEN
 157   UNDISCH_TAC `integer n` THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] THEN
 158   SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[integer] THEN
 159   REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_DIV; REAL_ABS_NUM] THEN
 160   REWRITE_TAC[REAL_ARITH `a / &2 = n <=> a = &2 * n`] THEN
 161   REWRITE_TAC[NOT_EXISTS_THM; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
 162   GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
 163   REWRITE_TAC[EVEN_MULT; ARITH]);;
 164
 165 (* ------------------------------------------------------------------------- *)
 166 (* The Borsuk-Ulam theorem for a general sphere.                             *)
 167 (* ------------------------------------------------------------------------- *)
 168
 169 let BORSUK_ULAM = prove
 170  (`!f:real^3->real^2 a r.
 171         &0 <= r /\ f continuous_on {z | norm(z - a) = r}
 172         ==> ?x. norm(x) = r /\ f(a + x) = f(a - x)`,
 173   REPEAT STRIP_TAC THEN
 174   MP_TAC(SPEC `\x. (f:real^3->real^2) (a + r % x)` THEOREM_1) THEN
 175   REWRITE_TAC[] THEN ANTS_TAC THENL
 176    [MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
 177     SIMP_TAC[CONTINUOUS_ON_ADD; CONTINUOUS_ON_CONST;
 178              CONTINUOUS_ON_CMUL; CONTINUOUS_ON_ID] THEN
 179     FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
 180         CONTINUOUS_ON_SUBSET)) THEN
 181     REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM];
 182     DISCH_THEN(X_CHOOSE_THEN `x:real^3` STRIP_ASSUME_TAC) THEN
 183     EXISTS_TAC `r % x:real^3` THEN
 184     ASM_REWRITE_TAC[VECTOR_ARITH `a - r % x:real^3 = a + r % --x`]] THEN
 185   ASM_SIMP_TAC[VECTOR_ADD_SUB; NORM_MUL] THEN ASM_REAL_ARITH_TAC);;