author eberlm Tue, 05 Jan 2016 17:54:10 +0100 changeset 62065 1546a042e87b parent 62060 b75764fc4c35 child 62066 4db2d39aa76c
 src/HOL/Library/Poly_Deriv.thy file | annotate | diff | comparison | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | comparison | revisions src/HOL/List.thy file | annotate | diff | comparison | revisions src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy file | annotate | diff | comparison | revisions
--- a/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Library/Poly_Deriv.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -95,6 +95,17 @@
lemma poly_DERIV[simp]: "DERIV (%x. poly p x) x :> poly (pderiv p) x"
by (induct p, auto intro!: derivative_eq_intros simp add: pderiv_pCons)

+lemma continuous_on_poly [continuous_intros]:
+  fixes p :: "'a :: {real_normed_field} poly"
+  assumes "continuous_on A f"
+  shows   "continuous_on A (\<lambda>x. poly p (f x))"
+proof -
+  have "continuous_on A (\<lambda>x. (\<Sum>i\<le>degree p. (f x) ^ i * coeff p i))"
+    by (intro continuous_intros assms)
+  also have "\<dots> = (\<lambda>x. poly p (f x))" by (intro ext) (simp add: poly_altdef mult_ac)
+  finally show ?thesis .
+qed
+
text\<open>Consequences of the derivative theorem above\<close>

lemma poly_differentiable[simp]: "(%x. poly p x) differentiable (at x::real filter)"
@@ -114,6 +125,12 @@
==> \<exists>x. a < x & x < b & (poly p x = 0)"
by (insert poly_IVT_pos [where p = "- p" ]) simp

+lemma poly_IVT:
+  fixes p::"real poly"
+  assumes "a<b" and "poly p a * poly p b < 0"
+  shows "\<exists>x>a. x < b \<and> poly p x = 0"
+by (metis assms(1) assms(2) less_not_sym mult_less_0_iff poly_IVT_neg poly_IVT_pos)
+
lemma poly_MVT: "(a::real) < b ==>
\<exists>x. a < x & x < b & (poly p b - poly p a = (b - a) * poly (pderiv p) x)"
using MVT [of a b "poly p"]
@@ -122,6 +139,53 @@
apply (auto simp add: mult_left_cancel poly_DERIV [THEN DERIV_unique])
done

+lemma poly_MVT':
+  assumes "{min a b..max a b} \<subseteq> A"
+  shows   "\<exists>x\<in>A. poly p b - poly p a = (b - a) * poly (pderiv p) (x::real)"
+proof (cases a b rule: linorder_cases)
+  case less
+  from poly_MVT[OF less, of p] guess x by (elim exE conjE)
+  thus ?thesis by (intro bexI[of _ x]) (auto intro!: subsetD[OF assms])
+
+next
+  case greater
+  from poly_MVT[OF greater, of p] guess x by (elim exE conjE)
+  thus ?thesis by (intro bexI[of _ x]) (auto simp: algebra_simps intro!: subsetD[OF assms])
+qed (insert assms, auto)
+
+lemma poly_pinfty_gt_lc:
+  fixes p:: "real poly"
+  assumes  "lead_coeff p > 0"
+  shows "\<exists> n. \<forall> x \<ge> n. poly p x \<ge> lead_coeff p" using assms
+proof (induct p)
+  case 0
+  thus ?case by auto
+next
+  case (pCons a p)
+  have "\<lbrakk>a\<noteq>0;p=0\<rbrakk> \<Longrightarrow> ?case" by auto
+  moreover have "p\<noteq>0 \<Longrightarrow> ?case"
+    proof -
+      assume "p\<noteq>0"
+      then obtain n1 where gte_lcoeff:"\<forall>x\<ge>n1. lead_coeff p \<le> poly p x" using that pCons by auto
+      have gt_0:"lead_coeff p >0" using pCons(3) `p\<noteq>0` by auto
+      def n\<equiv>"max n1 (1+ \<bar>a\<bar>/(lead_coeff p))"
+      show ?thesis
+        proof (rule_tac x=n in exI,rule,rule)
+          fix x assume "n \<le> x"
+          hence "lead_coeff p \<le> poly p x"
+            using gte_lcoeff unfolding n_def by auto
+          hence " \<bar>a\<bar>/(lead_coeff p) \<ge> \<bar>a\<bar>/(poly p x)" and "poly p x>0" using gt_0
+            by (intro frac_le,auto)
+          hence "x\<ge>1+ \<bar>a\<bar>/(poly p x)" using `n\<le>x`[unfolded n_def] by auto
+          thus "lead_coeff (pCons a p) \<le> poly (pCons a p) x"
+            using `lead_coeff p \<le> poly p x` `poly p x>0` `p\<noteq>0`
+        qed
+    qed
+  ultimately show ?case by fastforce
+qed
+
+
text\<open>Lemmas for Derivatives\<close>

