# HG changeset patch
# User Manuel Eberl <eberlm@in.tum.de>
# Date 1472133043 -7200
# Node ID 492bb53c3420fd02d26e0eb6830e1f24f1bc701f
# Parent  bcf2123d059ab1242f17e700027038ba02bc8b97
More analysis lemmas

diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Analysis/Complex_Transcendental.thy
--- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -1396,6 +1396,22 @@
   ultimately show ?thesis by (simp add: sums_iff)
 qed
 
+lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
+  by (drule Ln_series) (simp add: power_minus')
+
+lemma ln_series': 
+  assumes "abs (x::real) < 1"
+  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
+proof -
+  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
+    by (intro Ln_series') simp_all
+  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
+    by (rule ext) simp
+  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))" 
+    by (subst Ln_of_real [symmetric]) simp_all
+  finally show ?thesis by (subst (asm) sums_of_real_iff)
+qed
+
 lemma Ln_approx_linear:
   fixes z :: complex
   assumes "norm z < 1"
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Analysis/Gamma_Function.thy
--- a/src/HOL/Analysis/Gamma_Function.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -709,6 +709,37 @@
   using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z]
   by (simp add: summable_iff_convergent)
 
+lemma Digamma_LIMSEQ:
+  fixes z :: "'a :: {banach,real_normed_field}"
+  assumes z: "z \<noteq> 0"
+  shows   "(\<lambda>m. of_real (ln (real m)) - (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
+proof -
+  have "(\<lambda>n. of_real (ln (real n / (real (Suc n))))) \<longlonglongrightarrow> (of_real (ln 1) :: 'a)"
+    by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all
+  hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
+  hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
+  proof (rule Lim_transform_eventually [rotated])
+    show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) = 
+            of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
+      using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
+  qed
+
+  from summable_Digamma[OF z]
+    have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n)) 
+              sums (Digamma z + euler_mascheroni)"
+    by (simp add: Digamma_def summable_sums)
+  from sums_diff[OF this euler_mascheroni_sum]
+    have "(\<lambda>n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
+            sums Digamma z" by (simp add: add_ac)
+  hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) - 
+              (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
+    by (simp add: sums_def setsum_subtractf)
+  also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) = 
+                 (\<lambda>m. of_real (ln (m + 1)) :: 'a)"
+    by (subst setsum_lessThan_telescope) simp_all
+  finally show ?thesis by (rule Lim_transform) (insert lim, simp)
+qed
+
 lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
   fixes z :: complex
   assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
@@ -1641,6 +1672,12 @@
   using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2)
   by (cases "x = y") simp_all
 
+lemma Digamma_real_strict_mono: "(0::real) < x \<Longrightarrow> x < y \<Longrightarrow> Digamma x < Digamma y"
+  by (rule Polygamma_real_strict_mono) simp_all
+
+lemma Digamma_real_mono: "(0::real) < x \<Longrightarrow> x \<le> y \<Longrightarrow> Digamma x \<le> Digamma y"
+  by (rule Polygamma_real_mono) simp_all
+
 lemma Digamma_real_ge_three_halves_pos:
   assumes "x \<ge> 3/2"
   shows   "Digamma (x :: real) > 0"
@@ -2871,6 +2908,18 @@
   using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms
   by simp
 
+theorem wallis: "(\<lambda>n. \<Prod>k=1..n. (4*real k^2) / (4*real k^2 - 1)) \<longlonglongrightarrow> pi / 2"
+proof -
+  from tendsto_inverse[OF tendsto_mult[OF 
+         sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
+    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2" 
+    by (simp add: setprod_inversef [symmetric])
+  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
+               (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
+    by (intro ext setprod.cong refl) (simp add: divide_simps)
+  finally show ?thesis .
+qed
+
 
 subsection \<open>The Solution to the Basel problem\<close>
 
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Analysis/Harmonic_Numbers.thy
--- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -173,13 +173,23 @@
   thus ?thesis by simp
 qed
 
-lemma euler_mascheroni_sum:
+lemma euler_mascheroni_sum_real:
   "(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)) :: real)
        sums euler_mascheroni"
  using sums_add[OF telescope_sums[OF LIMSEQ_Suc[OF euler_mascheroni_LIMSEQ]]
                    telescope_sums'[OF LIMSEQ_inverse_real_of_nat]]
   by (simp_all add: harm_def algebra_simps)
 
+lemma euler_mascheroni_sum:
+  "(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2))))
+       sums (euler_mascheroni :: 'a :: {banach, real_normed_field})"
+proof -
+  have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))))
+       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"
 proof -
   let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
@@ -342,17 +352,18 @@
   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
   fix n :: nat
-  note summable = sums_summable[OF euler_mascheroni_sum, folded D_def]
+  note summable = sums_summable[OF euler_mascheroni_sum_real, folded D_def]
   have sums: "(\<lambda>k. (inv (Suc (k + (n+1))) - inv (Suc (Suc k + (n+1))))/2) sums ((inv (Suc (0 + (n+1))) - 0)/2)"
     unfolding inv_def
     by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
   have sums': "(\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) sums ((inv (Suc (0 + n)) - 0)/2)"
     unfolding inv_def
     by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
-  from euler_mascheroni_sum have "euler_mascheroni = (\<Sum>k. D k)"
+  from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
     by (simp add: sums_iff D_def)
   also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
-    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], subst lessThan_Suc_atMost) simp
+    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
+        subst lessThan_Suc_atMost) simp
   finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
 
   note sum
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
--- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -12533,4 +12533,101 @@
   shows   "(\<lambda>x. x powr a) integrable_on {0..c}"
   using has_integral_powr_from_0[OF assms] unfolding integrable_on_def by blast
 
