equal
deleted
inserted
replaced
46 finally show ?thesis . |
46 finally show ?thesis . |
47 qed |
47 qed |
48 |
48 |
49 lemma root_test_convergence: |
49 lemma root_test_convergence: |
50 fixes f :: "nat \<Rightarrow> 'a::banach" |
50 fixes f :: "nat \<Rightarrow> 'a::banach" |
51 assumes f: "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> x" \<comment> "could be weakened to lim sup" |
51 assumes f: "(\<lambda>n. root n (norm (f n))) \<longlonglongrightarrow> x" \<comment> \<open>could be weakened to lim sup\<close> |
52 and "x < 1" |
52 and "x < 1" |
53 shows "summable f" |
53 shows "summable f" |
54 proof - |
54 proof - |
55 have "0 \<le> x" |
55 have "0 \<le> x" |
56 by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1]) |
56 by (rule LIMSEQ_le[OF tendsto_const f]) (auto intro!: exI[of _ 1]) |