(* ========================================================================= *)
(* Borsuk-Ulam theorem for an ordinary 2-sphere in real^3.                   *)
(* From Andrew Browder's article, AMM vol. 113 (2006), pp. 935-6             *)
(* ========================================================================= *)

needs "Multivariate/moretop.ml";;

(* ------------------------------------------------------------------------- *)
(* The Borsuk-Ulam theorem for the unit sphere.                              *)
(* ------------------------------------------------------------------------- *)

let THEOREM_1 = 
prove
 (`!f:real^3->real^2.
        f continuous_on {x | norm(x) = &1}
        ==> ?x. norm(x) = &1 /\ f(--x) = f(x)`,

  REPEAT STRIP_TAC THEN GEN_REWRITE_TAC I [TAUT `p <=> ~ ~ p`] THEN
  PURE_REWRITE_TAC[NOT_EXISTS_THM; TAUT `~(a /\ b) <=> a ==> ~b`] THEN
  DISCH_TAC THEN
  ABBREV_TAC `(g:real^3->real^2) = \x. f(x) - f(--x)` THEN
  ABBREV_TAC `k = \z. (g:real^3->real^2)
                      (vector[Re z; Im z; sqrt(&1 - norm z pow 2)])` THEN
  MP_TAC(ISPECL [`k:complex->complex`; `Cx(&0)`; `&1`]
        CONTINUOUS_LOGARITHM_ON_CBALL) THEN
  MATCH_MP_TAC(TAUT `a /\ (a /\ b ==> c) ==> (a ==> b) ==> c`) THEN
  CONJ_TAC THENL
   [CONJ_TAC THENL
     [EXPAND_TAC "k" THEN
      MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
      CONJ_TAC THENL
       [REWRITE_TAC[CONTINUOUS_ON_EQ_CONTINUOUS_WITHIN;
                    CONTINUOUS_COMPONENTWISE] THEN
        SIMP_TAC[DIMINDEX_3; FORALL_3; VECTOR_3; ETA_AX] THEN
        REWRITE_TAC[REAL_CONTINUOUS_COMPLEX_COMPONENTS_WITHIN] THEN
        X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
        MATCH_MP_TAC(REWRITE_RULE[o_DEF] REAL_CONTINUOUS_WITHIN_COMPOSE) THEN
        SIMP_TAC[REAL_CONTINUOUS_SUB; REAL_CONTINUOUS_POW;
                 REAL_CONTINUOUS_CONST; REAL_CONTINUOUS_NORM_WITHIN] THEN
        MATCH_MP_TAC REAL_CONTINUOUS_WITHINREAL_SUBSET THEN
        EXISTS_TAC `{t | &0 <= t}` THEN
        REWRITE_TAC[REAL_CONTINUOUS_WITHIN_SQRT_STRONG] THEN
        SIMP_TAC[SUBSET; FORALL_IN_IMAGE; IN_CBALL; IN_ELIM_THM; dist;
                 COMPLEX_SUB_LZERO; NORM_NEG; REAL_SUB_LE] THEN
        REWRITE_TAC[ABS_SQUARE_LE_1; REAL_ABS_NORM];
        ALL_TAC] THEN
      EXPAND_TAC "g" THEN MATCH_MP_TAC CONTINUOUS_ON_SUB THEN
      CONJ_TAC THENL
       [ALL_TAC;
        MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN REWRITE_TAC[linear] THEN
          CONJ_TAC THEN VECTOR_ARITH_TAC;
          REWRITE_TAC[GSYM IMAGE_o]]] THEN
      MATCH_MP_TAC CONTINUOUS_ON_SUBSET THEN
      EXISTS_TAC `{x:real^3 | norm x = &1}` THEN ASM_REWRITE_TAC[] THEN
      REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; o_THM; IN_ELIM_THM] THEN
      SIMP_TAC[NORM_EQ_1; DOT_3; VECTOR_3; VECTOR_NEG_COMPONENT; dist;
               DIMINDEX_3; ARITH; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG] THEN
      REWRITE_TAC[REAL_NEG_MUL2] THEN X_GEN_TAC `z:complex` THEN DISCH_TAC;
      X_GEN_TAC `z:complex` THEN
      REWRITE_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG] THEN
      DISCH_TAC THEN MAP_EVERY EXPAND_TAC ["k";
 "g"] THEN
      REWRITE_TAC[COMPLEX_RING `x - y = Cx(&0) <=> y = x`] THEN
      FIRST_X_ASSUM MATCH_MP_TAC THEN
      REWRITE_TAC[NORM_EQ_1; DOT_3; VECTOR_3]] THEN
    REWRITE_TAC[GSYM REAL_POW_2; COMPLEX_SQNORM] THEN
    REWRITE_TAC[REAL_ARITH `r + i + s = &1 <=> s = &1 - (r + i)`] THEN
    MATCH_MP_TAC SQRT_POW_2 THEN REWRITE_TAC[GSYM COMPLEX_SQNORM] THEN
    ASM_SIMP_TAC[REAL_SUB_LE; ABS_SQUARE_LE_1; REAL_ABS_NORM];
    ALL_TAC] THEN
  DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(X_CHOOSE_THEN `h:complex->complex` STRIP_ASSUME_TAC) THEN
  ABBREV_TAC `m = \z:complex. (h(z) - h(--z)) / (Cx pi * ii)` THEN
  SUBGOAL_THEN
    `!z:complex. norm(z) = &1 ==> cexp(Cx pi * ii * m z) = cexp(Cx pi * ii)`
  MP_TAC THENL
   [EXPAND_TAC "m" THEN
    REWRITE_TAC[COMPLEX_SUB_LDISTRIB; complex_div; COMPLEX_SUB_RDISTRIB] THEN
    SIMP_TAC[CX_INJ; PI_NZ; CEXP_SUB; COMPLEX_FIELD
     `~(p = Cx(&0)) ==> p * ii * h * inv(p * ii) = h`] THEN
    X_GEN_TAC `z:complex` THEN DISCH_TAC THEN
    SUBGOAL_THEN `cexp(h z) = k z /\ cexp(h(--z:complex)) = k(--z)`
     (CONJUNCTS_THEN SUBST1_TAC)
    THENL
     [CONJ_TAC THEN CONV_TAC SYM_CONV THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG; REAL_LE_REFL];
      ALL_TAC] THEN
    REWRITE_TAC[EULER; RE_MUL_CX; IM_MUL_CX; RE_II; IM_II; COMPLEX_ADD_RID;
                REAL_MUL_RZERO; REAL_MUL_RID; SIN_PI; COS_PI; REAL_EXP_0;
                COMPLEX_MUL_RZERO; COMPLEX_MUL_LID] THEN
    MATCH_MP_TAC(COMPLEX_FIELD
     `~(y = Cx(&0)) /\ x = -- y ==> x / y = Cx(-- &1)`) THEN
    CONJ_TAC THENL
     [FIRST_X_ASSUM MATCH_MP_TAC THEN
      ASM_SIMP_TAC[dist; IN_CBALL; COMPLEX_SUB_LZERO; NORM_NEG; REAL_LE_REFL];
      MAP_EVERY EXPAND_TAC ["k"; "g"] THEN
      REWRITE_TAC[COMPLEX_NEG_SUB] THEN BINOP_TAC THEN AP_TERM_TAC THEN
      SIMP_TAC[CART_EQ; FORALL_3; VECTOR_3; VECTOR_NEG_COMPONENT;
               DIMINDEX_3; ARITH; RE_NEG; IM_NEG; NORM_NEG; REAL_NEG_NEG] THEN
      ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
      REWRITE_TAC[SQRT_0; REAL_NEG_0]];
    ALL_TAC] THEN
  REWRITE_TAC[CEXP_EQ; CX_MUL] THEN
  SIMP_TAC[CX_INJ; PI_NZ; COMPLEX_FIELD
   `~(p = Cx(&0))
    ==> (p * ii * m = p * ii + (t * n * p) * ii <=> m = t * n + Cx(&1))`] THEN
  REWRITE_TAC[GSYM CX_ADD; GSYM CX_MUL] THEN DISCH_THEN(LABEL_TAC "*") THEN
  SUBGOAL_THEN
   `?n. !z. z IN {z | norm(z) = &1} ==> (m:complex->complex)(z) = n`
  MP_TAC THENL
   [MATCH_MP_TAC CONTINUOUS_DISCRETE_RANGE_CONSTANT THEN CONJ_TAC THENL
     [ONCE_REWRITE_TAC[NORM_ARITH `norm z = dist(vec 0,z)`] THEN
      SIMP_TAC[GSYM sphere; CONNECTED_SPHERE; DIMINDEX_2; LE_REFL];
      ALL_TAC] THEN
    CONJ_TAC THENL
     [EXPAND_TAC "m" THEN MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_DIV THEN
      SIMP_TAC[CONTINUOUS_ON_CONST; COMPLEX_ENTIRE; II_NZ; CX_INJ; PI_NZ] THEN
      MATCH_MP_TAC CONTINUOUS_ON_SUB THEN CONJ_TAC THENL
       [ALL_TAC;
        MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
        CONJ_TAC THENL
         [MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN REWRITE_TAC[linear] THEN
          CONJ_TAC THEN VECTOR_ARITH_TAC;
          REWRITE_TAC[GSYM IMAGE_o]]] THEN
      FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP
       (REWRITE_RULE[IMP_CONJ] CONTINUOUS_ON_SUBSET)) THEN
      SIMP_TAC[SUBSET; FORALL_IN_IMAGE; NORM_NEG; IN_CBALL;
               COMPLEX_SUB_LZERO; dist; IN_ELIM_THM; REAL_LE_REFL];
      ALL_TAC] THEN
    X_GEN_TAC `z:complex` THEN REWRITE_TAC[IN_ELIM_THM] THEN
    DISCH_TAC THEN EXISTS_TAC `&1` THEN REWRITE_TAC[REAL_LT_01] THEN
    X_GEN_TAC `w:complex` THEN STRIP_TAC THEN
    REMOVE_THEN "*" (fun th -> MP_TAC(SPEC `w:complex` th) THEN
                               MP_TAC(SPEC `z:complex` th)) THEN
    ASM_REWRITE_TAC[] THEN
    REPEAT(DISCH_THEN(CHOOSE_THEN
     (CONJUNCTS_THEN2 ASSUME_TAC SUBST_ALL_TAC))) THEN
    REWRITE_TAC[GSYM CX_SUB; COMPLEX_NORM_CX] THEN
    MATCH_MP_TAC(REAL_ARITH
     `~(abs(x - y) < &1) ==> &1 <= abs((&2 * x + &1) - (&2 * y + &1))`) THEN
    ASM_SIMP_TAC[GSYM REAL_EQ_INTEGERS] THEN ASM_MESON_TAC[];
    REWRITE_TAC[IN_ELIM_THM] THEN DISCH_THEN(X_CHOOSE_TAC `v:complex`)] THEN
  SUBGOAL_THEN
    `?n. integer n /\ !z:complex. norm z = &1 ==> m z = Cx(&2 * n + &1)`
  MP_TAC THENL
   [REMOVE_THEN "*" (MP_TAC o SPEC `Cx(&1)`) THEN
    ASM_SIMP_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM] THEN ASM_MESON_TAC[];
    ALL_TAC] THEN
  DISCH_THEN(X_CHOOSE_THEN `n:real` MP_TAC) THEN EXPAND_TAC "m" THEN
  DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
  DISCH_THEN(fun th -> MP_TAC(SPEC `--Cx(&1)` th) THEN
                        MP_TAC(SPEC `Cx(&1)` th)) THEN
  REWRITE_TAC[NORM_NEG; COMPLEX_NORM_CX; REAL_ABS_NUM; COMPLEX_NEG_NEG] THEN
  REWRITE_TAC[complex_div; COMPLEX_SUB_RDISTRIB] THEN
  MATCH_MP_TAC(COMPLEX_RING
   `~(z = Cx(&0)) ==> a - b = z ==> ~(b - a = z)`) THEN
  REWRITE_TAC[CX_INJ; REAL_ARITH `&2 * n + &1 = &0 <=> n = --(&1 / &2)`] THEN
  UNDISCH_TAC `integer n` THEN GEN_REWRITE_TAC I [GSYM CONTRAPOS_THM] THEN
  SIMP_TAC[] THEN DISCH_TAC THEN REWRITE_TAC[integer] THEN
  REWRITE_TAC[REAL_ABS_NEG; REAL_ABS_DIV; REAL_ABS_NUM] THEN
  REWRITE_TAC[REAL_ARITH `a / &2 = n <=> a = &2 * n`] THEN
  REWRITE_TAC[NOT_EXISTS_THM; REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
  GEN_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `EVEN`) THEN
  REWRITE_TAC[EVEN_MULT; ARITH]);;