lemma order_unique_lemma:
@@ -225,6 +289,51 @@
done
qed

+lemma order_smult:
+  assumes "c \<noteq> 0"
+  shows "order x (smult c p) = order x p"
+proof (cases "p = 0")
+  case False
+  have "smult c p = [:c:] * p" by simp
+  also from assms False have "order x \<dots> = order x [:c:] + order x p"
+    by (subst order_mult) simp_all
+  also from assms have "order x [:c:] = 0" by (intro order_0I) auto
+  finally show ?thesis by simp
+qed simp
+
+(* Next two lemmas contributed by Wenda Li *)
+lemma order_1_eq_0 [simp]:"order x 1 = 0"
+  by (metis order_root poly_1 zero_neq_one)
+
+lemma order_power_n_n: "order a ([:-a,1:]^n)=n"
+proof (induct n) (*might be proved more concisely using nat_less_induct*)
+  case 0
+  thus ?case by (metis order_root poly_1 power_0 zero_neq_one)
+next
+  case (Suc n)
+  have "order a ([:- a, 1:] ^ Suc n)=order a ([:- a, 1:] ^ n) + order a [:-a,1:]"
+      one_neq_zero order_mult pCons_eq_0_iff power_add power_eq_0_iff power_one_right)
+  moreover have "order a [:-a,1:]=1" unfolding order_def
+    proof (rule Least_equality,rule ccontr)
+      assume  "\<not> \<not> [:- a, 1:] ^ Suc 1 dvd [:- a, 1:]"
+      hence "[:- a, 1:] ^ Suc 1 dvd [:- a, 1:]" by simp
+      hence "degree ([:- a, 1:] ^ Suc 1) \<le> degree ([:- a, 1:] )"
+        by (rule dvd_imp_degree_le,auto)
+      thus False by auto
+    next
+      fix y assume asm:"\<not> [:- a, 1:] ^ Suc y dvd [:- a, 1:]"
+      show "1 \<le> y"
+        proof (rule ccontr)
+          assume "\<not> 1 \<le> y"
+          hence "y=0" by auto
+          hence "[:- a, 1:] ^ Suc y dvd [:- a, 1:]" by auto
+          thus False using asm by auto
+        qed
+    qed
+  ultimately show ?case using Suc by auto
+qed
+
text\<open>Now justify the standard squarefree decomposition, i.e. f / gcd(f,f').\<close>

lemma order_divides: "[:-a, 1:] ^ n dvd p \<longleftrightarrow> p = 0 \<or> n \<le> order a p"
--- a/src/HOL/Library/Polynomial.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -281,7 +281,10 @@
lemma Poly_eq_0:
"Poly as = 0 \<longleftrightarrow> (\<exists>n. as = replicate n 0)"
by (induct as) (auto simp add: Cons_replicate_eq)
-
+
+lemma degree_Poly: "degree (Poly xs) \<le> length xs"
+  by (induction xs) simp_all
+
definition coeffs :: "'a poly \<Rightarrow> 'a::zero list"
where
"coeffs p = (if p = 0 then [] else map (\<lambda>i. coeff p i) [0 ..< Suc (degree p)])"
@@ -311,6 +314,14 @@
by (simp add: coeffs_def * upt_conv_Cons coeff_pCons map_decr_upt del: upt_Suc)
qed

+lemma length_coeffs: "p \<noteq> 0 \<Longrightarrow> length (coeffs p) = degree p + 1"
+
+lemma coeffs_nth:
+  assumes "p \<noteq> 0" "n \<le> degree p"
+  shows   "coeffs p ! n = coeff p n"
+  using assms unfolding coeffs_def by (auto simp del: upt_Suc)
+
lemma not_0_cCons_eq [simp]:
"p \<noteq> 0 \<Longrightarrow> a ## coeffs p = a # coeffs p"
@@ -450,6 +461,25 @@
"poly (pCons a p) x = a + x * poly p x"
by (cases "p = 0 \<and> a = 0") (auto simp add: poly_def)

+lemma poly_altdef:
+  "poly p (x :: 'a :: {comm_semiring_0, semiring_1}) = (\<Sum>i\<le>degree p. coeff p i * x ^ i)"
+proof (induction p rule: pCons_induct)
+  case (pCons a p)
+    show ?case
+    proof (cases "p = 0")
+      case False
+      let ?p' = "pCons a p"
+      note poly_pCons[of a p x]
+      also note pCons.IH
+      also have "a + x * (\<Sum>i\<le>degree p. coeff p i * x ^ i) =
+                 coeff ?p' 0 * x^0 + (\<Sum>i\<le>degree p. coeff ?p' (Suc i) * x^Suc i)"
+          by (simp add: field_simps setsum_right_distrib coeff_pCons)
+      also note setsum_atMost_Suc_shift[symmetric]
+      also note degree_pCons_eq[OF `p \<noteq> 0`, of a, symmetric]
+      finally show ?thesis .
+   qed simp
+qed simp
+

