src/HOL/Analysis/Summation_Tests.thy
 changeset 65578 e4997c181cce parent 64449 8c44dfb4ca8a child 66447 a1f5c5c26fa6
```     1.1 --- a/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 08:38:23 2017 +0200
1.2 +++ b/src/HOL/Analysis/Summation_Tests.thy	Tue Apr 25 16:39:54 2017 +0100
1.3 @@ -246,9 +246,9 @@
1.4  proof (cases "Re s \<le> 0")
1.5    let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
1.6    case False
1.7 -  with eventually_gt_at_top[of "0::nat"]
1.8 -    have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
1.9 -    by (auto intro!: ge_one_powr_ge_zero elim!: eventually_mono)
1.10 +  have "eventually (\<lambda>n. norm (1 :: real) \<le> norm (exp (?l n * s))) sequentially"
1.11 +    apply (rule eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
1.12 +    using False ge_one_powr_ge_zero by auto
1.13    from summable_comparison_test_ev[OF this] False show ?thesis by (auto simp: summable_const_iff)
1.14  next
1.15    let ?l = "\<lambda>n. complex_of_real (ln (of_nat n))"
1.16 @@ -387,11 +387,11 @@
1.17      by (auto simp: eventually_at_top_linorder)
1.18    hence A: "p n * f n < p (Suc n) * f (Suc n)" if "n \<ge> N" for n using that N[of n] N[of "Suc n"]
1.19      by (simp add: field_simps)
1.20 -  have "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
1.21 -      by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
1.22 -  from eventually_ge_at_top[of N] N this
1.23 -    have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
1.24 -    by (auto elim!: eventually_mono simp: field_simps abs_of_pos)
1.25 +  have B: "p n * f n \<ge> p N * f N" if "n \<ge> N" for n using that and A
1.26 +    by (induction n rule: dec_induct) (auto intro!: less_imp_le elim!: order.trans)
1.27 +  have "eventually (\<lambda>n. norm (p N * f N * inverse (p n)) \<le> f n) sequentially"
1.28 +    apply (rule eventually_mono [OF eventually_ge_at_top[of N]])
1.29 +    using B N  by (auto  simp: field_simps abs_of_pos)
1.30    from this and \<open>summable f\<close> have "summable (\<lambda>n. p N * f N * inverse (p n))"
1.31      by (rule summable_comparison_test_ev)
1.32    from summable_mult[OF this, of "inverse (p N * f N)"] N[OF le_refl]
1.33 @@ -779,9 +779,8 @@
1.34  proof -
1.35    have "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
1.36            limsup (\<lambda>n. ereal (norm c) * ereal (root n (norm (f n))))"
1.37 -    using eventually_gt_at_top[of "0::nat"]
1.38 -    by (intro Limsup_eq)
1.39 -       (auto elim!: eventually_mono simp: norm_mult norm_power real_root_mult real_root_power)
1.40 +    by (intro Limsup_eq eventually_mono [OF eventually_gt_at_top[of "0::nat"]])
1.41 +       (auto simp: norm_mult norm_power real_root_mult real_root_power)
1.42    also have "\<dots> = ereal (norm c) * limsup (\<lambda>n. ereal (root n (norm (f n))))"
1.43      using assms by (subst Limsup_ereal_mult_left[symmetric]) simp_all
1.44    finally have A: "limsup (\<lambda>n. ereal (root n (norm (c ^ n * f n)))) =
```