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