subsection \<open>Monomials\<close>

@@ -500,7 +530,7 @@
by (cases "a = 0", simp_all)
(induct n, simp_all add: mult.left_commute poly_def)

-
+

@@ -714,6 +744,9 @@
lemma poly_setsum: "poly (\<Sum>k\<in>A. p k) x = (\<Sum>k\<in>A. poly (p k) x)"
by (induct A rule: infinite_finite_induct) simp_all

+lemma Poly_snoc: "Poly (xs @ [x]) = Poly xs + monom x (length xs)"
+  by (induction xs) (simp_all add: monom_0 monom_Suc)
+

subsection \<open>Multiplication by a constant, polynomial multiplication and the unit polynomial\<close>

@@ -924,6 +957,28 @@
shows "poly (p ^ n) x = poly p x ^ n"
by (induct n) simp_all

+
+subsection \<open>Conversions from natural numbers\<close>
+
+lemma of_nat_poly: "of_nat n = [:of_nat n :: 'a :: comm_semiring_1:]"
+proof (induction n)
+  case (Suc n)
+  hence "of_nat (Suc n) = 1 + (of_nat n :: 'a poly)"
+    by simp
+  also have "(of_nat n :: 'a poly) = [: of_nat n :]"
+    by (subst Suc) (rule refl)
+  also have "1 = [:1:]" by (simp add: one_poly_def)
+  finally show ?case by (subst (asm) add_pCons) simp
+qed simp
+
+lemma degree_of_nat [simp]: "degree (of_nat n) = 0"
+
+lemma degree_numeral [simp]: "degree (numeral n) = 0"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+lemma numeral_poly: "numeral n = [:numeral n:]"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp

@@ -1787,6 +1842,9 @@
apply (metis dvd_power dvd_trans order_1)
done

+lemma order_0I: "poly p a \<noteq> 0 \<Longrightarrow> order a p = 0"
+  by (subst (asm) order_root) auto
+

subsection \<open>GCD of polynomials\<close>

@@ -1919,6 +1977,75 @@

