More analysis lemmas
authorManuel Eberl <eberlm@in.tum.de>
Thu Aug 25 15:50:43 2016 +0200 (2016-08-25)
changeset 63721492bb53c3420
parent 63720 bcf2123d059a
child 63722 b9c8da46443b
More analysis lemmas
src/HOL/Analysis/Complex_Transcendental.thy
src/HOL/Analysis/Gamma_Function.thy
src/HOL/Analysis/Harmonic_Numbers.thy
src/HOL/Analysis/Henstock_Kurzweil_Integration.thy
src/HOL/Limits.thy
src/HOL/NthRoot.thy
src/HOL/Set_Interval.thy
src/HOL/Transcendental.thy
     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Wed Aug 24 11:02:23 2016 +0200
     1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 25 15:50:43 2016 +0200
     1.3 @@ -1396,6 +1396,22 @@
     1.4    ultimately show ?thesis by (simp add: sums_iff)
     1.5  qed
     1.6  
     1.7 +lemma Ln_series': "cmod z < 1 \<Longrightarrow> (\<lambda>n. - ((-z)^n) / of_nat n) sums ln (1 + z)"
     1.8 +  by (drule Ln_series) (simp add: power_minus')
     1.9 +
    1.10 +lemma ln_series': 
    1.11 +  assumes "abs (x::real) < 1"
    1.12 +  shows   "(\<lambda>n. - ((-x)^n) / of_nat n) sums ln (1 + x)"
    1.13 +proof -
    1.14 +  from assms have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) sums ln (1 + complex_of_real x)"
    1.15 +    by (intro Ln_series') simp_all
    1.16 +  also have "(\<lambda>n. - ((-of_real x)^n) / of_nat n) = (\<lambda>n. complex_of_real (- ((-x)^n) / of_nat n))"
    1.17 +    by (rule ext) simp
    1.18 +  also from assms have "ln (1 + complex_of_real x) = of_real (ln (1 + x))" 
    1.19 +    by (subst Ln_of_real [symmetric]) simp_all
    1.20 +  finally show ?thesis by (subst (asm) sums_of_real_iff)
    1.21 +qed
    1.22 +
    1.23  lemma Ln_approx_linear:
    1.24    fixes z :: complex
    1.25    assumes "norm z < 1"
     2.1 --- a/src/HOL/Analysis/Gamma_Function.thy	Wed Aug 24 11:02:23 2016 +0200
     2.2 +++ b/src/HOL/Analysis/Gamma_Function.thy	Thu Aug 25 15:50:43 2016 +0200
     2.3 @@ -709,6 +709,37 @@
     2.4    using uniformly_convergent_imp_convergent[OF Polygamma_converges[OF assms, of 1], of z]
     2.5    by (simp add: summable_iff_convergent)
     2.6  
     2.7 +lemma Digamma_LIMSEQ:
     2.8 +  fixes z :: "'a :: {banach,real_normed_field}"
     2.9 +  assumes z: "z \<noteq> 0"
    2.10 +  shows   "(\<lambda>m. of_real (ln (real m)) - (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
    2.11 +proof -
    2.12 +  have "(\<lambda>n. of_real (ln (real n / (real (Suc n))))) \<longlonglongrightarrow> (of_real (ln 1) :: 'a)"
    2.13 +    by (intro tendsto_intros LIMSEQ_n_over_Suc_n) simp_all
    2.14 +  hence "(\<lambda>n. of_real (ln (real n / (real n + 1)))) \<longlonglongrightarrow> (0 :: 'a)" by (simp add: add_ac)
    2.15 +  hence lim: "(\<lambda>n. of_real (ln (real n)) - of_real (ln (real n + 1))) \<longlonglongrightarrow> (0::'a)"
    2.16 +  proof (rule Lim_transform_eventually [rotated])
    2.17 +    show "eventually (\<lambda>n. of_real (ln (real n / (real n + 1))) = 
    2.18 +            of_real (ln (real n)) - (of_real (ln (real n + 1)) :: 'a)) at_top"
    2.19 +      using eventually_gt_at_top[of "0::nat"] by eventually_elim (simp add: ln_div)
    2.20 +  qed
    2.21 +
    2.22 +  from summable_Digamma[OF z]
    2.23 +    have "(\<lambda>n. inverse (of_nat (n+1)) - inverse (z + of_nat n)) 
    2.24 +              sums (Digamma z + euler_mascheroni)"
    2.25 +    by (simp add: Digamma_def summable_sums)
    2.26 +  from sums_diff[OF this euler_mascheroni_sum]
    2.27 +    have "(\<lambda>n. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)) - inverse (z + of_nat n))
    2.28 +            sums Digamma z" by (simp add: add_ac)
    2.29 +  hence "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1))) - 
    2.30 +              (\<Sum>n<m. inverse (z + of_nat n))) \<longlonglongrightarrow> Digamma z"
    2.31 +    by (simp add: sums_def setsum_subtractf)
    2.32 +  also have "(\<lambda>m. (\<Sum>n<m. of_real (ln (real (Suc n) + 1)) - of_real (ln (real n + 1)))) = 
    2.33 +                 (\<lambda>m. of_real (ln (m + 1)) :: 'a)"
    2.34 +    by (subst setsum_lessThan_telescope) simp_all
    2.35 +  finally show ?thesis by (rule Lim_transform) (insert lim, simp)
    2.36 +qed
    2.37 +
    2.38  lemma has_field_derivative_ln_Gamma_complex [derivative_intros]:
    2.39    fixes z :: complex
    2.40    assumes z: "z \<notin> \<real>\<^sub>\<le>\<^sub>0"
    2.41 @@ -1641,6 +1672,12 @@
    2.42    using Polygamma_real_strict_mono[OF assms(1) _ assms(3), of y] assms(2)
    2.43    by (cases "x = y") simp_all
    2.44  
    2.45 +lemma Digamma_real_strict_mono: "(0::real) < x \<Longrightarrow> x < y \<Longrightarrow> Digamma x < Digamma y"
    2.46 +  by (rule Polygamma_real_strict_mono) simp_all
    2.47 +
    2.48 +lemma Digamma_real_mono: "(0::real) < x \<Longrightarrow> x \<le> y \<Longrightarrow> Digamma x \<le> Digamma y"
    2.49 +  by (rule Polygamma_real_mono) simp_all
    2.50 +
    2.51  lemma Digamma_real_ge_three_halves_pos:
    2.52    assumes "x \<ge> 3/2"
    2.53    shows   "Digamma (x :: real) > 0"
    2.54 @@ -2871,6 +2908,18 @@
    2.55    using tendsto_divide[OF sin_product_formula_real[of x] tendsto_const[of "pi * x"]] assms
    2.56    by simp
    2.57  
    2.58 +theorem wallis: "(\<lambda>n. \<Prod>k=1..n. (4*real k^2) / (4*real k^2 - 1)) \<longlonglongrightarrow> pi / 2"
    2.59 +proof -
    2.60 +  from tendsto_inverse[OF tendsto_mult[OF 
    2.61 +         sin_product_formula_real[of "1/2"] tendsto_const[of "2/pi"]]]
    2.62 +    have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) \<longlonglongrightarrow> pi/2" 
    2.63 +    by (simp add: setprod_inversef [symmetric])
    2.64 +  also have "(\<lambda>n. (\<Prod>k=1..n. inverse (1 - (1 / 2)\<^sup>2 / (real k)\<^sup>2))) =
    2.65 +               (\<lambda>n. (\<Prod>k=1..n. (4*real k^2)/(4*real k^2 - 1)))"
    2.66 +    by (intro ext setprod.cong refl) (simp add: divide_simps)
    2.67 +  finally show ?thesis .
    2.68 +qed
    2.69 +
    2.70  
    2.71  subsection \<open>The Solution to the Basel problem\<close>
    2.72  
     3.1 --- a/src/HOL/Analysis/Harmonic_Numbers.thy	Wed Aug 24 11:02:23 2016 +0200
     3.2 +++ b/src/HOL/Analysis/Harmonic_Numbers.thy	Thu Aug 25 15:50:43 2016 +0200
     3.3 @@ -173,13 +173,23 @@
     3.4    thus ?thesis by simp
     3.5  qed
     3.6  
     3.7 -lemma euler_mascheroni_sum:
     3.8 +lemma euler_mascheroni_sum_real:
     3.9    "(\<lambda>n. inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2)) :: real)
    3.10         sums euler_mascheroni"
    3.11   using sums_add[OF telescope_sums[OF LIMSEQ_Suc[OF euler_mascheroni_LIMSEQ]]
    3.12                     telescope_sums'[OF LIMSEQ_inverse_real_of_nat]]
    3.13    by (simp_all add: harm_def algebra_simps)
    3.14  
    3.15 +lemma euler_mascheroni_sum:
    3.16 +  "(\<lambda>n. inverse (of_nat (n+1)) + of_real (ln (of_nat (n+1))) - of_real (ln (of_nat (n+2))))
    3.17 +       sums (euler_mascheroni :: 'a :: {banach, real_normed_field})"
    3.18 +proof -
    3.19 +  have "(\<lambda>n. of_real (inverse (of_nat (n+1)) + ln (of_nat (n+1)) - ln (of_nat (n+2))))
    3.20 +       sums (of_real euler_mascheroni :: 'a :: {banach, real_normed_field})"
    3.21 +    by (subst sums_of_real_iff) (rule euler_mascheroni_sum_real)
    3.22 +  thus ?thesis by simp
    3.23 +qed
    3.24 +
    3.25  lemma alternating_harmonic_series_sums: "(\<lambda>k. (-1)^k / real_of_nat (Suc k)) sums ln 2"
    3.26  proof -
    3.27    let ?f = "\<lambda>n. harm n - ln (real_of_nat n)"
    3.28 @@ -342,17 +352,18 @@
    3.29    let ?g = "\<lambda>n. ln (of_nat (n+2)) - ln (of_nat (n+1)) - inverse (of_nat (n+1)) :: real"
    3.30    define inv where [abs_def]: "inv n = inverse (real_of_nat n)" for n
    3.31    fix n :: nat
    3.32 -  note summable = sums_summable[OF euler_mascheroni_sum, folded D_def]
    3.33 +  note summable = sums_summable[OF euler_mascheroni_sum_real, folded D_def]
    3.34    have sums: "(\<lambda>k. (inv (Suc (k + (n+1))) - inv (Suc (Suc k + (n+1))))/2) sums ((inv (Suc (0 + (n+1))) - 0)/2)"
    3.35      unfolding inv_def
    3.36      by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
    3.37    have sums': "(\<lambda>k. (inv (Suc (k + n)) - inv (Suc (Suc k + n)))/2) sums ((inv (Suc (0 + n)) - 0)/2)"
    3.38      unfolding inv_def
    3.39      by (intro sums_divide telescope_sums' LIMSEQ_ignore_initial_segment LIMSEQ_inverse_real_of_nat)
    3.40 -  from euler_mascheroni_sum have "euler_mascheroni = (\<Sum>k. D k)"
    3.41 +  from euler_mascheroni_sum_real have "euler_mascheroni = (\<Sum>k. D k)"
    3.42      by (simp add: sums_iff D_def)
    3.43    also have "\<dots> = (\<Sum>k. D (k + Suc n)) + (\<Sum>k\<le>n. D k)"
    3.44 -    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], subst lessThan_Suc_atMost) simp
    3.45 +    by (subst suminf_split_initial_segment[OF summable, of "Suc n"], 
    3.46 +        subst lessThan_Suc_atMost) simp
    3.47    finally have sum: "(\<Sum>k\<le>n. D k) - euler_mascheroni = -(\<Sum>k. D (k + Suc n))" by simp
    3.48  
    3.49    note sum
     4.1 --- a/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Wed Aug 24 11:02:23 2016 +0200
     4.2 +++ b/src/HOL/Analysis/Henstock_Kurzweil_Integration.thy	Thu Aug 25 15:50:43 2016 +0200
     4.3 @@ -12533,4 +12533,101 @@
     4.4    shows   "(\<lambda>x. x powr a) integrable_on {0..c}"
     4.5    using has_integral_powr_from_0[OF assms] unfolding integrable_on_def by blast
     4.6  
     4.7 +lemma has_integral_powr_to_inf:
     4.8 +  fixes a e :: real
     4.9 +  assumes "e < -1" "a > 0"
    4.10 +  shows   "((\<lambda>x. x powr e) has_integral -(a powr (e + 1)) / (e + 1)) {a..}"
    4.11 +proof -
    4.12 +  define f :: "nat \<Rightarrow> real \<Rightarrow> real" where "f = (\<lambda>n x. if x \<in> {a..n} then x powr e else 0)"
    4.13 +  define F where "F = (\<lambda>x. x powr (e + 1) / (e + 1))"
    4.14 +
    4.15 +  have has_integral_f: "(f n has_integral (F n - F a)) {a..}" 
    4.16 +    if n: "n \<ge> a" for n :: nat
    4.17 +  proof -
    4.18 +    from n assms have "((\<lambda>x. x powr e) has_integral (F n - F a)) {a..n}"
    4.19 +      by (intro fundamental_theorem_of_calculus) (auto intro!: derivative_eq_intros 
    4.20 +            simp: has_field_derivative_iff_has_vector_derivative [symmetric] F_def)
    4.21 +    hence "(f n has_integral (F n - F a)) {a..n}"
    4.22 +      by (rule has_integral_eq [rotated]) (simp add: f_def)
    4.23 +    thus "(f n has_integral (F n - F a)) {a..}"
    4.24 +      by (rule has_integral_on_superset [rotated 2]) (auto simp: f_def)
    4.25 +  qed
    4.26 +  have integral_f: "integral {a..} (f n) = (if n \<ge> a then F n - F a else 0)" for n :: nat
    4.27 +  proof (cases "n \<ge> a")
    4.28 +    case True
    4.29 +    with has_integral_f[OF this] show ?thesis by (simp add: integral_unique)
    4.30 +  next
    4.31 +    case False
    4.32 +    have "(f n has_integral 0) {a}" by (rule has_integral_refl)
    4.33 +    hence "(f n has_integral 0) {a..}" 
    4.34 +      by (rule has_integral_on_superset [rotated 2]) (insert False, simp_all add: f_def)
    4.35 +    with False show ?thesis by (simp add: integral_unique)
    4.36 +  qed
    4.37 +  
    4.38 +  have *: "(\<lambda>x. x powr e) integrable_on {a..} \<and> 
    4.39 +           (\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> integral {a..} (\<lambda>x. x powr e)"
    4.40 +  proof (intro monotone_convergence_increasing allI ballI)
    4.41 +    fix n :: nat
    4.42 +    from assms have "(\<lambda>x. x powr e) integrable_on {a..n}"
    4.43 +      by (auto intro!: integrable_continuous_real continuous_intros)
    4.44 +    hence "f n integrable_on {a..n}"
    4.45 +      by (rule integrable_eq [rotated]) (auto simp: f_def)
    4.46 +    thus "f n integrable_on {a..}"
    4.47 +      by (rule integrable_on_superset [rotated 2]) (auto simp: f_def)
    4.48 +  next
    4.49 +    fix n :: nat and x :: real
    4.50 +    show "f n x \<le> f (Suc n) x" by (auto simp: f_def)
    4.51 +  next
    4.52 +    fix x :: real assume x: "x \<in> {a..}"
    4.53 +    from filterlim_real_sequentially
    4.54 +      have "eventually (\<lambda>n. real n \<ge> x) at_top"
    4.55 +      by (simp add: filterlim_at_top)
    4.56 +    with x have "eventually (\<lambda>n. f n x = x powr e) at_top" 
    4.57 +      by (auto elim!: eventually_mono simp: f_def)
    4.58 +    thus "(\<lambda>n. f n x) \<longlonglongrightarrow> x powr e" by (simp add: Lim_eventually)
    4.59 +  next
    4.60 +    have "norm (integral {a..} (f n)) \<le> -F a" for n :: nat
    4.61 +    proof (cases "n \<ge> a")
    4.62 +      case True
    4.63 +      with assms have "a powr (e + 1) \<ge> n powr (e + 1)"
    4.64 +        by (intro powr_mono2') simp_all
    4.65 +      with assms show ?thesis by (auto simp: divide_simps F_def integral_f)
    4.66 +    qed (insert assms, simp add: integral_f F_def divide_simps)
    4.67 +    thus "bounded {integral {a..} (f n) |n. True}"
    4.68 +      unfolding bounded_iff by (intro exI[of _ "-F a"]) auto
    4.69 +  qed
    4.70 +
    4.71 +  from filterlim_real_sequentially
    4.72 +    have "eventually (\<lambda>n. real n \<ge> a) at_top"
    4.73 +    by (simp add: filterlim_at_top)
    4.74 +  hence "eventually (\<lambda>n. F n - F a = integral {a..} (f n)) at_top"
    4.75 +    by eventually_elim (simp add: integral_f)
    4.76 +  moreover have "(\<lambda>n. F n - F a) \<longlonglongrightarrow> 0 / (e + 1) - F a" unfolding F_def
    4.77 +    by (insert assms, (rule tendsto_intros filterlim_compose[OF tendsto_neg_powr] 
    4.78 +          filterlim_ident filterlim_real_sequentially | simp)+)
    4.79 +  hence "(\<lambda>n. F n - F a) \<longlonglongrightarrow> -F a" by simp
    4.80 +  ultimately have "(\<lambda>n. integral {a..} (f n)) \<longlonglongrightarrow> -F a" by (rule Lim_transform_eventually)
    4.81 +  from conjunct2[OF *] and this 
    4.82 +    have "integral {a..} (\<lambda>x. x powr e) = -F a" by (rule LIMSEQ_unique)
    4.83 +  with conjunct1[OF *] show ?thesis
    4.84 +    by (simp add: has_integral_integral F_def)
    4.85 +qed
    4.86 +
    4.87 +lemma has_integral_inverse_power_to_inf:
    4.88 +  fixes a :: real and n :: nat
    4.89 +  assumes "n > 1" "a > 0"
    4.90 +  shows   "((\<lambda>x. 1 / x ^ n) has_integral 1 / (real (n - 1) * a ^ (n - 1))) {a..}"
    4.91 +proof -
    4.92 +  from assms have "real_of_int (-int n) < -1" by simp
    4.93 +  note has_integral_powr_to_inf[OF this \<open>a > 0\<close>]
    4.94 +  also have "- (a powr (real_of_int (- int n) + 1)) / (real_of_int (- int n) + 1) = 
    4.95 +                 1 / (real (n - 1) * a powr (real (n - 1)))" using assms
    4.96 +    by (simp add: divide_simps powr_add [symmetric] of_nat_diff)
    4.97 +  also from assms have "a powr (real (n - 1)) = a ^ (n - 1)"
    4.98 +    by (intro powr_realpow)
    4.99 +  finally show ?thesis
   4.100 +    by (rule has_integral_eq [rotated])
   4.101 +       (insert assms, simp_all add: powr_minus powr_realpow divide_simps)
   4.102 +qed
   4.103 +
   4.104  end
     5.1 --- a/src/HOL/Limits.thy	Wed Aug 24 11:02:23 2016 +0200
     5.2 +++ b/src/HOL/Limits.thy	Thu Aug 25 15:50:43 2016 +0200
     5.3 @@ -1519,7 +1519,7 @@
     5.4    unfolding filterlim_uminus_at_bot tendsto_minus_cancel_left by simp
     5.5  
     5.6  lemma filterlim_pow_at_top:
     5.7 -  fixes f :: "real \<Rightarrow> real"
     5.8 +  fixes f :: "'a \<Rightarrow> real"
     5.9    assumes "0 < n"
    5.10      and f: "LIM x F. f x :> at_top"
    5.11    shows "LIM x F. (f x)^n :: real :> at_top"
     6.1 --- a/src/HOL/NthRoot.thy	Wed Aug 24 11:02:23 2016 +0200
     6.2 +++ b/src/HOL/NthRoot.thy	Thu Aug 25 15:50:43 2016 +0200
     6.3 @@ -469,6 +469,14 @@
     6.4  lemma real_less_rsqrt: "x\<^sup>2 < y \<Longrightarrow> x < sqrt y"
     6.5    using real_sqrt_less_mono[of "x\<^sup>2" y] by simp
     6.6  
     6.7 +lemma real_sqrt_power_even: 
     6.8 +  assumes "even n" "x \<ge> 0"
     6.9 +  shows   "sqrt x ^ n = x ^ (n div 2)"
    6.10 +proof -
    6.11 +  from assms obtain k where "n = 2*k" by (auto elim!: evenE)
    6.12 +  with assms show ?thesis by (simp add: power_mult)
    6.13 +qed
    6.14 +
    6.15  lemma sqrt_le_D: "sqrt x \<le> y \<Longrightarrow> x \<le> y\<^sup>2"
    6.16    by (meson not_le real_less_rsqrt)
    6.17  
     7.1 --- a/src/HOL/Set_Interval.thy	Wed Aug 24 11:02:23 2016 +0200
     7.2 +++ b/src/HOL/Set_Interval.thy	Thu Aug 25 15:50:43 2016 +0200
     7.3 @@ -1846,6 +1846,14 @@
     7.4    shows   "(\<Sum>k\<in>{Suc m..n}. f k - f (k - 1)) = f n - (f m :: 'a :: ab_group_add)"
     7.5    by (rule dec_induct[OF assms]) (simp_all add: algebra_simps)
     7.6  
     7.7 +lemma setsum_lessThan_telescope:
     7.8 +  "(\<Sum>n<m. f (Suc n) - f n :: 'a :: ab_group_add) = f m - f 0"
     7.9 +  by (induction m) (simp_all add: algebra_simps)
    7.10 +
    7.11 +lemma setsum_lessThan_telescope':
    7.12 +  "(\<Sum>n<m. f n - f (Suc n) :: 'a :: ab_group_add) = f 0 - f m"
    7.13 +  by (induction m) (simp_all add: algebra_simps)
    7.14 +
    7.15  
    7.16  subsubsection \<open>The formula for geometric sums\<close>
    7.17  
     8.1 --- a/src/HOL/Transcendental.thy	Wed Aug 24 11:02:23 2016 +0200
     8.2 +++ b/src/HOL/Transcendental.thy	Thu Aug 25 15:50:43 2016 +0200
     8.3 @@ -794,6 +794,44 @@
     8.4    using termdiffs_strong[OF assms[of "of_real (norm x + 1)"], of x]
     8.5    by (force simp del: of_real_add)
     8.6  
     8.7 +lemma termdiffs_strong':
     8.8 +  fixes z :: "'a :: {real_normed_field,banach}"
     8.9 +  assumes "\<And>z. norm z < K \<Longrightarrow> summable (\<lambda>n. c n * z ^ n)"
    8.10 +  assumes "norm z < K"
    8.11 +  shows   "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
    8.12 +proof (rule termdiffs_strong)
    8.13 +  define L :: real where "L =  (norm z + K) / 2"
    8.14 +  have "0 \<le> norm z" by simp
    8.15 +  also note \<open>norm z < K\<close>
    8.16 +  finally have K: "K \<ge> 0" by simp
    8.17 +  from assms K have L: "L \<ge> 0" "norm z < L" "L < K" by (simp_all add: L_def)
    8.18 +  from L show "norm z < norm (of_real L :: 'a)" by simp
    8.19 +  from L show "summable (\<lambda>n. c n * of_real L ^ n)" by (intro assms(1)) simp_all
    8.20 +qed
    8.21 +
    8.22 +lemma termdiffs_sums_strong:
    8.23 +  fixes z :: "'a :: {banach,real_normed_field}"
    8.24 +  assumes sums: "\<And>z. norm z < K \<Longrightarrow> (\<lambda>n. c n * z ^ n) sums f z"
    8.25 +  assumes deriv: "(f has_field_derivative f') (at z)"
    8.26 +  assumes norm: "norm z < K"
    8.27 +  shows   "(\<lambda>n. diffs c n * z ^ n) sums f'"
    8.28 +proof -
    8.29 +  have summable: "summable (\<lambda>n. diffs c n * z^n)"
    8.30 +    by (intro termdiff_converges[OF norm] sums_summable[OF sums])
    8.31 +  from norm have "eventually (\<lambda>z. z \<in> norm -` {..<K}) (nhds z)"
    8.32 +    by (intro eventually_nhds_in_open open_vimage) 
    8.33 +       (simp_all add: continuous_on_norm continuous_on_id)
    8.34 +  hence eq: "eventually (\<lambda>z. (\<Sum>n. c n * z^n) = f z) (nhds z)"
    8.35 +    by eventually_elim (insert sums, simp add: sums_iff)
    8.36 +
    8.37 +  have "((\<lambda>z. \<Sum>n. c n * z^n) has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
    8.38 +    by (intro termdiffs_strong'[OF _ norm] sums_summable[OF sums])
    8.39 +  hence "(f has_field_derivative (\<Sum>n. diffs c n * z^n)) (at z)"
    8.40 +    by (subst (asm) DERIV_cong_ev[OF refl eq refl])
    8.41 +  from this and deriv have "(\<Sum>n. diffs c n * z^n) = f'" by (rule DERIV_unique)
    8.42 +  with summable show ?thesis by (simp add: sums_iff)
    8.43 +qed
    8.44 +
    8.45  lemma isCont_powser:
    8.46    fixes K x :: "'a::{real_normed_field,banach}"
    8.47    assumes "summable (\<lambda>n. c n * K ^ n)"
    8.48 @@ -1114,6 +1152,18 @@
    8.49    from for_subinterval[OF this] show ?thesis .
    8.50  qed
    8.51  
    8.52 +lemma geometric_deriv_sums:
    8.53 +  fixes z :: "'a :: {real_normed_field,banach}"
    8.54 +  assumes "norm z < 1"
    8.55 +  shows   "(\<lambda>n. of_nat (Suc n) * z ^ n) sums (1 / (1 - z)^2)"
    8.56 +proof -
    8.57 +  have "(\<lambda>n. diffs (\<lambda>n. 1) n * z^n) sums (1 / (1 - z)^2)"
    8.58 +  proof (rule termdiffs_sums_strong)
    8.59 +    fix z :: 'a assume "norm z < 1"
    8.60 +    thus "(\<lambda>n. 1 * z^n) sums (1 / (1 - z))" by (simp add: geometric_sums)
    8.61 +  qed (insert assms, auto intro!: derivative_eq_intros simp: power2_eq_square)
    8.62 +  thus ?thesis unfolding diffs_def by simp
    8.63 +qed
    8.64  
    8.65  lemma isCont_pochhammer [continuous_intros]: "isCont (\<lambda>z. pochhammer z n) z"
    8.66    for z :: "'a::real_normed_field"