src/HOL/Analysis/Harmonic_Numbers.thy
changeset 65273 917ae0ba03a2
parent 65109 a79c1080f1e9
child 65395 7504569a73c7
     1.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Mar 15 21:52:04 2017 +0100
     1.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Mar 16 13:55:29 2017 +0000
     1.3 @@ -17,21 +17,6 @@
     1.4    and the Euler-Mascheroni constant.
     1.5  \<close>
     1.6  
     1.7 -lemma ln_2_less_1: "ln 2 < (1::real)"
     1.8 -proof -
     1.9 -  have "2 < 5/(2::real)" by simp
    1.10 -  also have "5/2 \<le> exp (1::real)" using exp_lower_taylor_quadratic[of 1, simplified] by simp
    1.11 -  finally have "exp (ln 2) < exp (1::real)" by simp
    1.12 -  thus "ln 2 < (1::real)" by (subst (asm) exp_less_cancel_iff) simp
    1.13 -qed
    1.14 -
    1.15 -lemma sum_Suc_diff':
    1.16 -  fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
    1.17 -  assumes "m \<le> n"
    1.18 -  shows "(\<Sum>i = m..<n. f (Suc i) - f i) = f n - f m"
    1.19 -using assms by (induct n) (auto simp: le_Suc_eq)
    1.20 -
    1.21 -
    1.22  subsection \<open>The Harmonic numbers\<close>
    1.23  
    1.24  definition harm :: "nat \<Rightarrow> 'a :: real_normed_field" where