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)))) =