+subsection \<open>Additional induction rules on polynomials\<close>
+
+text \<open>
+  An induction rule for induction over the roots of a polynomial with a certain property.
+  (e.g. all positive roots)
+\<close>
+lemma poly_root_induct [case_names 0 no_roots root]:
+  fixes p :: "'a :: idom poly"
+  assumes "Q 0"
+  assumes "\<And>p. (\<And>a. P a \<Longrightarrow> poly p a \<noteq> 0) \<Longrightarrow> Q p"
+  assumes "\<And>a p. P a \<Longrightarrow> Q p \<Longrightarrow> Q ([:a, -1:] * p)"
+  shows   "Q p"
+proof (induction "degree p" arbitrary: p rule: less_induct)
+  case (less p)
+  show ?case
+  proof (cases "p = 0")
+    assume nz: "p \<noteq> 0"
+    show ?case
+    proof (cases "\<exists>a. P a \<and> poly p a = 0")
+      case False
+      thus ?thesis by (intro assms(2)) blast
+    next
+      case True
+      then obtain a where a: "P a" "poly p a = 0"
+        by blast
+      hence "-[:-a, 1:] dvd p"
+        by (subst minus_dvd_iff) (simp add: poly_eq_0_iff_dvd)
+      then obtain q where q: "p = [:a, -1:] * q" by (elim dvdE) simp
+      with nz have q_nz: "q \<noteq> 0" by auto
+      have "degree p = Suc (degree q)"
+        by (subst q, subst degree_mult_eq) (simp_all add: q_nz)
+      hence "Q q" by (intro less) simp
+      from a(1) and this have "Q ([:a, -1:] * q)"
+        by (rule assms(3))
+      with q show ?thesis by simp
+    qed
+qed
+
+lemma dropWhile_replicate_append:
+  "dropWhile (op= a) (replicate n a @ ys) = dropWhile (op= a) ys"
+  by (induction n) simp_all
+
+lemma Poly_append_replicate_0: "Poly (xs @ replicate n 0) = Poly xs"
+  by (subst coeffs_eq_iff) (simp_all add: strip_while_def dropWhile_replicate_append)
+
+text \<open>
+  An induction rule for simultaneous induction over two polynomials,
+  prepending one coefficient in each step.
+\<close>
+lemma poly_induct2 [case_names 0 pCons]:
+  assumes "P 0 0" "\<And>a p b q. P p q \<Longrightarrow> P (pCons a p) (pCons b q)"
+  shows   "P p q"
+proof -
+  def n \<equiv> "max (length (coeffs p)) (length (coeffs q))"
+  def xs \<equiv> "coeffs p @ (replicate (n - length (coeffs p)) 0)"
+  def ys \<equiv> "coeffs q @ (replicate (n - length (coeffs q)) 0)"
+  have "length xs = length ys"
+    by (simp add: xs_def ys_def n_def)
+  hence "P (Poly xs) (Poly ys)"
+    by (induction rule: list_induct2) (simp_all add: assms)
+  also have "Poly xs = p"
+    by (simp add: xs_def Poly_append_replicate_0)
+  also have "Poly ys = q"
+    by (simp add: ys_def Poly_append_replicate_0)
+  finally show ?thesis .
+qed
+
+
subsection \<open>Composition of polynomials\<close>

definition pcompose :: "'a::comm_semiring_0 poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly"
@@ -1945,6 +2072,212 @@
apply (rule order_trans [OF degree_mult_le], simp)
done

