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
```