(* ------------------------------------------------------------------------- *)
(* The Borsuk-Ulam theorem for a general sphere.                             *)
(* ------------------------------------------------------------------------- *)

let BORSUK_ULAM = 
prove
 (`!f:real^3->real^2 a r.
        &0 <= r /\ f continuous_on {z | norm(z - a) = r}
        ==> ?x. norm(x) = r /\ f(a + x) = f(a - x)`,

  REPEAT STRIP_TAC THEN
  MP_TAC(SPEC `\x. (f:real^3->real^2) (a + r % x)` THEOREM_1) THEN
  REWRITE_TAC[] THEN ANTS_TAC THENL
   [MATCH_MP_TAC(REWRITE_RULE[o_DEF] CONTINUOUS_ON_COMPOSE) THEN
    SIMP_TAC[CONTINUOUS_ON_ADD; CONTINUOUS_ON_CONST;
             CONTINUOUS_ON_CMUL; CONTINUOUS_ON_ID] THEN
    FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
        CONTINUOUS_ON_SUBSET)) THEN
    REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_ELIM_THM];
    DISCH_THEN(X_CHOOSE_THEN `x:real^3` STRIP_ASSUME_TAC) THEN
    EXISTS_TAC `r % x:real^3` THEN
    ASM_REWRITE_TAC[VECTOR_ARITH `a - r % x:real^3 = a + r % --x`]] THEN
  ASM_SIMP_TAC[VECTOR_ADD_SUB; NORM_MUL] THEN ASM_REAL_ARITH_TAC);;