+  fixes p q r :: "'a :: {comm_semiring_0, ab_semigroup_add} poly"
+  shows "pcompose (p + q) r = pcompose p r + pcompose q r"
+proof (induction p q rule: poly_induct2)
+  case (pCons a p b q)
+  have "pcompose (pCons a p + pCons b q) r =
+          [:a + b:] + r * pcompose p r + r * pcompose q r"
+    by (simp_all add: pcompose_pCons pCons.IH algebra_simps)
+  also have "[:a + b:] = [:a:] + [:b:]" by simp
+  also have "\<dots> + r * pcompose p r + r * pcompose q r =
+                 pcompose (pCons a p) r + pcompose (pCons b q) r"
+    by (simp only: pcompose_pCons add_ac)
+  finally show ?case .
+qed simp
+
+lemma pcompose_minus:
+  fixes p r :: "'a :: comm_ring poly"
+  shows "pcompose (-p) r = -pcompose p r"
+  by (induction p) (simp_all add: pcompose_pCons)
+
+lemma pcompose_diff:
+  fixes p q r :: "'a :: comm_ring poly"
+  shows "pcompose (p - q) r = pcompose p r - pcompose q r"
+
+lemma pcompose_smult:
+  fixes p r :: "'a :: comm_semiring_0 poly"
+  shows "pcompose (smult a p) r = smult a (pcompose p r)"
+  by (induction p)
+
+lemma pcompose_mult:
+  fixes p q r :: "'a :: comm_semiring_0 poly"
+  shows "pcompose (p * q) r = pcompose p r * pcompose q r"
+  by (induction p arbitrary: q)
+
+lemma pcompose_assoc:
+  "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) =
+     pcompose (pcompose p q) r"
+  by (induction p arbitrary: q)
+
+
+(* The remainder of this section and the next were contributed by Wenda Li *)
+
+lemma degree_mult_eq_0:
+  fixes p q:: "'a :: idom poly"
+  shows "degree (p*q) = 0 \<longleftrightarrow> p=0 \<or> q=0 \<or> (p\<noteq>0 \<and> q\<noteq>0 \<and> degree p =0 \<and> degree q =0)"
+
+lemma pcompose_const[simp]:"pcompose [:a:] q = [:a:]" by (subst pcompose_pCons,simp)
+
+lemma pcompose_0':"pcompose p 0=[:coeff p 0:]"
+  apply (induct p)
+done
+
+lemma degree_pcompose:
+  fixes p q:: "'a::idom poly"
+  shows "degree(pcompose p q) = degree p * degree q"
+proof (induct p)
+  case 0
+  thus ?case by auto
+next
+  case (pCons a p)
+  have "degree (q * pcompose p q) = 0 \<Longrightarrow> ?case"
+    proof (cases "p=0")
+      case True
+      thus ?thesis by auto
+    next
+      case False assume "degree (q * pcompose p q) = 0"
+      hence "degree q=0 \<or> pcompose p q=0" by (auto simp add:degree_mult_eq_0)
+      moreover have "\<lbrakk>pcompose p q=0;degree q\<noteq>0\<rbrakk> \<Longrightarrow> False" using pCons.hyps(2) `p\<noteq>0`
+        proof -
+          assume "pcompose p q=0" "degree q\<noteq>0"
+          hence "degree p=0" using pCons.hyps(2) by auto
+          then obtain a1 where "p=[:a1:]"
+            by (metis degree_pCons_eq_if old.nat.distinct(2) pCons_cases)
+          thus False using `pcompose p q=0` `p\<noteq>0` by auto
+        qed
+      ultimately have "degree (pCons a p) * degree q=0" by auto
+      moreover have "degree (pcompose (pCons a p) q) = 0"
+        proof -
+          have" 0 = max (degree [:a:]) (degree (q*pcompose p q))"
+            using `degree (q * pcompose p q) = 0` by simp
+          also have "... \<ge> degree ([:a:] + q * pcompose p q)"
+          finally show ?thesis by (auto simp add:pcompose_pCons)
+        qed
+      ultimately show ?thesis by simp
+    qed
+  moreover have "degree (q * pcompose p q)>0 \<Longrightarrow> ?case"
+    proof -
+      assume asm:"0 < degree (q * pcompose p q)"
+      hence "p\<noteq>0" "q\<noteq>0" "pcompose p q\<noteq>0" by auto
+      have "degree (pcompose (pCons a p) q) = degree ( q * pcompose p q)"
+        unfolding pcompose_pCons
+        using degree_add_eq_right[of "[:a:]" ] asm by auto
+      thus ?thesis
+        using pCons.hyps(2) degree_mult_eq[OF `q\<noteq>0` `pcompose p q\<noteq>0`] by auto
+    qed
+  ultimately show ?case by blast
+qed
+
+lemma pcompose_eq_0:
+  fixes p q:: "'a::idom poly"
+  assumes "pcompose p q=0" "degree q>0"
+  shows "p=0"
+proof -
+  have "degree p=0" using assms degree_pcompose[of p q] by auto
+  then obtain a where "p=[:a:]"
+    by (metis degree_pCons_eq_if gr0_conv_Suc neq0_conv pCons_cases)
+  hence "a=0" using assms(1) by auto
+  thus ?thesis using `p=[:a:]` by simp
+qed
+
+
+
+definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where
+  "lead_coeff p= coeff p (degree p)"
+
+    "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a"
+
+
+   fixes p q::"'a ::idom poly"
+
+  assumes "degree p < degree q"
+
+
+
+  fixes p q:: "'a::idom poly"
+  assumes "degree q > 0"
+proof (induct p)
+  case 0
+  thus ?case unfolding lead_coeff_def by auto
+next
+  case (pCons a p)
+  have "degree ( q * pcompose p q) = 0 \<Longrightarrow> ?case"
+    proof -
+      assume "degree ( q * pcompose p q) = 0"
+      hence "pcompose p q = 0" by (metis assms degree_0 degree_mult_eq_0 neq0_conv)
+      hence "p=0" using pcompose_eq_0[OF _ `degree q > 0`] by simp
+      thus ?thesis by auto
+    qed
+  moreover have "degree ( q * pcompose p q) > 0 \<Longrightarrow> ?case"
+    proof -
+      assume "degree ( q * pcompose p q) > 0"
+      hence "lead_coeff (pcompose (pCons a p) q) =lead_coeff ( q * pcompose p q)"
+        using pCons.hyps(2) lead_coeff_mult[of q "pcompose p q"] by simp
+      also have "... = lead_coeff p * lead_coeff q ^ (degree p + 1)"
+        by auto
+      finally show ?thesis by auto
+    qed
+  ultimately show ?case by blast
+qed
+
+  "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p"
+proof -
+  have "smult c p = [:c:] * p" by simp
+  finally show ?thesis .
+qed
+
+
+  "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})"
+
+  "lead_coeff (numeral n) = numeral n"
+  by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp
+
+  "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n"
+
+
+

