src/HOL/Analysis/Harmonic_Numbers.thy
changeset 63721 492bb53c3420
parent 63627 6ddb43c6b711
child 64267 b9a1486e79be
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 24 11:02:23 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 25 15:50:43 2016 +0200
     1.3 @@ -173,13 +173,23 @@
     1.4    thus ?thesis by simp
     1.5  qed
     1.6  
     1.7 -lemma euler_mascheroni_sum:
     1.8 +lemma euler_mascheroni_sum_real:
     1.9    "(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)) :: real)
    1.10         sums euler_mascheroni"
    1.11   using sums_add[OF telescope_sums[OF LIMSEQ_Suc[OF euler_mascheroni_LIMSEQ]]
    1.12                     telescope_sums'[OF LIMSEQ_inverse_real_of_nat]]
    1.13    by (simp_all add: harm_def algebra_simps)
    1.14  
    1.15 +lemma euler_mascheroni_sum:
    1.16 +  "(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2))))
    1.17 +       sums (euler_mascheroni :: 'a :: {banach, real_normed_field})"
    1.18 +proof -
    1.19 +  have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))))
    1.20 +       sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})"
    1.21 +    by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real)
    1.22 +  thus ?thesis by simp
    1.23 +qed
    1.24 +
    1.25  lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    1.26  proof -
    1.27    let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
    1.28 @@ -342,17 +352,18 @@
    1.29    let ?g = "\<lambda>n. ln (of_nat (n+2)) - ln (of_nat (n+1)) - inverse (of_nat (n+1)) :: real"
    1.30    define inv where [abs_def]: "inv n = inverse (real_of_nat n)" for n
    1.31    fix n :: nat
    1.32 -  note summable = sums_summable[OF euler_mascheroni_sum, folded D_def]
    1.33 +  note summable = sums_summable[OF euler_mascheroni_sum_real, folded D_def]
    1.34    have sums: "(\<lambda>k. (inv (Suc (k + (n+1))) - inv (Suc (Suc k + (n+1))))/2) sums ((inv (Suc (0 + (n+1))) - 0)/2)"
    1.35      unfolding inv_def
    1.36      by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
    1.37    have sums': "(\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) sums ((inv (Suc (0 + n)) - 0)/2)"
    1.38      unfolding inv_def
    1.39      by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
    1.40 -  from euler_mascheroni_sum have "euler_mascheroni = (\<Sum>k. D k)"
    1.41 +  from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
    1.42      by (simp add: sums_iff D_def)
    1.43    also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
    1.44 -    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], subst lessThan_Suc_atMost) simp
    1.45 +    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
    1.46 +        subst lessThan_Suc_atMost) simp
    1.47    finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
    1.48  
    1.49    note sum