author paulson Wed, 23 Dec 2020 16:25:52 +0000 changeset 72980 4fc3dc37f406 parent 72979 e734cd65c926 child 72995 eac16c76273e child 73001 21c919addd8c
default simprule for geometric series
 src/HOL/Series.thy file | annotate | diff | comparison | revisions src/HOL/Transcendental.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Series.thy	Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Series.thy	Wed Dec 23 16:25:52 2020 +0000
@@ -614,7 +614,7 @@
lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)"
by (rule sums_unique[symmetric]) (rule geometric_sums)

-lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
+lemma summable_geometric_iff [simp]: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1"
proof
assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)"
then have "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0"```
```--- a/src/HOL/Transcendental.thy	Tue Dec 22 23:36:32 2020 +0100
+++ b/src/HOL/Transcendental.thy	Wed Dec 23 16:25:52 2020 +0000
@@ -1886,10 +1886,8 @@
next
fix x :: real
assume "x \<in> {- 1<..<1}"
-      then have "norm (-x) < 1" by auto
-      show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
-        unfolding One_nat_def
-        by (auto simp: power_mult_distrib[symmetric] summable_geometric[OF \<open>norm (-x) < 1\<close>])
+      then show "summable (\<lambda>n. (- 1) ^ n * (1 / real (n + 1)) * real (Suc n) * x^n)"
+        by (simp add: abs_if flip: power_mult_distrib)
qed
then have "DERIV (\<lambda>x. suminf (?f x)) (x - 1) :> suminf (?f' x)"
unfolding One_nat_def by auto```