(* ========================================================================= *) (* Taylor series for tan and cot, via partial fractions expansion of cot. *) (* ========================================================================= *) (* ------------------------------------------------------------------------- *) (* The formulas marked with a star on p. 205 of Knopp's book. *) (* ------------------------------------------------------------------------- *) let COT_HALF_TAN = prove (`~(integer x) ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) - tan(pi * x / &2)))`, REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN REWRITE_TAC[cot; tan] THEN REWRITE_TAC[REAL_MUL_RID] THEN SUBGOAL_THEN `pi * x = &2 * pi * x / &2` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN ABBREV_TAC `y = pi * x / &2` THEN REWRITE_TAC[COS_DOUBLE; SIN_DOUBLE] THEN SUBGOAL_THEN `~(sin y = &0) /\ ~(cos y = &0)` STRIP_ASSUME_TAC THENL [EXPAND_TAC "y" THEN REWRITE_TAC[SIN_ZERO; COS_ZERO; real_div] THEN CONJ_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c = d) = (b * a * c = d)`] THEN SIMP_TAC[GSYM REAL_MUL_LNEG; REAL_EQ_MUL_RCANCEL; REAL_ENTIRE; REAL_INV_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ; REAL_LT_IMP_NZ; PI_POS] THEN REWRITE_TAC[OR_EXISTS_THM] THEN REWRITE_TAC[TAUT `a /\ b \/ a /\ c = a /\ (b \/ c)`] THEN DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN (MP_TAC o AP_TERM `abs`) o CONJUNCT2)) THEN UNDISCH_TAC `~(integer x)` THEN SIMP_TAC[integer; REAL_ABS_NEG; REAL_ABS_NUM; NOT_EXISTS_THM]; ALL_TAC] THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&2 * sin y * cos y` THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_ARITH `(h * (c * s' - s * c')) * t * s * c = (t * h) * (c * c * s * s' - s * s * c * c')`] THEN ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_RID; REAL_MUL_LID; REAL_POW_2]);; let COT_HALF_POS = prove (`~(integer x) ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) + cot(pi * (x + &1) / &2)))`, REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN REWRITE_TAC[cot; COS_ADD; SIN_ADD; COS_PI2; SIN_PI2] THEN REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_LID; REAL_SUB_LZERO] THEN REWRITE_TAC[REAL_MUL_RID] THEN SUBGOAL_THEN `pi * x = &2 * pi * x / &2` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [ONCE_REWRITE_TAC[AC REAL_MUL_AC `a * b * c = (a * c) * b`] THEN SIMP_TAC[REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN ABBREV_TAC `y = pi * x / &2` THEN REWRITE_TAC[COS_DOUBLE; SIN_DOUBLE] THEN SUBGOAL_THEN `~(sin y = &0) /\ ~(cos y = &0)` STRIP_ASSUME_TAC THENL [EXPAND_TAC "y" THEN REWRITE_TAC[SIN_ZERO; COS_ZERO; real_div] THEN CONJ_TAC THEN ONCE_REWRITE_TAC[REAL_ARITH `(a * b * c = d) = (b * a * c = d)`] THEN SIMP_TAC[GSYM REAL_MUL_LNEG; REAL_EQ_MUL_RCANCEL; REAL_ENTIRE; REAL_INV_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ; REAL_LT_IMP_NZ; PI_POS] THEN REWRITE_TAC[OR_EXISTS_THM] THEN REWRITE_TAC[TAUT `a /\ b \/ a /\ c = a /\ (b \/ c)`] THEN DISCH_THEN(CHOOSE_THEN(DISJ_CASES_THEN (MP_TAC o AP_TERM `abs`) o CONJUNCT2)) THEN UNDISCH_TAC `~(integer x)` THEN SIMP_TAC[integer; REAL_ABS_NEG; REAL_ABS_NUM; NOT_EXISTS_THM]; ALL_TAC] THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&2 * sin y * cos y` THEN ASM_SIMP_TAC[REAL_DIV_RMUL; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_ARITH `(h * c * s' + h * --s * c') * t * s * c = (t * h) * (c * c * s * s' - s * s * c * c')`] THEN ASM_SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[REAL_MUL_RID; REAL_MUL_LID; REAL_POW_2]);; let COT_HALF_NEG = prove (`~(integer x) ==> (cot(pi * x) = &1 / &2 * (cot(pi * x / &2) + cot(pi * (x - &1) / &2)))`, STRIP_TAC THEN ASM_SIMP_TAC[COT_HALF_POS] THEN AP_TERM_TAC THEN AP_TERM_TAC THEN SUBST1_TAC(REAL_ARITH `x + &1 = (x - &1) + &2`) THEN ABBREV_TAC `y = x - &1` THEN REWRITE_TAC[real_div; REAL_ADD_RDISTRIB; REAL_ADD_LDISTRIB] THEN SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[cot; SIN_ADD; COS_ADD; SIN_PI; COS_PI] THEN REWRITE_TAC[REAL_MUL_RZERO; REAL_ADD_RID; REAL_SUB_RZERO] THEN REWRITE_TAC[real_div; REAL_MUL_RNEG; REAL_MUL_LNEG; REAL_INV_NEG] THEN REWRITE_TAC[REAL_NEG_NEG; REAL_MUL_RID]);; (* ------------------------------------------------------------------------- *) (* By induction, the formula marked with the dagger. *) (* ------------------------------------------------------------------------- *) let COT_HALF_MULTIPLE = prove (`~(integer x) ==> !n. cot(pi * x) = Sum(0,2 EXP n) (\k. cot(pi * (x + &k) / &2 pow n) + cot(pi * (x - &k) / &2 pow n)) / &2 pow (n + 1)`, DISCH_TAC THEN INDUCT_TAC THENL [REWRITE_TAC[EXP; real_pow; REAL_DIV_1; ADD_CLAUSES; REAL_POW_1] THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[real_div; REAL_ADD_RID; REAL_SUB_RZERO; GSYM REAL_MUL_2] THEN REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c = b * a * c`] THEN SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID; REAL_OF_NUM_EQ; ARITH_EQ]; ALL_TAC] THEN FIRST_X_ASSUM(fun th -> GEN_REWRITE_TAC LAND_CONV [th]) THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `Sum(0,2 EXP n) (\k. &1 / &2 * (cot (pi * (x + &k) / &2 pow n / &2) + cot (pi * ((x + &k) / &2 pow n + &1) / &2)) + &1 / &2 * (cot (pi * (x - &k) / &2 pow n / &2) + cot (pi * ((x - &k) / &2 pow n - &1) / &2))) / &2 pow (n + 1)` THEN CONJ_TAC THENL [AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `k:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[] THEN BINOP_TAC THENL [MATCH_MP_TAC COT_HALF_POS THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = &2 pow n * (x + &k) / &2 pow n - &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; MATCH_MP_TAC COT_HALF_NEG THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = &2 pow n * (x - &k) / &2 pow n + &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; SUM_CMUL] THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN ONCE_REWRITE_TAC[real_div] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN BINOP_TAC THENL [ALL_TAC; REWRITE_TAC[real_pow; REAL_POW_ADD; REAL_INV_MUL; GSYM REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV] THEN SUBGOAL_THEN `!k. (x + &k) / &2 pow n + &1 = (x + &(2 EXP n + k)) / &2 pow n` (fun th -> ONCE_REWRITE_TAC[th]) THENL [GEN_TAC THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&2 pow n` THEN ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES; REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_MUL_RID; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN REWRITE_TAC[REAL_ADD_AC]; ALL_TAC] THEN SUBGOAL_THEN `!k. (x - &k) / &2 pow n - &1 = (x - &(2 EXP n + k)) / &2 pow n` (fun th -> ONCE_REWRITE_TAC[th]) THENL [GEN_TAC THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&2 pow n` THEN ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES; REAL_SUB_LDISTRIB] THEN REWRITE_TAC[REAL_MUL_RID; GSYM REAL_OF_NUM_ADD; GSYM REAL_OF_NUM_POW] THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[EXP; MULT_2; GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_OFFSET)] THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; GSYM REAL_INV_MUL] THEN REWRITE_TAC[ONCE_REWRITE_RULE[REAL_MUL_SYM] (GSYM(CONJUNCT2 real_pow))] THEN REWRITE_TAC[SUM_ADD] THEN CONV_TAC(ONCE_DEPTH_CONV (ALPHA_CONV `j:num`)) THEN REWRITE_TAC[REAL_ADD_AC; ADD_AC]);; let COT_HALF_KNOPP = prove (`~(integer x) ==> !n. cot(pi * x) = cot(pi * x / &2 pow n) / &2 pow n + Sum(1,2 EXP n - 1) (\k. cot(pi * (x + &k) / &2 pow (n + 1)) + cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1)`, DISCH_TAC THEN GEN_TAC THEN FIRST_ASSUM(SUBST1_TAC o SPEC `n:num` o MATCH_MP COT_HALF_MULTIPLE) THEN SUBGOAL_THEN `!f. Sum(0,2 EXP n) f = f 0 + Sum(1,2 EXP n - 1) f` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [GEN_TAC THEN SUBGOAL_THEN `2 EXP n = 1 + (2 EXP n - 1)` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [SIMP_TAC[ARITH_RULE `~(x = 0) ==> (1 + (x - 1) = x)`; EXP_EQ_0; ARITH_EQ]; ALL_TAC] THEN REWRITE_TAC[GSYM(ONCE_REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN REWRITE_TAC[SUM_1; REAL_ADD_AC]; ALL_TAC] THEN REWRITE_TAC[REAL_ADD_RID; REAL_SUB_RZERO; GSYM REAL_MUL_2] THEN GEN_REWRITE_TAC LAND_CONV [real_div] THEN GEN_REWRITE_TAC LAND_CONV [REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC EQ_TRANS THEN EXISTS_TAC `(&2 * cot (pi * x / &2 pow n)) / &2 pow (n + 1) + Sum(1,2 EXP n - 1) (\k. &1 / &2 * (cot (pi * (x + &k) / &2 pow n / &2) + cot (pi * ((x + &k) / &2 pow n - &1) / &2)) + &1 / &2 * (cot (pi * (x - &k) / &2 pow n / &2) + cot (pi * ((x - &k) / &2 pow n + &1) / &2))) / &2 pow (n + 1)` THEN CONJ_TAC THENL [AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `k:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[] THEN BINOP_TAC THENL [MATCH_MP_TAC COT_HALF_NEG THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = &2 pow n * (x + &k) / &2 pow n - &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; MATCH_MP_TAC COT_HALF_POS THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = &2 pow n * (x - &k) / &2 pow n + &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [SIMP_TAC[REAL_DIV_LMUL; REAL_POW2_CLAUSES; REAL_LT_IMP_NZ] THEN REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; SUM_CMUL] THEN ONCE_REWRITE_TAC[AC REAL_ADD_AC `(a + b) + (c + d) = (a + c) + (b + d)`] THEN GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [SUM_ADD] THEN GEN_REWRITE_TAC (funpow 2 (LAND_CONV o RAND_CONV) o RAND_CONV) [SUM_REVERSE] THEN SUBGOAL_THEN `(2 EXP n - 1 + 2 * 1) - 1 = 2 EXP n` SUBST1_TAC THENL [SUBGOAL_THEN `~(2 EXP n = 0)` MP_TAC THENL [REWRITE_TAC[EXP_EQ_0; ARITH_EQ]; SPEC_TAC(`2 EXP n`,`m:num`) THEN ARITH_TAC]; ALL_TAC] THEN REWRITE_TAC[GSYM SUM_ADD] THEN BINOP_TAC THENL [GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [REAL_MUL_SYM] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[real_div; REAL_POW_ADD; REAL_INV_MUL; REAL_MUL_ASSOC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN AP_THM_TAC THEN AP_TERM_TAC THEN REWRITE_TAC[GSYM SUM_CMUL] THEN MATCH_MP_TAC SUM_EQ THEN X_GEN_TAC `k:num` THEN REWRITE_TAC[LE_0; ADD_CLAUSES] THEN STRIP_TAC THEN GEN_REWRITE_TAC LAND_CONV [REAL_MUL_SYM] THEN GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [real_div] THEN REWRITE_TAC[REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN MATCH_MP_TAC(REAL_ARITH `(a = e) /\ (d = e) /\ (b = f) /\ (c = f) ==> ((a + b) + (c + d) = (e + f) * &2)`) THEN UNDISCH_TAC `k < 2 EXP n - 1 + 1` THEN SIMP_TAC[ARITH_RULE `~(p = 0) ==> (k < p - 1 + 1 = k < p)`; EXP_EQ_0; ARITH_EQ] THEN DISCH_TAC THEN SUBGOAL_THEN `!x. (x / &2 pow n + &1 = (x + &2 pow n) / &2 pow n) /\ (x / &2 pow n - &1 = (x - &2 pow n) / &2 pow n)` (fun th -> REWRITE_TAC[th]) THENL [SIMP_TAC[REAL_EQ_RDIV_EQ; REAL_POW2_CLAUSES; REAL_ADD_RDISTRIB; REAL_SUB_RDISTRIB; REAL_MUL_LID; REAL_DIV_RMUL; REAL_LT_IMP_NZ]; ALL_TAC] THEN SUBGOAL_THEN `!x. x / &2 pow n / &2 = x / &2 pow (n + 1)` (fun th -> REWRITE_TAC[th]) THENL [REWRITE_TAC[REAL_POW_ADD; real_div; REAL_POW_1; REAL_INV_MUL; GSYM REAL_MUL_ASSOC]; ALL_TAC] THEN ASM_SIMP_TAC[LT_IMP_LE; GSYM REAL_OF_NUM_SUB; GSYM REAL_OF_NUM_POW] THEN CONJ_TAC THEN AP_TERM_TAC THEN AP_TERM_TAC THEN AP_THM_TAC THEN AP_TERM_TAC THEN REAL_ARITH_TAC);; (* ------------------------------------------------------------------------- *) (* Bounds on the terms in this series. *) (* ------------------------------------------------------------------------- *) let SIN_SUMDIFF_LEMMA = prove (`!x y. sin(x + y) * sin(x - y) = (sin x + sin y) * (sin x - sin y)`, REPEAT GEN_TAC THEN REWRITE_TAC[REAL_ARITH `(x + y) * (x - y) = x * x - y * y`] THEN REWRITE_TAC[SIN_ADD; real_sub; SIN_NEG; COS_NEG] THEN REWRITE_TAC[REAL_ADD_LDISTRIB; REAL_ADD_RDISTRIB] THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_MUL_ASSOC; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG] THEN REWRITE_TAC[REAL_ARITH `(a = sx * sx + --(sy * sy)) = (a + sy * sy + --(sx * sx) = &0)`] THEN REWRITE_TAC[REAL_ARITH `a + --(sx * cy * cx * sy) + cx * sy * sx * cy + b = a + b`] THEN REWRITE_TAC[REAL_ARITH `(sx * cy * sx * cy + --(cx * sy * cx * sy)) + sy * sy + --(sx * sx) = (sy * sy + (sx * sx + cx * cx) * (cy * cy)) - (sx * sx + (sy * sy + cy * cy) * (cx * cx))`] THEN REWRITE_TAC[REWRITE_RULE[REAL_POW_2] SIN_CIRCLE; REAL_MUL_LID] THEN REWRITE_TAC[REAL_SUB_REFL]);; let SIN_ZERO_LEMMA = prove (`!x. (sin(pi * x) = &0) = integer(x)`, REWRITE_TAC[integer; SIN_ZERO; EVEN_EXISTS] THEN ONCE_REWRITE_TAC[TAUT `a /\ b = ~(a ==> ~b)`] THEN SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN REWRITE_TAC[GSYM REAL_OF_NUM_MUL] THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c * d = c * b * a * d`] THEN SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_EQ; REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_MUL_RNEG] THEN SIMP_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB; REAL_EQ_MUL_LCANCEL; PI_POS; REAL_LT_IMP_NZ] THEN REWRITE_TAC[NOT_IMP; NOT_FORALL_THM] THEN ONCE_REWRITE_TAC[SWAP_EXISTS_THM] THEN REWRITE_TAC[LEFT_EXISTS_AND_THM; EXISTS_REFL] THEN REWRITE_TAC[REAL_MUL_RNEG; OR_EXISTS_THM] THEN REWRITE_TAC[REAL_ARITH `(abs(x) = a) = &0 <= a /\ ((x = a) \/ (x = --a))`] THEN REWRITE_TAC[REAL_POS]);; let NOT_INTEGER_LEMMA = prove (`~(x = &0) /\ abs(x) < &1 ==> ~(integer x)`, ONCE_REWRITE_TAC[GSYM REAL_ABS_ZERO] THEN CONV_TAC CONTRAPOS_CONV THEN SIMP_TAC[integer; LEFT_IMP_EXISTS_THM] THEN GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[REAL_OF_NUM_EQ; REAL_OF_NUM_LT] THEN ARITH_TAC);; let NOT_INTEGER_DIV_POW2 = prove (`~(integer x) ==> ~(integer(x / &2 pow n))`, REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = &2 pow n * x / &2 pow n` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [SIMP_TAC[REAL_DIV_LMUL; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES]; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]);; let SIN_ABS_LEMMA = prove (`!x. abs(x) < pi ==> (abs(sin x) = sin(abs x))`, GEN_TAC THEN ASM_CASES_TAC `x = &0` THEN ASM_REWRITE_TAC[SIN_0; REAL_ABS_NUM] THEN REWRITE_TAC[real_abs] THEN ASM_CASES_TAC `&0 <= x` THEN ASM_REWRITE_TAC[] THEN STRIP_TAC THENL [SUBGOAL_THEN `&0 < sin x` (fun th -> ASM_SIMP_TAC[th; REAL_LT_IMP_LE]) THEN MATCH_MP_TAC SIN_POS_PI THEN ASM_REWRITE_TAC[real_abs] THEN ASM_REWRITE_TAC[REAL_LT_LE]; SUBGOAL_THEN `&0 < --(sin x)` (fun th -> SIMP_TAC[th; SIN_NEG; REAL_ARITH `&0 < --x ==> ~(&0 <= x)`]) THEN REWRITE_TAC[GSYM SIN_NEG] THEN MATCH_MP_TAC SIN_POS_PI THEN ASM_SIMP_TAC[REAL_ARITH `~(x = &0) /\ ~(&0 <= x) ==> &0 < --x`]]);; let SIN_EQ_LEMMA = prove (`!x y. &0 <= x /\ x < pi / &2 /\ &0 <= y /\ y < pi / &2 ==> ((sin x = sin y) = (x = y))`, SUBGOAL_THEN `!x y. &0 <= x /\ x < pi / &2 /\ &0 <= y /\ y < pi / &2 /\ x < y ==> sin x < sin y` ASSUME_TAC THENL [ALL_TAC; REPEAT STRIP_TAC THEN EQ_TAC THEN SIMP_TAC[] THEN CONV_TAC CONTRAPOS_CONV THEN REWRITE_TAC[REAL_ARITH `~(x = y) = x < y \/ y < x`] THEN ASM_MESON_TAC[]] THEN REPEAT STRIP_TAC THEN MP_TAC(SPECL [`sin`; `cos`; `x:real`; `y:real`] MVT_ALT) THEN ASM_REWRITE_TAC[DIFF_SIN; REAL_EQ_SUB_RADD] THEN DISCH_THEN(X_CHOOSE_THEN `z:real` STRIP_ASSUME_TAC) THEN ASM_REWRITE_TAC[REAL_ARITH `x < a + x = &0 < a`] THEN MATCH_MP_TAC REAL_LT_MUL THEN ASM_REWRITE_TAC[REAL_SUB_LT] THEN MATCH_MP_TAC COS_POS_PI2 THEN ASM_MESON_TAC[REAL_LET_TRANS; REAL_LT_TRANS]);; let KNOPP_TERM_EQUIVALENT = prove (`~(integer x) /\ k < 2 EXP n ==> ((cot(pi * (x + &k) / &2 pow (n + 1)) + cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1) = cot(pi * x / &2 pow (n + 1)) / &2 pow n / (&1 - sin(pi * &k / &2 pow (n + 1)) pow 2 / sin(pi * x / &2 pow (n + 1)) pow 2))`, let lemma = prove (`~(x = &0) /\ (x * a = b) ==> (a = b / x)`, REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `x:real` THEN ASM_SIMP_TAC[REAL_DIV_LMUL]) in REPEAT STRIP_TAC THEN SIMP_TAC[REAL_EQ_LDIV_EQ; REAL_POW2_CLAUSES] THEN GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [REAL_POW_ADD] THEN REWRITE_TAC[REAL_POW_1; real_div] THEN GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC `((a * b') * c) * b * &2 = (&2 * a) * c * b * b'`] THEN SIMP_TAC[REAL_MUL_RINV; REAL_POW_EQ_0; REAL_OF_NUM_EQ; ARITH_EQ] THEN REWRITE_TAC[real_div; REAL_ADD_LDISTRIB; REAL_SUB_LDISTRIB; REAL_ADD_RDISTRIB; REAL_SUB_RDISTRIB] THEN REWRITE_TAC[REAL_MUL_RID; GSYM real_div] THEN ABBREV_TAC `a = pi * x / &2 pow (n + 1)` THEN ABBREV_TAC `b = pi * &k / &2 pow (n + 1)` THEN SUBGOAL_THEN `~(sin(a + b) = &0) /\ ~(sin a = &0) /\ ~(sin(a - b) = &0) /\ ~(&1 - sin(b) pow 2 / sin(a) pow 2 = &0)` STRIP_ASSUME_TAC THENL [MATCH_MP_TAC(TAUT `(a /\ b /\ c) /\ (b ==> d) ==> a /\ b /\ c /\ d`) THEN CONJ_TAC THENL [MAP_EVERY EXPAND_TAC ["a"; "b"] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[SIN_ZERO_LEMMA] THEN REWRITE_TAC[real_div] THEN REWRITE_TAC[GSYM REAL_ADD_RDISTRIB; GSYM REAL_SUB_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN REPEAT CONJ_TAC THEN MATCH_MP_TAC NOT_INTEGER_DIV_POW2 THEN ASM_REWRITE_TAC[] THENL [UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = (x + &k) - &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = (x - &k) + &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_0] THEN DISCH_THEN(MP_TAC o AP_TERM `( * ) (sin(a) pow 2)`) THEN ASM_SIMP_TAC[REAL_DIV_LMUL; REAL_POW_EQ_0; REAL_MUL_RID] THEN REWRITE_TAC[REAL_POW_2] THEN ONCE_REWRITE_TAC[REAL_ARITH `(a * a = b * b) = ((a + b) * (a - b) = &0)`] THEN REWRITE_TAC[GSYM SIN_SUMDIFF_LEMMA] THEN REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM] THEN MAP_EVERY EXPAND_TAC ["a"; "b"] THEN REWRITE_TAC[GSYM REAL_ADD_LDISTRIB; GSYM REAL_SUB_LDISTRIB] THEN REWRITE_TAC[SIN_ZERO_LEMMA] THEN REWRITE_TAC[real_div; GSYM REAL_ADD_RDISTRIB; GSYM REAL_SUB_RDISTRIB] THEN REWRITE_TAC[GSYM real_div] THEN CONJ_TAC THEN MATCH_MP_TAC NOT_INTEGER_DIV_POW2 THENL [UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = (x + &k) - &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN SUBGOAL_THEN `x = (x - &k) + &k` (fun th -> GEN_REWRITE_TAC (RAND_CONV o RAND_CONV) [th]) THENL [REAL_ARITH_TAC; SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]]; ALL_TAC] THEN REWRITE_TAC[cot; TAN_ADD; real_sub] THEN REWRITE_TAC[GSYM real_sub] THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a + b)` THEN ASM_SIMP_TAC[REAL_ADD_LDISTRIB; REAL_DIV_LMUL] THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a - b)` THEN ONCE_REWRITE_TAC[REAL_ARITH `a * (b + c * d) = a * b + c * a * d`] THEN ASM_SIMP_TAC[REAL_ADD_LDISTRIB; REAL_DIV_LMUL] THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `&1 - sin(b) pow 2 / sin(a) pow 2` THEN ONCE_REWRITE_TAC[REAL_ARITH `a * b * c * da = b * c * a * da`] THEN ASM_SIMP_TAC[REAL_DIV_LMUL] THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `sin(a) pow 2` THEN ASM_REWRITE_TAC[REAL_POW_2; REAL_ENTIRE] THEN REWRITE_TAC[real_div; REAL_INV_MUL] THEN ONCE_REWRITE_TAC[REAL_ARITH `((sa * sa) * (&1 - sb2 * sa' * sa') * others = (sa * sa) * v * w * x * y * sa') = (others * (sa * sa - sb2 * (sa * sa') * (sa * sa')) = sa * v * w * x * y * sa * sa')`] THEN ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_LID; REAL_MUL_RID] THEN SUBGOAL_THEN `sin(a - b) * cos(a + b) + sin(a + b) * cos(a - b) = sin(&2 * a)` SUBST1_TAC THENL [GEN_REWRITE_TAC (LAND_CONV o RAND_CONV) [REAL_MUL_SYM] THEN REWRITE_TAC[GSYM SIN_ADD] THEN AP_TERM_TAC THEN REAL_ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[SIN_DOUBLE] THEN GEN_REWRITE_TAC RAND_CONV [REAL_ARITH `sa * samb * sapb * &2 * ca = (&2 * sa * ca) * samb * sapb`] THEN AP_TERM_TAC THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[SIN_SUMDIFF_LEMMA] THEN REAL_ARITH_TAC);; let SIN_LINEAR_ABOVE = prove (`!x. abs(x) < &1 ==> abs(sin x) <= &2 * abs(x)`, REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`; `2`] MCLAURIN_SIN) THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[real_pow; REAL_POW_1] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_DIV_1; REAL_MUL_LID; REAL_POW_1; REAL_ADD_LID] THEN MATCH_MP_TAC(REAL_ARITH `abs(a) <= abs(x) ==> abs(s - x) <= a ==> abs(s) <= &2 * abs(x)`) THEN REWRITE_TAC[REAL_POW_2; REAL_MUL_ASSOC; REAL_ABS_MUL] THEN REWRITE_TAC[REAL_ABS_ABS] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&1 / &2 * &1` THEN CONJ_TAC THENL [ALL_TAC; CONV_TAC REAL_RAT_REDUCE_CONV] THEN MATCH_MP_TAC REAL_LE_LMUL THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN CONV_TAC REAL_RAT_REDUCE_CONV);; let SIN_LINEAR_BELOW = prove (`!x. abs(x) < &2 ==> abs(sin x) >= abs(x) / &3`, REPEAT STRIP_TAC THEN MP_TAC(SPECL [`x:real`; `3`] MCLAURIN_SIN) THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[real_pow; REAL_POW_1] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_DIV_1; REAL_MUL_LID; REAL_POW_1; REAL_ADD_LID] THEN REWRITE_TAC[REAL_MUL_LZERO; REAL_ADD_RID] THEN SIMP_TAC[real_ge; REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN MATCH_MP_TAC(REAL_ARITH `&3 * abs(a) <= &2 * abs(x) ==> abs(s - x) <= a ==> abs(x) <= abs(s) * &3`) THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_ABS; REAL_MUL_ASSOC] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN CONV_TAC(LAND_CONV(RAND_CONV(RAND_CONV num_CONV))) THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[real_pow; GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_LE_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN REWRITE_TAC[GSYM REAL_POW_2] THEN MATCH_MP_TAC REAL_POW_LE2 THEN ASM_SIMP_TAC[REAL_ABS_POS; REAL_LT_IMP_LE]);; let KNOPP_TERM_BOUND_LEMMA = prove (`~(integer x) /\ k < 2 EXP n /\ &6 * abs(x) < &k ==> abs(a / (&1 - sin(pi * &k / &2 pow (n + 1)) pow 2 / sin(pi * x / &2 pow (n + 1)) pow 2)) <= abs(a) / ((&k / (&6 * x)) pow 2 - &1)`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL [UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `(~b ==> ~a) = (a ==> b)`] THEN SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]; ALL_TAC] THEN REWRITE_TAC[REAL_ABS_DIV] THEN ONCE_REWRITE_TAC[real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_INV2 THEN CONJ_TAC THENL [REWRITE_TAC[REAL_SUB_LT] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_MUL; REAL_ABS_NUM] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN REWRITE_TAC[GSYM REAL_POW_2] THEN MATCH_MP_TAC REAL_POW_LT2 THEN REWRITE_TAC[REAL_OF_NUM_LE; ARITH] THEN UNDISCH_TAC `&6 * abs(x) < &k` THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV) [GSYM REAL_MUL_LID] THEN MATCH_MP_TAC(TAUT `(b = a) ==> a ==> b`) THEN MATCH_MP_TAC REAL_LT_RDIV_EQ THEN ASM_SIMP_TAC[REAL_LT_MUL; REAL_OF_NUM_LT; ARITH; GSYM REAL_ABS_NZ]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ x <= y ==> x - &1 <= abs(&1 - y)`) THEN CONJ_TAC THENL [REWRITE_TAC[REAL_POW_2; REAL_LE_SQUARE]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_POW_DIV] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `(abs(pi * &k / &2 pow (n + 1)) / &3) * inv(&2 * abs(pi * x / &2 pow (n + 1)))` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_MUL; REAL_ABS_POW; REAL_ABS_NUM] THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_INV_MUL] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `p * k * q' * k1 * k2 * p' * x' * q = k * (k1 * k2) * x' * (p * p') * (q * q')`] THEN SIMP_TAC[REAL_INV_INV; REAL_MUL_RINV; REAL_ABS_ZERO; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES; PI_POS] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_RID; REAL_LE_REFL]; ALL_TAC] THEN GEN_REWRITE_TAC RAND_CONV [REAL_ABS_DIV] THEN GEN_REWRITE_TAC RAND_CONV [real_div] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN SIMP_TAC[REAL_LE_INV_EQ; REAL_LE_DIV; REAL_LE_MUL; REAL_ABS_POS; REAL_POS] THEN CONJ_TAC THENL [REWRITE_TAC[GSYM real_ge] THEN MATCH_MP_TAC SIN_LINEAR_BELOW THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM; REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN SIMP_TAC[real_abs; REAL_LT_IMP_LE; PI_POS] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `pi * &2 pow n` THEN CONJ_TAC THENL [ASM_SIMP_TAC[REAL_LT_LMUL_EQ; PI_POS; REAL_OF_NUM_POW; REAL_OF_NUM_LT]; ALL_TAC] THEN ONCE_REWRITE_TAC[ADD_SYM] THEN REWRITE_TAC[REAL_POW_ADD; REAL_MUL_ASSOC] THEN SIMP_TAC[REAL_LE_RMUL_EQ; REAL_POW2_CLAUSES] THEN MATCH_MP_TAC(C MATCH_MP PI_APPROX_225_BITS (REAL_ARITH `abs(p - y) <= e ==> y + e <= a ==> p <= a`)) THEN CONV_TAC REAL_RAT_REDUCE_CONV; MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[GSYM REAL_ABS_NZ; SIN_ZERO_LEMMA] THEN ASM_SIMP_TAC[NOT_INTEGER_DIV_POW2] THEN MATCH_MP_TAC SIN_LINEAR_ABOVE THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM; REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN REWRITE_TAC[REAL_MUL_LID] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN MATCH_MP_TAC REAL_LT_LCANCEL_IMP THEN EXISTS_TAC `abs(&6)` THEN CONV_TAC (LAND_CONV REAL_RAT_REDUCE_CONV) THEN REWRITE_TAC[GSYM REAL_ABS_MUL; REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `abs(&k * pi)` THEN CONJ_TAC THENL [ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LT_RMUL THEN ASM_REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN SIMP_TAC[PI_POS; REAL_ARITH `&0 < x ==> &0 < abs x`]; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(&2 pow n * pi)` THEN CONJ_TAC THENL [ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_NUM; REAL_OF_NUM_POW; REAL_OF_NUM_LE] THEN ASM_SIMP_TAC[LT_IMP_LE]; ALL_TAC] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN REWRITE_TAC[REAL_POW_ADD; REAL_ABS_POW; REAL_ABS_NUM; REAL_ABS_MUL; GSYM REAL_MUL_ASSOC] THEN SIMP_TAC[REAL_LE_LMUL_EQ; REAL_POW2_CLAUSES] THEN MATCH_MP_TAC(C MATCH_MP PI_APPROX_225_BITS (REAL_ARITH `abs(p - y) <= e ==> abs y + e <= a ==> abs p <= a`)) THEN CONV_TAC REAL_RAT_REDUCE_CONV]);; let KNOPP_TERM_BOUND = prove (`~(integer x) /\ k < 2 EXP n /\ &6 * abs(x) < &k ==> abs((cot(pi * (x + &k) / &2 pow (n + 1)) + cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1)) <= abs(cot(pi * x / &2 pow (n + 1)) / &2 pow n) * (&36 * x pow 2) / (&k pow 2 - &36 * x pow 2)`, REPEAT STRIP_TAC THEN ASM_SIMP_TAC[KNOPP_TERM_EQUIVALENT] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(cot(pi * x / &2 pow (n + 1)) / &2 pow n) / ((&k / (&6 * x)) pow 2 - &1)` THEN ASM_SIMP_TAC[KNOPP_TERM_BOUND_LEMMA] THEN GEN_REWRITE_TAC LAND_CONV [real_div] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_EQ_IMP_LE THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_INV_DIV] THEN AP_TERM_TAC THEN SUBST1_TAC(SYM(REAL_RAT_REDUCE_CONV `&6 pow 2`)) THEN REWRITE_TAC[GSYM REAL_POW_MUL] THEN REWRITE_TAC[REAL_POW_DIV] THEN SUBGOAL_THEN `&0 < (&6 * x) pow 2` (fun th -> SIMP_TAC[th; REAL_EQ_RDIV_EQ; REAL_SUB_RDISTRIB; REAL_MUL_LID; REAL_DIV_RMUL; REAL_LT_IMP_NZ]) THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN MATCH_MP_TAC REAL_POW_LT THEN REWRITE_TAC[GSYM REAL_ABS_NZ; REAL_ENTIRE; REAL_OF_NUM_EQ; ARITH_EQ] THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `(~b ==> ~a) = (a ==> b)`] THEN SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]);; (* ------------------------------------------------------------------------- *) (* Show that the series we're looking at do in fact converge... *) (* ------------------------------------------------------------------------- *) let SUMMABLE_INVERSE_SQUARES_LEMMA = prove (`(\n. inv(&(n + 1) * &(n + 2))) sums &1`, REWRITE_TAC[sums] THEN SUBGOAL_THEN `!n. Sum(0,n) (\m. inv(&(m + 1) * &(m + 2))) = &1 - inv(&(n + 1))` (fun th -> REWRITE_TAC[th]) THENL [INDUCT_TAC THEN REWRITE_TAC[Sum] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN ASM_REWRITE_TAC[ADD_CLAUSES] THEN REWRITE_TAC[REAL_ARITH `(&1 - a + b = &1 - c) = (b + c = a)`] THEN CONV_TAC SYM_CONV THEN MATCH_MP_TAC REAL_MUL_LINV_UNIQ THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_INV_MUL; REAL_MUL_ASSOC; REAL_ADD_LDISTRIB] THEN SIMP_TAC[REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_RULE `~(n + 1 = 0)`] THEN REWRITE_TAC[REAL_MUL_LID; ARITH_RULE `SUC(n + 1) = n + 2`] THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&(n + 2)` THEN SIMP_TAC[REAL_ADD_RDISTRIB; real_div; GSYM REAL_MUL_ASSOC; REAL_OF_NUM_EQ; REAL_MUL_LINV; ARITH_RULE `~(n + 2 = 0)`; REAL_MUL_LID; REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN ARITH_TAC; ALL_TAC] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_SUB_RZERO] THEN MATCH_MP_TAC SEQ_SUB THEN REWRITE_TAC[SEQ_CONST] THEN MATCH_MP_TAC SEQ_INV0 THEN X_GEN_TAC `x:real` THEN X_CHOOSE_TAC `N:num` (SPEC `x:real` REAL_ARCH_SIMPLE) THEN EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[real_gt; GE] THEN DISCH_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[] THEN ASM_SIMP_TAC[REAL_OF_NUM_LT; ARITH_RULE `a < b + 1 = a <= b`]);; let SUMMABLE_INVERSE_SQUARES = prove (`summable (\n. inv(&n pow 2))`, MATCH_MP_TAC SUM_SUMMABLE THEN EXISTS_TAC `Sum(0,2) (\n. inv(&n pow 2)) + suminf (\n. inv(&(n + 2) pow 2))` THEN MATCH_MP_TAC SER_OFFSET_REV THEN MATCH_MP_TAC SER_ACONV THEN MATCH_MP_TAC SER_COMPARA THEN EXISTS_TAC `\n. inv(&(n + 1) * &(n + 2))` THEN CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC SUM_SUMMABLE THEN EXISTS_TAC `&1` THEN REWRITE_TAC[SUMMABLE_INVERSE_SQUARES_LEMMA]] THEN EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[REAL_POW_2; REAL_INV_MUL; REAL_ABS_INV; REAL_ABS_NUM; REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_RMUL THEN REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC);; let SUMMABLE_INVERSE_POWERS = prove (`!m. 2 <= m ==> summable (\n. inv(&(n + 1) pow m))`, REPEAT STRIP_TAC THEN MATCH_MP_TAC SER_COMPAR THEN EXISTS_TAC `\m. inv (&(m + 1) pow 2)` THEN CONJ_TAC THENL [EXISTS_TAC `0` THEN X_GEN_TAC `n:num` THEN DISCH_THEN(K ALL_TAC) THEN REWRITE_TAC[REAL_ABS_INV; REAL_ABS_POW; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LE_INV2 THEN SIMP_TAC[REAL_POW_LT; REAL_OF_NUM_LT; ARITH_RULE `0 < n + 1`] THEN MATCH_MP_TAC REAL_POW_MONO THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC; REWRITE_TAC[summable] THEN EXISTS_TAC `suminf (\m. inv (&m pow 2)) - Sum(0,1) (\m. inv (&m pow 2))` THEN MATCH_MP_TAC(REWRITE_RULE[RIGHT_IMP_FORALL_THM] SER_OFFSET) THEN REWRITE_TAC[SUMMABLE_INVERSE_SQUARES]]);; let COT_TYPE_SERIES_CONVERGES = prove (`!x. ~(integer x) ==> summable (\n. inv(&n pow 2 - x))`, REPEAT STRIP_TAC THEN MATCH_MP_TAC SER_ACONV THEN MATCH_MP_TAC SER_COMPARA THEN EXISTS_TAC `\n. &2 / &n pow 2` THEN CONJ_TAC THENL [ALL_TAC; MATCH_MP_TAC SUM_SUMMABLE THEN EXISTS_TAC `&2 * suminf (\n. inv(&n pow 2))` THEN REWRITE_TAC[real_div] THEN MATCH_MP_TAC SER_CMUL THEN MATCH_MP_TAC SUMMABLE_SUM THEN REWRITE_TAC[SUMMABLE_INVERSE_SQUARES]] THEN MP_TAC(SPEC `&2 * abs x + &1` REAL_ARCH_SIMPLE) THEN DISCH_THEN(X_CHOOSE_TAC `N:num`) THEN EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN SUBGOAL_THEN `&0 < &n pow 2` (fun th -> SIMP_TAC[th; REAL_LE_RDIV_EQ]) THENL [MATCH_MP_TAC REAL_POW_LT THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN UNDISCH_TAC `&2 * abs x + &1 <= &N` THEN REAL_ARITH_TAC; ALL_TAC] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN REWRITE_TAC[REAL_ABS_INV] THEN REWRITE_TAC[GSYM real_div] THEN SUBGOAL_THEN `&0 < abs(&n pow 2 - x)` (fun th -> SIMP_TAC[REAL_LE_LDIV_EQ; th]) THENL [REWRITE_TAC[GSYM REAL_ABS_NZ] THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN DISCH_TAC THEN SUBST1_TAC(REAL_ARITH `x = &n pow 2 - (&n pow 2 - x)`) THEN ASM_REWRITE_TAC[REAL_SUB_RZERO] THEN SIMP_TAC[integer; REAL_INTEGER_CLOSURES]; ALL_TAC] THEN MATCH_MP_TAC(REAL_ARITH `&2 * abs(x) + &1 <= a ==> a <= &2 * abs(a - x)`) THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&N pow 2` THEN CONJ_TAC THENL [REWRITE_TAC[REAL_OF_NUM_POW; REAL_OF_NUM_LE; EXP_2; LE_SQUARE_REFL]; ASM_SIMP_TAC[REAL_POW_LE2; REAL_OF_NUM_LE; LE_0]]);; (* ------------------------------------------------------------------------- *) (* Now the rather tricky limiting argument gives the result. *) (* ------------------------------------------------------------------------- *) let SIN_X_RANGE = prove (`!x. abs(sin(x) - x) <= abs(x) pow 2 / &2`, GEN_TAC THEN MP_TAC(SPECL [`x:real`; `2`] MCLAURIN_SIN) THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[ARITH; REAL_MUL_LZERO; REAL_ADD_LID; REAL_ADD_RID] THEN CONV_TAC NUM_REDUCE_CONV THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_DIV_1; REAL_POW_1; REAL_MUL_LID] THEN REWRITE_TAC[real_div; REAL_MUL_LID] THEN REWRITE_TAC[REAL_MUL_AC]);; let SIN_X_X_RANGE = prove (`!x. ~(x = &0) ==> abs(sin(x) / x - &1) <= abs(x) / &2`, REPEAT STRIP_TAC THEN MATCH_MP_TAC REAL_LE_LCANCEL_IMP THEN EXISTS_TAC `abs(x)` THEN ASM_REWRITE_TAC[GSYM REAL_ABS_MUL; GSYM REAL_ABS_NZ] THEN ASM_SIMP_TAC[REAL_SUB_LDISTRIB; REAL_DIV_LMUL] THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC; REAL_MUL_RID] THEN REWRITE_TAC[GSYM REAL_POW_2; SIN_X_RANGE; GSYM real_div]);; let SIN_X_LIMIT = prove (`((\x. sin(x) / x) tends_real_real &1)(&0)`, REWRITE_TAC[LIM] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN REWRITE_TAC[REAL_SUB_RZERO] THEN EXISTS_TAC `e:real` THEN ASM_REWRITE_TAC[] THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs(x) / &2` THEN ASM_SIMP_TAC[SIN_X_X_RANGE; REAL_ABS_NZ] THEN ASM_SIMP_TAC[REAL_LT_LDIV_EQ; REAL_OF_NUM_LT; ARITH] THEN UNDISCH_TAC `abs(x) < e` THEN REAL_ARITH_TAC);; let COT_X_LIMIT = prove (`((\x. x * cot(x)) tends_real_real &1)(&0)`, SUBGOAL_THEN `(cos tends_real_real &1)(&0)` MP_TAC THENL [MP_TAC(SPEC `&0` DIFF_COS) THEN DISCH_THEN(MP_TAC o MATCH_MP DIFF_CONT) THEN REWRITE_TAC[contl; REAL_ADD_LID; COS_0] THEN CONV_TAC(ONCE_DEPTH_CONV ETA_CONV) THEN REWRITE_TAC[]; ALL_TAC] THEN DISCH_THEN(MP_TAC o C CONJ SIN_X_LIMIT) THEN DISCH_THEN(MP_TAC o C CONJ (REAL_ARITH `~(&1 = &0)`)) THEN REWRITE_TAC[GSYM CONJ_ASSOC] THEN DISCH_THEN(MP_TAC o MATCH_MP LIM_DIV) THEN REWRITE_TAC[REAL_DIV_1; cot] THEN REWRITE_TAC[real_div; REAL_INV_MUL; REAL_MUL_AC; REAL_INV_INV]);; let COT_LIMIT_LEMMA = prove (`!x. ~(x = &0) ==> (\n. (x / &2 pow n) * cot(x / &2 pow n)) tends_num_real &1`, GEN_TAC THEN DISCH_TAC THEN REWRITE_TAC[SEQ] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN MP_TAC COT_X_LIMIT THEN REWRITE_TAC[LIM] THEN DISCH_THEN(MP_TAC o SPEC `e:real`) THEN ASM_REWRITE_TAC[] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` MP_TAC) THEN DISCH_THEN(CONJUNCTS_THEN2 ASSUME_TAC MP_TAC) THEN REWRITE_TAC[REAL_SUB_RZERO] THEN DISCH_TAC THEN X_CHOOSE_TAC `N:num` (SPEC `abs(x) / d` REAL_ARCH_POW2) THEN EXISTS_TAC `N:num` THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN FIRST_ASSUM MATCH_MP_TAC THEN REWRITE_TAC[REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM] THEN ASM_SIMP_TAC[REAL_POW2_CLAUSES; REAL_LT_DIV; GSYM REAL_ABS_NZ] THEN SIMP_TAC[REAL_LT_LDIV_EQ; REAL_POW2_CLAUSES] THEN ONCE_REWRITE_TAC[REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&2 pow N` THEN ASM_REWRITE_TAC[REAL_POW2_THM]);; let COT_LIMIT_LEMMA1 = prove (`~(x = &0) ==> (\n. (pi / &2 pow (n + 1)) * cot(pi * x / &2 pow (n + 1))) tends_num_real (inv(x))`, DISCH_TAC THEN MP_TAC(SPEC `pi * x * inv(&2)` COT_LIMIT_LEMMA) THEN ASM_SIMP_TAC[REAL_ENTIRE; REAL_LT_IMP_NZ; PI_POS] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[real_div; REAL_MUL_LID; GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `p * x * a * b * c = x * (p * (a * b)) * c`] THEN REWRITE_TAC[GSYM REAL_INV_MUL] THEN REWRITE_TAC[GSYM(CONJUNCT2 real_pow)] THEN REWRITE_TAC[ADD1; GSYM real_div] THEN DISCH_TAC THEN GEN_REWRITE_TAC (LAND_CONV o BINDER_CONV) [GSYM REAL_MUL_LID] THEN FIRST_ASSUM(SUBST1_TAC o GSYM o MATCH_MP REAL_MUL_LINV) THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN GEN_REWRITE_TAC RAND_CONV [GSYM REAL_MUL_RID] THEN MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `x * p * q * c = x * (p * q) * c`] THEN ASM_REWRITE_TAC[GSYM real_div]);; let COT_X_BOUND_LEMMA_POS = prove (`?M. !x. &0 < x /\ abs(x) <= &1 ==> abs(x * cot(x)) <= M`, MP_TAC COT_X_LIMIT THEN REWRITE_TAC[LIM] THEN DISCH_THEN(MP_TAC o SPEC `&1`) THEN REWRITE_TAC[REAL_LT_01] THEN REWRITE_TAC[REAL_SUB_RZERO] THEN DISCH_THEN(X_CHOOSE_THEN `d:real` STRIP_ASSUME_TAC) THEN MP_TAC(SPECL [`\x. x * cot(x)`; `d:real`; `&1`] CONT_BOUNDED_ABS) THEN W(C SUBGOAL_THEN (fun th -> REWRITE_TAC[th]) o funpow 2 lhand o snd) THENL [X_GEN_TAC `x:real` THEN STRIP_TAC THEN MATCH_MP_TAC CONT_MUL THEN CONJ_TAC THENL [MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC `&1` THEN REWRITE_TAC[DIFF_X]; ALL_TAC] THEN GEN_REWRITE_TAC LAND_CONV [GSYM ETA_AX] THEN REWRITE_TAC[cot] THEN MATCH_MP_TAC CONT_DIV THEN REPEAT CONJ_TAC THENL [MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC `--(sin x)` THEN REWRITE_TAC[DIFF_COS]; MATCH_MP_TAC DIFF_CONT THEN EXISTS_TAC `cos x` THEN REWRITE_TAC[DIFF_SIN]; MATCH_MP_TAC REAL_LT_IMP_NZ THEN MATCH_MP_TAC SIN_POS_PI THEN SUBGOAL_THEN `&1 < pi` (fun th -> ASM_MESON_TAC[th; REAL_LET_TRANS; REAL_LTE_TRANS]) THEN MP_TAC PI_APPROX_225_BITS THEN MATCH_MP_TAC(REAL_ARITH `&1 + e < a ==> abs(p - a) <= e ==> &1 < p`) THEN CONV_TAC REAL_RAT_REDUCE_CONV]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_TAC `M:real`) THEN EXISTS_TAC `abs M + &2` THEN X_GEN_TAC `x:real` THEN STRIP_TAC THEN DISJ_CASES_TAC(SPECL [`abs x`; `d:real`] REAL_LTE_TOTAL) THENL [MATCH_MP_TAC(REAL_ARITH `abs(x - &1) < &1 ==> abs(x) <= abs(m) + &2`) THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`]; MATCH_MP_TAC(REAL_ARITH `x <= m ==> x <= abs(m) + &2`) THEN FIRST_ASSUM MATCH_MP_TAC THEN MAP_EVERY UNDISCH_TAC [`&0 < x`; `abs(x) <= &1`; `d <= abs(x)`] THEN REAL_ARITH_TAC]);; let COT_X_BOUND_LEMMA = prove (`?M. !x. ~(x = &0) /\ abs(x) <= &1 ==> abs(x * cot(x)) <= M`, X_CHOOSE_TAC `M:real` COT_X_BOUND_LEMMA_POS THEN EXISTS_TAC `M:real` THEN X_GEN_TAC `x:real` THEN REPEAT STRIP_TAC THEN FIRST_ASSUM(DISJ_CASES_TAC o MATCH_MP (REAL_ARITH `~(x = &0) ==> &0 < x \/ &0 < --x`)) THEN ASM_SIMP_TAC[] THEN SUBGOAL_THEN `x * cot(x) = --x * cot(--x)` SUBST1_TAC THENL [ALL_TAC; ASM_SIMP_TAC[REAL_ABS_NEG]] THEN REWRITE_TAC[cot; SIN_NEG; COS_NEG; real_div; REAL_INV_NEG; REAL_MUL_LNEG; REAL_MUL_RNEG; REAL_NEG_NEG]);; let COT_PARTIAL_FRACTIONS = prove (`~(integer x) ==> (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2)) sums ((pi * x) * cot(pi * x) + &1)`, REPEAT STRIP_TAC THEN SUBGOAL_THEN `~(x = &0)` ASSUME_TAC THENL [UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `(~b ==> ~a) = (a ==> b)`] THEN SIMP_TAC[integer; REAL_ABS_NUM; REAL_OF_NUM_EQ; GSYM EXISTS_REFL]; ALL_TAC] THEN ABBREV_TAC `A = \n k. (pi * x / &2 pow n) * cot(pi * x / &2 pow n) + (pi * x / &2 pow (n + 1)) * Sum(1,k) (\m. cot (pi * (x + &m) / &2 pow (n + 1)) + cot (pi * (x - &m) / &2 pow (n + 1)))` THEN ABBREV_TAC `B = \n k. (pi * x / &2 pow (n + 1)) * Sum(k + 1,2 EXP n - 1 - k) (\m. cot(pi * (x + &m) / &2 pow (n + 1)) + cot(pi * (x - &m) / &2 pow (n + 1)))` THEN SUBGOAL_THEN `!n. ~(x - &n = &0)` ASSUME_TAC THENL [X_GEN_TAC `n:num` THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN DISCH_TAC THEN SUBGOAL_THEN `x = (x - &n) + &n` SUBST1_TAC THENL [REAL_ARITH_TAC; ASM_SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; ALL_TAC] THEN SUBGOAL_THEN `!n. ~(x + &n = &0)` ASSUME_TAC THENL [X_GEN_TAC `n:num` THEN UNDISCH_TAC `~(integer x)` THEN REWRITE_TAC[TAUT `~a ==> ~b = b ==> a`] THEN DISCH_TAC THEN SUBGOAL_THEN `x = (x + &n) - &n` SUBST1_TAC THENL [REAL_ARITH_TAC; ASM_SIMP_TAC[integer; REAL_INTEGER_CLOSURES]]; ALL_TAC] THEN SUBGOAL_THEN `!n. ~(x pow 2 - &n pow 2 = &0)` ASSUME_TAC THENL [GEN_TAC THEN REWRITE_TAC[REAL_POW_2] THEN ONCE_REWRITE_TAC[REAL_ARITH `a * a - b * b = (a + b) * (a - b)`] THEN ASM_REWRITE_TAC[REAL_ENTIRE; DE_MORGAN_THM]; ALL_TAC] THEN SUBGOAL_THEN `!n. (&2 * x) / (x pow 2 - &n pow 2) = inv(x + &n) + inv(x - &n)` ASSUME_TAC THENL [X_GEN_TAC `n:num` THEN MATCH_MP_TAC REAL_EQ_LCANCEL_IMP THEN EXISTS_TAC `x pow 2 - &n pow 2` THEN ASM_SIMP_TAC[REAL_DIV_LMUL] THEN REWRITE_TAC[REAL_POW_2; REAL_ADD_LDISTRIB] THEN ONCE_REWRITE_TAC[REAL_ARITH `a * a - b * b = (a + b) * (a - b)`] THEN ONCE_REWRITE_TAC[REAL_ARITH `(p * m) * p' + (p * m) * m' = m * p * p' + p * m * m'`] THEN ASM_SIMP_TAC[REAL_MUL_RINV; REAL_MUL_RID] THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `!k. (\n. A n k) tends_num_real (&1 + Sum(1,k) (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2)))` ASSUME_TAC THENL [X_GEN_TAC `k:num` THEN EXPAND_TAC "A" THEN REWRITE_TAC[] THEN MATCH_MP_TAC SEQ_ADD THEN CONJ_TAC THENL [REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC COT_LIMIT_LEMMA THEN ASM_SIMP_TAC[REAL_ENTIRE; PI_POS; REAL_LT_IMP_NZ]; ALL_TAC] THEN REWRITE_TAC[GSYM SUM_CMUL] THEN MATCH_MP_TAC SEQ_SUM THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[REAL_POW_2; real_div] THEN ONCE_REWRITE_TAC[REAL_ARITH `(&2 * x * x) * d = x * (&2 * x) * d`] THEN REWRITE_TAC[GSYM REAL_POW_2; GSYM real_div] THEN ASM_REWRITE_TAC[] THEN REWRITE_TAC[REAL_ADD_LDISTRIB] THEN MATCH_MP_TAC SEQ_ADD THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[REAL_ARITH `(p * x * d) * cc = x * (p * d) * cc`] THEN CONJ_TAC THEN MATCH_MP_TAC SEQ_MUL THEN REWRITE_TAC[SEQ_CONST] THEN REWRITE_TAC[GSYM real_div] THEN ASM_SIMP_TAC[COT_LIMIT_LEMMA1]; ALL_TAC] THEN SUBGOAL_THEN `!k n. &6 * abs(x) < &k ==> abs(B n k) <= abs((pi * x / &2 pow (n + 1)) * cot(pi * x / &2 pow (n + 1))) * Sum(k + 1,2 EXP n - 1 - k) (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2))` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN EXPAND_TAC "B" THEN REWRITE_TAC[GSYM SUM_CMUL] THEN W(fun (asl,w) -> MP_TAC(PART_MATCH lhand SUM_ABS_LE (lhand w))) THEN MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN REWRITE_TAC[ARITH_RULE `k + 1 <= r /\ r < (p - 1 - k) + k + 1 = k < r /\ r < p`] THEN STRIP_TAC THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LE_RCANCEL_IMP THEN EXISTS_TAC `abs(inv(&2 pow (n + 1)))` THEN REWRITE_TAC[GSYM REAL_ABS_MUL] THEN REWRITE_TAC[GSYM real_div] THEN SIMP_TAC[REAL_ARITH `&0 < x ==> &0 < abs(x)`; REAL_LT_INV_EQ; REAL_POW2_CLAUSES] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `abs(cot (pi * x / &2 pow (n + 1)) / &2 pow n) * (&36 * x pow 2) / (&r pow 2 - &36 * x pow 2)` THEN CONJ_TAC THENL [MATCH_MP_TAC KNOPP_TERM_BOUND THEN ASM_REWRITE_TAC[] THEN MATCH_MP_TAC REAL_LT_TRANS THEN EXISTS_TAC `&k` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LT]; ALL_TAC] THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; REAL_POW_ADD; REAL_ABS_MUL; REAL_INV_MUL] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_ABS_POS] THEN GEN_REWRITE_TAC RAND_CONV [AC REAL_MUL_AC `a * b * c * d * e = b * c * d * a * e`] THEN CONV_TAC REAL_RAT_REDUCE_CONV THEN REWRITE_TAC[REAL_MUL_AC; REAL_LE_REFL]; ALL_TAC] THEN SUBGOAL_THEN `!e. &0 < e ==> ?N. !n k:num. N <= k /\ pi * abs(x) <= &2 pow (n + 1) ==> abs(B n k) < e` ASSUME_TAC THENL [X_CHOOSE_TAC `Bd:real` COT_X_BOUND_LEMMA THEN SUBGOAL_THEN `!k n. &9 * abs x < &k ==> abs(Sum(k + 1,2 EXP n - 1 - k) (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2))) <= &144 * x pow 2 / &k` ASSUME_TAC THENL [REPEAT STRIP_TAC THEN REWRITE_TAC[real_div; SUM_CMUL] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM; REAL_ABS_POW; REAL_POW2_ABS] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ONCE_REWRITE_TAC[REAL_ARITH `&144 * x * y = &72 * x * &2 * y`] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_LE_SQUARE; REAL_POW_2] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&2 * Sum(k + 1,2 EXP n - 1 - k) (\m. inv(&m * &m))` THEN CONJ_TAC THENL [REWRITE_TAC[GSYM SUM_CMUL] THEN W(fun (asl,w) -> MP_TAC(PART_MATCH lhand SUM_ABS_LE (lhand w))) THEN MATCH_MP_TAC(REAL_ARITH `a <= b ==> x <= a ==> x <= b`) THEN MATCH_MP_TAC SUM_LE THEN X_GEN_TAC `r:num` THEN STRIP_TAC THEN REWRITE_TAC[] THEN SUBGOAL_THEN `&0 < &r * &r - &36 * x * x` ASSUME_TAC THENL [REWRITE_TAC[GSYM REAL_POW_2] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN REWRITE_TAC[REAL_POW_2] THEN REWRITE_TAC[REAL_ARITH `&0 < r * r - &36 * x * x = (&6 * x) * (&6 * x) < r * r`] THEN MATCH_MP_TAC REAL_LT_MUL2 THEN SIMP_TAC[REAL_LE_MUL; REAL_POS; REAL_ABS_POS] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&k` THEN ASM_REWRITE_TAC[REAL_ABS_NUM] THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN ASM_SIMP_TAC[REAL_ARITH `&9 * abs(x) < a ==> &6 * abs(x) < a`] THEN UNDISCH_TAC `k + 1 <= r` THEN ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[real_abs; REAL_LT_IMP_LE; REAL_LE_INV_EQ] THEN GEN_REWRITE_TAC LAND_CONV [GSYM REAL_MUL_LID] THEN ASM_SIMP_TAC[GSYM real_div; REAL_LE_LDIV_EQ] THEN REWRITE_TAC[real_div] THEN ONCE_REWRITE_TAC[AC REAL_MUL_AC `(a * b) * c = (a * c) * b`] THEN REWRITE_TAC[GSYM real_div] THEN SUBGOAL_THEN `&0 < &r` ASSUME_TAC THENL [UNDISCH_TAC `k + 1 <= r` THEN REWRITE_TAC[REAL_OF_NUM_LT] THEN ARITH_TAC; ALL_TAC] THEN ASM_SIMP_TAC[REAL_LE_RDIV_EQ; REAL_LT_MUL] THEN REWRITE_TAC[REAL_ARITH `&1 * x <= &2 * (x - y) = &2 * y <= x`] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= x /\ &81 * x <= y ==> &2 * &36 * x <= y`) THEN REWRITE_TAC[REAL_LE_SQUARE] THEN REWRITE_TAC[REAL_ARITH `&81 * x * x = (&9 * x) * (&9 * x)`] THEN REWRITE_TAC[GSYM REAL_POW_2] THEN ONCE_REWRITE_TAC[GSYM REAL_POW2_ABS] THEN MATCH_MP_TAC REAL_POW_LE2 THEN REWRITE_TAC[REAL_ABS_POS] THEN REWRITE_TAC[REAL_ABS_MUL; REAL_ABS_NUM] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `&k` THEN ASM_SIMP_TAC[REAL_LT_IMP_LE] THEN UNDISCH_TAC `k + 1 <= r` THEN REWRITE_TAC[REAL_OF_NUM_LE] THEN ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LE_LMUL THEN REWRITE_TAC[REAL_POS] THEN REWRITE_TAC[SUM_REINDEX] THEN SUBGOAL_THEN `?d. k = 1 + d` (CHOOSE_THEN SUBST1_TAC) THENL [REWRITE_TAC[GSYM LE_EXISTS] THEN MATCH_MP_TAC(ARITH_RULE `0 < k ==> 1 <= k`) THEN REWRITE_TAC[GSYM REAL_OF_NUM_LT] THEN UNDISCH_TAC `&9 * abs(x) < &k` THEN REAL_ARITH_TAC; ALL_TAC] THEN SPEC_TAC(`2 EXP n - 1 - (1 + d)`,`n:num`) THEN POP_ASSUM_LIST(K ALL_TAC) THEN GEN_TAC THEN GEN_REWRITE_TAC (LAND_CONV o LAND_CONV o LAND_CONV) [ADD_SYM] THEN REWRITE_TAC[SUM_REINDEX] THEN REWRITE_TAC[ARITH_RULE `(r + 1) + 1 = r + 2`] THEN MATCH_MP_TAC REAL_LE_TRANS THEN EXISTS_TAC `Sum(d,n) (\r. inv(&(r + 1) * &(r + 2)))` THEN CONJ_TAC THENL [MATCH_MP_TAC SUM_LE THEN REPEAT STRIP_TAC THEN SIMP_TAC[REAL_LE_RMUL_EQ; REAL_LT_INV_EQ; REAL_OF_NUM_LT; REAL_INV_MUL; ARITH_RULE `0 < n + 2`] THEN MATCH_MP_TAC REAL_LE_INV2 THEN REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_LE] THEN ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `!n. Sum(d,n) (\r. inv (&(r + 1) * &(r + 2))) = inv(&(d + 1)) - inv(&(d + n + 1))` (fun th -> REWRITE_TAC[th]) THENL [INDUCT_TAC THEN REWRITE_TAC[Sum; ADD_CLAUSES; REAL_SUB_REFL] THEN ASM_REWRITE_TAC[REAL_ARITH `((a - x) + y = a - z) = (y + z = x)`] THEN REWRITE_TAC[GSYM ADD_ASSOC; REAL_INV_MUL; ARITH_RULE `SUC(d + n + 1) = d + n + 2`] THEN MATCH_MP_TAC REAL_EQ_RCANCEL_IMP THEN EXISTS_TAC `&(d + n + 1) * &(d + n + 2)` THEN REWRITE_TAC[REAL_ARITH `(dn1' * dn2' + dn2') * (dn1 * dn2) = (dn1 * dn1' + dn1) * (dn2 * dn2')`] THEN SIMP_TAC[REAL_ENTIRE; REAL_MUL_RINV; REAL_OF_NUM_EQ; ARITH_RULE `~(d + n + 1 = 0) /\ ~(d + n + 2 = 0)`] THEN SIMP_TAC[REAL_MUL_ASSOC; REAL_MUL_LINV; REAL_OF_NUM_EQ; ARITH_RULE `~(d + n + 1 = 0)`] THEN REWRITE_TAC[REAL_OF_NUM_MUL; REAL_OF_NUM_ADD; REAL_OF_NUM_EQ] THEN ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[ADD_AC] THEN MATCH_MP_TAC(REAL_ARITH `&0 <= y ==> x - y <= x`) THEN REWRITE_TAC[REAL_LE_INV_EQ; REAL_POS]; ALL_TAC] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN SUBGOAL_THEN `?N. &9 * abs(x) + &1 <= &N /\ (Bd * &144 * x pow 2) / e + &1 <= &N` (X_CHOOSE_THEN `N:num` STRIP_ASSUME_TAC) THENL [X_CHOOSE_TAC `N1:num` (SPEC `&9 * abs(x) + &1` REAL_ARCH_SIMPLE) THEN X_CHOOSE_TAC `N2:num` (SPEC `(Bd * &144 * x pow 2) / e + &1` REAL_ARCH_SIMPLE) THEN EXISTS_TAC `N1 + N2:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN ASM_MESON_TAC[REAL_POS; REAL_ARITH `a <= m /\ b <= n /\ &0 <= m /\ &0 <= n ==> a <= m + n /\ b <= m + n`]; ALL_TAC] THEN EXISTS_TAC `N:num` THEN MAP_EVERY X_GEN_TAC [`n:num`; `k:num`] THEN STRIP_TAC THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `abs((pi * x / &2 pow (n + 1)) * cot (pi * x / &2 pow (n + 1))) * Sum(k + 1,2 EXP n - 1 - k) (\m. (&72 * x pow 2) / (&m pow 2 - &36 * x pow 2))` THEN CONJ_TAC THENL [FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN REAL_ARITH_TAC; ALL_TAC] THEN MATCH_MP_TAC REAL_LET_TRANS THEN EXISTS_TAC `Bd * &144 * x pow 2 / &k` THEN CONJ_TAC THENL [ALL_TAC; REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN SUBGOAL_THEN `&0 < &k` (fun th -> SIMP_TAC[REAL_LT_LDIV_EQ; th]) THENL [MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN REAL_ARITH_TAC; ALL_TAC] THEN GEN_REWRITE_TAC RAND_CONV [REAL_MUL_SYM] THEN ASM_SIMP_TAC[GSYM REAL_LT_LDIV_EQ] THEN REWRITE_TAC[real_div; REAL_MUL_ASSOC] THEN REWRITE_TAC[GSYM real_div] THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N` THEN ASM_REWRITE_TAC[GSYM REAL_MUL_ASSOC; REAL_OF_NUM_LE] THEN ASM_SIMP_TAC[REAL_ARITH `x + &1 <= y ==> x < y`]] THEN MATCH_MP_TAC(REAL_ARITH `abs(x) <= a ==> x <= a`) THEN ONCE_REWRITE_TAC[REAL_ABS_MUL] THEN MATCH_MP_TAC REAL_LE_MUL2 THEN REWRITE_TAC[REAL_ABS_POS] THEN CONJ_TAC THENL [REWRITE_TAC[REAL_ABS_ABS] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_SIMP_TAC[real_div; REAL_ENTIRE; REAL_LT_IMP_NZ; REAL_POW2_CLAUSES; REAL_MUL_ASSOC; REAL_LT_INV_EQ; PI_POS] THEN SIMP_TAC[GSYM real_div; REAL_ABS_DIV; REAL_ABS_POW; REAL_ABS_NUM] THEN SIMP_TAC[REAL_LE_LDIV_EQ; REAL_POW2_CLAUSES; REAL_MUL_LID] THEN REWRITE_TAC[REAL_ABS_MUL] THEN SIMP_TAC[real_abs; REAL_LT_IMP_LE; PI_POS] THEN ASM_REWRITE_TAC[GSYM real_abs]; ALL_TAC] THEN FIRST_ASSUM MATCH_MP_TAC THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `&N:real` THEN ASM_REWRITE_TAC[REAL_OF_NUM_LE] THEN UNDISCH_TAC `&9 * abs x + &1 <= &N` THEN REAL_ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `!n k. k < 2 EXP n ==> ((pi * x) * (cot (pi * x / &2 pow n) / &2 pow n + Sum (1,2 EXP n - 1) (\k. cot(pi * (x + &k) / &2 pow (n + 1)) + cot(pi * (x - &k) / &2 pow (n + 1))) / &2 pow (n + 1)) = A n k + B n k)` MP_TAC THENL [REPEAT GEN_TAC THEN DISCH_TAC THEN MAP_EVERY EXPAND_TAC ["A"; "B"] THEN REWRITE_TAC[GSYM REAL_ADD_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN GEN_REWRITE_TAC (funpow 3 RAND_CONV o funpow 3 LAND_CONV) [ARITH_RULE `x = 0 + x`] THEN REWRITE_TAC[SUM_REINDEX] THEN ONCE_REWRITE_TAC [REWRITE_RULE[REAL_ARITH `(a = b - c) = (c + a = b)`] SUM_DIFF] THEN ASM_SIMP_TAC[ARITH_RULE `n < p ==> (n + p - 1 - n = p - 1)`] THEN GEN_REWRITE_TAC (LAND_CONV o funpow 2 RAND_CONV o funpow 3 LAND_CONV) [ARITH_RULE `x = 0 + x`] THEN REWRITE_TAC[SUM_REINDEX] THEN REWRITE_TAC[real_div; GSYM REAL_MUL_ASSOC; GSYM REAL_ADD_LDISTRIB] THEN REWRITE_TAC[REAL_MUL_AC]; ALL_TAC] THEN FIRST_ASSUM(MP_TAC o MATCH_MP COT_HALF_KNOPP) THEN DISCH_THEN(fun th -> ONCE_REWRITE_TAC[GSYM th]) THEN DISCH_TAC THEN REWRITE_TAC[sums; SEQ] THEN X_GEN_TAC `e:real` THEN DISCH_TAC THEN UNDISCH_TAC `!e. &0 < e ==> ?N. !n k:num. N <= k /\ pi * abs(x) <= &2 pow (n + 1) ==> abs (B n k) < e` THEN DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN DISCH_THEN(X_CHOOSE_THEN `N1:num` STRIP_ASSUME_TAC) THEN EXISTS_TAC `N1 + 1` THEN X_GEN_TAC `n:num` THEN REWRITE_TAC[GE] THEN DISCH_TAC THEN UNDISCH_TAC `!k. (\n. A n k) tends_num_real &1 + Sum (1,k) (\n. (&2 * x pow 2) / (x pow 2 - &n pow 2))` THEN DISCH_THEN(MP_TAC o SPEC `n - 1`) THEN REWRITE_TAC[SEQ] THEN DISCH_THEN(MP_TAC o SPEC `e / &2`) THEN ASM_SIMP_TAC[REAL_LT_DIV; REAL_OF_NUM_LT; ARITH] THEN REWRITE_TAC[GE] THEN DISCH_THEN(X_CHOOSE_THEN `N2:num` ASSUME_TAC) THEN SUBGOAL_THEN `?m. n - 1 < 2 EXP m /\ N2 <= m /\ pi * abs(x) <= &2 pow (m + 1)` MP_TAC THENL [SUBGOAL_THEN `?m. &(n - 1) + &1 <= &m /\ &N2 <= &m /\ pi * abs(x) <= &m` MP_TAC THENL [X_CHOOSE_TAC `m1:num` (SPEC `&(n - 1) + &1` REAL_ARCH_SIMPLE) THEN X_CHOOSE_TAC `m2:num` (SPEC `&N2` REAL_ARCH_SIMPLE) THEN X_CHOOSE_TAC `m3:num` (SPEC `pi * abs(x)` REAL_ARCH_SIMPLE) THEN EXISTS_TAC `m1 + m2 + m3:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_ADD] THEN MATCH_MP_TAC(REAL_ARITH `x <= a /\ y <= b /\ z <= c /\ &0 <= a /\ &0 <= b /\ &0 <= c ==> x <= a + b + c /\ y <= a + b + c /\ z <= a + b + c`) THEN ASM_REWRITE_TAC[REAL_POS]; ALL_TAC] THEN REWRITE_TAC[GSYM REAL_OF_NUM_LT; GSYM REAL_OF_NUM_LE] THEN MATCH_MP_TAC MONO_EXISTS THEN X_GEN_TAC `m:num` THEN REWRITE_TAC[GSYM REAL_OF_NUM_POW] THEN MATCH_MP_TAC(REAL_ARITH `m <= m2 /\ m2 <= m22 ==> x1 + &1 <= m /\ x2 <= m /\ x3 <= m ==> x1 < m2 /\ x2 <= m /\ x3 <= m22`) THEN REWRITE_TAC[REAL_POW_ADD; REAL_POW_1] THEN REWRITE_TAC[REAL_ARITH `x <= x * &2 = &0 <= x`] THEN REWRITE_TAC[REAL_POW2_CLAUSES] THEN MATCH_MP_TAC REAL_LT_IMP_LE THEN REWRITE_TAC[REAL_OF_NUM_LT; REAL_OF_NUM_POW] THEN POP_ASSUM_LIST(K ALL_TAC) THEN SPEC_TAC(`m:num`,`n:num`) THEN INDUCT_TAC THEN REWRITE_TAC[EXP; ARITH] THEN MATCH_MP_TAC LTE_TRANS THEN EXISTS_TAC `SUC(2 EXP n)` THEN ASM_REWRITE_TAC[LT_SUC] THEN REWRITE_TAC[MULT_2; ADD1; LE_ADD_LCANCEL] THEN REWRITE_TAC[num_CONV `1`; LE_SUC_LT; EXP_LT_0; ARITH_EQ]; ALL_TAC] THEN DISCH_THEN(X_CHOOSE_THEN `m:num` STRIP_ASSUME_TAC) THEN MATCH_MP_TAC REAL_LTE_TRANS THEN EXISTS_TAC `e / &2 + e / &2` THEN CONJ_TAC THENL [ALL_TAC; SIMP_TAC[REAL_LE_REFL; GSYM REAL_MUL_2; REAL_DIV_LMUL; REAL_OF_NUM_EQ; ARITH_EQ]] THEN UNDISCH_TAC `!n k. k < 2 EXP n ==> ((pi * x) * cot (pi * x) = A n k + B n k)` THEN DISCH_THEN(MP_TAC o SPECL [`m:num`; `n - 1`]) THEN ASM_SIMP_TAC[] THEN DISCH_THEN(K ALL_TAC) THEN MATCH_MP_TAC(REAL_ARITH `abs(b) < e /\ abs((s - &1) - a) < e ==> abs(s - ((a + b) + &1)) < e + e`) THEN CONJ_TAC THENL [FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[] THEN UNDISCH_TAC `N1 + 1 <= n` THEN ARITH_TAC; ALL_TAC] THEN SUBGOAL_THEN `Sum (0,n) (\r. (&2 * x pow 2) / (x pow 2 - &r pow 2)) - &1 = &1 + Sum(1,n-1) (\r. (&2 * x pow 2) / (x pow 2 - &r pow 2))` SUBST1_TAC THENL [SUBGOAL_THEN `n = 1 + (n - 1)` (fun th -> GEN_REWRITE_TAC (LAND_CONV o ONCE_DEPTH_CONV) [th]) THENL [UNDISCH_TAC `N1 + 1 <= n` THEN ARITH_TAC; ALL_TAC] THEN REWRITE_TAC[GSYM(REWRITE_RULE[REAL_EQ_SUB_LADD] SUM_DIFF)] THEN MATCH_MP_TAC(REAL_ARITH `(a = &2) ==> ((x + a) - &1 = &1 + x)`) THEN CONV_TAC(ONCE_DEPTH_CONV REAL_SUM_CONV) THEN REWRITE_TAC[REAL_POW_2; REAL_MUL_LZERO; REAL_SUB_RZERO] THEN REWRITE_TAC[GSYM REAL_POW_2] THEN REWRITE_TAC[real_div] THEN REWRITE_TAC[GSYM REAL_MUL_ASSOC] THEN ASM_SIMP_TAC[GSYM real_div; REAL_DIV_REFL; REAL_POW_EQ_0] THEN REWRITE_TAC[REAL_MUL_RID]; ALL_TAC] THEN ONCE_REWRITE_TAC[REAL_ABS_SUB] THEN FIRST_ASSUM MATCH_MP_TAC THEN ASM_REWRITE_TAC[]);;