src/HOL/Analysis/Harmonic_Numbers.thy
changeset 66447 a1f5c5c26fa6
parent 65395 7504569a73c7
child 66495 0b46bd081228
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:40:42 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 17 14:52:56 2017 +0200
     1.3 @@ -215,7 +215,7 @@
     1.4    moreover have "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real))
     1.5                       \<longlonglongrightarrow> euler_mascheroni - euler_mascheroni + ln 2"
     1.6      by (intro tendsto_intros euler_mascheroni_LIMSEQ filterlim_compose[OF euler_mascheroni_LIMSEQ]
     1.7 -              filterlim_subseq) (auto simp: subseq_def)
     1.8 +              filterlim_subseq) (auto simp: strict_mono_def)
     1.9    hence "(\<lambda>n. ?em (2*n) - ?em n + ln (2::real)) \<longlonglongrightarrow> ln 2" by simp
    1.10    ultimately have "(\<lambda>n. (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) \<longlonglongrightarrow> ln 2"
    1.11      by (rule Lim_transform_eventually)
    1.12 @@ -227,7 +227,7 @@
    1.13      by (simp add: summable_sums_iff divide_inverse sums_def)
    1.14    from filterlim_compose[OF this filterlim_subseq[of "op * (2::nat)"]]
    1.15      have "(\<lambda>n. \<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) \<longlonglongrightarrow> (\<Sum>k. (-1)^k / real_of_nat (Suc k))"
    1.16 -    by (simp add: subseq_def)
    1.17 +    by (simp add: strict_mono_def)
    1.18    ultimately have "(\<Sum>k. (- 1) ^ k / real_of_nat (Suc k)) = ln 2" by (intro LIMSEQ_unique)
    1.19    with A show ?thesis by (simp add: sums_def)
    1.20  qed