src/HOL/Analysis/Harmonic_Numbers.thy
changeset 68643 3db6c9338ec1
parent 67399 eab6ce8368fa
child 69064 5840724b1d71
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 15:24:06 2018 +0200
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Mon Jul 16 17:50:07 2018 +0200
     1.3 @@ -19,7 +19,7 @@
     1.4  
     1.5  subsection \<open>The Harmonic numbers\<close>
     1.6  
     1.7 -definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
     1.8 +definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
     1.9    "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
    1.10  
    1.11  lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
    1.12 @@ -54,7 +54,7 @@
    1.13    finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
    1.14  qed (simp_all add: harm_def)
    1.15  
    1.16 -lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
    1.17 +theorem not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
    1.18  proof -
    1.19    have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow>
    1.20              convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm)
    1.21 @@ -156,7 +156,7 @@
    1.22    thus ?thesis by (subst (asm) convergent_Suc_iff)
    1.23  qed
    1.24  
    1.25 -lemma euler_mascheroni_LIMSEQ:
    1.26 +lemma%important euler_mascheroni_LIMSEQ:
    1.27    "(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
    1.28    unfolding euler_mascheroni_def
    1.29    by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
    1.30 @@ -187,7 +187,7 @@
    1.31    thus ?thesis by simp
    1.32  qed
    1.33  
    1.34 -lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    1.35 +theorem alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    1.36  proof -
    1.37    let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
    1.38    let ?g = "\<lambda>n. if even n then 0 else (2::real)"
    1.39 @@ -250,7 +250,7 @@
    1.40  qed
    1.41  
    1.42  
    1.43 -subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
    1.44 +subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
    1.45  
    1.46  (* TODO: Move? *)
    1.47  lemma ln_inverse_approx_le:
    1.48 @@ -340,9 +340,9 @@
    1.49  
    1.50  
    1.51  lemma euler_mascheroni_lower:
    1.52 -        "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
    1.53 -  and euler_mascheroni_upper:
    1.54 -        "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
    1.55 +          "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
    1.56 +    and euler_mascheroni_upper:
    1.57 +          "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
    1.58  proof -
    1.59    define D :: "_ \<Rightarrow> real"
    1.60      where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n