author Manuel Eberl Thu Aug 25 15:50:43 2016 +0200 (2016-08-25) changeset 63721 492bb53c3420 parent 63720 bcf2123d059a child 63722 b9c8da46443b
More analysis lemmas
 src/HOL/Analysis/Complex_Transcendental.thy file | annotate | diff | revisions src/HOL/Analysis/Gamma_Function.thy file | annotate | diff | revisions src/HOL/Analysis/Harmonic_Numbers.thy file | annotate | diff | revisions src/HOL/Analysis/Henstock_Kurzweil_Integration.thy file | annotate | diff | revisions src/HOL/Limits.thy file | annotate | diff | revisions src/HOL/NthRoot.thy file | annotate | diff | revisions src/HOL/Set_Interval.thy file | annotate | diff | revisions src/HOL/Transcendental.thy file | annotate | diff | revisions
```     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.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.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.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"
```