src/HOL/Analysis/Harmonic_Numbers.thy
changeset 65395 7504569a73c7
parent 65273 917ae0ba03a2
child 66447 a1f5c5c26fa6
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Apr 03 22:18:56 2017 +0200
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Tue Apr 04 08:57:21 2017 +0200
     1.3 @@ -37,6 +37,9 @@
     1.4  lemma of_real_harm: "of_real (harm n) = harm n"
     1.5    unfolding harm_def by simp
     1.6  
     1.7 +lemma abs_harm [simp]: "(abs (harm n) :: real) = harm n"
     1.8 +  using harm_nonneg[of n] by (rule abs_of_nonneg)    
     1.9 +
    1.10  lemma norm_harm: "norm (harm n) = harm n"
    1.11    by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)
    1.12  
    1.13 @@ -91,6 +94,15 @@
    1.14    finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp
    1.15  qed (simp_all add: harm_def)
    1.16  
    1.17 +lemma harm_at_top: "filterlim (harm :: nat \<Rightarrow> real) at_top sequentially"
    1.18 +proof (rule filterlim_at_top_mono)
    1.19 +  show "eventually (\<lambda>n. harm n \<ge> ln (real (Suc n))) at_top"
    1.20 +    using ln_le_harm by (intro always_eventually allI) (simp_all add: add_ac)
    1.21 +  show "filterlim (\<lambda>n. ln (real (Suc n))) at_top sequentially"
    1.22 +    by (intro filterlim_compose[OF ln_at_top] filterlim_compose[OF filterlim_real_sequentially] 
    1.23 +              filterlim_Suc)
    1.24 +qed
    1.25 +
    1.26  
    1.27  subsection \<open>The Euler--Mascheroni constant\<close>
    1.28