1266 apply (rule_tac [2] summable_exp) |
1266 apply (rule_tac [2] summable_exp) |
1267 apply (rule_tac x = 0 in exI) |
1267 apply (rule_tac x = 0 in exI) |
1268 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) |
1268 apply (auto simp add: divide_inverse abs_mult power_abs [symmetric] zero_le_mult_iff) |
1269 done |
1269 done |
1270 |
1270 |
1271 lemma lemma_STAR_sin: |
|
1272 "(if even n then 0 |
|
1273 else -1 ^ ((n - Suc 0) div 2)/(real (fact n))) * 0 ^ n = 0" |
|
1274 by (induct "n", auto) |
|
1275 |
|
1276 lemma lemma_STAR_cos: |
|
1277 "0 < n --> |
|
1278 -1 ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" |
|
1279 by (induct "n", auto) |
|
1280 |
|
1281 lemma lemma_STAR_cos1: |
|
1282 "0 < n --> |
|
1283 (-1) ^ (n div 2)/(real (fact n)) * 0 ^ n = 0" |
|
1284 by (induct "n", auto) |
|
1285 |
|
1286 lemma lemma_STAR_cos2: |
|
1287 "(\<Sum>n=1..<n. if even n then -1 ^ (n div 2)/(real (fact n)) * 0 ^ n |
|
1288 else 0) = 0" |
|
1289 apply (induct "n") |
|
1290 apply (case_tac [2] "n", auto) |
|
1291 done |
|
1292 |
|
1293 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)" |
1271 lemma sin_converges: "(\<lambda>n. sin_coeff n * x ^ n) sums sin(x)" |
1294 unfolding sin_def by (rule summable_sin [THEN summable_sums]) |
1272 unfolding sin_def by (rule summable_sin [THEN summable_sums]) |
1295 |
1273 |
1296 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)" |
1274 lemma cos_converges: "(\<lambda>n. cos_coeff n * x ^ n) sums cos(x)" |
1297 unfolding cos_def by (rule summable_cos [THEN summable_sums]) |
1275 unfolding cos_def by (rule summable_cos [THEN summable_sums]) |