no_notation cCons (infixr "##" 65)

--- a/src/HOL/List.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/List.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -3663,6 +3663,10 @@

+  "remdups_adj (replicate n x) = (if n = 0 then [] else [x])"
+  by (induction n) (auto simp: remdups_adj_Cons)
+
lemma remdups_upt [simp]: "remdups [m..<n] = [m..<n]"
proof (cases "m \<le> n")
case False then show ?thesis by simp
--- a/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 15:38:37 2016 +0100
+++ b/src/HOL/Multivariate_Analysis/Harmonic_Numbers.thy	Tue Jan 05 17:54:10 2016 +0100
@@ -72,6 +72,9 @@
lemma harm_nonneg: "harm n \<ge> (0 :: 'a :: {real_normed_field,linordered_field})"
unfolding harm_def by (intro setsum_nonneg) simp_all

+lemma harm_pos: "n > 0 \<Longrightarrow> harm n > (0 :: 'a :: {real_normed_field,linordered_field})"
+  unfolding harm_def by (intro setsum_pos) simp_all
+
lemma of_real_harm: "of_real (harm n) = harm n"
unfolding harm_def by simp

@@ -79,6 +82,7 @@
by (subst of_real_harm [symmetric]) (simp add: harm_nonneg)

lemma harm_expand:
+  "harm 0 = 0"
"harm (Suc 0) = 1"
"harm (numeral n) = harm (pred_numeral n) + inverse (numeral n)"
proof -
@@ -86,7 +90,7 @@
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)" .

lemma not_convergent_harm: "\<not>convergent (harm :: nat \<Rightarrow> 'a :: real_normed_field)"
proof -
@@ -102,6 +106,32 @@
finally show ?thesis by (blast dest: convergent_norm)
qed

+lemma harm_pos_iff [simp]: "harm n > (0 :: 'a :: {real_normed_field,linordered_field}) \<longleftrightarrow> n > 0"
+  by (rule iffI, cases n, simp add: harm_expand, simp, rule harm_pos)
+
+lemma ln_diff_le_inverse:
+  assumes "x \<ge> (1::real)"
+  shows   "ln (x + 1) - ln x < 1 / x"
+proof -
+  from assms have "\<exists>z>x. z < x + 1 \<and> ln (x + 1) - ln x = (x + 1 - x) * inverse z"
+    by (intro MVT2) (auto intro!: derivative_eq_intros simp: field_simps)
+  then obtain z where z: "z > x" "z < x + 1" "ln (x + 1) - ln x = inverse z" by auto
+  have "ln (x + 1) - ln x = inverse z" by fact
+  also from z(1,2) assms have "\<dots> < 1 / x" by (simp add: field_simps)
+  finally show ?thesis .
+qed
+
+lemma ln_le_harm: "ln (real n + 1) \<le> (harm n :: real)"
+proof (induction n)
+  fix n assume IH: "ln (real n + 1) \<le> harm n"
+  have "ln (real (Suc n) + 1) = ln (real n + 1) + (ln (real n + 2) - ln (real n + 1))" by simp
+  also have "(ln (real n + 2) - ln (real n + 1)) \<le> 1 / real (Suc n)"