src/HOL/Analysis/Harmonic_Numbers.thy

   and the Euler-Mascheroni constant.
 \<close>
 
 subsection \<open>The Harmonic numbers\<close>
 
-definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
+definition%important harm :: "nat \<Rightarrow> 'a :: real_normed_field" where
   "harm n = (\<Sum>k=1..n. inverse (of_nat k))"
 
 lemma harm_altdef: "harm n = (\<Sum>k<n. inverse (of_nat (Suc k)))"
   unfolding harm_def by (induction n) simp_all
 

   also have "harm \<dots> = harm (pred_numeral n) + inverse (numeral n)"
     by (subst harm_Suc, subst numeral_eq_Suc[symmetric]) simp
   finally show "harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)" .
 qed (simp_all add: harm_def)
 
-lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
+theorem not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
 proof -
   have "convergent (\<lambda>n. norm (harm n :: 'a)) \<longleftrightarrow>
             convergent (harm :: nat \<Rightarrow> real)" by (simp add: norm_harm)
   also have "\<dots> \<longleftrightarrow> convergent (\<lambda>n. \<Sum>k=Suc 0..Suc n. inverse (of_nat k) :: real)"
     unfolding harm_def[abs_def] by (subst convergent_Suc_iff) simp_all

   have "convergent (\<lambda>n. harm (Suc n) - ln (of_nat (Suc n) :: real))"
     by (subst A) (fact euler_mascheroni.sum_integral_diff_series_convergent)
   thus ?thesis by (subst (asm) convergent_Suc_iff)
 qed
 
-lemma euler_mascheroni_LIMSEQ:
+lemma%important euler_mascheroni_LIMSEQ:
   "(\<lambda>n. harm n - ln (of_nat n) :: real) \<longlonglongrightarrow> euler_mascheroni"
   unfolding euler_mascheroni_def
   by (simp add: convergent_LIMSEQ_iff [symmetric] euler_mascheroni_convergent)
 
 lemma euler_mascheroni_LIMSEQ_of_real:

        sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})"
     by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real)
   thus ?thesis by simp
 qed
 
-lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
+theorem alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
 proof -
   let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
   let ?g = "\<lambda>n. if even n then 0 else (2::real)"
   let ?em = "\<lambda>n. harm n - ln (real_of_nat n)"
   have "eventually (\<lambda>n. ?em (2*n) - ?em n + ln 2 = (\<Sum>k<2*n. (-1)^k / real_of_nat (Suc k))) at_top"

       by (induction n) (simp_all add: inverse_eq_divide)
   qed
 qed
 
 
-subsection \<open>Bounds on the Euler-Mascheroni constant\<close>
+subsection%unimportant \<open>Bounds on the Euler-Mascheroni constant\<close>
 
 (* TODO: Move? *)
 lemma ln_inverse_approx_le:
   assumes "(x::real) > 0" "a > 0"
   shows   "ln (x + a) - ln x \<le> a * (inverse x + inverse (x + a))/2" (is "_ \<le> ?A")

   finally show ?thesis .
 qed
 
 
 lemma euler_mascheroni_lower:
-        "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
-  and euler_mascheroni_upper:
-        "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
+          "euler_mascheroni \<ge> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 2))"
+    and euler_mascheroni_upper:
+          "euler_mascheroni \<le> harm (Suc n) - ln (real_of_nat (n + 2)) + 1/real_of_nat (2 * (n + 1))"
 proof -
   define D :: "_ \<Rightarrow> real"
     where "D n = inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))" for n
   let ?g = "\<lambda>n. ln (of_nat (n+2)) - ln (of_nat (n+1)) - inverse (of_nat (n+1)) :: real"
   define inv where [abs_def]: "inv n = inverse (real_of_nat n)" for n