equal
deleted
inserted
replaced
394 apply (rule eventually_mono [OF eventually_ge_at_top[of N]]) |
394 apply (rule eventually_mono [OF eventually_ge_at_top[of N]]) |
395 using B N by (auto simp: field_simps abs_of_pos) |
395 using B N by (auto simp: field_simps abs_of_pos) |
396 from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))" |
396 from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))" |
397 by (rule summable_comparison_test_ev) |
397 by (rule summable_comparison_test_ev) |
398 from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl] |
398 from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl] |
399 have "summable (\<lambda>n. inverse (p n))" by (simp add: divide_simps) |
399 have "summable (\<lambda>n. inverse (p n))" by (simp add: field_split_simps) |
400 with divergent_p show False by contradiction |
400 with divergent_p show False by contradiction |
401 qed |
401 qed |
402 |
402 |
403 |
403 |
404 subsubsection \<open>Ratio test\<close> |
404 subsubsection \<open>Ratio test\<close> |
755 show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all |
755 show "c \<ge> 0" by (intro Lim_bounded2[OF lim]) simp_all |
756 next |
756 next |
757 fix r assume r: "0 < r" "ereal r < c" |
757 fix r assume r: "0 < r" "ereal r < c" |
758 let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" |
758 let ?l = "liminf (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" |
759 have "?l = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" |
759 have "?l = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" |
760 using r by (simp add: norm_mult norm_power divide_simps) |
760 using r by (simp add: norm_mult norm_power field_split_simps) |
761 also from r have "\<dots> = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" |
761 also from r have "\<dots> = liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" |
762 by (intro Liminf_ereal_mult_right) simp_all |
762 by (intro Liminf_ereal_mult_right) simp_all |
763 also have "liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c" |
763 also have "liminf (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c" |
764 by (intro lim_imp_Liminf lim) simp |
764 by (intro lim_imp_Liminf lim) simp |
765 finally have l: "?l = c * ereal (inverse r)" by simp |
765 finally have l: "?l = c * ereal (inverse r)" by simp |
769 (insert r nz l l', auto elim!: eventually_mono) |
769 (insert r nz l l', auto elim!: eventually_mono) |
770 next |
770 next |
771 fix r assume r: "0 < r" "ereal r > c" |
771 fix r assume r: "0 < r" "ereal r > c" |
772 let ?l = "limsup (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" |
772 let ?l = "limsup (\<lambda>n. ereal (norm (f n * of_real r ^ n) / norm (f (Suc n) * of_real r ^ Suc n)))" |
773 have "?l = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" |
773 have "?l = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n)))) * ereal (inverse r))" |
774 using r by (simp add: norm_mult norm_power divide_simps) |
774 using r by (simp add: norm_mult norm_power field_split_simps) |
775 also from r have "\<dots> = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" |
775 also from r have "\<dots> = limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) * ereal (inverse r)" |
776 by (intro Limsup_ereal_mult_right) simp_all |
776 by (intro Limsup_ereal_mult_right) simp_all |
777 also have "limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c" |
777 also have "limsup (\<lambda>n. ereal (norm (f n) / (norm (f (Suc n))))) = c" |
778 by (intro lim_imp_Limsup lim) simp |
778 by (intro lim_imp_Limsup lim) simp |
779 finally have l: "?l = c * ereal (inverse r)" by simp |
779 finally have l: "?l = c * ereal (inverse r)" by simp |