src/HOL/Analysis/Complex_Transcendental.thy
 changeset 66447 a1f5c5c26fa6 parent 66252 b73f94b366b7 child 66453 cc19f7ca2ed6
```     1.1 --- a/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:40:42 2017 +0200
1.2 +++ b/src/HOL/Analysis/Complex_Transcendental.thy	Thu Aug 17 14:52:56 2017 +0200
1.3 @@ -2420,7 +2420,7 @@
1.4                 intro!: mult_pos_pos divide_pos_pos always_eventually)
1.5      thus "summable (\<lambda>n. g n * u^n)"
1.6        by (subst summable_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
1.7 -         (auto simp: power_mult subseq_def g_def h_def elim!: oddE)
1.8 +         (auto simp: power_mult strict_mono_def g_def h_def elim!: oddE)
1.10
1.11    have "\<exists>c. \<forall>u\<in>ball 0 1. Arctan u - G u = c"
1.12 @@ -2436,7 +2436,7 @@
1.13        by (intro ext) (simp_all del: of_nat_Suc add: g_def diffs_def power_mult_distrib)
1.14      also have "suminf \<dots> = (\<Sum>n. (-(u^2))^n)"
1.15        by (subst suminf_mono_reindex[of "\<lambda>n. 2*n", symmetric])
1.16 -         (auto elim!: evenE simp: subseq_def power_mult power_mult_distrib)
1.17 +         (auto elim!: evenE simp: strict_mono_def power_mult power_mult_distrib)
1.18      also from u have "norm u^2 < 1^2" by (intro power_strict_mono) simp_all
1.19      hence "(\<Sum>n. (-(u^2))^n) = inverse (1 + u^2)"
1.20        by (subst suminf_geometric) (simp_all add: norm_power inverse_eq_divide)
1.21 @@ -2450,7 +2450,7 @@
1.22    with c z have "Arctan z = G z" by simp
1.23    with summable[OF z] show "(\<lambda>n. g n * z^n) sums Arctan z" unfolding G_def by (simp add: sums_iff)
1.24    thus "h z sums Arctan z" by (subst (asm) sums_mono_reindex[of "\<lambda>n. 2*n+1", symmetric])
1.25 -                              (auto elim!: oddE simp: subseq_def power_mult g_def h_def)
1.26 +                              (auto elim!: oddE simp: strict_mono_def power_mult g_def h_def)
1.27  qed
1.28
1.29  text \<open>A quickly-converging series for the logarithm, based on the arctangent.\<close>
```