summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | eberlm |

Tue, 05 Jan 2016 17:54:10 +0100 | |

changeset 62065 | 1546a042e87b |

parent 62060 | b75764fc4c35 |

child 62066 | 4db2d39aa76c |

Added some facts about polynomials

--- 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` + by (auto simp add:field_simps) + 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:]" + by (metis (no_types, hide_lams) One_nat_def add_Suc_right monoid_add_class.add.right_neutral + 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" + by (simp add: coeffs_def) + +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" by (simp add: cCons_def) @@ -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) - + subsection \<open>Addition and subtraction\<close> instantiation poly :: (comm_monoid_add) comm_monoid_add @@ -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" + by (simp add: of_nat_poly) + +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 subsection \<open>Lemmas about divisibility\<close> @@ -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 @@ by (simp add: gcd_poly.simps) +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 (simp add: assms(1)) +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 +lemma pcompose_add: + 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" + using pcompose_add[of p "-q"] by (simp add: pcompose_minus) + +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) + (simp_all add: pcompose_pCons pcompose_add smult_add_right) + +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) + (simp_all add: pcompose_add pcompose_smult pcompose_pCons algebra_simps) + +lemma pcompose_assoc: + "pcompose p (pcompose q r :: 'a :: comm_semiring_0 poly ) = + pcompose (pcompose p q) r" + by (induction p arbitrary: q) + (simp_all add: pcompose_pCons pcompose_add pcompose_mult) + + +(* 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)" +by (auto simp add:degree_mult_eq) + +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) + apply (auto simp add:pcompose_pCons) +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)" + by (rule degree_add_le_max) + 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 + + +section{*lead coefficient*} + +definition lead_coeff:: "'a::zero poly \<Rightarrow> 'a" where + "lead_coeff p= coeff p (degree p)" + +lemma lead_coeff_pCons[simp]: + "p\<noteq>0 \<Longrightarrow>lead_coeff (pCons a p) = lead_coeff p" + "p=0 \<Longrightarrow> lead_coeff (pCons a p) = a" +unfolding lead_coeff_def by auto + +lemma lead_coeff_0[simp]:"lead_coeff 0 =0" + unfolding lead_coeff_def by auto + +lemma lead_coeff_mult: + fixes p q::"'a ::idom poly" + shows "lead_coeff (p * q) = lead_coeff p * lead_coeff q" +by (unfold lead_coeff_def,cases "p=0 \<or> q=0",auto simp add:coeff_mult_degree_sum degree_mult_eq) + +lemma lead_coeff_add_le: + assumes "degree p < degree q" + shows "lead_coeff (p+q) = lead_coeff q" +using assms unfolding lead_coeff_def +by (metis coeff_add coeff_eq_0 monoid_add_class.add.left_neutral degree_add_eq_right) + +lemma lead_coeff_minus: + "lead_coeff (-p) = - lead_coeff p" +by (metis coeff_minus degree_minus lead_coeff_def) + + +lemma lead_coeff_comp: + fixes p q:: "'a::idom poly" + assumes "degree q > 0" + shows "lead_coeff (pcompose p q) = lead_coeff p * lead_coeff q ^ (degree p)" +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)" + by (auto simp add:pcompose_pCons lead_coeff_add_le) + also have "... = lead_coeff q * (lead_coeff p * lead_coeff q ^ degree p)" + 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 + +lemma lead_coeff_smult: + "lead_coeff (smult c p :: 'a :: idom poly) = c * lead_coeff p" +proof - + have "smult c p = [:c:] * p" by simp + also have "lead_coeff \<dots> = c * lead_coeff p" + by (subst lead_coeff_mult) simp_all + finally show ?thesis . +qed + +lemma lead_coeff_1 [simp]: "lead_coeff 1 = 1" + by (simp add: lead_coeff_def) + +lemma lead_coeff_of_nat [simp]: + "lead_coeff (of_nat n) = (of_nat n :: 'a :: {comm_semiring_1,semiring_char_0})" + by (induction n) (simp_all add: lead_coeff_def of_nat_poly) + +lemma lead_coeff_numeral [simp]: + "lead_coeff (numeral n) = numeral n" + unfolding lead_coeff_def + by (subst of_nat_numeral [symmetric], subst of_nat_poly) simp + +lemma lead_coeff_power: + "lead_coeff (p ^ n :: 'a :: idom poly) = lead_coeff p ^ n" + by (induction n) (simp_all add: lead_coeff_mult) + +lemma lead_coeff_nonzero: "p \<noteq> 0 \<Longrightarrow> lead_coeff p \<noteq> 0" + by (simp add: lead_coeff_def) + + 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 @@ shows "remdups_adj (map f xs) = map f (remdups_adj xs)" by (induct xs rule: remdups_adj.induct) (auto simp add: injD[OF assms]) +lemma remdups_adj_replicate: + "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)" . -qed (simp add: harm_def) +qed (simp_all add: harm_def) 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)" + using ln_diff_le_inverse[of "real n + 1"] by (simp add: add_ac) + also note IH + also have "harm n + 1 / real (Suc n) = harm (Suc n)" by (simp add: harm_Suc field_simps) + finally show "ln (real (Suc n) + 1) \<le> harm (Suc n)" by - simp +qed (simp_all add: harm_def) + subsection \<open>The Eulerâ€“Mascheroni constant\<close>