+lemma has_integral_powr_to_inf:
+  fixes a e :: real
+  assumes "e < -1" "a > 0"
+  shows   "((\<lambda>x. x powr e) has_integral -(a powr (e + 1)) / (e + 1)) {a..}"
+proof -
+  define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
+  define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
+
+  have has_integral_f: "(f n has_integral (F n - F a)) {a..}" 
+    if n: "n \<ge> a" for n :: nat
+  proof -
+    from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
+      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros 
+            simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
+    hence "(f n has_integral (F n - F a)) {a..n}"
+      by (rule has_integral_eq [rotated]) (simp add: f_def)
+    thus "(f n has_integral (F n - F a)) {a..}"
+      by (rule has_integral_on_superset [rotated 2]) (auto simp: f_def)
+  qed
+  have integral_f: "integral {a..} (f n) = (if n \<ge> a then F n - F a else 0)" for n :: nat
+  proof (cases "n \<ge> a")
+    case True
+    with has_integral_f[OF this] show ?thesis by (simp add: integral_unique)
+  next
+    case False
+    have "(f n has_integral 0) {a}" by (rule has_integral_refl)
+    hence "(f n has_integral 0) {a..}" 
+      by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
+    with False show ?thesis by (simp add: integral_unique)
+  qed
+  
+  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and> 
+           (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
+  proof (intro monotone_convergence_increasing allI ballI)
+    fix n :: nat
+    from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
+      by (auto intro!: integrable_continuous_real continuous_intros)
+    hence "f n integrable_on {a..n}"
+      by (rule integrable_eq [rotated]) (auto simp: f_def)
+    thus "f n integrable_on {a..}"
+      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
+  next
+    fix n :: nat and x :: real
+    show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
+  next
+    fix x :: real assume x: "x \<in> {a..}"
+    from filterlim_real_sequentially
+      have "eventually (\<lambda>n. real n \<ge> x) at_top"
+      by (simp add: filterlim_at_top)
+    with x have "eventually (\<lambda>n. f n x = x powr e) at_top" 
+      by (auto elim!: eventually_mono simp: f_def)
+    thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
+  next
+    have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
+    proof (cases "n \<ge> a")
+      case True
+      with assms have "a powr (e + 1) \<ge> n powr (e + 1)"
+        by (intro powr_mono2') simp_all
+      with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
+    qed (insert assms, simp add: integral_f F_def divide_simps)
+    thus "bounded {integral {a..} (f n) |n. True}"
+      unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
+  qed
+
+  from filterlim_real_sequentially
+    have "eventually (\<lambda>n. real n \<ge> a) at_top"
+    by (simp add: filterlim_at_top)
+  hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
+    by eventually_elim (simp add: integral_f)
+  moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
+    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr] 
+          filterlim_ident filterlim_real_sequentially | simp)+)
+  hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
+  ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
+  from conjunct2[OF *] and this 
+    have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
+  with conjunct1[OF *] show ?thesis
+    by (simp add: has_integral_integral F_def)
+qed
+
+lemma has_integral_inverse_power_to_inf:
+  fixes a :: real and n :: nat
+  assumes "n > 1" "a > 0"
+  shows   "((\<lambda>x. 1 / x ^ n) has_integral 1 / (real (n - 1) * a ^ (n - 1))) {a..}"
+proof -
+  from assms have "real_of_int (-int n) < -1" by simp
+  note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
+  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 
+                 1 / (real (n - 1) * a powr (real (n - 1)))" using assms
+    by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
+  also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
+    by (intro powr_realpow)
+  finally show ?thesis
+    by (rule has_integral_eq [rotated])
+       (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
+qed
+
 end
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Limits.thy
--- a/src/HOL/Limits.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Limits.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -1519,7 +1519,7 @@
   unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
 
 lemma filterlim_pow_at_top:
-  fixes f :: "real \<Rightarrow> real"
+  fixes f :: "'a \<Rightarrow> real"
   assumes "0 < n"
     and f: "LIM x F. f x :> at_top"
   shows "LIM x F. (f x)^n :: real :> at_top"
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/NthRoot.thy
--- a/src/HOL/NthRoot.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/NthRoot.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -469,6 +469,14 @@
 lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
   using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
 
+lemma real_sqrt_power_even: 
+  assumes "even n" "x \<ge> 0"
+  shows   "sqrt x ^ n = x ^ (n div 2)"
+proof -
+  from assms obtain k where "n = 2*k" by (auto elim!: evenE)
+  with assms show ?thesis by (simp add: power_mult)
+qed
+
 lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
   by (meson not_le real_less_rsqrt)
 
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Set_Interval.thy
--- a/src/HOL/Set_Interval.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Set_Interval.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -1846,6 +1846,14 @@
   shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
   by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
 
+lemma setsum_lessThan_telescope:
+  "(\<Sum>n<m. f (Suc n) - f n :: 'a :: ab_group_add) = f m - f 0"
+  by (induction m) (simp_all add: algebra_simps)
+
+lemma setsum_lessThan_telescope':
+  "(\<Sum>n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m"
+  by (induction m) (simp_all add: algebra_simps)
+
 
 subsubsection \<open>The formula for geometric sums\<close>
 
diff -r bcf2123d059a -r 492bb53c3420 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Aug 24 11:02:23 2016 +0200
+++ b/src/HOL/Transcendental.thy	Thu Aug 25 15:50:43 2016 +0200
@@ -794,6 +794,44 @@
   using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
   by (force simp del: of_real_add)
 
+lemma termdiffs_strong':
+  fixes z :: "'a :: {real_normed_field,banach}"
+  assumes "\<And>z. norm z < K \<Longrightarrow> summable (\<lambda>n. c n * z ^ n)"
+  assumes "norm z < K"
+  shows   "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+proof (rule termdiffs_strong)
+  define L :: real where "L =  (norm z + K) / 2"
+  have "0 \<le> norm z" by simp
+  also note \<open>norm z < K\<close>
+  finally have K: "K \<ge> 0" by simp
+  from assms K have L: "L \<ge> 0" "norm z < L" "L < K" by (simp_all add: L_def)
+  from L show "norm z < norm (of_real L :: 'a)" by simp
+  from L show "summable (\<lambda>n. c n * of_real L ^ n)" by (intro assms(1)) simp_all
+qed
+
+lemma termdiffs_sums_strong:
+  fixes z :: "'a :: {banach,real_normed_field}"
+  assumes sums: "\<And>z. norm z < K \<Longrightarrow> (\<lambda>n. c n * z ^ n) sums f z"
+  assumes deriv: "(f has_field_derivative f') (at z)"
+  assumes norm: "norm z < K"
+  shows   "(\<lambda>n. diffs c n * z ^ n) sums f'"
+proof -
+  have summable: "summable (\<lambda>n. diffs c n * z^n)"
+    by (intro termdiff_converges[OF norm] sums_summable[OF sums])
+  from norm have "eventually (\<lambda>z. z \<in> norm -` {..<K}) (nhds z)"
+    by (intro eventually_nhds_in_open open_vimage) 
+       (simp_all add: continuous_on_norm continuous_on_id)
+  hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)"
+    by eventually_elim (insert sums, simp add: sums_iff)
+
+  have "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+    by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums])
+  hence "(f has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
+    by (subst (asm) DERIV_cong_ev[OF refl eq refl])
+  from this and deriv have "(\<Sum>n. diffs c n * z^n) = f'" by (rule DERIV_unique)
+  with summable show ?thesis by (simp add: sums_iff)
+qed
+
 lemma isCont_powser:
   fixes K x :: "'a::{real_normed_field,banach}"
   assumes "summable (\<lambda>n. c n * K ^ n)"
@@ -1114,6 +1152,18 @@
   from for_subinterval[OF this] show ?thesis .
 qed
 
+lemma geometric_deriv_sums:
+  fixes z :: "'a :: {real_normed_field,banach}"
+  assumes "norm z < 1"
+  shows   "(\<lambda>n. of_nat (Suc n) * z ^ n) sums (1 / (1 - z)^2)"
+proof -
+  have "(\<lambda>n. diffs (\<lambda>n. 1) n * z^n) sums (1 / (1 - z)^2)"
+  proof (rule termdiffs_sums_strong)
+    fix z :: 'a assume "norm z < 1"
+    thus "(\<lambda>n. 1 * z^n) sums (1 / (1 - z))" by (simp add: geometric_sums)
+  qed (insert assms, auto intro!: derivative_eq_intros simp: power2_eq_square)
+  thus ?thesis unfolding diffs_def by simp
+qed
 
 lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z. pochhammer z n) z"
   for z :: "'a::real_normed_field"