equal
deleted
inserted
replaced
622 from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1" |
622 from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1" |
623 by (auto simp: eventually_at_top_linorder) |
623 by (auto simp: eventually_at_top_linorder) |
624 then show "norm c < 1" using one_le_power[of "norm c" n] |
624 then show "norm c < 1" using one_le_power[of "norm c" n] |
625 by (cases "norm c \<ge> 1") (linarith, simp) |
625 by (cases "norm c \<ge> 1") (linarith, simp) |
626 qed (rule summable_geometric) |
626 qed (rule summable_geometric) |
|
627 |
|
628 end |
|
629 |
|
630 text \<open>Biconditional versions for constant factors\<close> |
|
631 context |
|
632 fixes c :: "'a::real_normed_field" |
|
633 begin |
|
634 |
|
635 lemma summable_cmult_iff [simp]: "summable (\<lambda>n. c * f n) \<longleftrightarrow> c=0 \<or> summable f" |
|
636 proof - |
|
637 have "\<lbrakk>summable (\<lambda>n. c * f n); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f" |
|
638 using summable_mult_D by blast |
|
639 then show ?thesis |
|
640 by (auto simp: summable_mult) |
|
641 qed |
|
642 |
|
643 lemma summable_divide_iff [simp]: "summable (\<lambda>n. f n / c) \<longleftrightarrow> c=0 \<or> summable f" |
|
644 proof - |
|
645 have "\<lbrakk>summable (\<lambda>n. f n / c); c \<noteq> 0\<rbrakk> \<Longrightarrow> summable f" |
|
646 by (auto dest: summable_divide [where c = "1/c"]) |
|
647 then show ?thesis |
|
648 by (auto simp: summable_divide) |
|
649 qed |
627 |
650 |
628 end |
651 end |
629 |
652 |
630 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1" |
653 lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1" |
631 proof - |
654 proof - |