583 |
583 |
584 |
584 |
585 text \<open>Sum of a geometric progression.\<close> |
585 text \<open>Sum of a geometric progression.\<close> |
586 |
586 |
587 lemma geometric_sums: |
587 lemma geometric_sums: |
588 assumes less_1: "norm c < 1" |
588 assumes "norm c < 1" |
589 shows "(\<lambda>n. c^n) sums (1 / (1 - c))" |
589 shows "(\<lambda>n. c^n) sums (1 / (1 - c))" |
590 proof - |
590 proof - |
591 from less_1 have neq_1: "c \<noteq> 1" by auto |
591 have neq_0: "c - 1 \<noteq> 0" |
592 then have neq_0: "c - 1 \<noteq> 0" by simp |
592 using assms by auto |
593 from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0" |
|
594 by (rule LIMSEQ_power_zero) |
|
595 then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)" |
593 then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)" |
596 using neq_0 by (intro tendsto_intros) |
594 by (intro tendsto_intros assms) |
597 then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)" |
595 then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)" |
598 by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) |
596 by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) |
599 then show "(\<lambda>n. c ^ n) sums (1 / (1 - c))" |
597 with neq_0 show "(\<lambda>n. c ^ n) sums (1 / (1 - c))" |
600 by (simp add: sums_def geometric_sum neq_1) |
598 by (simp add: sums_def geometric_sum) |
601 qed |
599 qed |
602 |
600 |
603 lemma summable_geometric: "norm c < 1 \<Longrightarrow> summable (\<lambda>n. c^n)" |
601 lemma summable_geometric: "norm c < 1 \<Longrightarrow> summable (\<lambda>n. c^n)" |
604 by (rule geometric_sums [THEN sums_summable]) |
602 by (rule geometric_sums [THEN sums_summable]) |
605 |
603 |