3 (* ========================================================================== *)
4 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Lemma: Taylor Series for atn function *)
7 (* Chapter: Nonlinear Inequalities *)
8 (* Author: Thomas C. Hales *)
10 (* ========================================================================== *)
14 This file gives the half-angle identity for atan
15 atn (2 x) = 2 atn (...)
17 It gives a general formula for the nth derivative of catn
19 It gives the complex Taylor polynomial of catn at Cx(&0).
21 It gives the real Taylor polynomial of atn at (&0)
24 module Taylor_atn = struct
27 let FORCE_EQ = REPEAT (CHANGED_TAC (AP_TERM_TAC ORELSE AP_THM_TAC ORELSE BINOP_TAC)) ;;
29 let FORCE_MATCH = (MATCH_MP_TAC (TAUT `(a = b) ==> (a ==> b)`)) THEN FORCE_EQ ;;
31 let FORCE_MATCH_MP_TAC th =
32 MP_TAC th THEN ANTS_TAC THENL[ALL_TAC;FORCE_MATCH
35 (* first we develop the half-angle identity for the atn function *)
37 let halfatn = new_definition `halfatn x = x / (sqrt(&1 + x pow 2) + &1)`;;
40 `!x. &0 < &1 + x pow 2 `,
41 MESON_TAC[Collect_geom.pow_g;REAL_ARITH `&0 <= t ==> &0 < &1 + t`];
44 let ssqrt = new_definition `!x. ssqrt x = (if x < &0 then &0 else sqrt x)`;;
46 let halfsqrt_ssqrt = prove_by_refinement(
47 `!x. sqrt(&1+ x pow 2) = ssqrt(&1 + x pow 2)`,
51 MESON_TAC[pos1;REAL_ARITH `&0 < x ==> ~(x < &0)`];
56 `!x. &0 < sqrt(&1 + x pow 2) + &1`,
58 MESON_TAC[pos1;REAL_ARITH `(&0 <= t ==> &0 < t + &1) /\ (&0 < t ==> &0 <= t)`;SQRT_POS_LE;]
61 let halfatn_bounds_abs = prove_by_refinement(
62 `!x. abs(halfatn x) < &1 `,
65 REWRITE_TAC[halfatn;REAL_ABS_DIV];
67 ASSUME_TAC (ISPEC `x:real` pos2);
68 ASM_SIMP_TAC[REAL_ARITH `(&0 < x ==> abs(x) = x)/\ (&1 * t = t)`;REAL_LT_LDIV_EQ];
70 REWRITE_TAC[GSYM POW_2_SQRT_ABS];
71 MATCH_MP_TAC REAL_LET_TRANS;
72 EXISTS_TAC `sqrt(&1 + x pow 2)`;
74 MATCH_MP_TAC SQRT_MONO_LE;
75 REWRITE_TAC[Collect_geom.pow_g];
81 let halfatn_bounds = prove(
82 `!x. -- &1 < halfatn x /\ halfatn x < &1 `,
83 REWRITE_TAC[REAL_BOUNDS_LT;halfatn_bounds_abs]);;
85 let halfatn_half = prove_by_refinement(
86 `!x t. (abs (x) < t ==> abs(halfatn x) < t / &2) `,
89 REWRITE_TAC[halfatn;REAL_ABS_DIV];
91 ASSUME_TAC (ISPEC `x:real` pos2);
92 ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`;REAL_LT_LDIV_EQ];
93 MATCH_MP_TAC REAL_LTE_TRANS;
95 ASM_REWRITE_TAC[REAL_ARITH `(t / &2 * x = t * (x / &2)) /\ (t <= t * x/ &2 <=> t * &2 <= t * x)`];
96 MATCH_MP_TAC REAL_LE_LMUL;
98 UNDISCH_TAC `abs x < t`;
100 ASM_SIMP_TAC [REAL_ARITH `&0 < x ==> (abs(x) = x)`];
101 REWRITE_TAC[REAL_ARITH `(&2 <= x + &1) = (&1 <= x)`];
102 MATCH_MP_TAC REAL_LE_TRANS;
103 EXISTS_TAC `sqrt(&1)`;
105 REWRITE_TAC[SQRT_1;REAL_ARITH `&1 <= &1`];
106 MATCH_MP_TAC SQRT_MONO_LE;
109 MATCH_MP_TAC (REAL_ARITH `&0 <= x ==> &1 <= &1 + x`);
110 REWRITE_TAC[Collect_geom.pow_g];
114 let abs_pass_through = prove_by_refinement (
115 `(!x f. (f (-- x) = -- f x) /\ (!y. &0 <= y ==> &0 <= f y)
116 ==> (abs (f x) = f (abs x)))`,
120 DISJ_CASES_TAC (REAL_ARITH `&0 <= x \/ &0 <= --x`);
123 MESON_TAC[REAL_ARITH `&0 <= x ==> abs(x ) = x`];
124 REPEAT (POP_ASSUM MP_TAC);
125 MESON_TAC[REAL_ARITH `&0 <= --x ==> abs(x) = -- x`; REAL_ARITH `abs( -- x ) = abs(x)`];
129 let atn_abs = prove_by_refinement(
130 `!x. abs(atn x) = atn (abs x) `,
134 MATCH_MP_TAC abs_pass_through;
135 REWRITE_TAC[ATN_NEG;ATN_POS_LE];
139 let atn_half_range = prove_by_refinement (
140 `!x. abs(atn (halfatn x)) < pi / &4 `,
143 REWRITE_TAC[GSYM ATN_1;atn_abs;ATN_MONO_LT_EQ];
145 REWRITE_TAC [halfatn_bounds;GSYM REAL_BOUNDS_LT];
149 let tan_one_one = prove_by_refinement(
150 `!x y. (abs(x) < pi/ &2 /\ (abs y < pi / &2 ) /\ (tan x = tan y) ==> (x = y))`,
154 DISJ_CASES_TAC (REAL_ARITH `x < y \/ y < x \/ x = (y:real)`);
155 REPEAT (POP_ASSUM MP_TAC);
156 REWRITE_TAC[GSYM REAL_BOUNDS_LT];
157 MESON_TAC[TAN_MONO_LT_EQ;REAL_ARITH `(x:real<y ) ==> ~(x = y)`];
158 POP_ASSUM DISJ_CASES_TAC;
159 REPEAT (POP_ASSUM MP_TAC);
160 REWRITE_TAC[GSYM REAL_BOUNDS_LT];
161 MESON_TAC[TAN_MONO_LT_EQ;REAL_ARITH `(x:real<y ) ==> ~(x = y)`];
166 let abs_lemma = prove(
167 `!f x. (?n. x = f n) \/ (?n. x = -- f n) <=> (?n. abs(x) = abs(f n))`,
168 ASM_MESON_TAC[REAL_ARITH `!x y. abs(x) = abs(y) <=> (x = y)\/ (x = -- y)`]);;
170 let cos_nz = prove_by_refinement (
171 `!x. (abs(x) < pi / &2) ==> ~(cos x = &0) `,
176 REWRITE_TAC[COS_ZERO_PI;abs_lemma];
177 ONCE_REWRITE_TAC[TAUT `(a ==> ~b) <=> (b ==> ~a)`];
178 ONCE_REWRITE_TAC[REAL_ARITH `~(x < y) <=> (y <= x)`];
181 MATCH_MP_TAC REAL_LE_TRANS;
182 EXISTS_TAC`(&n + &1/ &2) * pi `;
183 REWRITE_TAC[REAL_ARITH `x <= abs(x)`];
185 MP_TAC (REAL_ARITH `&1/ &2 <= (&n + &1/ &2)`);
186 REWRITE_TAC[REAL_ARITH `pi / &2 = (&1 / &2) * pi`];
187 ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 <= x`;Real_ext.REAL_LE_RMUL_IMP];
192 let cos_2nz = prove_by_refinement(
193 `!x. (abs(x) < pi / &4) ==> ~(cos (&2 * x) = &0) `,
196 STRIP_TAC THEN STRIP_TAC;
198 REWRITE_TAC[REAL_ABS_MUL;REAL_ARITH `abs(&2)= &2 /\ (&2 * x < pi/ &2 <=> x < pi/ &4)`];
203 let halfatn_double =prove_by_refinement(
204 `!x. ~(cos (atn (halfatn x)) = &0) /\ ~(cos(&2 * atn (halfatn x)) = &0) `,
207 REPLICATE_TAC 2 (STRIP_TAC);
209 MATCH_MP_TAC REAL_LTE_TRANS;
211 REWRITE_TAC[atn_half_range];
214 MATCH_MP_TAC cos_2nz;
215 REWRITE_TAC[atn_half_range];
219 let REAL_DIV_MUL2z = REAL_FIELD
220 `!x y z. (&0 < x) ==> (y /z = (x pow 2 * y) / (x pow 2* z)) `;;
222 let atn_half = prove_by_refinement (
223 `!x. atn x = &2 * atn (halfatn x) `,
227 MATCH_MP_TAC tan_one_one;
228 MATCH_MP_TAC (TAUT `a /\ b /\ (a /\ b ==> c) ==> a /\ b /\ c`);
230 REWRITE_TAC[GSYM REAL_BOUNDS_LT;ATN_BOUNDS];
232 REWRITE_TAC[REAL_ABS_MUL;REAL_ARITH `abs (&2) = &2`;REAL_ARITH `&2 * x < y / &2 <=> x < y / &4`;atn_half_range];
235 ASSUME_TAC (ISPEC `x:real` halfatn_double);
236 ASM_SIMP_TAC[TAN_DOUBLE;ATN_TAN];
237 REWRITE_TAC[halfatn];
238 ASSUME_TAC (ISPEC `x:real` pos2);
239 ABBREV_TAC `t = sqrt(&1 + x pow 2) + &1`;
240 MP_TAC (ISPECL [`t:real`;`&2 * x / t`;`&1 - (x / t) pow 2`] REAL_DIV_MUL2z);
242 DISCH_THEN (fun t-> REWRITE_TAC[t]);
243 ASM_SIMP_TAC[REAL_FIELD `&0 < t ==> t pow 2 * &2 * x / t = t * &2 * x`];
244 ASM_SIMP_TAC[REAL_FIELD `&0 < t ==> t pow 2 * (&1 - (x / t) pow 2) = t pow 2 - x pow 2`];
246 REWRITE_TAC[REAL_FIELD `(a + &1) pow 2 = a pow 2 + &2 * a + &1`];
247 ASM_SIMP_TAC[pos1;REAL_ARITH `!x. &0 < x ==> &0 <= x`;SQRT_POW_2];
248 ASM_REWRITE_TAC[REAL_ARITH `((&1 + v) + &2 * u + &1) - v = (u + &1) * &2`];
249 UNDISCH_TAC `&0 < t`;
254 (* complex taylor for atn *)
256 prioritize_complex();;
258 let id1 = COMPLEX_RING `inv (Cx (&1) + z pow 2) = (inv (Cx (&2))) * ( ( inv (Cx (&1) + z pow 2) * (Cx (&1) - ii *z)) + (inv (Cx (&1) + z pow 2)) * ( (Cx (&1) + ii * z)))`;;
260 let id2 = SIMPLE_COMPLEX_ARITH ` (Cx (&1) + ii * z) * (Cx (&1) - ii * z) = (Cx (&1) - ii * ii * z * z)`;;
262 let id3 = prove_by_refinement (`!u a. a - ii * ii * u = a + u`,
266 SIMPLE_COMPLEX_ARITH_TAC;
270 let id4 = prove_by_refinement (`!z. (Cx (&1) + z pow 2) = (Cx (&1) + ii*z) * (Cx (&1) - ii*z)`,
273 REWRITE_TAC[id2;id3;COMPLEX_POW_2];
278 let tactic_list = [SUBGOAL_THEN `(Re (z) = &0) /\ (abs(Im (z)) = &1)` ASSUME_TAC ;
281 REWRITE_TAC[REAL_ARITH `abs(x) = &1 <=> (x = &1 \/ x = -- &1)`;ii] ;
282 SIMPLE_COMPLEX_ARITH_TAC ;
285 let idz = prove_by_refinement(
286 `!z a. (Re z = &0 ==> abs(Im z) < &1) /\ ((a = ii \/ a = --ii)) ==>
287 ~(Cx (&1) + a * z = Cx (&0))`,
290 ASSUME_TAC (REAL_ARITH `~(&1 < &1)`);
292 ] @ (tactic_list @ tactic_list));;
296 let id4a = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1)
297 ==>( inv(Cx (&1) + ii* z) * (Cx (&1) + ii*z) = Cx (&1))`,
301 MATCH_MP_TAC COMPLEX_MUL_LINV;
307 let id4b = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1)
308 ==>( inv(Cx (&1) - ii* z) * (Cx (&1) - ii*z) = Cx (&1))`,
312 MATCH_MP_TAC COMPLEX_MUL_LINV;
313 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a - ii * z = a + (-- ii) * z`];
319 let id5 = prove_by_refinement (`!z. (Re z = &0 ==> abs(Im z) < &1) ==> ( inv (Cx (&1) + z pow 2) = (inv (Cx (&2))) * ( inv (Cx (&1) + ii * z) + inv (Cx (&1) - ii * z)))`,
323 ONCE_REWRITE_TAC[id1];
324 REWRITE_TAC[id4;COMPLEX_INV_MUL];
325 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `((a*b)*c + (e*f)*g = (a:complex)*(b*c) + f * (e *g))`];
326 ASM_SIMP_TAC[id4a;id4b];
327 REWRITE_TAC[COMPLEX_MUL_RID];
331 let taylor_coeff_catn = new_definition `taylor_coeff_catn n (z:complex) =
332 if (n=0) then catn z else Cx (& (FACT (n-1))) *
333 (inv(Cx (&2))) * ( ( (-- ii) pow (n - 1) * ((inv (Cx (&1) + ii * z)) pow n)) +
334 ( ii pow (n - 1) * ((inv (Cx (&1) - ii * z)) pow n)))`;;
336 let taylor_coeff_catn0 = prove_by_refinement (
337 `taylor_coeff_catn 0 = catn `,
340 ONCE_REWRITE_TAC[FUN_EQ_THM];
341 REWRITE_TAC[taylor_coeff_catn];
345 let taylor_coeff_catn1 = prove_by_refinement (
346 `!z. (Re z = &0 ==> abs(Im z) < &1) ==>
347 (catn has_complex_derivative (taylor_coeff_catn 1 z)) (at z)`,
351 SUBGOAL_THEN `taylor_coeff_catn 1 z = inv (Cx (&1) + z pow 2)` ASSUME_TAC;
352 REWRITE_TAC[taylor_coeff_catn;ARITH_RULE `~(1=0) /\ (1-1 = 0) /\ (FACT 0 =1)`;COMPLEX_POW_1;complex_pow;COMPLEX_MUL_LID];
355 ASM_SIMP_TAC[HAS_COMPLEX_DERIVATIVE_CATN;];
359 let taylor_coeff_catn_pos = prove_by_refinement(
360 `!n. (n > 0) ==> (taylor_coeff_catn n = (\z.
361 Cx (& (FACT (n-1))) *
362 (inv(Cx (&2))) * ( ( (-- ii) pow (n - 1) * ((inv (Cx (&1) + ii * z)) pow n)) +
363 ( ii pow (n - 1) * ((inv (Cx (&1) - ii * z)) pow n))) ))`,
367 ONCE_REWRITE_TAC[FUN_EQ_THM];
368 REWRITE_TAC[taylor_coeff_catn];
369 ASM_SIMP_TAC[ARITH_RULE `n > 0 ==> ~(n=0)`];
373 let taylor_series_inv_pow = prove_by_refinement(
374 `!n a z. ~(Cx (&1) + a * z = Cx(&0)) ==>
375 (((\z. (inv (Cx (&1) + a * z)) pow n) has_complex_derivative
376 (-- Cx(&n) * a * (inv (Cx(&1) + a * z)) pow (n+1))) (at z))`,
381 DISJ_CASES_TAC (ARITH_RULE `(n=0) \/ (n > 0)`);
382 ASM_REWRITE_TAC[ARITH_RULE `0+1=1`;complex_pow;COMPLEX_POW_1;SIMPLE_COMPLEX_ARITH `-- Cx (&0) * u = Cx(&0)`;HAS_COMPLEX_DERIVATIVE_CONST];
383 ASM_SIMP_TAC[ARITH_RULE `(n>0) ==> (n+1 = 2 + (n-1))`;];
384 REWRITE_TAC[COMPLEX_POW_ADD];
385 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `-- r * s * t * u = r * u * ( -- s * t)`];
386 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_POW_AT;
387 REWRITE_TAC[COMPLEX_POW_INV;GSYM complex_div];
388 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_INV_AT;
390 CONV_TAC (PATH_CONV "lr" (ONCE_REWRITE_CONV[SIMPLE_COMPLEX_ARITH `a = Cx(&0) + a * Cx (&1)` ]));
391 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_ADD;
392 REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_CONST];
393 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT;
394 REWRITE_TAC[HAS_COMPLEX_DERIVATIVE_ID];
399 let factorial_lemma = prove_by_refinement(
400 `!n. (n>0) ==> (FACT n = n * FACT (n-1))`,
404 DISJ_CASES_TAC (ISPEC `n:num` num_CASES);
405 ASM_MESON_TAC[ARITH_RULE `(n>0) ==> ~(n=0)`];
406 ASM_MESON_TAC[FACT;ARITH_RULE `SUC n - 1 = n`];
410 let taylor_coeff_catn_deriv = prove_by_refinement(
411 `!z n. (Re z = &0 ==> abs(Im z) < &1) ==>
412 ((taylor_coeff_catn n) has_complex_derivative
413 (taylor_coeff_catn (n+1) z)) (at z)`,
417 DISJ_CASES_TAC (ARITH_RULE `(n = 0) \/ (n >0)`);
418 ASM_SIMP_TAC[ taylor_coeff_catn0;taylor_coeff_catn1;ARITH_RULE `0+1=1`];
419 REWRITE_TAC[taylor_coeff_catn;ARITH_RULE `(n+1)-1 = n`];
420 ASM_SIMP_TAC[ARITH_RULE `(n>0) ==> ~(n+1=0)`];
421 ASM_SIMP_TAC[taylor_coeff_catn_pos;factorial_lemma];
423 SUBGOAL_THEN `!u. Cx (&(n * FACT (n-1))) * u = Cx (&n) * (Cx (&(FACT (n-1))) * u)` MP_TAC;
424 REWRITE_TAC[CX_MUL;GSYM REAL_OF_NUM_MUL];
425 SIMPLE_COMPLEX_ARITH_TAC;
426 DISCH_THEN (fun t-> REWRITE_TAC[t]);
427 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(a:complex) * b * c * d = b * c * a * d`];
428 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `(a:complex) * b * u = (a*b)*u`];
429 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT;
430 REWRITE_TAC[COMPLEX_ADD_LDISTRIB];
431 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_ADD;
432 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a - ii * z = a + (-- ii) * z`];
433 SUBGOAL_THEN `!a b r. a * b pow n * r = b pow (n-1) * ( -- a * ( -- b) * r)` MP_TAC;
435 MP_TAC(ARITH_RULE `n>0 ==> n = (n-1) + 1`);
437 DISCH_THEN (fun t -> CONV_TAC (PATH_CONV "lr" (ONCE_REWRITE_CONV[t])));
438 REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_1];
439 SIMPLE_COMPLEX_ARITH_TAC;
440 DISCH_THEN (fun t->REWRITE_TAC[t]);
441 CONJ_TAC THEN (MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_LMUL_AT) ;
442 (* highly parallel branches *)
443 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `-- --ii = ii`];
444 MATCH_MP_TAC taylor_series_inv_pow;
448 MATCH_MP_TAC taylor_series_inv_pow;
454 let ipows2 = prove_by_refinement(
455 `!n. (--ii ) pow (n + 2) = -- ((-- ii) pow n)`,
459 REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_2;];
460 MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(a * a = -- Cx(&1) ) ==> r * a * a = -- r`);
462 SIMPLE_COMPLEX_ARITH_TAC;
466 let ipowsc2 = prove_by_refinement(
467 `!n. (ii ) pow (n + 2) = -- ((ii) pow n)`,
471 REWRITE_TAC[COMPLEX_POW_ADD;COMPLEX_POW_2;];
472 MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(a * a = -- Cx(&1) ) ==> r * a * a = -- r`);
474 SIMPLE_COMPLEX_ARITH_TAC;
479 let taylor_coeff0 = prove_by_refinement(
480 `!n. (taylor_coeff_catn n (Cx (&0)) = if (EVEN n) then (Cx (&0)) else
481 Cx (&(FACT (n-1)) * (-- &1) pow ((n - 1) DIV 2)))`,
485 DISJ_CASES_TAC (ISPEC `n:num` EVEN_OR_ODD);
486 DISJ_CASES_TAC (ARITH_RULE `(n=0) \/ (n >0)`);
487 ASM_REWRITE_TAC[taylor_coeff_catn;GSYM CX_ATN;ATN_0];
489 ASM_SIMP_TAC[taylor_coeff_catn_pos];
490 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a + b * Cx(&0) = a /\ a - b * Cx(&0) =a`];
491 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `inv(Cx (&1)) = Cx (&1) /\ a * Cx(&1) = a`;COMPLEX_POW_ONE];
492 MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `c = Cx(&0) ==> a*b*c = Cx(&0)`);
493 SUBGOAL_THEN ( `EVEN n ==> (?k. (n - 1) = 2 * k + 1)`) MP_TAC;
494 REWRITE_TAC[EVEN_EXISTS];
497 REPEAT (POP_ASSUM MP_TAC);
502 SPEC_TAC (`k:num`,`k:num`);
504 REWRITE_TAC[ARITH_RULE `2* 0 + 1 = 1`;COMPLEX_POW_1];
505 SIMPLE_COMPLEX_ARITH_TAC;
506 ASM_REWRITE_TAC[ipows2;ipowsc2;ARITH_RULE `2* SUC k' + 1 = (2 * k' + 1) + 2`;SIMPLE_COMPLEX_ARITH `--a + --b = --(a+b) /\ -- Cx(&0) = Cx(&0) `];
508 ASM_REWRITE_TAC[GSYM NOT_ODD];
509 SUBGOAL_THEN (`ODD n ==> (?k. n = 2 * k + 1)`) MP_TAC;
510 REWRITE_TAC[ODD_EXISTS];
517 SUBGOAL_THEN `n > 0` ASSUME_TAC;
520 ASM_SIMP_TAC[taylor_coeff_catn_pos];
521 REWRITE_TAC[SIMPLE_COMPLEX_ARITH `a + b * Cx (&0) = a /\ a - b * Cx (&0) = a /\ inv (Cx (&1)) = Cx (&1) /\ a * Cx (&1) = a`;COMPLEX_POW_ONE;ARITH_RULE `(2 * k + 1 ) - 1 = 2 * k`;CX_MUL];
522 MATCH_MP_TAC (SIMPLE_COMPLEX_ARITH `(b = c) ==> (a*b = a*c)`);
523 SPEC_TAC (`k:num`,`k:num`);
525 REWRITE_TAC[ARITH_RULE `2 * 0 =0 /\ 0 DIV 2 = 0`;complex_pow;real_pow];
526 SIMPLE_COMPLEX_ARITH_TAC;
527 REWRITE_TAC[ARITH_RULE `2 * SUC k' = 2 * k' + 2 /\ (2 * SUC k) DIV 2 = ((2 * k) DIV 2) + 1`;SIMPLE_COMPLEX_ARITH `a * (-- b + -- c) = -- (a * (b+c))`;ipows2;ipowsc2;COMPLEX_POW_ADD;REAL_POW_ADD;CX_MUL;REAL_POW_1];
529 SIMPLE_COMPLEX_ARITH_TAC;
533 let term_bound = prove_by_refinement(
534 `!a n z. Im (z) = &0 ==>
535 norm((Cx(a)* ii) pow n * ((inv (Cx (&1) - Cx(a)* ii * z)) pow (n+1)))
540 REWRITE_TAC[COMPLEX_NORM_MUL;COMPLEX_NORM_II;COMPLEX_NORM_CX;COMPLEX_NORM_POW;COMPLEX_NORM_INV;REAL_ARITH `a * &1 = a`];
541 MATCH_MP_TAC (MESON[REAL_LE_LMUL;REAL_ARITH `x = x* &1`] ( `!x y. &0 <= x /\ y <= &1 ==> x *y <= x`)) ;
543 MATCH_MP_TAC REAL_POW_LE;
544 REWRITE_TAC[REAL_ABS_POS];
545 MATCH_MP_TAC (MESON[REAL_POW_LE2;REAL_POW_ONE] `!x. &0 <= x /\ x <= &1 ==> x pow n <= &1`);
546 REWRITE_TAC[REAL_LE_INV_EQ;NORM_POS_LE];
547 MATCH_MP_TAC (MESON[REAL_LE_INV2;REAL_INV_1;REAL_ARITH `&0 < &1`] `&1 <= x ==> inv (x) <= &1`);
548 SUBGOAL_THEN `Im z = &0 ==> Cx(&1) - Cx a * ii * z = complex(&1, -- a * Re(z))` MP_TAC;
550 SIMPLE_COMPLEX_ARITH_TAC;
552 DISCH_THEN (fun t -> REWRITE_TAC[t]);
554 MATCH_MP_TAC (MESON[Collect_geom.POW2_COND;REAL_ARITH `&0 <= &1 /\ &1 pow 2 = &1`;NORM_POS_LE] `&1 <= norm x pow 2 ==> &1 <= norm x`);
555 REWRITE_TAC[COMPLEX_SQNORM;RE;IM];
556 MESON_TAC[Collect_geom.pow_g;REAL_ARITH `&1 pow 2 = &1 /\ (&0 <= t ==> &1 <= &1 + t)`];
560 let taylor_error_bound = prove_by_refinement(
561 `!n z. Im(z) = &0 ==> norm(taylor_coeff_catn (n+1) z) <= &(FACT n)`,
566 SIMP_TAC[taylor_coeff_catn_pos;ARITH_RULE `(n+1)>0 /\ ((n+1)-1 = n)`];
567 REWRITE_TAC[COMPLEX_NORM_MUL;COMPLEX_NORM_NUM;COMPLEX_NORM_INV];
568 REWRITE_TAC[COMPLEX_NORM_NUM];
569 MATCH_MP_TAC (MESON[REAL_LE_LMUL;REAL_ARITH `x = x* &1`] ( `!x y. &0 <= x /\ y <= &1 ==> x *y <= x`)) ;
571 REWRITE_TAC[REAL_OF_NUM_LE];
573 MATCH_MP_TAC (REAL_ARITH `x <= &1 + &1 ==> inv (&2)* x <= &1`);
574 MATCH_MP_TAC REAL_LE_TRANS;
575 EXISTS_TAC `norm (--ii pow n * inv (Cx (&1) + ii * z) pow (n + 1)) + norm ( ii pow n * inv (Cx (&1) - ii * z) pow (n + 1))`;
576 REWRITE_TAC[NORM_TRIANGLE];
577 MATCH_MP_TAC REAL_LE_ADD2;
580 (* FORCE_MATCH_MP_TAC *)
581 FORCE_MATCH_MP_TAC (ISPECL [`-- &1`;`n:num`;`z:complex`] term_bound);
583 ONCE_REWRITE_TAC[FUN_EQ_THM];
584 SIMPLE_COMPLEX_ARITH_TAC;
585 SIMPLE_COMPLEX_ARITH_TAC;
586 REWRITE_TAC[REAL_ABS_NEG;REAL_ABS_NUM;REAL_POW_ONE];
588 ONCE_REWRITE_TAC[SIMPLE_COMPLEX_ARITH `ii * z = Cx(&1) * ii * z`];
589 FORCE_MATCH_MP_TAC (ISPECL [` &1`;`n:num`;`z:complex`] term_bound);
591 SIMPLE_COMPLEX_ARITH_TAC;
592 REWRITE_TAC[REAL_ABS_NEG;REAL_ABS_NUM;REAL_POW_ONE];
597 let complex_taylor_catn = prove_by_refinement(
598 ` !n s. (s = {z | Im (z) = &0 }) ==> (!z.
599 (Cx(&0)) IN s /\ z IN s
603 (\i. taylor_coeff_catn i (Cx(&0)) * (z) pow i / Cx (&(FACT i)))) <=
604 norm (z) pow (n + 1) )`,
608 GEN_TAC THEN GEN_TAC;
610 MP_TAC (SPECL[`taylor_coeff_catn`;`n:num`;`s:complex->bool`;`&(FACT n)`] COMPLEX_TAYLOR);
611 ASM_REWRITE_TAC[IN_ELIM_THM];
613 REPEAT (CONJ_TAC THEN (REPEAT STRIP_TAC));
614 REWRITE_TAC[convex;IN_ELIM_THM;IM_ADD;IM_CMUL];
615 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[];
617 MATCH_MP_TAC HAS_COMPLEX_DERIVATIVE_AT_WITHIN;
618 MATCH_MP_TAC taylor_coeff_catn_deriv;
619 ASM_REWRITE_TAC[] THEN REAL_ARITH_TAC;
621 MATCH_MP_TAC taylor_error_bound;
623 DISCH_THEN (MP_TAC o (ISPEC `Cx (&0)`));
624 REWRITE_TAC[taylor_coeff_catn0;SIMPLE_COMPLEX_ARITH `z - Cx (&0) = z /\ Im (Cx (&0)) = &0`];
625 DISCH_THEN (fun t-> REPEAT STRIP_TAC THEN MP_TAC t) ;
626 DISCH_THEN (MP_TAC o (ISPEC `z:complex`));
627 DISCH_THEN FORCE_MATCH_MP_TAC;
629 MATCH_MP_TAC REAL_DIV_LMUL;
630 REWRITE_TAC[REAL_OF_NUM_EQ];
631 MESON_TAC[ FACT_LT;ARITH_RULE `0 < x ==> ~(x =0)`];
636 let real_axis = prove_by_refinement( (* not needed *)
637 `!z. (Im z = &0 <=> (?x. z = Cx(x)))`,
645 SIMPLE_COMPLEX_ARITH_TAC;
646 REPEAT STRIP_TAC THEN ASM_REWRITE_TAC[IM_CX];
650 let THREAD_IF = prove_by_refinement(
651 `!x y z f. (f:A->B) (if x then y else z) = if x then f y else f z`,
655 BOOL_CASES_TAC `x:bool` THEN REWRITE_TAC[];
660 let real_taylor_atn_ver1 = prove_by_refinement(
661 `!n x. abs(atn x - sum (0..n) (\i. if EVEN i then &0 else ( -- &1 pow ((i-1) DIV 2) * x pow i / &i ))) <= abs(x) pow (n+1)`,
665 MP_TAC (ISPECL [`n:num`;`{ z | Im(z) = &0 }`] complex_taylor_catn);
667 DISCH_THEN (fun t -> MP_TAC (ISPEC `Cx (x)` t));
668 REWRITE_TAC[VSUM_CX_NUMSEG;COMPLEX_NORM_CX;GSYM CX_SUB;GSYM CX_POW;IN_ELIM_THM;GSYM CX_MUL;GSYM CX_DIV;GSYM CX_ATN;IM_CX;taylor_coeff0;GSYM THREAD_IF];
670 ONCE_REWRITE_TAC[FUN_EQ_THM];
673 DISJ_CASES_TAC (TAUT `EVEN i \/ ~(EVEN i)`) THEN ASM_REWRITE_TAC[];
676 REWRITE_TAC[NOT_EVEN;ODD_EXISTS];
678 ASM_REWRITE_TAC[ARITH_RULE `SUC x - 1 = x`;FACT;GSYM REAL_OF_NUM_MUL ];
679 ONCE_REWRITE_TAC[REAL_FIELD `((a:real) * b) * c/(d*a) = (b * c/d) * (a/a)`];
680 MATCH_MP_TAC (REAL_FIELD `x = &1 ==> (y * x = y)`);
681 MATCH_MP_TAC REAL_DIV_REFL;
682 REWRITE_TAC[REAL_OF_NUM_EQ];
683 MESON_TAC[FACT_LT;ARITH_RULE `0 < x ==> ~(x = 0)`];
687 let sum_odd = prove_by_refinement(
688 `!(g:num->real) n. sum { i | ODD i /\ i IN 0.. 2 * n + 2 } g = sum (0.. n) (\i. g (2 * i +1))`,
692 FORCE_MATCH_MP_TAC (ISPECL [`\i. (2 * i + 1)`; `g:num->real`;`(0..n)`] SUM_IMAGE);
695 REWRITE_TAC[IMAGE;numseg;IN_ELIM_THM;ODD_EXISTS];
696 ONCE_REWRITE_TAC[FUN_EQ_THM];
697 REWRITE_TAC[IN_ELIM_THM];
704 REPEAT (POP_ASSUM MP_TAC);
706 REPEAT (POP_ASSUM MP_TAC);
710 REPEAT (POP_ASSUM MP_TAC);
712 ONCE_REWRITE_TAC[FUN_EQ_THM;];
717 let sum_even = prove_by_refinement(
718 `!g n. sum {i | ODD i /\ i IN 0..n } (\i. if EVEN i then &0 else g i) = sum (0..n) (\i. if EVEN i then &0 else g i)`,
722 ONCE_REWRITE_TAC [MESON[] `x = y <=> y = x`];
723 FORCE_MATCH_MP_TAC (ISPECL [`(\i. if EVEN i then &0 else (g i))`;`{i | ODD i /\ i IN 0..n}`;`(0..n)`] SUM_SUPERSET);
726 REPEAT (POP_ASSUM MP_TAC);
727 REWRITE_TAC[IN_ELIM_THM;numseg];
733 let real_taylor_atn = prove_by_refinement(
734 `!n x. abs(atn x - sum (0..n) (\j. (-- &1 pow j) * x pow (2 * j + 1)/ &(2 * j+ 1))) <= abs(x) pow (2 * n + 3)`,
738 MP_TAC (ISPECL [`2*n + 2`;`x:real`] real_taylor_atn_ver1);
739 REWRITE_TAC[ARITH_RULE `(2*n + 2) +1 = 2 *n + 3`];
740 REWRITE_TAC[GSYM sum_even];
741 REWRITE_TAC[sum_odd];
742 SUBGOAL_THEN `!i. ~(EVEN (2 *i + 1))` MP_TAC;
744 REWRITE_TAC[EVEN_EXISTS;ODD_EXISTS;ARITH_RULE `!m. SUC (m) = m+1`];
748 REWRITE_TAC[ARITH_RULE `((2 * i + 1) - 1) DIV 2 = i`];
752 let halfatn4 = new_definition `halfatn4 = halfatn o halfatn o halfatn o halfatn`;;
754 let real_taylor_atn_halfatn4 = prove_by_refinement(
755 `!n x. abs (atn(halfatn4 x) - sum (0..n) (\j. (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1))) <= inv (&8 pow (2 * n + 3))`,
759 MATCH_MP_TAC REAL_LE_TRANS;
760 EXISTS_TAC `abs(halfatn4 x) pow (2 * n + 3)`;
761 REWRITE_TAC[real_taylor_atn;REAL_INV_POW];
762 MATCH_MP_TAC Real_ext.REAL_PROP_LE_POW;
763 REWRITE_TAC[REAL_ABS_POS;halfatn4;o_THM];
764 MATCH_MP_TAC (REAL_ARITH `x < y ==> x <= y`);
765 MP_TAC (ISPEC `x:real` halfatn_bounds_abs);
766 REPLICATE_TAC 3( DISCH_THEN (fun t-> MP_TAC (MATCH_MP halfatn_half t)));
772 let atn_halfatn4 = prove_by_refinement(
773 `!x. atn x = &16 * atn(halfatn4 x)`,
776 ONCE_REWRITE_TAC[REAL_ARITH `&16 * x = &2 * &2 * &2 * &2 * x`];
777 REWRITE_TAC[halfatn4;o_THM;GSYM atn_half];
781 let real_taylor_atn_halfatn4_a = prove_by_refinement(
782 `!n x. abs (atn x - &16 * sum (0..n) (\j. (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1))) <= inv (&2 pow (6 * n + 5 ))`,
786 ONCE_REWRITE_TAC [atn_halfatn4];
787 REWRITE_TAC[REAL_ARITH `abs (&16 * x - &16 * y) <= z <=> abs(x - y) <= z *inv (&2 pow 4)`];
788 MP_TAC (ISPECL [`n:num`;`x:real`] real_taylor_atn_halfatn4);
790 REWRITE_TAC[GSYM REAL_INV_MUL;GSYM REAL_POW_ADD;REAL_ARITH `&8 = &2 pow 3`;REAL_POW_POW];
796 let halfatn4_co = new_definition `halfatn4_co x j = (-- &1 pow j) * halfatn4 x pow (2 * j + 1)/ &(2 * j+ 1)`;;
798 let atn_bounds_anti = prove_by_refinement(
799 `!x y. x <= y ==> abs(atn x - atn y) <= abs(x - y)`,
803 MP_TAC (ISPECL [`atn`;`(\t. inv(&1 + t pow 2))`;`x:real`;`y:real`] REAL_MVT_VERY_SIMPLE);
804 REWRITE_TAC[real_interval;IN_ELIM_THM];
808 MATCH_MP_TAC HAS_REAL_DERIVATIVE_ATREAL_WITHIN;
809 REWRITE_TAC[HAS_REAL_DERIVATIVE_ATN];
811 ONCE_REWRITE_TAC[REAL_ARITH `abs(y - x) = abs(x-y)`];
813 REWRITE_TAC[REAL_ABS_MUL];
814 FORCE_MATCH_MP_TAC (ISPECL [`abs(inv (&1 + x' pow 2))`;`&1`;`abs(y-x)`] REAL_LE_RMUL);
815 REWRITE_TAC[REAL_ABS_POS;REAL_ABS_INV];
816 FORCE_MATCH_MP_TAC (ISPECL [`&1`;`abs(&1 + x' pow 2)`] REAL_LE_INV2);
817 CONJ_TAC THEN TRY(REAL_ARITH_TAC);
818 MP_TAC (ISPEC `x':real` pos1);
819 SIMP_TAC [REAL_ARITH `(&0 < x ==> (abs x = x)) /\ (&1 <= &1 + u <=> &0 <= u)`;Real_ext.REAL_LE_POW_2];
827 let atn_bounds = prove_by_refinement(
828 `!x y. abs(atn x - atn y) <= abs(x-y)`,
832 DISJ_CASES_TAC (REAL_ARITH `x<= y \/ y <= x`);
833 ASM_SIMP_TAC[atn_bounds_anti];
834 ONCE_REWRITE_TAC[REAL_ARITH `abs(x -y) = abs(y-x)`];
835 ASM_SIMP_TAC[atn_bounds_anti];
839 let real_taylor_atn_approx = prove_by_refinement(
840 `!n x v eps1 eps2 eps.
841 inv (&2 pow (6 * n + 5)) <= eps1 /\
842 abs(&16 *sum (0..n) (halfatn4_co x) - v )<= eps2 /\
843 (eps1 + eps2 <= eps) ==>
844 abs(atn(x) - v) <= eps`,
848 MATCH_MP_TAC REAL_LE_TRANS;
849 EXISTS_TAC `( eps1:real) + eps2`;
851 MATCH_MP_TAC REAL_LE_TRANS;
852 ABBREV_TAC `r = &16 * sum(0..n) (halfatn4_co x)`;
853 EXISTS_TAC`abs(atn x - r) + abs(r - v)`;
855 MESON_TAC[REAL_ABS_TRIANGLE;REAL_ARITH `atn x - v = (atn x - r) + r - v`];
856 MATCH_MP_TAC (REAL_ARITH `a1 <= b1 /\ a2 <= b2 ==> a1 + a2 <= b1 + b2`);
858 MATCH_MP_TAC REAL_LE_TRANS;
859 EXISTS_TAC `inv(&2 pow (6 * n + 5))`;
862 MP_TAC (ISPECL [`n:num`;`x:real`] real_taylor_atn_halfatn4_a);
864 REWRITE_TAC[FUN_EQ_THM;halfatn4_co];