(* ========================================================================= *)
(* Complex transcendentals and their real counterparts. *)
(* *)
(* (c) Copyright, John Harrison 1998-2008 *)
(* ========================================================================= *)
needs "Multivariate/determinants.ml";;
needs "Multivariate/canal.ml";;
prioritize_complex();;
(* ------------------------------------------------------------------------- *)
(* The complex exponential function. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Add it to the database. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV
HAS_COMPLEX_DERIVATIVE_CEXP)));;
(* ------------------------------------------------------------------------- *)
(* Hence the main results. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Crude bounds on complex exponential function, usable to get tighter ones. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Complex trig functions. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Euler and de Moivre formulas. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real exponential function. Same names as old Library/transc.ml. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real trig functions, their reality, derivatives of complex versions. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV
HAS_COMPLEX_DERIVATIVE_CSIN)));;
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN_UNIV
HAS_COMPLEX_DERIVATIVE_CCOS)));;
(* ------------------------------------------------------------------------- *)
(* Slew of theorems for compatibility with old transc.ml file. *)
(* ------------------------------------------------------------------------- *)
let (SIN_BOUND,COS_BOUND) = (CONJ_PAIR o prove)
(`(!x. abs(sin x) <= &1) /\ (!x. abs(cos x) <= &1)`,
CONJ_TAC THEN GEN_TAC THEN ONCE_REWRITE_TAC[GSYM REAL_ABS_NUM] THEN
ONCE_REWRITE_TAC[REAL_LE_SQUARE_ABS] THEN
MP_TAC(SPEC `x:real` SIN_CIRCLE) THEN
MAP_EVERY (MP_TAC o C SPEC REAL_LE_SQUARE) [`sin x`; `cos x`] THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Get a nice real/imaginary separation in Euler's formula. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some special intermediate value theorems over the reals. *)
(* ------------------------------------------------------------------------- *)
let IVT_INCREASING_RE = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f
continuous at (Cx x)) /\
Re(f(Cx a)) <= y /\ y <= Re(f(Cx b))
==> ?x. a <= x /\ x <= b /\ Re(f(Cx x)) = y`,
let IVT_DECREASING_RE = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f
continuous at (Cx x)) /\
Re(f(Cx b)) <= y /\ y <= Re(f(Cx a))
==> ?x. a <= x /\ x <= b /\ Re(f(Cx x)) = y`,
let IVT_INCREASING_IM = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f
continuous at (Cx x)) /\
Im(f(Cx a)) <= y /\ y <= Im(f(Cx b))
==> ?x. a <= x /\ x <= b /\ Im(f(Cx x)) = y`,
let IVT_DECREASING_IM = prove
(`!f a b y.
a <= b /\
(!x. a <= x /\ x <= b ==> f
continuous at (Cx x)) /\
Im(f(Cx b)) <= y /\ y <= Im(f(Cx a))
==> ?x. a <= x /\ x <= b /\ Im(f(Cx x)) = y`,
(* ------------------------------------------------------------------------- *)
(* Some minimal properties of real logs help to define complex logs. *)
(* ------------------------------------------------------------------------- *)
let LOG_MUL = prove
(`!x y. &0 < x /\ &0 < y ==> (log(x * y) = log(x) + log(y))`,
let LOG_INJ = prove
(`!x y. &0 < x /\ &0 < y ==> (log(x) = log(y) <=> x = y)`,
REPEAT STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [GSYM
REAL_EXP_INJ] THEN
ASM_SIMP_TAC[
EXP_LOG]);;
let LOG_DIV = prove
(`!x y. &0 < x /\ &0 < y ==> log(x / y) = log(x) - log(y)`,
(* ------------------------------------------------------------------------- *)
(* Deduce periodicity just from derivative and zero values. *)
(* ------------------------------------------------------------------------- *)
let pi = new_definition
`pi = @p. &0 < p /\ sin(p) = &0 /\ !x. &0 < x /\ x < p ==> ~(sin(x) = &0)`;;
(* ------------------------------------------------------------------------- *)
(* Now more relatively easy consequences. *)
(* ------------------------------------------------------------------------- *)
let COS_POS_PI = prove
(`!x. --(
pi / &2) < x /\ x <
pi / &2 ==> &0 <
cos(x)`,
GEN_TAC THEN MP_TAC(SPEC `abs x`
COS_POS_PI2) THEN REWRITE_TAC[
COS_ABS] THEN
ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[
COS_0] THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
let COS_EQ_0 = prove
(`!x.
cos(x) = &0 <=> ?n.
integer n /\ x = (n + &1 / &2) *
pi`,
GEN_TAC THEN REWRITE_TAC[
COS_SIN;
SIN_EQ_0] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
EXISTS_TAC `--n:real` THEN ASM_REWRITE_TAC[
INTEGER_NEG] THEN
ASM_REAL_ARITH_TAC);;
let COS_ZERO_PI = prove
(`!x.
cos(x) = &0 <=>
(?n. x = (&n + &1 / &2) *
pi) \/ (?n. x = --((&n + &1 / &2) *
pi))`,
GEN_TAC THEN REWRITE_TAC[
COS_EQ_0;
INTEGER_CASES;
RIGHT_OR_DISTRIB] THEN
REWRITE_TAC[
EXISTS_OR_THM;
LEFT_AND_EXISTS_THM] THEN
ONCE_REWRITE_TAC[
SWAP_EXISTS_THM] THEN SIMP_TAC[
UNWIND_THM2] THEN EQ_TAC THEN
DISCH_THEN(DISJ_CASES_THEN (X_CHOOSE_THEN `n:num` SUBST1_TAC)) THENL
[DISJ1_TAC THEN EXISTS_TAC `n:num`;
ASM_CASES_TAC `n = 0` THENL
[DISJ1_TAC THEN EXISTS_TAC `0`;
DISJ2_TAC THEN EXISTS_TAC `n - 1`];
DISJ1_TAC THEN EXISTS_TAC `n:num`;
DISJ2_TAC THEN EXISTS_TAC `n + 1`] THEN
ASM_SIMP_TAC[GSYM
REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_ADD;
ARITH_RULE `1 <= n <=> ~(n = 0)`] THEN
REAL_ARITH_TAC);;
let COS_ZERO = prove
(`!x.
cos(x) = &0 <=> (?n. ~EVEN n /\ (x = &n * (
pi / &2))) \/
(?n. ~EVEN n /\ (x = --(&n * (
pi / &2))))`,
let COS_ONE_2PI = prove
(`!x. (
cos(x) = &1) <=> (?n. x = &n * &2 *
pi) \/ (?n. x = --(&n * &2 *
pi))`,
GEN_TAC THEN EQ_TAC THEN DISCH_TAC THENL
[FIRST_ASSUM(MP_TAC o SPEC `
sin(x)` o MATCH_MP (REAL_RING
`c = &1 ==> !s. s pow 2 + c pow 2 = &1 ==> s = &0`)) THEN
REWRITE_TAC[
SIN_ZERO_PI;
SIN_CIRCLE] THEN
DISCH_THEN(DISJ_CASES_THEN(X_CHOOSE_THEN `n:num` SUBST_ALL_TAC)) THEN
POP_ASSUM MP_TAC THEN REWRITE_TAC[
COS_NEG;
COS_NPI;
REAL_POW_NEG] THEN
COND_CASES_TAC THEN REWRITE_TAC[
REAL_POW_ONE] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
FIRST_X_ASSUM(MP_TAC o REWRITE_RULE[
EVEN_EXISTS]) THEN
REWRITE_TAC[
OR_EXISTS_THM] THEN MATCH_MP_TAC
MONO_EXISTS THEN
SIMP_TAC[GSYM REAL_OF_NUM_MUL] THEN REAL_ARITH_TAC;
FIRST_X_ASSUM (DISJ_CASES_THEN CHOOSE_TAC) THEN
ASM_REWRITE_TAC[
COS_NEG; REAL_MUL_ASSOC; REAL_OF_NUM_MUL;
COS_NPI;
REAL_POW_NEG;
EVEN_MULT; ARITH;
REAL_POW_ONE]]);;
(* ------------------------------------------------------------------------- *)
(* Prove totality of trigs. *)
(* ------------------------------------------------------------------------- *)
let SINCOS_TOTAL_PI2 = prove
(`!x y. &0 <= x /\ &0 <= y /\ x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t <=
pi / &2 /\ x =
cos t /\ y =
sin t`,
REPEAT STRIP_TAC THEN MP_TAC(SPEC `y:real`
SIN_TOTAL_POS) THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[] THEN FIRST_ASSUM(MATCH_MP_TAC o MATCH_MP (REAL_ARITH
`x pow 2 + y pow 2 = &1
==> (&1 < y ==> &1 pow 2 < y pow 2) /\ &0 <= x * x
==> y <= &1`)) THEN
SIMP_TAC[
REAL_LE_SQUARE;
REAL_POW_LT2;
REAL_POS; ARITH];
MATCH_MP_TAC
MONO_EXISTS THEN X_GEN_TAC `t:real` THEN
STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `x =
cos t \/ x = --(
cos t)` MP_TAC THENL
[MP_TAC(SPEC `t:real`
SIN_CIRCLE);
MP_TAC(SPEC `t:real`
COS_POS_PI_LE)] THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC REAL_FIELD]);;
let SINCOS_TOTAL_PI = prove
(`!x y. &0 <= y /\ x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t <=
pi /\ x =
cos t /\ y =
sin t`,
REPEAT STRIP_TAC THEN DISJ_CASES_TAC(REAL_ARITH `&0 <= x \/ &0 <= --x`) THENL
[MP_TAC(SPECL [`x:real`; `y:real`]
SINCOS_TOTAL_PI2);
MP_TAC(SPECL [`--x:real`; `y:real`]
SINCOS_TOTAL_PI2)] THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `t:real`; EXISTS_TAC `
pi - t`] THEN
ASM_REWRITE_TAC[
SIN_SUB;
COS_SUB;
SIN_PI;
COS_PI] THEN
ASM_REAL_ARITH_TAC);;
let SINCOS_TOTAL_2PI = prove
(`!x y. x pow 2 + y pow 2 = &1
==> ?t. &0 <= t /\ t < &2 *
pi /\ x =
cos t /\ y =
sin t`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `x = &1 /\ y = &0` THENL
[EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[
SIN_0;
COS_0] THEN
MP_TAC
PI_POS THEN REAL_ARITH_TAC;
ALL_TAC] THEN
DISJ_CASES_TAC(REAL_ARITH `&0 <= y \/ &0 <= --y`) THENL
[MP_TAC(SPECL [`x:real`; `y:real`]
SINCOS_TOTAL_PI);
MP_TAC(SPECL [`x:real`; `--y:real`]
SINCOS_TOTAL_PI)] THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; ARITH] THEN
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THENL
[EXISTS_TAC `t:real`; EXISTS_TAC `&2 *
pi - t`] THEN
ASM_REWRITE_TAC[
SIN_SUB;
COS_SUB;
SIN_NPI;
COS_NPI] THENL
[MP_TAC
PI_POS THEN ASM_REAL_ARITH_TAC;
ALL_TAC] THEN
REPEAT(POP_ASSUM MP_TAC) THEN ASM_CASES_TAC `t = &0` THEN
ASM_REWRITE_TAC[
SIN_0;
COS_0] THEN POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Polar representation. *)
(* ------------------------------------------------------------------------- *)
let CCOS_EQ_1 = prove
(`!z.
ccos z = Cx(&1) <=> ?n.
integer n /\ z = Cx(&2 * n *
pi)`,
GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o RAND_CONV)
[COMPLEX_RING `z = Cx(&2) * z / Cx(&2)`] THEN
REWRITE_TAC[
CCOS_DOUBLE_CSIN; COMPLEX_RING
`a - Cx(&2) * s pow 2 = a <=> s = Cx(&0)`] THEN
REWRITE_TAC[
CSIN_EQ_0;
CX_MUL] THEN
EQ_TAC THEN MATCH_MP_TAC
MONO_EXISTS THEN SIMP_TAC[] THEN
CONV_TAC COMPLEX_RING);;
let CSIN_EQ_MINUS1 = prove
(`!z.
csin z = --Cx(&1) <=>
?n.
integer n /\ z = Cx((&2 * n + &3 / &2) *
pi)`,
GEN_TAC THEN REWRITE_TAC[COMPLEX_RING `z:complex = --w <=> --z = w`] THEN
REWRITE_TAC[GSYM
CSIN_NEG;
CSIN_EQ_1] THEN
REWRITE_TAC[COMPLEX_RING `--z:complex = w <=> z = --w`] THEN
EQ_TAC THEN DISCH_THEN(X_CHOOSE_THEN `n:real` STRIP_ASSUME_TAC) THEN
ASM_REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
EXISTS_TAC `--(n + &1)` THEN
ASM_SIMP_TAC[
INTEGER_CLOSED] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Taylor series for complex exponential. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Approximation to e. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Taylor series for complex sine and cosine. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* The argument of a complex number, where 0 <= arg(z) < 2 pi *)
(* ------------------------------------------------------------------------- *)
let Arg_DEF = new_definition
`Arg z = if z = Cx(&0) then &0
else @t. &0 <= t /\ t < &2 * pi /\
z = Cx(norm(z)) * cexp(ii * Cx t)`;;
let ARG_UNIQUE = prove
(`!a r z. &0 < r /\ Cx r *
cexp(
ii * Cx a) = z /\ &0 <= a /\ a < &2 *
pi
==> Arg z = a`,
REPEAT STRIP_TAC THEN ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN
MATCH_MP_TAC(COMPLEX_RING `
ii * x =
ii * y ==> x = y`) THEN
MATCH_MP_TAC
COMPLEX_EQ_CEXP THEN CONJ_TAC THENL
[REWRITE_TAC[
IM_MUL_II;
RE_CX] THEN
MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x < p /\ &0 <= y /\ y < p
==> abs(x - y) < p`) THEN
ASM_SIMP_TAC[
ARG];
MATCH_MP_TAC(COMPLEX_RING
`!a b. Cx a = Cx b /\ ~(Cx b = Cx(&0)) /\
Cx a * w = Cx b * z ==> w = z`) THEN
MAP_EVERY EXISTS_TAC [`
norm(z:complex)`; `r:real`] THEN
ASM_REWRITE_TAC[GSYM
ARG] THEN ASM_SIMP_TAC[
CX_INJ;
REAL_LT_IMP_NZ] THEN
EXPAND_TAC "z" THEN
REWRITE_TAC[
NORM_CEXP_II;
COMPLEX_NORM_MUL;
COMPLEX_NORM_CX] THEN
ASM_REAL_ARITH_TAC]);;
let ARG_EQ = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> (Arg w = Arg z <=> ?x. &0 < x /\ w = Cx(x) * z)`,
let ARG_LE_DIV_SUM = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0)) /\ Arg(w) <= Arg(z)
==> Arg(z) = Arg(w) + Arg(z / w)`,
let ARG_LE_DIV_SUM_EQ = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> (Arg(w) <= Arg(z) <=> Arg(z) = Arg(w) + Arg(z / w))`,
let REAL_SUB_ARG = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg w - Arg z = if Arg(z) <= Arg(w) then Arg(w / z)
else Arg(w / z) - &2 *
pi`,
REPEAT STRIP_TAC THEN COND_CASES_TAC THENL
[MP_TAC(ISPECL [`z:complex`; `w:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
MP_TAC(ISPECL [`w:complex`; `z:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN
ANTS_TAC THENL [ASM_REAL_ARITH_TAC; DISCH_THEN SUBST1_TAC] THEN
REWRITE_TAC[REAL_ARITH `a - (a + b):real = --b`] THEN
GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [GSYM
COMPLEX_INV_DIV] THEN
MATCH_MP_TAC(REAL_ARITH `x = &2 *
pi - y ==> --x = y - &2 *
pi`) THEN
MATCH_MP_TAC
ARG_INV THEN REWRITE_TAC[GSYM
ARG_EQ_0] THEN
ONCE_REWRITE_TAC[GSYM
COMPLEX_INV_DIV] THEN
REWRITE_TAC[
ARG_INV_EQ_0] THEN
MP_TAC(ISPECL [`w:complex`; `z:complex`]
ARG_LE_DIV_SUM) THEN
ASM_REWRITE_TAC[] THEN ASM_REAL_ARITH_TAC]);;
let REAL_ADD_ARG = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg(w) + Arg(z) =
if Arg w + Arg z < &2 *
pi
then Arg(w * z)
else Arg(w * z) + &2 *
pi`,
REPEAT STRIP_TAC THEN
MP_TAC(SPECL [`w * z:complex`; `z:complex`]
REAL_SUB_ARG) THEN
MP_TAC(SPECL [`z:complex`; `w * z:complex`]
ARG_LE_DIV_SUM_EQ) THEN
ASM_SIMP_TAC[
COMPLEX_ENTIRE; COMPLEX_FIELD
`~(z = Cx(&0)) ==> (w * z) / z = w`] THEN
ASM_CASES_TAC `Arg (w * z) = Arg z + Arg w` THEN ASM_REWRITE_TAC[] THENL
[ASM_MESON_TAC[
ARG; REAL_ADD_SYM];
SIMP_TAC[REAL_ARITH `wz - z = w - &2 *
pi <=> w + z = wz + &2 *
pi`] THEN
REWRITE_TAC[REAL_ARITH `w + p < p <=> ~(&0 <= w)`;
ARG]]);;
let ARG_MUL = prove
(`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
==> Arg(w * z) = if Arg w + Arg z < &2 *
pi
then Arg w + Arg z
else (Arg w + Arg z) - &2 *
pi`,
REPEAT GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
REAL_ADD_ARG) THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Properties of 2-D rotations, and their interpretation using cexp. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Homotopy staying within the set of orthogonal transformations *)
(* ------------------------------------------------------------------------- *)
let NULLHOMOTOPIC_ORTHOGONAL_TRANSFORMATION = prove
(`!f:real^N->real^N.
orthogonal_transformation f /\
det(
matrix f) = &1
==>
homotopic_with orthogonal_transformation ((:real^N),(:real^N)) f I`,
let lemma0 = prove
(`!a x:real^N.
2 <= dimindex(:N) /\ a IN span {basis 1,basis 2}
==> reflect_along (vector[a$1; a$2]:real^2) (lambda i. x$i) =
(lambda i. reflect_along a x$i)`,
REPEAT STRIP_TAC THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; reflect_along; VECTOR_SUB_COMPONENT;
VECTOR_MUL_COMPONENT; DIMINDEX_2; FORALL_2; VECTOR_2; ARITH] THEN
CONJ_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN
AP_TERM_TAC THEN BINOP_TAC THEN REWRITE_TAC[dot] THEN
CONV_TAC SYM_CONV THEN MATCH_MP_TAC SUM_EQ_SUPERSET THEN
ASM_SIMP_TAC[FINITE_NUMSEG; IN_NUMSEG; FORALL_2; DIMINDEX_2; LAMBDA_BETA;
ARITH; VECTOR_2; SUBSET_NUMSEG] THEN
REWRITE_TAC[ARITH_RULE
`(1 <= i /\ i <= n) /\ ~(1 <= i /\ i <= 2) <=>
1 <= i /\ 3 <= i /\ i <= n`] THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE RAND_CONV [SPAN_2]) THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
STRIP_TAC THEN
ASM_REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
SIMP_TAC[BASIS_COMPONENT] THEN
REPEAT STRIP_TAC THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RZERO]) THEN
ASM_ARITH_TAC) in
let lemma1 = prove
(`!a b:real^2 r.
~(a = vec 0) /\ ~(b = vec 0)
==> homotopic_with orthogonal_transformation ((:real^2),(:real^2))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN
MP_TAC(SPEC `reflect_along (a:real^2) o reflect_along b`
ROTATION_ROTATE2D) THEN
ANTS_TAC THENL
[REPEAT(FIRST_X_ASSUM(MP_TAC o
MATCH_MP ROTOINVERSION_MATRIX_REFLECT_ALONG)) THEN
REWRITE_TAC[rotoinversion_matrix] THEN
SIMP_TAC[ORTHOGONAL_MATRIX_MATRIX;
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG;
ORTHOGONAL_TRANSFORMATION_COMPOSE; MATRIX_COMPOSE;
LINEAR_REFLECT_ALONG; DET_MUL] THEN
CONV_TAC REAL_RAT_REDUCE_CONV;
DISCH_THEN(X_CHOOSE_THEN `t:real` STRIP_ASSUME_TAC) THEN
ONCE_REWRITE_TAC[HOMOTOPIC_WITH_SYM] THEN
ASM_REWRITE_TAC[homotopic_with] THEN
EXISTS_TAC `\z. rotate2d (drop(fstcart z) * t) (sndcart z)` THEN
SIMP_TAC[ORTHOGONAL_TRANSFORMATION_ROTATE2D; SNDCART_PASTECART;
ETA_AX; FSTCART_PASTECART; DROP_VEC; I_THM; NORM_ROTATE2D;
REAL_MUL_LZERO; REAL_MUL_LID; SUBSET; FORALL_IN_IMAGE; IN_UNIV;
FORALL_IN_PCROSS; IN_SPHERE_0; ROTATE2D_ZERO] THEN
REWRITE_TAC[ROTATE2D_COMPLEX] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_MUL THEN
SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_SNDCART] THEN
GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
REWRITE_TAC[CONTINUOUS_ON_CEXP; CX_MUL] THEN
ONCE_REWRITE_TAC[COMPLEX_RING `ii * x * t = (ii * t) * x`] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPLEX_LMUL THEN
MATCH_MP_TAC CONTINUOUS_ON_CX_DROP THEN
SIMP_TAC[LINEAR_CONTINUOUS_ON; LINEAR_FSTCART]]) in
let lemma2 = prove
(`!a b:real^N r.
2 <= dimindex(:N) /\
~(a = vec 0) /\ ~(b = vec 0) /\
{a,b} SUBSET span {basis 1,basis 2}
==> homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN
SUBGOAL_THEN
`homotopic_with orthogonal_transformation
((:real^N),(:real^N))
((\z. (lambda i. if i <= 2 then (fstcart z)$i
else (sndcart z)$i):real^N) o
(\z. pastecart
(((reflect_along (vector [(a:real^N)$1; a$2]) o
reflect_along (vector [(b:real^N)$1; b$2]))
:real^2->real^2)(fstcart z))
(sndcart z)) o
(\z:real^N. pastecart ((lambda i. z$i) :real^2) z))
((\z. (lambda i. if i <= 2 then (fstcart z)$i
else (sndcart z)$i):real^N) o
I o
(\z:real^N. pastecart ((lambda i. z$i) :real^2) z))`
MP_TAC THENL
[MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `(:real^2) PCROSS (:real^N)` THEN
REWRITE_TAC[SUBSET_UNIV] THEN CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN
ONCE_REWRITE_TAC[LINEAR_COMPONENTWISE] THEN
SIMP_TAC[LAMBDA_BETA] THEN X_GEN_TAC `i:num` THEN
STRIP_TAC THEN ASM_CASES_TAC `i <= 2` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[linear; FSTCART_ADD; FSTCART_CMUL;
SNDCART_ADD; SNDCART_CMUL] THEN
REWRITE_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT] THEN
REWRITE_TAC[LIFT_ADD; LIFT_CMUL]] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^2) PCROSS (:real^N)` THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_UNIV; PASTECART_IN_PCROSS] THEN
CONJ_TAC THENL
[ALL_TAC;
MATCH_MP_TAC LINEAR_CONTINUOUS_ON THEN
MATCH_MP_TAC LINEAR_PASTECART THEN REWRITE_TAC[LINEAR_ID] THEN
SIMP_TAC[linear; CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT]] THEN
SUBGOAL_THEN
`I = \z:real^(2,N)finite_sum. pastecart (fstcart z) (sndcart z)`
SUBST1_TAC THENL
[REWRITE_TAC[PASTECART_FST_SND; I_DEF]; ALL_TAC] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_PCROSS THEN
EXISTS_TAC `orthogonal_transformation:(real^2->real^2)->bool` THEN
EXISTS_TAC `\f:real^N->real^N. f = I` THEN REPEAT CONJ_TAC THENL
[REWRITE_TAC[GSYM I_DEF; ETA_AX] THEN MATCH_MP_TAC lemma1 THEN
FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [INSERT_SUBSET]) THEN
REWRITE_TAC[SING_SUBSET; SPAN_2; IN_ELIM_THM; IN_UNIV] THEN
DISCH_THEN(REPEAT_TCL STRIP_THM_THEN SUBST_ALL_TAC) THEN
POP_ASSUM_LIST(MP_TAC o end_itlist CONJ o rev) THEN
REWRITE_TAC[CART_EQ; VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
DIMINDEX_2; FORALL_2; VECTOR_2] THEN
SIMP_TAC[BASIS_COMPONENT; ARITH; DIMINDEX_2; VEC_COMPONENT;
DIMINDEX_GE_1; LE_REFL] THEN
MATCH_MP_TAC(TAUT
`(r ==> q) /\ (s ==> p) ==> a /\ ~p /\ ~q ==> ~s /\ ~r`) THEN
SIMP_TAC[REAL_MUL_RZERO; REAL_MUL_LZERO; REAL_MUL_RID;
REAL_ADD_LID; REAL_ADD_RID];
REWRITE_TAC[HOMOTOPIC_WITH_REFL; SUBSET_UNIV; I_DEF] THEN
REWRITE_TAC[CONTINUOUS_ON_ID];
SIMP_TAC[o_DEF; FSTCART_PASTECART; SNDCART_PASTECART;
LAMBDA_BETA; DIMINDEX_2; ARITH; I_THM] THEN
REWRITE_TAC[ORTHOGONAL_TRANSFORMATION; NORM_EQ] THEN
X_GEN_TAC `f:real^2->real^2` THEN GEN_TAC THEN STRIP_TAC THEN
CONJ_TAC THENL
[FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [linear]) THEN
SIMP_TAC[linear; CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT; DIMINDEX_2; ARITH] THEN
MATCH_MP_TAC MONO_AND THEN CONJ_TAC THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN GEN_TAC THEN
GEN_TAC THEN X_GEN_TAC `i:num` THEN STRIP_TAC THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[] THEN
AP_THM_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; VECTOR_ADD_COMPONENT;
VECTOR_MUL_COMPONENT];
X_GEN_TAC `v:real^N` THEN REWRITE_TAC[dot; GSYM REAL_POW_2] THEN
SUBGOAL_THEN `dimindex(:N) = 2 + (dimindex(:N) - 2)` SUBST1_TAC THENL
[ASM_ARITH_TAC; ALL_TAC] THEN
ASM_SIMP_TAC[SUM_ADD_SPLIT; ARITH_RULE `1 <= n + 1`] THEN
BINOP_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[dot; DIMINDEX_2; GSYM REAL_POW_2]) THEN
FIRST_X_ASSUM(MP_TAC o SPEC `(lambda i. (v:real^N)$i):real^2`) THEN
MATCH_MP_TAC EQ_IMP THEN BINOP_TAC THEN
MATCH_MP_TAC SUM_EQ_NUMSEG THEN
FIRST_ASSUM(MP_TAC o MATCH_MP (ARITH_RULE
`2 <= n ==> !i. i <= 2 ==> i <= n`)) THEN
SIMP_TAC[LAMBDA_BETA; DIMINDEX_2];
ASM_SIMP_TAC[ARITH_RULE `2 <= n ==> 2 + n - 2 = n`] THEN
MATCH_MP_TAC SUM_EQ_NUMSEG THEN
SIMP_TAC[ARITH_RULE `2 + 1 <= i ==> 1 <= i`;
LAMBDA_BETA; DIMINDEX_2] THEN
REPEAT STRIP_TAC THEN COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
ASM_ARITH_TAC]]];
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
REWRITE_TAC[IN_UNIV; GSYM FUN_EQ_THM] THEN
SIMP_TAC[o_DEF; FSTCART_PASTECART; SNDCART_PASTECART;
LAMBDA_BETA; DIMINDEX_2; ARITH; I_THM] THEN
RULE_ASSUM_TAC(REWRITE_RULE[INSERT_SUBSET; EMPTY_SUBSET]) THEN
ASM_SIMP_TAC[lemma0] THEN
SIMP_TAC[CART_EQ; LAMBDA_BETA; DIMINDEX_2; ARITH; COND_ID] THEN
MAP_EVERY X_GEN_TAC [`x:real^N`; `i:num`] THEN STRIP_TAC THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[] THEN
SUBGOAL_THEN `(a:real^N)$i = &0 /\ (b:real^N)$i = &0` ASSUME_TAC THENL
[FIRST_X_ASSUM(CONJUNCTS_THEN MP_TAC) THEN
REWRITE_TAC[SPAN_2; IN_ELIM_THM; IN_UNIV] THEN REPEAT STRIP_TAC THEN
ASM_SIMP_TAC[VECTOR_ADD_COMPONENT; VECTOR_MUL_COMPONENT;
BASIS_COMPONENT] THEN
REPEAT(COND_CASES_TAC THEN ASM_REWRITE_TAC[]) THEN
(REAL_ARITH_TAC ORELSE ASM_ARITH_TAC);
ASM_REWRITE_TAC[reflect_along; VECTOR_SUB_COMPONENT; REAL_MUL_RZERO;
VECTOR_MUL_COMPONENT; REAL_SUB_RZERO]]]) in
let lemma3 = prove
(`!a b:real^N r.
~(a = vec 0) /\ ~(b = vec 0)
==> homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(reflect_along a o reflect_along b) I`,
REPEAT STRIP_TAC THEN ASM_CASES_TAC `dimindex(:N) = 1` THENL
[ASM_SIMP_TAC[o_DEF; I_DEF; REFLECT_ALONG_1D; VECTOR_NEG_NEG] THEN
REWRITE_TAC[HOMOTOPIC_WITH_REFL; SUBSET_UNIV; CONTINUOUS_ON_ID] THEN
REWRITE_TAC[ORTHOGONAL_TRANSFORMATION_ID];
FIRST_X_ASSUM(MP_TAC o MATCH_MP(ARITH_RULE
`~(n = 1) ==> 1 <= n ==> 2 <= n`)) THEN
REWRITE_TAC[DIMINDEX_GE_1] THEN DISCH_TAC] THEN
MP_TAC(ISPECL [`span{a:real^N,b}`; `span{basis 1:real^N,basis 2}`]
ORTHOGONAL_TRANSFORMATION_INTO_SUBSPACE) THEN
REWRITE_TAC[SUBSPACE_SPAN; DIM_SPAN] THEN ANTS_TAC THENL
[ASM_REWRITE_TAC[DIM_INSERT; SPAN_SING; SPAN_EMPTY;
IN_SING; DIM_EMPTY] THEN
MATCH_MP_TAC(ARITH_RULE `m <= 2 /\ n = 2 ==> m <= n`) THEN
CONJ_TAC THENL [ASM_ARITH_TAC; ALL_TAC] THEN
ASM_SIMP_TAC[BASIS_NONZERO; ARITH] THEN
REWRITE_TAC[IN_ELIM_THM; IN_UNIV] THEN
COND_CASES_TAC THEN REWRITE_TAC[] THEN
FIRST_X_ASSUM(CHOOSE_THEN (MP_TAC o AP_TERM `(\x:real^N. x$1)`)) THEN
ASM_SIMP_TAC[BASIS_COMPONENT; VECTOR_MUL_COMPONENT;
ARITH; DIMINDEX_GE_1] THEN
REAL_ARITH_TAC;
DISCH_THEN(X_CHOOSE_THEN `f:real^N->real^N` STRIP_ASSUME_TAC) THEN
MP_TAC(ISPEC `f:real^N->real^N` ORTHOGONAL_TRANSFORMATION_INVERSE_o) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `g:real^N->real^N` STRIP_ASSUME_TAC)] THEN
SUBGOAL_THEN
`homotopic_with orthogonal_transformation ((:real^N),(:real^N))
(g o (f o (reflect_along a o reflect_along b) o (g:real^N->real^N)) o f)
(g o (f o I o (g:real^N->real^N)) o f)`
MP_TAC THENL
[ALL_TAC;
ASM_REWRITE_TAC[o_ASSOC] THEN ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID]] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR; LINEAR_CONTINUOUS_ON] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR; LINEAR_CONTINUOUS_ON] THEN
ASM_REWRITE_TAC[I_O_ID] THEN
MP_TAC(ISPEC `f:real^N->real^N` REFLECT_ALONG_LINEAR_IMAGE) THEN
ASM_REWRITE_TAC[GSYM ORTHOGONAL_TRANSFORMATION] THEN
DISCH_THEN(ASSUME_TAC o GSYM) THEN
SUBGOAL_THEN
`!h:real^N->real^N.
orthogonal_transformation (g o h o (f:real^N->real^N)) <=>
orthogonal_transformation h`
(fun th -> REWRITE_TAC[th; ETA_AX])
THENL
[GEN_TAC THEN EQ_TAC THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE] THEN
DISCH_TAC THEN
SUBGOAL_THEN `h:real^N->real^N = f o (g o h o f) o (g:real^N->real^N)`
SUBST1_TAC THENL
[ALL_TAC; ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE]] THEN
ASM_REWRITE_TAC[o_ASSOC] THEN ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID];
ALL_TAC] THEN
SUBGOAL_THEN
`(f:real^N->real^N) o (reflect_along a o reflect_along b) o g =
reflect_along (f a) o reflect_along (f b)`
SUBST1_TAC THENL
[RULE_ASSUM_TAC(REWRITE_RULE[FUN_EQ_THM; o_THM; I_THM]) THEN
ASM_REWRITE_TAC[o_DEF];
MATCH_MP_TAC lemma2 THEN RULE_ASSUM_TAC
(REWRITE_RULE[GSYM NORM_EQ_0; ORTHOGONAL_TRANSFORMATION]) THEN
ASM_REWRITE_TAC[GSYM NORM_EQ_0] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ_ALT]
SUBSET_TRANS)) THEN
ASM_SIMP_TAC[GSYM SPAN_LINEAR_IMAGE; IMAGE_CLAUSES] THEN
REWRITE_TAC[SPAN_INC]]) in
GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MP_TAC(ISPECL [`f:real^N->real^N`; `dimindex(:N)`]
ORTHOGONAL_TRANSFORMATION_GENERATED_BY_REFLECTIONS) THEN
ASM_REWRITE_TAC[ARITH_RULE `n:num <= a + n`] THEN
DISCH_THEN(X_CHOOSE_THEN `l:(real^N)list` STRIP_ASSUME_TAC) THEN
UNDISCH_TAC `ALL (\v:real^N. ~(v = vec 0)) l` THEN
UNDISCH_TAC `orthogonal_transformation(f:real^N->real^N)` THEN
MATCH_MP_TAC(TAUT `r /\ (p /\ q ==> s) ==> r ==> p ==> q ==> s`) THEN
ASM_REWRITE_TAC[IMP_IMP] THEN
SPEC_TAC(`l:(real^N)list`,`l:(real^N)list`) THEN
POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN
WF_INDUCT_TAC `LENGTH(l:(real^N)list)` THEN POP_ASSUM MP_TAC THEN
SPEC_TAC(`l:(real^N)list`,`l:(real^N)list`) THEN
MATCH_MP_TAC list_INDUCT THEN
REWRITE_TAC[ALL; ITLIST; HOMOTOPIC_WITH_REFL] THEN
REWRITE_TAC[REWRITE_RULE[GSYM I_DEF] CONTINUOUS_ON_ID;
ORTHOGONAL_TRANSFORMATION_I; SUBSET_UNIV] THEN
X_GEN_TAC `a:real^N` THEN MATCH_MP_TAC list_INDUCT THEN
REWRITE_TAC[ALL; ITLIST; I_O_ID; DET_MATRIX_REFLECT_ALONG] THEN
REWRITE_TAC[ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG] THEN
CONJ_TAC THENL [MESON_TAC[REAL_ARITH `~(-- &1 = &1)`]; ALL_TAC] THEN
MAP_EVERY X_GEN_TAC [`b:real^N`; `l:(real^N)list`] THEN
REPLICATE_TAC 2 (DISCH_THEN(K ALL_TAC)) THEN
DISCH_THEN(MP_TAC o SPEC `l:(real^N)list`) THEN
REWRITE_TAC[LENGTH; ARITH_RULE `n < SUC(SUC n)`] THEN
SIMP_TAC[LINEAR_COMPOSE; LINEAR_REFLECT_ALONG; MATRIX_COMPOSE;
ORTHGOONAL_TRANSFORMATION_REFLECT_ALONG;
ORTHOGONAL_TRANSFORMATION_COMPOSE; ORTHOGONAL_TRANSFORMATION_LINEAR] THEN
DISCH_THEN(fun th ->
DISCH_THEN(CONJUNCTS_THEN2 STRIP_ASSUME_TAC MP_TAC) THEN MP_TAC th) THEN
ASM_SIMP_TAC[DET_MUL; DET_MATRIX_REFLECT_ALONG; REAL_ARITH
`-- &1 * -- &1 * x = x`] THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
DISCH_THEN(fun th -> DISCH_TAC THEN MP_TAC th) THEN
ASM_REWRITE_TAC[] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] HOMOTOPIC_WITH_TRANS) THEN
GEN_REWRITE_TAC RAND_CONV [MESON[I_O_ID] `f = I o f`] THEN
REWRITE_TAC[o_ASSOC] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_RIGHT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[LINEAR_CONTINUOUS_ON; ORTHOGONAL_TRANSFORMATION_LINEAR] THEN
ABBREV_TAC `g = ITLIST (\v:real^N h. reflect_along v o h) l I` THEN
SUBGOAL_THEN
`(\f:real^N->real^N.
orthogonal_transformation (f o g)) = orthogonal_transformation`
SUBST1_TAC THENL [ALL_TAC; MATCH_MP_TAC lemma3 THEN ASM_REWRITE_TAC[]] THEN
REWRITE_TAC[FUN_EQ_THM] THEN X_GEN_TAC `f:real^N->real^N` THEN
EQ_TAC THEN ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE] THEN
DISCH_TAC THEN
MP_TAC(ISPEC `g:real^N->real^N` ORTHOGONAL_TRANSFORMATION_INVERSE_o) THEN
ASM_REWRITE_TAC[LEFT_IMP_EXISTS_THM] THEN X_GEN_TAC `h:real^N->real^N` THEN
STRIP_TAC THEN
SUBGOAL_THEN `f = ((f:real^N->real^N) o (g:real^N->real^N)) o h`
SUBST1_TAC THENL
[ASM_REWRITE_TAC[GSYM o_ASSOC; I_O_ID];
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE]]);;
let HOMOTOPIC_SPECIAL_ORTHOGONAL_TRANSFORMATIONS,
HOMOTOPIC_ORTHOGONAL_TRANSFORMATIONS = (CONJ_PAIR o prove)
(`(!f g. homotopic_with
(\h. orthogonal_transformation h /\ det(matrix h) = det(matrix f))
((:real^N),(:real^N)) f g <=>
homotopic_with
orthogonal_transformation ((:real^N),(:real^N)) f g) /\
!f g. homotopic_with orthogonal_transformation ((:real^N),(:real^N)) f g <=>
orthogonal_transformation f /\ orthogonal_transformation g /\
det(matrix f) = det(matrix g)`,
REWRITE_TAC[AND_FORALL_THM] THEN REPEAT GEN_TAC THEN MATCH_MP_TAC(TAUT
`(u ==> s) /\ (s ==> t) /\ (t ==> u)
==> (u <=> t) /\ (t <=> s)`) THEN
REPEAT CONJ_TAC THENL
[DISCH_THEN(MP_TAC o MATCH_MP HOMOTOPIC_WITH_IMP_PROPERTY) THEN MESON_TAC[];
STRIP_TAC THEN
MP_TAC(ISPEC `g:real^N->real^N` ORTHOGONAL_TRANSFORMATION_INVERSE_o) THEN
ASM_REWRITE_TAC[] THEN
DISCH_THEN(X_CHOOSE_THEN `h:real^N->real^N` STRIP_ASSUME_TAC) THEN
SUBGOAL_THEN
`(f:real^N->real^N) = g o (h:real^N->real^N) o f /\ g = g o I`
(fun th -> ONCE_REWRITE_TAC[th])
THENL [ASM_REWRITE_TAC[o_ASSOC; I_O_ID]; ALL_TAC] THEN
MATCH_MP_TAC HOMOTOPIC_WITH_COMPOSE_CONTINUOUS_LEFT THEN
EXISTS_TAC `(:real^N)` THEN REWRITE_TAC[SUBSET_UNIV] THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_LINEAR; LINEAR_CONTINUOUS_ON] THEN
SUBGOAL_THEN
`!k:real^N->real^N.
orthogonal_transformation (g o k) <=> orthogonal_transformation k`
(fun th -> REWRITE_TAC[th; ETA_AX])
THENL
[GEN_TAC THEN EQ_TAC THEN
ASM_SIMP_TAC[ORTHOGONAL_TRANSFORMATION_COMPOSE] THEN DISCH_THEN
(MP_TAC o SPEC `h:real^N->real^N` o MATCH_MP (ONCE_REWRITE_RULE
[IMP_CONJ_ALT] ORTHOGONAL_TRANSFORMATION_COMPOSE)) THEN
ASM_SIMP_TAC[o_ASSOC; I_O_ID];
MATCH_MP_TAC NULLHOMOTOPIC_ORTHOGONAL_TRANSFORMATION THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o AP_TERM
`\f:real^N->real^N. det(matrix f)`)) THEN
ASM_SIMP_TAC[MATRIX_COMPOSE; ORTHOGONAL_TRANSFORMATION_LINEAR;
ORTHOGONAL_TRANSFORMATION_COMPOSE; DET_MUL;
MATRIX_I; DET_I]];
REWRITE_TAC[homotopic_with] THEN MATCH_MP_TAC MONO_EXISTS THEN
X_GEN_TAC `k:real^(1,N)finite_sum->real^N` THEN
STRIP_TAC THEN ASM_SIMP_TAC[] THEN MP_TAC(ISPECL
[`\t. lift(
det(matrix((k:real^(1,N)finite_sum->real^N) o pastecart t)))`;
`interval[vec 0:real^1,vec 1]`]
CONTINUOUS_DISCRETE_RANGE_CONSTANT) THEN
REWRITE_TAC[CONNECTED_INTERVAL] THEN ANTS_TAC THENL
[CONJ_TAC THENL
[MATCH_MP_TAC CONTINUOUS_ON_LIFT_DET THEN
SIMP_TAC[matrix; LAMBDA_BETA; o_DEF] THEN
MAP_EVERY X_GEN_TAC [`i:num`; `j:num`] THEN STRIP_TAC THEN
MATCH_MP_TAC CONTINUOUS_ON_LIFT_COMPONENT_COMPOSE THEN
ASM_REWRITE_TAC[] THEN GEN_REWRITE_TAC LAND_CONV [GSYM o_DEF] THEN
MATCH_MP_TAC CONTINUOUS_ON_COMPOSE THEN
SIMP_TAC[CONTINUOUS_ON_PASTECART; CONTINUOUS_ON_CONST;
CONTINUOUS_ON_ID] THEN
FIRST_X_ASSUM(MATCH_MP_TAC o MATCH_MP (REWRITE_RULE[IMP_CONJ]
CONTINUOUS_ON_SUBSET)) THEN
SIMP_TAC[SUBSET; FORALL_IN_IMAGE; PASTECART_IN_PCROSS; IN_UNIV];
X_GEN_TAC `t:real^1` THEN DISCH_TAC THEN EXISTS_TAC `&1` THEN
REWRITE_TAC[REAL_LT_01] THEN X_GEN_TAC `u:real^1` THEN
DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
REWRITE_TAC[GSYM LIFT_SUB; NORM_LIFT; LIFT_EQ] THEN
SUBGOAL_THEN
`orthogonal_transformation
((k:real^(1,N)finite_sum->real^N) o pastecart t) /\
orthogonal_transformation (k o pastecart u)`
MP_TAC THENL [ASM_SIMP_TAC[o_DEF]; ALL_TAC] THEN
DISCH_THEN(CONJUNCTS_THEN
(STRIP_ASSUME_TAC o MATCH_MP DET_ORTHOGONAL_MATRIX o
MATCH_MP ORTHOGONAL_MATRIX_MATRIX)) THEN
ASM_REWRITE_TAC[] THEN CONV_TAC REAL_RAT_REDUCE_CONV];
REWRITE_TAC[o_DEF; LEFT_IMP_EXISTS_THM] THEN
X_GEN_TAC `a:real^1` THEN DISCH_TAC THEN
REPEAT(FIRST_X_ASSUM(MP_TAC o GEN_REWRITE_RULE I [GSYM FUN_EQ_THM])) THEN
REPEAT(DISCH_THEN(SUBST1_TAC o SYM)) THEN
ASM_SIMP_TAC[ENDS_IN_UNIT_INTERVAL; GSYM LIFT_EQ]]]);;
(* ------------------------------------------------------------------------- *)
(* Complex tangent function. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Analytic properties of tangent function. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CTAN)));;
(* ------------------------------------------------------------------------- *)
(* Real tangent function. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Monotonicity theorems for the basic trig functions. *)
(* ------------------------------------------------------------------------- *)
let TAN_BOUND_PI2 = prove
(`!x. abs(x) <
pi / &4 ==> abs(
tan x) < &1`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM
TAN_PI4] THEN
REWRITE_TAC[GSYM
TAN_NEG; REAL_ARITH `abs(x) < a <=> --a < x /\ x < a`] THEN
CONJ_TAC THEN MATCH_MP_TAC
TAN_MONO_LT THEN
POP_ASSUM MP_TAC THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Approximation to pi. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Complex logarithms (the conventional principal value). *)
(* ------------------------------------------------------------------------- *)
let clog = new_definition
`clog z = @w. cexp(w) = z /\ --pi < Im(w) /\ Im(w) <= pi`;;
(* ------------------------------------------------------------------------- *)
(* Derivative of clog away from the branch cut. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CLOG)));;
(* ------------------------------------------------------------------------- *)
(* Relation to real log. *)
(* ------------------------------------------------------------------------- *)
let CX_LOG = prove
(`!z. &0 < z ==> Cx(log z) =
clog(Cx z)`,
REPEAT STRIP_TAC THEN FIRST_ASSUM(fun
th ->
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV)
[SYM(MATCH_MP
EXP_LOG th)]) THEN
REWRITE_TAC[
CX_EXP] THEN CONV_TAC SYM_CONV THEN
MATCH_MP_TAC
CLOG_CEXP THEN REWRITE_TAC[
IM_CX] THEN
MP_TAC
PI_POS THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Quadrant-type results for clog. *)
(* ------------------------------------------------------------------------- *)
let RE_CLOG_POS_LT = prove
(`!z. ~(z = Cx(&0)) ==> (abs(Im(
clog z)) <
pi / &2 <=> &0 < Re(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun
th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM
th])
MP_TAC) THEN
SIMP_TAC[
RE_CEXP;
REAL_LT_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`
clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> --(p / &2) < x /\ x < p / &2 \/
--(p / &2) <= p + x /\ p + x <= p / &2 \/
--(p / &2) <= x - p /\ x - p <= p / &2`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
COS_ADD;
COS_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let RE_CLOG_POS_LE = prove
(`!z. ~(z = Cx(&0)) ==> (abs(Im(
clog z)) <=
pi / &2 <=> &0 <= Re(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun
th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM
th])
MP_TAC) THEN
SIMP_TAC[
RE_CEXP;
REAL_LE_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`
clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> --(p / &2) <= x /\ x <= p / &2 \/
--(p / &2) < p + x /\ p + x < p / &2 \/
--(p / &2) < x - p /\ x - p < p / &2`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
COS_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
COS_ADD;
COS_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let IM_CLOG_POS_LT = prove
(`!z. ~(z = Cx(&0)) ==> (&0 < Im(
clog z) /\ Im(
clog z) <
pi <=> &0 < Im(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun
th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM
th])
MP_TAC) THEN
SIMP_TAC[
IM_CEXP;
REAL_LT_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`
clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> &0 < x /\ x < p \/
&0 <= x + p /\ x + p <= p \/
&0 <= x - p /\ x - p <= p`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
SIN_ADD;
SIN_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
let IM_CLOG_POS_LE = prove
(`!z. ~(z = Cx(&0)) ==> (&0 <= Im(
clog z) <=> &0 <= Im(z))`,
GEN_TAC THEN DISCH_THEN(MP_TAC o MATCH_MP
CLOG_WORKS) THEN
DISCH_THEN(CONJUNCTS_THEN2
(fun
th -> GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [SYM
th])
MP_TAC) THEN
SIMP_TAC[
IM_CEXP;
REAL_LE_MUL_EQ;
REAL_EXP_POS_LT] THEN
SPEC_TAC(`
clog z`,`z:complex`) THEN GEN_TAC THEN
DISCH_THEN(MP_TAC o MATCH_MP (REAL_ARITH
`--p < x /\ x <= p
==> &0 <= x /\ x <= p \/
&0 < x + p /\ x + p < p \/
&0 < p - x /\ p - x < p`)) THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC) THEN
(FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI) ORELSE
FIRST_ASSUM(MP_TAC o MATCH_MP
SIN_POS_PI_LE)) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
REWRITE_TAC[
SIN_ADD;
SIN_SUB;
COS_PI;
SIN_PI] THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Various properties. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation between square root and exp/log, and hence its derivative. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CSQRT)));;
(* ------------------------------------------------------------------------- *)
(* Complex powers. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("cpow",(24,"left"));;
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(GEN `s:complex`
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
(SPEC `s:complex` HAS_COMPLEX_DERIVATIVE_CPOW)))));;
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(GEN `s:complex`
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
(SPEC `s:complex` HAS_COMPLEX_DERIVATIVE_CPOW_RIGHT)))));;
(* ------------------------------------------------------------------------- *)
(* Product rule. *)
(* ------------------------------------------------------------------------- *)
let CLOG_NEG = prove
(`!z. ~(z = Cx(&0))
==>
clog(--z) = if Im(z) <= &0 /\ ~(Re(z) < &0 /\ Im(z) = &0)
then
clog(z) +
ii * Cx(
pi)
else
clog(z) -
ii * Cx(
pi)`,
REPEAT STRIP_TAC THEN
SUBST1_TAC(SIMPLE_COMPLEX_ARITH `--z = --Cx(&1) * z`) THEN
ASM_SIMP_TAC[
CLOG_MUL; COMPLEX_RING `~(--Cx(&1) = Cx(&0))`] THEN
REWRITE_TAC[
CLOG_NEG_1;
IM_ADD;
IM_MUL_II;
RE_CX] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH
`--p < x /\ x <= p ==> ~(p + x <= --p)`] THEN
REWRITE_TAC[REAL_ARITH `p + x > p <=> &0 < x`] THEN
ASM_SIMP_TAC[GSYM
IM_CLOG_EQ_PI] THEN
ONCE_REWRITE_TAC[REAL_ARITH `Im z <= &0 <=> ~(&0 < Im z)`] THEN
ASM_SIMP_TAC[GSYM
IM_CLOG_POS_LT] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH `x <= p ==> (x < p <=> ~(x = p))`] THEN
REWRITE_TAC[TAUT `~(a /\ ~b) /\ ~b <=> ~a /\ ~b`] THEN
ASM_CASES_TAC `Im(
clog z) =
pi` THEN ASM_REWRITE_TAC[
PI_POS] THEN
ASM_CASES_TAC `&0 < Im(
clog z)` THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[
CX_MUL] THEN CONV_TAC COMPLEX_RING);;
let CLOG_MUL_II = prove
(`!z. ~(z = Cx(&0))
==>
clog(
ii * z) = if &0 <= Re(z) \/ Im(z) < &0
then
clog(z) +
ii * Cx(
pi / &2)
else
clog(z) -
ii * Cx(&3 *
pi / &2)`,
REPEAT STRIP_TAC THEN ASM_SIMP_TAC[
CLOG_MUL;
II_NZ;
CLOG_II] THEN
REWRITE_TAC[
IM_ADD;
IM_MUL_II;
RE_CX] THEN
ASM_SIMP_TAC[
CLOG_WORKS; REAL_ARITH
`--p < x /\ x <= p ==> ~(p / &2 + x <= --p)`] THEN
REWRITE_TAC[REAL_ARITH `p / &2 + x > p <=> p / &2 < x`] THEN
REWRITE_TAC[REAL_ARITH `Im z < &0 <=> ~(&0 <= Im z)`] THEN
ASM_SIMP_TAC[GSYM
RE_CLOG_POS_LE; GSYM
IM_CLOG_POS_LE] THEN
MATCH_MP_TAC(MESON[]
`(p <=> ~q) /\ x = a /\ y = b
==> ((if p then x else y) = (if q then b else a))`) THEN
CONJ_TAC THENL
[MP_TAC
PI_POS THEN REAL_ARITH_TAC;
REWRITE_TAC[
CX_MUL;
CX_DIV] THEN CONV_TAC COMPLEX_RING]);;
(* ------------------------------------------------------------------------- *)
(* Unwinding number gives another version of log-product formula. *)
(* Note that in this special case the unwinding number is -1, 0 or 1. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Complex arctangent (branch cut gives standard bounds in real case). *)
(* ------------------------------------------------------------------------- *)
let CTAN_CATN = prove
(`!z. ~(z pow 2 = --Cx(&1)) ==>
ctan(
catn z) = z`,
REPEAT STRIP_TAC THEN
REWRITE_TAC[
catn;
ctan;
csin;
ccos;
COMPLEX_RING `--i * i / Cx(&2) * z = --(i * i) / Cx(&2) * z`;
COMPLEX_RING `i * i / Cx(&2) * z = (i * i) / Cx(&2) * z`] THEN
REWRITE_TAC[
COMPLEX_POW_II_2; GSYM
COMPLEX_POW_2] THEN
REWRITE_TAC[COMPLEX_RING `--Cx(&1) / Cx(&2) * x = --(Cx(&1) / Cx(&2) * x)`;
CEXP_NEG] THEN
SUBGOAL_THEN
`~(
cexp(Cx(&1) / Cx(&2) *
(
clog((Cx(&1) -
ii * z) / (Cx(&1) +
ii * z)))) pow 2 = --Cx(&1))`
ASSUME_TAC THENL
[REWRITE_TAC[GSYM
CEXP_N;
CEXP_SUB; COMPLEX_RING
`Cx(&2) * Cx(&1) / Cx(&2) * z = z`] THEN
ASM_SIMP_TAC[
CEXP_CLOG;
COMPLEX_POW_II_2;
COMPLEX_FIELD `~(w = Cx(&0)) /\ ~(z = Cx(&0)) ==> ~(w / z = Cx(&0))`;
COMPLEX_FIELD `~(w = Cx(&0)) ==> (x / w = y <=> x = y * w)`;
COMPLEX_FIELD
`
ii pow 2 = --Cx(&1) /\ ~(z pow 2 = --Cx(&1))
==> ~(Cx(&1) -
ii * z = Cx(&0)) /\ ~(Cx(&1) +
ii * z = Cx(&0))`] THEN
POP_ASSUM MP_TAC THEN CONV_TAC COMPLEX_FIELD;
ALL_TAC] THEN
REWRITE_TAC[COMPLEX_RING `-- --Cx (&1) / Cx (&2) = Cx(&1) / Cx(&2)`] THEN
ASM_SIMP_TAC[
CEXP_NZ; COMPLEX_FIELD
`~(z = Cx(&0)) /\ ~(z pow 2 = --Cx(&1))
==> ((inv(z) - z) / (Cx(&2) *
ii)) / ((inv(z) + z) / Cx(&2)) =
inv
ii * ((Cx(&1) - z pow 2) / (Cx(&1) + z pow 2))`] THEN
ASM_SIMP_TAC[GSYM
CEXP_N;
CEXP_SUB;
COMPLEX_RING `Cx(&2) * Cx(&1) / Cx(&2) * z = z`] THEN
ASM_SIMP_TAC[
CEXP_CLOG; COMPLEX_FIELD
`~(z pow 2 = --Cx(&1))
==> ~((Cx(&1) -
ii * z) / (Cx(&1) +
ii * z) = Cx(&0))`] THEN
UNDISCH_TAC `~(z pow 2 = --Cx(&1))` THEN CONV_TAC COMPLEX_FIELD);;
let RE_CATN_BOUNDS = prove
(`!z. (Re z = &0 ==> abs(Im z) < &1) ==> abs(Re(
catn z)) <
pi / &2`,
REWRITE_TAC[
catn;
complex_div; GSYM
CX_INV; GSYM
COMPLEX_MUL_ASSOC] THEN
REPEAT STRIP_TAC THEN REWRITE_TAC[
RE_MUL_II;
IM_MUL_CX] THEN
MATCH_MP_TAC(REAL_ARITH `abs x < p ==> abs(--(inv(&2) * x)) < p / &2`) THEN
MATCH_MP_TAC(REAL_ARITH `(--p < x /\ x <= p) /\ ~(x = p) ==> abs x < p`) THEN
SUBGOAL_THEN `~(z =
ii) /\ ~(z = --ii)` STRIP_ASSUME_TAC THENL
[CONJ_TAC THEN
DISCH_THEN(fun
th -> POP_ASSUM MP_TAC THEN SUBST1_TAC
th) THEN
REWRITE_TAC[
RE_II;
IM_II;
RE_NEG;
IM_NEG] THEN REAL_ARITH_TAC;
ALL_TAC] THEN
REWRITE_TAC[GSYM
complex_div] THEN CONJ_TAC THENL
[SUBGOAL_THEN `~((Cx(&1) -
ii * z) / (Cx(&1) +
ii * z) = Cx(&0))`
(fun
th -> MESON_TAC[
th;
CLOG_WORKS]) THEN
REPEAT(POP_ASSUM MP_TAC) THEN CONV_TAC COMPLEX_FIELD;
ALL_TAC] THEN
DISCH_TAC THEN
MP_TAC(ISPEC `
clog((Cx(&1) -
ii * z) / (Cx(&1) +
ii * z))`
EULER) THEN
ASM_REWRITE_TAC[
SIN_PI;
COS_PI;
CX_NEG] THEN
REWRITE_TAC[COMPLEX_RING
`x = y * (--Cx(&1) + z * Cx(&0)) <=> x + y = Cx(&0)`] THEN
REWRITE_TAC[
CX_EXP] THEN
ASM_SIMP_TAC[
CEXP_CLOG; COMPLEX_FIELD
`~(z =
ii) /\ ~(z = --ii)
==> ~((Cx(&1) -
ii * z) / (Cx(&1) +
ii * z) = Cx(&0))`] THEN
REWRITE_TAC[GSYM
CX_EXP] THEN DISCH_THEN(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[
IM_ADD;
IM_CX;
REAL_ADD_RID;
IM_COMPLEX_DIV_LEMMA] THEN
DISCH_TAC THEN UNDISCH_TAC `Re z = &0 ==> abs (Im z) < &1` THEN
ASM_REWRITE_TAC[] THEN DISCH_TAC THEN
SUBGOAL_THEN `
ii * z = --Cx(Im z)` SUBST_ALL_TAC THENL
[ASM_REWRITE_TAC[
COMPLEX_EQ;
RE_NEG;
IM_NEG;
RE_MUL_II;
IM_MUL_II;
RE_CX;
IM_CX;
REAL_NEG_0];
ALL_TAC] THEN
UNDISCH_TAC
`Im(
clog((Cx(&1) - --Cx(Im z)) / (Cx(&1) + --Cx(Im z)))) =
pi` THEN
REWRITE_TAC[
COMPLEX_SUB_RNEG; GSYM
complex_sub] THEN
REWRITE_TAC[GSYM
CX_ADD; GSYM
CX_SUB; GSYM
CX_DIV] THEN
SUBGOAL_THEN `&0 < (&1 + Im z) / (&1 - Im z)` ASSUME_TAC THENL
[MATCH_MP_TAC
REAL_LT_DIV THEN ASM_REAL_ARITH_TAC;
ASM_SIMP_TAC[GSYM
CX_LOG;
IM_CX;
PI_NZ]]);;
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CATN)));;
(* ------------------------------------------------------------------------- *)
(* Real arctangent. *)
(* ------------------------------------------------------------------------- *)
let ATN_TAN = prove
(`!y.
tan(
atn y) = y`,
GEN_TAC THEN REWRITE_TAC[
tan_def;
atn] THEN
MATCH_MP_TAC
EQ_TRANS THEN EXISTS_TAC `Re(
ctan(
catn(Cx y)))` THEN
CONJ_TAC THENL [REWRITE_TAC[GSYM
CX_ATN;
RE_CX]; ALL_TAC] THEN
GEN_REWRITE_TAC RAND_CONV [GSYM
RE_CX] THEN AP_TERM_TAC THEN
MATCH_MP_TAC
CTAN_CATN THEN MATCH_MP_TAC(COMPLEX_RING
`~(z =
ii) /\ ~(z = --ii) ==> ~(z pow 2 = --Cx(&1))`) THEN
CONJ_TAC THEN DISCH_THEN(MP_TAC o AP_TERM `Im`) THEN
REWRITE_TAC[
IM_II;
IM_CX;
IM_NEG] THEN REAL_ARITH_TAC);;
let ATN_LT_PI4 = prove
(`!x. abs(x) < &1 ==> abs(
atn x) <
pi / &4`,
GEN_TAC THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 < x ==> &0 < y) /\
(x < &0 ==> y < &0) /\
((x = &0) ==> (y = &0)) /\
(x < a ==> y < b) /\
(--a < x ==> --b < y)
==> abs(x) < a ==> abs(y) < b`) THEN
SIMP_TAC[
ATN_LT_PI4_POS;
ATN_LT_PI4_NEG;
ATN_0] THEN CONJ_TAC THEN
GEN_REWRITE_TAC (RAND_CONV o ONCE_DEPTH_CONV) [GSYM
ATN_0] THEN
SIMP_TAC[
ATN_MONO_LT]);;
(* ------------------------------------------------------------------------- *)
(* Some bound theorems where a bit of simple calculus is handy. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Probably not very useful, but for compatibility with old analysis theory. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some slightly ad hoc lemmas useful here. *)
(* ------------------------------------------------------------------------- *)
let ABS_SQUARE_EQ_1 = prove
(`!x. x pow 2 = &1 <=> abs(x) = &1`,
REWRITE_TAC[REAL_RING `x pow 2 = &1 <=> x = &1 \/ x = -- &1`] THEN
REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Inverse sine. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CASN)));;
(* ------------------------------------------------------------------------- *)
(* Inverse cosine. *)
(* ------------------------------------------------------------------------- *)
add_complex_differentiation_theorems
(CONJUNCTS(REWRITE_RULE[FORALL_AND_THM]
(MATCH_MP HAS_COMPLEX_DERIVATIVE_CHAIN
HAS_COMPLEX_DERIVATIVE_CACS)));;
(* ------------------------------------------------------------------------- *)
(* Some crude range theorems (could be sharpened). *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Interrelations between the two functions. *)
(* ------------------------------------------------------------------------- *)
let CCOS_CASN_NZ = prove
(`!z. ~(z pow 2 = Cx(&1)) ==> ~(
ccos(
casn z) = Cx(&0))`,
REWRITE_TAC[
ccos;
casn;
CEXP_NEG; COMPLEX_RING `
ii * --ii * z = z`;
COMPLEX_RING `--ii * --ii * z = --z`] THEN
SIMP_TAC[
CEXP_CLOG;
CASN_BODY_LEMMA;
COMPLEX_FIELD `~(x = Cx(&0))
==> ((x + inv(x)) / Cx(&2) = Cx(&0) <=>
x pow 2 = --Cx(&1))`] THEN
SIMP_TAC[
CSQRT; COMPLEX_FIELD
`s pow 2 = Cx(&1) - z pow 2
==> ((
ii * z + s) pow 2 = --Cx(&1) <=>
ii * s * z = Cx(&1) - z pow 2)`] THEN
GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC(COMPLEX_RING
`~(x pow 2 + y pow 2 = Cx(&0)) ==> ~(
ii * x = y)`) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN CONV_TAC COMPLEX_RING);;
let CSIN_CACS_NZ = prove
(`!z. ~(z pow 2 = Cx(&1)) ==> ~(
csin(
cacs z) = Cx(&0))`,
REWRITE_TAC[
csin;
cacs;
CEXP_NEG; COMPLEX_RING `
ii * --ii * z = z`;
COMPLEX_RING `--ii * --ii * z = --z`] THEN
SIMP_TAC[
CEXP_CLOG;
CACS_BODY_LEMMA;
COMPLEX_FIELD `~(x = Cx(&0))
==> ((x - inv(x)) / (Cx(&2) *
ii) = Cx(&0) <=>
x pow 2 = Cx(&1))`] THEN
SIMP_TAC[
CSQRT; COMPLEX_FIELD
`s pow 2 = Cx(&1) - z pow 2
==> ((z +
ii * s) pow 2 = Cx(&1) <=>
ii * s * z = Cx(&1) - z pow 2)`] THEN
GEN_TAC THEN STRIP_TAC THEN
MATCH_MP_TAC(COMPLEX_RING
`~(x pow 2 + y pow 2 = Cx(&0)) ==> ~(
ii * x = y)`) THEN
REPEAT(POP_ASSUM MP_TAC) THEN
MP_TAC(SPEC `Cx(&1) - z pow 2`
CSQRT) THEN CONV_TAC COMPLEX_RING);;
let CASN_CACS_SQRT_POS = prove
(`!z. (&0 < Re z \/ Re z = &0 /\ &0 <= Im z)
==>
casn(z) =
cacs(
csqrt(Cx(&1) - z pow 2))`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
casn;
cacs] THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(COMPLEX_RING `w = z ==>
ii * z + s = s +
ii * w`) THEN
MATCH_MP_TAC
CSQRT_UNIQUE THEN
ASM_REWRITE_TAC[
CSQRT] THEN CONV_TAC COMPLEX_RING);;
let CACS_CASN_SQRT_POS = prove
(`!z. (&0 < Re z \/ Re z = &0 /\ &0 <= Im z)
==>
cacs(z) =
casn(
csqrt(Cx(&1) - z pow 2))`,
GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[
casn;
cacs] THEN
AP_TERM_TAC THEN AP_TERM_TAC THEN
MATCH_MP_TAC(COMPLEX_RING `w = z ==> z +
ii * s =
ii * s + w`) THEN
MATCH_MP_TAC
CSQRT_UNIQUE THEN
ASM_REWRITE_TAC[
CSQRT] THEN CONV_TAC COMPLEX_RING);;
(* ------------------------------------------------------------------------- *)
(* Real arcsin. *)
(* ------------------------------------------------------------------------- *)
let ASN_NEG = prove
(`!x. -- &1 <= x /\ x <= &1 ==>
asn(--x) = --asn(x)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(fun
th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
[GSYM(MATCH_MP
SIN_ASN th)]) THEN
REWRITE_TAC[GSYM
SIN_NEG] THEN MATCH_MP_TAC
ASN_SIN THEN
REWRITE_TAC[REAL_ARITH `--a <= --x /\ --x <= a <=> --a <= x /\ x <= a`] THEN
ASM_SIMP_TAC[
ASN_BOUNDS]);;
let COS_ASN_NZ = prove
(`!x. --(&1) < x /\ x < &1 ==> ~(
cos(
asn(x)) = &0)`,
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ASN;
CX_COS;
REAL_ARITH `--(&1) < x /\ x < &1 ==> abs(x) <= &1`] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
CCOS_CASN_NZ THEN
SIMP_TAC[COMPLEX_RING `x pow 2 = Cx(&1) <=> x = Cx(&1) \/ x = --Cx(&1)`] THEN
REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Real arccosine. *)
(* ------------------------------------------------------------------------- *)
let ACS_NEG = prove
(`!x. -- &1 <= x /\ x <= &1 ==>
acs(--x) =
pi -
acs(x)`,
GEN_TAC THEN DISCH_TAC THEN
FIRST_ASSUM(fun
th -> GEN_REWRITE_TAC (LAND_CONV o RAND_CONV o RAND_CONV)
[GSYM(MATCH_MP
COS_ACS th)]) THEN
ONCE_REWRITE_TAC[GSYM
COS_NEG] THEN REWRITE_TAC[GSYM
COS_PERIODIC_PI] THEN
REWRITE_TAC[REAL_ARITH `--x + y:real = y - x`] THEN MATCH_MP_TAC
ACS_COS THEN
SIMP_TAC[REAL_ARITH `&0 <= p - x /\ p - x <= p <=> &0 <= x /\ x <= p`] THEN
ASM_SIMP_TAC[
ACS_BOUNDS]);;
let SIN_ACS_NZ = prove
(`!x. --(&1) < x /\ x < &1 ==> ~(
sin(
acs(x)) = &0)`,
ONCE_REWRITE_TAC[GSYM
CX_INJ] THEN SIMP_TAC[
CX_ACS;
CX_SIN;
REAL_ARITH `--(&1) < x /\ x < &1 ==> abs(x) <= &1`] THEN
GEN_TAC THEN STRIP_TAC THEN MATCH_MP_TAC
CSIN_CACS_NZ THEN
SIMP_TAC[COMPLEX_RING `x pow 2 = Cx(&1) <=> x = Cx(&1) \/ x = --Cx(&1)`] THEN
REWRITE_TAC[GSYM
CX_NEG;
CX_INJ] THEN
ASM_REAL_ARITH_TAC);;
let ACS_INJ = prove
(`!x y. abs(x) <= &1 /\ abs(y) <= &1 ==> (
acs x =
acs y <=> x = y)`,
REPEAT STRIP_TAC THEN REWRITE_TAC[GSYM REAL_LE_ANTISYM] THEN
ASM_SIMP_TAC[
ACS_MONO_LE_EQ] THEN REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* Some interrelationships among the real inverse trig functions. *)
(* ------------------------------------------------------------------------- *)
let ASN_ACS_SQRT_NEG = prove
(`!x. -- &1 <= x /\ x <= &0 ==>
asn(x) = --acs(
sqrt(&1 - x pow 2))`,
REPEAT STRIP_TAC THEN
ONCE_REWRITE_TAC[REAL_ARITH `x = --y <=> (--x:real) = y`] THEN
ASM_SIMP_TAC[GSYM
ASN_NEG; REAL_ARITH `x <= &0 ==> x <= &1`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `(x:real) pow 2 = (--x) pow 2`] THEN
MATCH_MP_TAC
ASN_ACS_SQRT_POS THEN ASM_REAL_ARITH_TAC);;
(* ------------------------------------------------------------------------- *)
(* More delicate continuity results for arcsin and arccos. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Some limits, most involving sequences of transcendentals. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Roots of unity. *)
(* ------------------------------------------------------------------------- *)
let COMPLEX_ROOT_POLYFUN = prove
(`!n z a.
1 <= n
==> (z pow n = a <=>
vsum(0..n) (\i. (if i = 0 then --a else if i = n then Cx(&1)
else Cx(&0)) * z pow i) = Cx(&0))`,
(* ------------------------------------------------------------------------- *)
(* Relation between clog and Arg, and hence continuity of Arg. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Relation between Arg and arctangent in upper halfplane. *)
(* ------------------------------------------------------------------------- *)
(* ------------------------------------------------------------------------- *)
(* Real n'th roots. *)
(* ------------------------------------------------------------------------- *)
let root = new_definition
`root(n) x = @u:real. (&0 <= x ==> &0 <= u) /\ u pow n = x`;;
let ROOT_WORKS = prove
(`!n x.
ODD n \/ ~(n = 0) /\ &0 <= x
==> (&0 <= x ==> &0 <=
root n x) /\ (
root n x) pow n = x`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `n = 0` THEN ASM_REWRITE_TAC[ARITH] THEN DISCH_TAC THEN
REWRITE_TAC[
root] THEN CONV_TAC SELECT_CONV THEN
REPEAT_TCL DISJ_CASES_THEN ASSUME_TAC
(REAL_ARITH `x = &0 \/ &0 < x \/ &0 < --x`)
THENL
[EXISTS_TAC `&0` THEN ASM_REWRITE_TAC[
REAL_POW_ZERO];
EXISTS_TAC `
exp(log x / &n)` THEN REWRITE_TAC[
REAL_EXP_POS_LE] THEN
ASM_SIMP_TAC[GSYM
REAL_EXP_N;
REAL_DIV_LMUL; REAL_OF_NUM_EQ;
EXP_LOG];
FIRST_X_ASSUM(DISJ_CASES_THEN ASSUME_TAC) THENL
[ALL_TAC; ASM_REAL_ARITH_TAC] THEN
EXISTS_TAC `--exp(log(--x) / &n)` THEN REWRITE_TAC[
REAL_POW_NEG] THEN
ASM_SIMP_TAC[GSYM
NOT_ODD; REAL_ARITH `&0 < --x ==> ~(&0 <= x)`] THEN
ASM_SIMP_TAC[GSYM
REAL_EXP_N;
REAL_DIV_LMUL; REAL_OF_NUM_EQ;
EXP_LOG;
REAL_NEG_NEG]]);;
let ROOT_UNIQUE = prove
(`!n x y. y pow n = x /\ (
ODD n \/ ~(n = 0) /\ &0 <= y) ==>
root n x = y`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN ASSUME_TAC) THEN
UNDISCH_THEN `(y:real) pow n = x` (SUBST_ALL_TAC o SYM) THEN
MATCH_MP_TAC
REAL_ROOT_POW THEN ASM_REWRITE_TAC[]);;
let ROOT_MONO_LT = prove
(`!n x y. ~(n = 0) /\ &0 <= x /\ x < y ==>
root n x <
root n y`,
REPEAT GEN_TAC THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN
MATCH_MP_TAC(REAL_ARITH
`(&0 <= x /\ &0 <= y ==> (v <= u ==> y <= x))
==> &0 <= x /\ x < y ==> u < v`) THEN
REPEAT STRIP_TAC THEN
SUBGOAL_THEN `(
root n y) pow n <= (
root n x) pow n` MP_TAC THENL
[MATCH_MP_TAC
REAL_POW_LE2 THEN ASM_SIMP_TAC[
ROOT_POS_LE];
ASM_SIMP_TAC[
REAL_POW_ROOT]]);;
(* ------------------------------------------------------------------------- *)
(* Real power function. This involves a few arbitrary choices. *)
(* *)
(* The value of x^y is unarguable when x > 0. *)
(* *)
(* We make 0^0 = 1 to agree with "pow", but otherwise 0^y = 0. *)
(* *)
(* There is a sensible real value for (-x)^(p/q) where q is odd and either *)
(* p is even [(-x)^y = x^y] or odd [(-x)^y = -x^y]. *)
(* *)
(* In all other cases, we return (-x)^y = -x^y. This is meaningless but at *)
(* least it covers half the cases above without another case split. *)
(* *)
(* As for laws of indices, we do have x^-y = 1/x^y. Of course we can't have *)
(* x^(yz) = x^y^z or x^(y+z) = x^y x^z since then (-1)^(1/2)^2 = -1. *)
(* ------------------------------------------------------------------------- *)
parse_as_infix("rpow",(24,"left"));;
let rpow = new_definition
`x rpow y = if &0 < x then exp(y * log x)
else if x = &0 then if y = &0 then &1 else &0
else if ?m n. ODD(m) /\ ODD(n) /\ (abs y = &m / &n)
then --(exp(y * log(--x)))
else exp(y * log(--x))`;;
let RPOW_POW = prove
(`!x n. x
rpow &n = x pow n`,
REPEAT GEN_TAC THEN REWRITE_TAC[
rpow] THEN
COND_CASES_TAC THEN ASM_SIMP_TAC[
REAL_EXP_N;
EXP_LOG] THEN
COND_CASES_TAC THEN ASM_REWRITE_TAC[
REAL_POW_ZERO; REAL_OF_NUM_EQ] THEN
ASM_SIMP_TAC[
EXP_LOG; REAL_ARITH `~(&0 < x) /\ ~(x = &0) ==> &0 < --x`] THEN
REWRITE_TAC[
REAL_POW_NEG;
REAL_ABS_NUM] THEN
SUBGOAL_THEN `(?p q.
ODD(p) /\
ODD(q) /\ &n = &p / &q) <=>
ODD n`
(fun
th -> SIMP_TAC[
th; GSYM
NOT_ODD;
REAL_NEG_NEG;
COND_ID]) THEN
EQ_TAC THEN REWRITE_TAC[
LEFT_IMP_EXISTS_THM] THENL
[REPEAT GEN_TAC THEN ASM_CASES_TAC `q = 0` THEN
ASM_REWRITE_TAC[
ARITH_ODD] THEN
REPEAT(DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC)) THEN
ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
`~(q = &0) ==> (n = p / q <=> q * n = p)`] THEN
REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_EQ] THEN
ASM_MESON_TAC[
ODD_MULT];
DISCH_TAC THEN MAP_EVERY EXISTS_TAC [`n:num`; `1`] THEN
ASM_REWRITE_TAC[
REAL_DIV_1;
ARITH_ODD]]);;
let RPOW_ADD_ALT = prove
(`!x y z. &0 <= x /\ (x = &0 /\ y + z = &0 ==> y = &0 \/ z = &0)
==> x
rpow (y + z) = x
rpow y * x
rpow z`,
REPEAT GEN_TAC THEN
ASM_CASES_TAC `x = &0` THEN ASM_SIMP_TAC[
REAL_LE_LT;
RPOW_ADD] THEN
REWRITE_TAC[
RPOW_ZERO] THEN
ASM_CASES_TAC `y = &0` THEN
ASM_REWRITE_TAC[REAL_MUL_LID; REAL_ADD_LID] THEN
ASM_CASES_TAC `y + z = &0` THEN ASM_REWRITE_TAC[] THEN
ASM_REAL_ARITH_TAC);;
let RPOW_SQRT = prove
(`!x. &0 <= x ==> x
rpow (&1 / &2) =
sqrt x`,
REPEAT STRIP_TAC THEN
MATCH_MP_TAC(REAL_RING
`x pow 2 = y pow 2 /\ (x + y = &0 ==> x = &0 /\ y = &0)
==> x = y`) THEN
CONJ_TAC THENL
[ASM_SIMP_TAC[
SQRT_POW_2] THEN
ASM_SIMP_TAC[GSYM
RPOW_POW;
RPOW_RPOW] THEN
CONV_TAC REAL_RAT_REDUCE_CONV THEN
REWRITE_TAC[
RPOW_POW;
REAL_POW_1];
MATCH_MP_TAC(REAL_ARITH
`&0 <= x /\ &0 <= y ==> x + y = &0 ==> x = &0 /\ y = &0`) THEN
ASM_SIMP_TAC[
SQRT_POS_LE;
RPOW_POS_LE]]);;
let REAL_ROOT_RPOW = prove
(`!n x. ~(n = 0) /\ (&0 <= x \/
ODD n) ==>
root n x = x
rpow (inv(&n))`,
REPEAT GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN
ASM_SIMP_TAC[
ROOT_0;
RPOW_ZERO;
REAL_INV_EQ_0; REAL_OF_NUM_EQ] THEN
ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL
[ASM_SIMP_TAC[
ROOT_EXP_LOG;
rpow;
REAL_LT_LE] THEN AP_TERM_TAC THEN
REAL_ARITH_TAC;
ASM_REWRITE_TAC[
rpow] THEN COND_CASES_TAC THENL
[ASM_REAL_ARITH_TAC; ALL_TAC] THEN
REWRITE_TAC[
REAL_ABS_INV;
REAL_ABS_NUM] THEN
REWRITE_TAC[REAL_ARITH `inv x = &1 / x`] THEN
COND_CASES_TAC THENL [ALL_TAC; ASM_MESON_TAC[ARITH]] THEN
MATCH_MP_TAC
ROOT_UNIQUE THEN
ASM_REWRITE_TAC[
REAL_POW_NEG; GSYM
REAL_EXP_N; GSYM
NOT_ODD] THEN
ASM_SIMP_TAC[REAL_OF_NUM_EQ; REAL_FIELD
`~(n = &0) ==> n * &1 / n * x = x`] THEN
ONCE_REWRITE_TAC[REAL_ARITH `--x:real = y <=> x = --y`] THEN
MATCH_MP_TAC
EXP_LOG THEN ASM_REAL_ARITH_TAC]);;
(* ------------------------------------------------------------------------- *)
(* Formulation of loop homotopy in terms of maps out of S^1 *)
(* ------------------------------------------------------------------------- *)
let SIMPLY_CONNECTED_EQ_HOMOTOPIC_CIRCLEMAPS,
SIMPLY_CONNECTED_EQ_CONTRACTIBLE_CIRCLEMAP =
(CONJ_PAIR o prove)
(`(!s:real^N->bool.
simply_connected s <=>
!f g:complex->real^N.
f continuous_on sphere(vec 0,&1) /\
IMAGE f (sphere(vec 0,&1)) SUBSET s /\
g continuous_on sphere(vec 0,&1) /\
IMAGE g (sphere(vec 0,&1)) SUBSET s
==> homotopic_with (\h. T) (sphere(vec 0,&1),s) f g) /\
(!s:real^N->bool.
simply_connected s <=>
path_connected s /\
!f:real^2->real^N.
f continuous_on sphere(vec 0,&1) /\
IMAGE f (sphere(vec 0,&1)) SUBSET s
==> ?a. homotopic_with (\h. T) (sphere(vec 0,&1),s) f (\x. a))`,
REWRITE_TAC[AND_FORALL_THM] THEN GEN_TAC THEN MATCH_MP_TAC(TAUT
`(p ==> q) /\ (q ==> r) /\ (r ==> p) ==> (p <=> q) /\ (p <=> r)`) THEN
REPEAT CONJ_TAC THENL
[REWRITE_TAC[simply_connected] THEN DISCH_TAC THEN
MAP_EVERY X_GEN_TAC [`f:complex->real^N`; `g:complex->real^N`] THEN
STRIP_TAC THEN FIRST_X_ASSUM(MP_TAC o SPECL
[`(f:complex->real^N) o cexp o (\t. Cx(&2 * pi * drop t) * ii)`;
`(g:complex->real^N) o cexp o (\t. Cx(&2 * pi * drop t) * ii)`]) THEN
ONCE_REWRITE_TAC[TAUT `p1 /\ q1 /\ r1 /\ p2 /\ q2 /\ r2 <=>
(p1 /\ r1 /\ q1) /\ (p2 /\ r2 /\ q2)`] THEN
REWRITE_TAC[GSYM HOMOTOPIC_LOOPS_REFL] THEN
ASM_SIMP_TAC[HOMOTOPIC_CIRCLEMAPS_IMP_HOMOTOPIC_LOOPS;
HOMOTOPIC_WITH_REFL] THEN
DISCH_THEN(MP_TAC o MATCH_MP HOMOTOPIC_LOOPS_IMP_HOMOTOPIC_CIRCLEMAPS) THEN
MATCH_MP_TAC(ONCE_REWRITE_RULE[IMP_CONJ_ALT] HOMOTOPIC_WITH_EQ) THEN
REWRITE_TAC[IN_SPHERE_0; LIFT_DROP; o_DEF] THEN X_GEN_TAC `z:complex` THEN
REPEAT STRIP_TAC THEN AP_TERM_TAC THEN MP_TAC(SPEC `z:complex` ARG) THEN
ASM_REWRITE_TAC[COMPLEX_MUL_LID] THEN
DISCH_THEN(STRIP_ASSUME_TAC o GSYM) THEN SIMP_TAC[PI_POS;
REAL_FIELD `&0 < pi ==> &2 * pi * x / (&2 * pi) = x`] THEN
ASM_MESON_TAC[COMPLEX_MUL_SYM];
DISCH_TAC THEN CONJ_TAC THENL
[REWRITE_TAC[PATH_CONNECTED_EQ_HOMOTOPIC_POINTS] THEN
MAP_EVERY X_GEN_TAC [`a:real^N`; `b:real^N`] THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPECL
[`(\x. a):complex->real^N`; `(\x. b):complex->real^N`]) THEN
REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
ANTS_TAC THENL [ASM SET_TAC[]; ALL_TAC] THEN DISCH_THEN
(MP_TAC o MATCH_MP HOMOTOPIC_CIRCLEMAPS_IMP_HOMOTOPIC_LOOPS) THEN
REWRITE_TAC[o_DEF; LINEPATH_REFL];
X_GEN_TAC `f:complex->real^N` THEN STRIP_TAC THEN
EXISTS_TAC `f(Cx(&1)):real^N` THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
ASM_REWRITE_TAC[CONTINUOUS_ON_CONST] THEN
RULE_ASSUM_TAC(REWRITE_RULE[SUBSET; FORALL_IN_IMAGE; IN_SPHERE_0]) THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_SPHERE_0] THEN
REPEAT STRIP_TAC THEN FIRST_X_ASSUM MATCH_MP_TAC THEN
REWRITE_TAC[COMPLEX_NORM_CX] THEN REAL_ARITH_TAC];
STRIP_TAC THEN
ASM_REWRITE_TAC[SIMPLY_CONNECTED_EQ_CONTRACTIBLE_LOOP_SOME] THEN
X_GEN_TAC `p:real^1->real^N` THEN STRIP_TAC THEN
FIRST_X_ASSUM(MP_TAC o SPEC
`(p:real^1->real^N) o (\z. lift(Arg z / (&2 * pi)))`) THEN
ANTS_TAC THENL
[MP_TAC(ISPECL [`s:real^N->bool`; `p:real^1->real^N`]
HOMOTOPIC_LOOPS_REFL) THEN
ASM_REWRITE_TAC[] THEN DISCH_THEN(MP_TAC o MATCH_MP
HOMOTOPIC_LOOPS_IMP_HOMOTOPIC_CIRCLEMAPS) THEN
SIMP_TAC[HOMOTOPIC_WITH_REFL];
MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `a:real^N` THEN
STRIP_TAC THEN FIRST_ASSUM
(MP_TAC o MATCH_MP HOMOTOPIC_CIRCLEMAPS_IMP_HOMOTOPIC_LOOPS) THEN
FIRST_ASSUM(MP_TAC o MATCH_MP HOMOTOPIC_WITH_IMP_SUBSET) THEN
REWRITE_TAC[SUBSET; FORALL_IN_IMAGE; IN_SPHERE_0; o_DEF] THEN
DISCH_THEN(MP_TAC o SPEC `Cx(&1)` o CONJUNCT2) THEN
REWRITE_TAC[COMPLEX_NORM_CX; REAL_ABS_NUM] THEN
STRIP_TAC THEN ASM_REWRITE_TAC[LINEPATH_REFL] THEN
MATCH_MP_TAC(REWRITE_RULE[IMP_CONJ] HOMOTOPIC_LOOPS_TRANS) THEN
MATCH_MP_TAC HOMOTOPIC_LOOPS_EQ THEN ASM_REWRITE_TAC[] THEN
REWRITE_TAC[IN_INTERVAL_1; FORALL_LIFT; LIFT_DROP; DROP_VEC] THEN
X_GEN_TAC `t:real` THEN STRIP_TAC THEN ASM_CASES_TAC `t = &1` THENL
[ASM_REWRITE_TAC[REAL_ARITH `&2 * pi * &1 = &2 * &1 * pi`] THEN
SIMP_TAC[CEXP_INTEGER_2PI; INTEGER_CLOSED; ARG_NUM] THEN
REWRITE_TAC[real_div; REAL_MUL_LZERO; LIFT_NUM] THEN
ASM_MESON_TAC[pathstart; pathfinish];
AP_TERM_TAC THEN AP_TERM_TAC THEN SIMP_TAC[PI_POS; REAL_FIELD
`&0 < pi ==> (t = x / (&2 * pi) <=> x = &2 * pi * t)`] THEN
MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `Im(Cx (&2 * pi * t) * ii)` THEN
CONJ_TAC THENL [MATCH_MP_TAC ARG_CEXP; ALL_TAC] THEN
SIMP_TAC[IM_MUL_II; RE_CX; REAL_ARITH
`a < &2 * pi <=> a < &2 * pi * &1`] THEN
ASM_SIMP_TAC[REAL_LE_MUL; REAL_LT_LMUL_EQ; REAL_OF_NUM_LT; ARITH;
PI_POS; REAL_LT_IMP_LE; REAL_POS; REAL_LE_MUL] THEN
ASM_REWRITE_TAC[REAL_LT_LE]]]]);;
(* ------------------------------------------------------------------------- *)
(* Homeomorphism of simple closed curves to circles. *)
(* ------------------------------------------------------------------------- *)