src/HOL/Analysis/Harmonic_Numbers.thy
changeset 64267 b9a1486e79be
parent 63721 492bb53c3420
child 65109 a79c1080f1e9
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Sun Oct 16 22:43:51 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Oct 17 11:46:22 2016 +0200
     1.3 @@ -25,7 +25,7 @@
     1.4    thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
     1.5  qed
     1.6  
     1.7 -lemma setsum_Suc_diff':
     1.8 +lemma sum_Suc_diff':
     1.9    fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
    1.10    assumes "m \<le> n"
    1.11    shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
    1.12 @@ -44,10 +44,10 @@
    1.13    by (simp add: harm_def)
    1.14  
    1.15  lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})"
    1.16 -  unfolding harm_def by (intro setsum_nonneg) simp_all
    1.17 +  unfolding harm_def by (intro sum_nonneg) simp_all
    1.18  
    1.19  lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})"
    1.20 -  unfolding harm_def by (intro setsum_pos) simp_all
    1.21 +  unfolding harm_def by (intro sum_pos) simp_all
    1.22  
    1.23  lemma of_real_harm: "of_real (harm n) = harm n"
    1.24    unfolding harm_def by simp
    1.25 @@ -73,7 +73,7 @@
    1.26    also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k=Suc 0..Suc n. inverse (of_nat k) :: real)"
    1.27      unfolding harm_def[abs_def] by (subst convergent_Suc_iff) simp_all
    1.28    also have "... \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k\<le>n. inverse (of_nat (Suc k)) :: real)"
    1.29 -    by (subst setsum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
    1.30 +    by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: atLeast0AtMost)
    1.31    also have "... \<longleftrightarrow> summable (\<lambda>n. inverse (of_nat n) :: real)"
    1.32      by (subst summable_Suc_iff [symmetric]) (simp add: summable_iff_convergent')
    1.33    also have "\<not>..." by (rule not_summable_harmonic)
    1.34 @@ -126,7 +126,7 @@
    1.35    "euler_mascheroni.sum_integral_diff_series n = harm (Suc n) - ln (of_nat (Suc n))"
    1.36  proof -
    1.37    have "harm (Suc n) = (\<Sum>k=0..n. inverse (of_nat k + 1) :: real)" unfolding harm_def
    1.38 -    unfolding One_nat_def by (subst setsum_shift_bounds_cl_Suc_ivl) (simp add: add_ac)
    1.39 +    unfolding One_nat_def by (subst sum_shift_bounds_cl_Suc_ivl) (simp add: add_ac)
    1.40    moreover have "((\<lambda>x. inverse (x + 1) :: real) has_integral ln (of_nat n + 1) - ln (0 + 1))
    1.41                     {0..of_nat n}"
    1.42      by (intro fundamental_theorem_of_calculus)
    1.43 @@ -201,16 +201,16 @@
    1.44      fix n :: nat assume n: "n > 0"
    1.45      have "(\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k)) =
    1.46                (\<Sum>k<2*n. ((-1)^k + ?g k) / of_nat (Suc k)) - (\<Sum>k<2*n. ?g k / of_nat (Suc k))"
    1.47 -      by (simp add: setsum.distrib algebra_simps divide_inverse)
    1.48 +      by (simp add: sum.distrib algebra_simps divide_inverse)
    1.49      also have "(\<Sum>k<2*n. ((-1)^k + ?g k) / real_of_nat (Suc k)) = harm (2*n)"
    1.50 -      unfolding harm_altdef by (intro setsum.cong) (auto simp: field_simps)
    1.51 +      unfolding harm_altdef by (intro sum.cong) (auto simp: field_simps)
    1.52      also have "(\<Sum>k<2*n. ?g k / real_of_nat (Suc k)) = (\<Sum>k|k<2*n \<and> odd k. ?g k / of_nat (Suc k))"
    1.53 -      by (intro setsum.mono_neutral_right) auto
    1.54 +      by (intro sum.mono_neutral_right) auto
    1.55      also have "\<dots> = (\<Sum>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k)))"
    1.56 -      by (intro setsum.cong) auto
    1.57 +      by (intro sum.cong) auto
    1.58      also have "(\<Sum>k|k<2*n \<and> odd k. 2 / (real_of_nat (Suc k))) = harm n"
    1.59        unfolding harm_altdef
    1.60 -      by (intro setsum.reindex_cong[of "\<lambda>n. 2*n+1"]) (auto simp: inj_on_def field_simps elim!: oddE)
    1.61 +      by (intro sum.reindex_cong[of "\<lambda>n. 2*n+1"]) (auto simp: inj_on_def field_simps elim!: oddE)
    1.62      also have "harm (2*n) - harm n = ?em (2*n) - ?em n + ln 2" using n
    1.63        by (simp_all add: algebra_simps ln_mult)
    1.64      finally show "?em (2*n) - ?em n + ln 2 = (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))" ..
    1.65 @@ -388,9 +388,9 @@
    1.66    finally have "euler_mascheroni \<ge> (\<Sum>k\<le>n. D k) + 1 / (of_nat (2 * (n+2)))"
    1.67      by (simp add: inv_def field_simps)
    1.68    also have "(\<Sum>k\<le>n. D k) = harm (Suc n) - (\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1)))"
    1.69 -    unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add:  setsum.distrib setsum_subtractf)
    1.70 +    unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add:  sum.distrib sum_subtractf)
    1.71    also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1))) = ln (of_nat (n+2))"
    1.72 -    by (subst atLeast0AtMost [symmetric], subst setsum_Suc_diff) simp_all
    1.73 +    by (subst atLeast0AtMost [symmetric], subst sum_Suc_diff) simp_all
    1.74    finally show "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
    1.75      by simp
    1.76  
    1.77 @@ -422,9 +422,9 @@
    1.78    finally have "euler_mascheroni \<le> (\<Sum>k\<le>n. D k) + 1 / of_nat (2 * (n+1))"
    1.79      by (simp add: inv_def field_simps)
    1.80    also have "(\<Sum>k\<le>n. D k) = harm (Suc n) - (\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1)))"
    1.81 -    unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add:  setsum.distrib setsum_subtractf)
    1.82 +    unfolding harm_altdef D_def by (subst lessThan_Suc_atMost) (simp add:  sum.distrib sum_subtractf)
    1.83    also have "(\<Sum>k\<le>n. ln (real_of_nat (Suc k+1)) - ln (of_nat (k+1))) = ln (of_nat (n+2))"
    1.84 -    by (subst atLeast0AtMost [symmetric], subst setsum_Suc_diff) simp_all
    1.85 +    by (subst atLeast0AtMost [symmetric], subst sum_Suc_diff) simp_all
    1.86    finally show "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
    1.87      by simp
    1.88  qed