colo12-c703.uibk.ac.at Git - Complex Analysis/.git/blob - Complex/complex_transc.ml

   1 (* ========================================================================= *)
   2 (* Complex transcendental functions.                                         *)
   3 (* ========================================================================= *)
   4
   5 needs "Library/transc.ml";;
   6 needs "Library/floor.ml";;
   7 needs "Complex/complexnumbers.ml";;
   8
   9 unparse_as_infix "exp";;
  10 remove_interface "exp";;
  11
  12 (* ------------------------------------------------------------------------- *)
  13 (* Complex square roots.                                                     *)
  14 (* ------------------------------------------------------------------------- *)
  15
  16 let csqrt = new_definition
  17   `csqrt(z) = if Im(z) = &0 then
  18                 if &0 <= Re(z) then complex(sqrt(Re(z)),&0)
  19                 else complex(&0,sqrt(--Re(z)))
  20               else complex(sqrt((norm(z) + Re(z)) / &2),
  21                            (Im(z) / abs(Im(z))) *
  22                            sqrt((norm(z) - Re(z)) / &2))`;;
  23
  24 let COMPLEX_NORM_GE_RE_IM = prove
  25  (`!z. abs(Re(z)) <= norm(z) /\ abs(Im(z)) <= norm(z)`,
  26   GEN_TAC THEN ONCE_REWRITE_TAC[GSYM POW_2_SQRT_ABS] THEN
  27   REWRITE_TAC[complex_norm] THEN
  28   CONJ_TAC THEN
  29   MATCH_MP_TAC SQRT_MONO_LE THEN
  30   ASM_SIMP_TAC[REAL_LE_ADDR; REAL_LE_ADDL; REAL_POW_2; REAL_LE_SQUARE]);;
  31
  32 let CSQRT = prove
  33  (`!z. csqrt(z) pow 2 = z`,
  34   GEN_TAC THEN REWRITE_TAC[COMPLEX_POW_2; csqrt] THEN COND_CASES_TAC THENL
  35    [COND_CASES_TAC THEN
  36     ASM_REWRITE_TAC[CX_DEF; complex_mul; RE; IM; REAL_MUL_RZERO; REAL_MUL_LZERO;
  37       REAL_SUB_LZERO; REAL_SUB_RZERO; REAL_ADD_LID; COMPLEX_EQ] THEN
  38     REWRITE_TAC[REAL_NEG_EQ; GSYM REAL_POW_2] THEN
  39     ASM_SIMP_TAC[SQRT_POW_2; REAL_ARITH `~(&0 <= x) ==> &0 <= --x`];
  40     ALL_TAC] THEN
  41   REWRITE_TAC[complex_mul; RE; IM] THEN
  42   ONCE_REWRITE_TAC[REAL_ARITH
  43    `(s * s - (i * s') * (i * s') = s * s - (i * i) * (s' * s')) /\
  44     (s * i * s' + (i * s')* s = &2 * i * s * s')`] THEN
  45   REWRITE_TAC[GSYM REAL_POW_2] THEN
  46   SUBGOAL_THEN `&0 <= norm(z) + Re(z) /\ &0 <= norm(z) - Re(z)`
  47   STRIP_ASSUME_TAC THENL
  48    [MP_TAC(SPEC `z:complex` COMPLEX_NORM_GE_RE_IM) THEN REAL_ARITH_TAC;
  49     ALL_TAC] THEN
  50   ASM_SIMP_TAC[REAL_LE_DIV; REAL_POS; GSYM SQRT_MUL; SQRT_POW_2] THEN
  51   REWRITE_TAC[COMPLEX_EQ; RE; IM] THEN CONJ_TAC THENL
  52    [ASM_SIMP_TAC[REAL_POW_DIV; REAL_POW2_ABS;
  53                  REAL_POW_EQ_0; REAL_DIV_REFL] THEN
  54     REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_SUB_RDISTRIB] THEN
  55     REWRITE_TAC[REAL_ARITH `(m + r) - (m - r) = r * &2`] THEN
  56     REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
  57     REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN
  58   REWRITE_TAC[real_div] THEN
  59   ONCE_REWRITE_TAC[AC REAL_MUL_AC
  60     `(a * b) * a' * b = (a * a') * (b * b:real)`] THEN
  61   REWRITE_TAC[REAL_DIFFSQ] THEN
  62   REWRITE_TAC[complex_norm; GSYM REAL_POW_2] THEN
  63   SIMP_TAC[SQRT_POW_2; REAL_LE_ADD;
  64            REWRITE_RULE[GSYM REAL_POW_2] REAL_LE_SQUARE] THEN
  65   REWRITE_TAC[REAL_ADD_SUB; GSYM REAL_POW_MUL] THEN
  66   REWRITE_TAC[POW_2_SQRT_ABS] THEN
  67   REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_INV; REAL_ABS_NUM] THEN
  68   ONCE_REWRITE_TAC[AC REAL_MUL_AC
  69     `&2 * (i * a') * a * h = i * (&2 * h) * a * a'`] THEN
  70   CONV_TAC REAL_RAT_REDUCE_CONV THEN
  71   REWRITE_TAC[REAL_MUL_LID; GSYM real_div] THEN
  72   ASM_SIMP_TAC[REAL_DIV_REFL; REAL_ABS_ZERO; REAL_MUL_RID]);;
  73
  74 (* ------------------------------------------------------------------------- *)
  75 (* Complex exponential.                                                      *)
  76 (* ------------------------------------------------------------------------- *)
  77
  78 let cexp = new_definition
  79  `cexp z = Cx(exp(Re z)) * complex(cos(Im z),sin(Im z))`;;
  80
  81 let CX_CEXP = prove
  82  (`!x. Cx(exp x) = cexp(Cx x)`,
  83   REWRITE_TAC[cexp; CX_DEF; RE; IM; SIN_0; COS_0] THEN
  84   REWRITE_TAC[GSYM CX_DEF; GSYM CX_MUL; REAL_MUL_RID]);;
  85
  86 let CEXP_0 = prove
  87  (`cexp(Cx(&0)) = Cx(&1)`,
  88   REWRITE_TAC[GSYM CX_CEXP; REAL_EXP_0]);;
  89
  90 let CEXP_ADD = prove
  91  (`!w z. cexp(w + z) = cexp(w) * cexp(z)`,
  92   REWRITE_TAC[COMPLEX_EQ; cexp; complex_mul; complex_add; RE; IM; CX_DEF] THEN
  93   REWRITE_TAC[REAL_EXP_ADD; SIN_ADD; COS_ADD] THEN CONV_TAC REAL_RING);;
  94
  95 let CEXP_MUL = prove
  96  (`!n z. cexp(Cx(&n) * z) = cexp(z) pow n`,
  97   INDUCT_TAC THEN REWRITE_TAC[complex_pow] THEN
  98   REWRITE_TAC[COMPLEX_MUL_LZERO; CEXP_0] THEN
  99   REWRITE_TAC[GSYM REAL_OF_NUM_SUC; COMPLEX_ADD_RDISTRIB; CX_ADD] THEN
 100   ASM_REWRITE_TAC[CEXP_ADD; COMPLEX_MUL_LID] THEN
 101   REWRITE_TAC[COMPLEX_MUL_AC]);;
 102
 103 let CEXP_NONZERO = prove
 104  (`!z. ~(cexp z = Cx(&0))`,
 105   GEN_TAC THEN REWRITE_TAC[cexp; COMPLEX_ENTIRE; CX_INJ; REAL_EXP_NZ] THEN
 106   REWRITE_TAC[CX_DEF; RE; IM; COMPLEX_EQ] THEN
 107   MP_TAC(SPEC `Im z` SIN_CIRCLE) THEN CONV_TAC REAL_RING);;
 108
 109 let CEXP_NEG_LMUL = prove
 110  (`!z. cexp(--z) * cexp(z) = Cx(&1)`,
 111   REWRITE_TAC[GSYM CEXP_ADD; COMPLEX_ADD_LINV; CEXP_0]);;
 112
 113 let CEXP_NEG_RMUL = prove
 114  (`!z. cexp(z) * cexp(--z) = Cx(&1)`,
 115   REWRITE_TAC[GSYM CEXP_ADD; COMPLEX_ADD_RINV; CEXP_0]);;
 116
 117 let CEXP_NEG = prove
 118  (`!z. cexp(--z) = inv(cexp z)`,
 119   MESON_TAC[CEXP_NEG_LMUL; COMPLEX_MUL_LINV_UNIQ]);;
 120
 121 let CEXP_SUB = prove
 122  (`!w z. cexp(w - z) = cexp(w) / cexp(z)`,
 123   REWRITE_TAC[complex_sub; complex_div; CEXP_NEG; CEXP_ADD]);;
 124
 125 (* ------------------------------------------------------------------------- *)
 126 (* Complex trig functions.                                                   *)
 127 (* ------------------------------------------------------------------------- *)
 128
 129 let ccos = new_definition
 130   `ccos z = (cexp(ii * z) + cexp(--ii * z)) / Cx(&2)`;;
 131
 132 let csin = new_definition
 133   `csin z = (cexp(ii * z) - cexp(--ii * z)) / (Cx(&2) * ii)`;;
 134
 135 let CX_CSIN,CX_CCOS = (CONJ_PAIR o prove)
 136  (`(!x. Cx(sin x) = csin(Cx x)) /\ (!x. Cx(cos x) = ccos(Cx x))`,
 137   REWRITE_TAC[csin; ccos; cexp; CX_DEF; ii; RE; IM; complex_mul; complex_add;
 138               REAL_MUL_RZERO; REAL_MUL_LZERO; REAL_SUB_RZERO;
 139               REAL_MUL_LID; complex_neg; REAL_EXP_0; REAL_ADD_LID;
 140               REAL_MUL_LNEG; REAL_NEG_0; REAL_ADD_RID; complex_sub;
 141               SIN_NEG; COS_NEG; GSYM REAL_MUL_2; GSYM real_sub;
 142               complex_div; REAL_SUB_REFL; complex_inv; REAL_SUB_RNEG] THEN
 143   CONJ_TAC THEN GEN_TAC THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN
 144   REWRITE_TAC[REAL_MUL_RZERO] THEN
 145   AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN CONV_TAC REAL_RING);;
 146
 147 let CSIN_0 = prove
 148  (`csin(Cx(&0)) = Cx(&0)`,
 149   REWRITE_TAC[GSYM CX_CSIN; SIN_0]);;
 150
 151 let CCOS_0 = prove
 152  (`ccos(Cx(&0)) = Cx(&1)`,
 153   REWRITE_TAC[GSYM CX_CCOS; COS_0]);;
 154
 155 let CSIN_CIRCLE = prove
 156  (`!z. csin(z) pow 2 + ccos(z) pow 2 = Cx(&1)`,
 157   GEN_TAC THEN REWRITE_TAC[csin; ccos] THEN
 158   MP_TAC(SPEC `ii * z` CEXP_NEG_LMUL) THEN
 159   MP_TAC COMPLEX_POW_II_2 THEN REWRITE_TAC[COMPLEX_MUL_LNEG] THEN
 160   CONV_TAC COMPLEX_FIELD);;
 161
 162 let CSIN_ADD = prove
 163  (`!w z. csin(w + z) = csin(w) * ccos(z) + ccos(w) * csin(z)`,
 164   REPEAT GEN_TAC THEN
 165   REWRITE_TAC[csin; ccos; COMPLEX_ADD_LDISTRIB; CEXP_ADD] THEN
 166   MP_TAC COMPLEX_POW_II_2 THEN CONV_TAC COMPLEX_FIELD);;
 167
 168 let CCOS_ADD = prove
 169  (`!w z. ccos(w + z) = ccos(w) * ccos(z) - csin(w) * csin(z)`,
 170   REPEAT GEN_TAC THEN
 171   REWRITE_TAC[csin; ccos; COMPLEX_ADD_LDISTRIB; CEXP_ADD] THEN
 172   MP_TAC COMPLEX_POW_II_2 THEN CONV_TAC COMPLEX_FIELD);;
 173
 174 let CSIN_NEG = prove
 175  (`!z. csin(--z) = --(csin(z))`,
 176   REWRITE_TAC[csin; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG] THEN
 177   GEN_TAC THEN MP_TAC COMPLEX_POW_II_2 THEN
 178   CONV_TAC COMPLEX_FIELD);;
 179
 180 let CCOS_NEG = prove
 181  (`!z. ccos(--z) = ccos(z)`,
 182   REWRITE_TAC[ccos; COMPLEX_MUL_LNEG; COMPLEX_MUL_RNEG; COMPLEX_NEG_NEG] THEN
 183   GEN_TAC THEN MP_TAC COMPLEX_POW_II_2 THEN
 184   CONV_TAC COMPLEX_FIELD);;
 185
 186 let CSIN_DOUBLE = prove
 187  (`!z. csin(Cx(&2) * z) = Cx(&2) * csin(z) * ccos(z)`,
 188   REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`; CSIN_ADD] THEN
 189   CONV_TAC COMPLEX_RING);;
 190
 191 let CCOS_DOUBLE = prove
 192  (`!z. ccos(Cx(&2) * z) = (ccos(z) pow 2) - (csin(z) pow 2)`,
 193   REWRITE_TAC[COMPLEX_RING `Cx(&2) * x = x + x`; CCOS_ADD] THEN
 194   CONV_TAC COMPLEX_RING);;
 195
 196 (* ------------------------------------------------------------------------- *)
 197 (* Euler and de Moivre formulas.                                             *)
 198 (* ------------------------------------------------------------------------- *)
 199
 200 let CEXP_EULER = prove
 201  (`!z. cexp(ii * z) = ccos(z) + ii * csin(z)`,
 202   REWRITE_TAC[ccos; csin] THEN MP_TAC COMPLEX_POW_II_2 THEN
 203   CONV_TAC COMPLEX_FIELD);;
 204
 205 let DEMOIVRE = prove
 206  (`!z n. (ccos z + ii * csin z) pow n =
 207          ccos(Cx(&n) * z) + ii * csin(Cx(&n) * z)`,
 208   REWRITE_TAC[GSYM CEXP_EULER; GSYM CEXP_MUL] THEN
 209   REWRITE_TAC[COMPLEX_MUL_AC]);;
 210
 211 (* ------------------------------------------------------------------------- *)
 212 (* Some lemmas.                                                              *)
 213 (* ------------------------------------------------------------------------- *)
 214
 215 let EXISTS_COMPLEX = prove
 216  (`!P. (?z. P (Re z) (Im z)) <=> ?x y. P x y`,
 217   MESON_TAC[RE; IM; COMPLEX]);;
 218
 219 let COMPLEX_UNIMODULAR_POLAR = prove
 220  (`!z. (norm z = &1) ==> ?x. z = complex(cos(x),sin(x))`,
 221   GEN_TAC THEN
 222   DISCH_THEN(MP_TAC o C AP_THM `2` o AP_TERM `(pow):real->num->real`) THEN
 223   REWRITE_TAC[complex_norm] THEN
 224   SIMP_TAC[REAL_POW_2; REWRITE_RULE[REAL_POW_2] SQRT_POW_2;
 225            REAL_LE_SQUARE; REAL_LE_ADD] THEN
 226   REWRITE_TAC[GSYM REAL_POW_2; REAL_MUL_LID] THEN
 227   DISCH_THEN(X_CHOOSE_TAC `t:real` o MATCH_MP CIRCLE_SINCOS) THEN
 228   EXISTS_TAC `t:real` THEN ASM_REWRITE_TAC[COMPLEX_EQ; RE; IM]);;
 229
 230 let SIN_INTEGER_2PI = prove
 231  (`!n. integer n ==> sin((&2 * pi) * n) = &0`,
 232   REWRITE_TAC[integer; REAL_ARITH `abs(x) = &n <=> x = &n \/ x = -- &n`] THEN
 233   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RNEG; SIN_NEG] THEN
 234   REWRITE_TAC[GSYM REAL_MUL_ASSOC; SIN_DOUBLE] THEN
 235   REWRITE_TAC[REAL_ARITH `pi * &n = &n * pi`; SIN_NPI] THEN
 236   REWRITE_TAC[REAL_MUL_LZERO; REAL_MUL_RZERO; REAL_NEG_0]);;
 237
 238 let COS_INTEGER_2PI = prove
 239  (`!n. integer n ==> cos((&2 * pi) * n) = &1`,
 240   REWRITE_TAC[integer; REAL_ARITH `abs(x) = &n <=> x = &n \/ x = -- &n`] THEN
 241   REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[REAL_MUL_RNEG; COS_NEG] THEN
 242   REWRITE_TAC[GSYM REAL_MUL_ASSOC; COS_DOUBLE] THEN
 243   REWRITE_TAC[REAL_ARITH `pi * &n = &n * pi`; SIN_NPI; COS_NPI] THEN
 244   REWRITE_TAC[REAL_POW_POW] THEN ONCE_REWRITE_TAC[MULT_SYM] THEN
 245   REWRITE_TAC[GSYM REAL_POW_POW; REAL_POW_2] THEN
 246   CONV_TAC REAL_RAT_REDUCE_CONV THEN
 247   REWRITE_TAC[REAL_POW_ONE; REAL_SUB_RZERO]);;
 248
 249 let SINCOS_PRINCIPAL_VALUE = prove
 250  (`!x. ?y. (--pi < y /\ y <= pi) /\ (sin(y) = sin(x) /\ cos(y) = cos(x))`,
 251   GEN_TAC THEN EXISTS_TAC `pi - (&2 * pi) * frac((pi - x) / (&2 * pi))` THEN
 252   CONJ_TAC THENL
 253    [SIMP_TAC[REAL_ARITH `--p < p - x <=> x < (&2 * p) * &1`;
 254              REAL_ARITH `p - x <= p <=> (&2 * p) * &0 <= x`;
 255              REAL_LT_LMUL_EQ; REAL_LE_LMUL_EQ; REAL_LT_MUL;
 256              PI_POS; REAL_OF_NUM_LT; ARITH; FLOOR_FRAC];
 257    REWRITE_TAC[FRAC_FLOOR; REAL_SUB_LDISTRIB] THEN
 258    SIMP_TAC[REAL_DIV_LMUL; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH; REAL_LT_IMP_NZ;
 259     PI_POS; REAL_ARITH `a - (a - b - c):real = b + c`; SIN_ADD; COS_ADD] THEN
 260    SIMP_TAC[FLOOR_FRAC; SIN_INTEGER_2PI; COS_INTEGER_2PI] THEN
 261    CONV_TAC REAL_RING]);;
 262
 263 (* ------------------------------------------------------------------------- *)
 264 (* Complex logarithms (the conventional principal value).                    *)
 265 (* ------------------------------------------------------------------------- *)
 266
 267 let clog = new_definition
 268  `clog z = @w. cexp(w) = z /\ --pi < Im(w) /\ Im(w) <= pi`;;
 269
 270 let CLOG_WORKS = prove
 271  (`!z. ~(z = Cx(&0))
 272        ==> cexp(clog z) = z /\ --pi < Im(clog z) /\ Im(clog z) <= pi`,
 273   GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[clog] THEN CONV_TAC SELECT_CONV THEN
 274   REWRITE_TAC[cexp; EXISTS_COMPLEX] THEN
 275   EXISTS_TAC `ln(norm(z:complex))` THEN
 276   SUBGOAL_THEN `exp(ln(norm(z:complex))) = norm(z)` SUBST1_TAC THENL
 277    [ASM_MESON_TAC[REAL_EXP_LN; COMPLEX_NORM_NZ]; ALL_TAC] THEN
 278   MP_TAC(SPEC `z / Cx(norm z)` COMPLEX_UNIMODULAR_POLAR) THEN ANTS_TAC THENL
 279    [ASM_SIMP_TAC[COMPLEX_NORM_DIV; COMPLEX_NORM_CX] THEN
 280     ASM_SIMP_TAC[COMPLEX_ABS_NORM; REAL_DIV_REFL; COMPLEX_NORM_ZERO];
 281     ALL_TAC] THEN
 282   DISCH_THEN(X_CHOOSE_THEN `x:real` STRIP_ASSUME_TAC) THEN
 283   MP_TAC(SPEC `x:real` SINCOS_PRINCIPAL_VALUE) THEN
 284   MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `y:real` THEN
 285   STRIP_TAC THEN ASM_REWRITE_TAC[] THEN
 286   ASM_MESON_TAC[CX_INJ; COMPLEX_DIV_LMUL; COMPLEX_NORM_ZERO]);;
 287
 288 let CEXP_CLOG = prove
 289  (`!z. ~(z = Cx(&0)) ==> cexp(clog z) = z`,
 290   SIMP_TAC[CLOG_WORKS]);;
 291
 292 (* ------------------------------------------------------------------------- *)
 293 (* Unwinding number.                                                         *)
 294 (* ------------------------------------------------------------------------- *)
 295
 296 let unwinding = new_definition
 297  `unwinding(z) = (z - clog(cexp z)) / (Cx(&2 * pi) * ii)`;;
 298
 299 let COMPLEX_II_NZ = prove
 300  (`~(ii = Cx(&0))`,
 301   MP_TAC COMPLEX_POW_II_2 THEN CONV_TAC COMPLEX_RING);;
 302
 303 let UNWINDING_2PI = prove
 304  (`Cx(&2 * pi) * ii * unwinding(z) = z - clog(cexp z)`,
 305   REWRITE_TAC[unwinding; COMPLEX_MUL_ASSOC] THEN
 306   MATCH_MP_TAC COMPLEX_DIV_LMUL THEN
 307   REWRITE_TAC[COMPLEX_ENTIRE; CX_INJ; COMPLEX_II_NZ] THEN
 308   MP_TAC PI_POS THEN REAL_ARITH_TAC);;
 309
 310 (* ------------------------------------------------------------------------- *)
 311 (* An example of how to get nice identities with unwinding number.           *)
 312 (* ------------------------------------------------------------------------- *)
 313
 314 let CLOG_MUL = prove
 315  (`!w z. ~(w = Cx(&0)) /\ ~(z = Cx(&0))
 316            ==> clog(w * z) =
 317                clog(w) + clog(z) -
 318                Cx(&2 * pi) * ii * unwinding(clog w + clog z)`,
 319   REWRITE_TAC[UNWINDING_2PI;
 320     COMPLEX_RING `w + z - ((w + z) - c) = c:complex`] THEN
 321   ASM_SIMP_TAC[CEXP_ADD; CEXP_CLOG]);;