equal
deleted
inserted
replaced
332 apply (drule_tac x = m in spec, auto) |
332 apply (drule_tac x = m in spec, auto) |
333 done |
333 done |
334 |
334 |
335 text{*Sum of a geometric progression.*} |
335 text{*Sum of a geometric progression.*} |
336 |
336 |
337 lemma sumr_geometric: |
337 lemmas sumr_geometric = geometric_sum [where 'a = real] |
338 "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)" |
|
339 apply (induct "n", auto) |
|
340 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1]) |
|
341 apply (auto simp add: mult_assoc left_distrib) |
|
342 apply (simp add: right_distrib diff_minus mult_commute) |
|
343 done |
|
344 |
338 |
345 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" |
339 lemma geometric_sums: "abs(x) < 1 ==> (%n. x ^ n) sums (1/(1 - x))" |
346 apply (case_tac "x = 1") |
340 apply (case_tac "x = 1") |
347 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 |
341 apply (auto dest!: LIMSEQ_rabs_realpow_zero2 |
348 simp add: sumr_geometric sums_def diff_minus add_divide_distrib) |
342 simp add: sumr_geometric sums_def diff_minus add_divide_distrib) |