author | wenzelm |
Tue, 26 Jul 2016 10:33:39 +0200 | |
changeset 63550 | 3a0f40a6fa42 |
parent 63365 | 5340fb6633d0 |
child 63680 | 6e1e8b5abbfa |
permissions | -rw-r--r-- |
10751 | 1 |
(* Title : Series.thy |
2 |
Author : Jacques D. Fleuriot |
|
3 |
Copyright : 1998 University of Cambridge |
|
14416 | 4 |
|
5 |
Converted to Isar and polished by lcp |
|
15539 | 6 |
Converted to setsum and polished yet more by TNN |
16819 | 7 |
Additional contributions by Jeremy Avigad |
41970 | 8 |
*) |
10751 | 9 |
|
60758 | 10 |
section \<open>Infinite Series\<close> |
10751 | 11 |
|
15131 | 12 |
theory Series |
59712
6c013328b885
add inequalities (move from AFP/Amortized_Complexity)
hoelzl
parents:
59613
diff
changeset
|
13 |
imports Limits Inequalities |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
14 |
begin |
15561 | 15 |
|
60758 | 16 |
subsection \<open>Definition of infinite summability\<close> |
56213 | 17 |
|
63550 | 18 |
definition sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool" |
19 |
(infixr "sums" 80) |
|
20 |
where "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s" |
|
14416 | 21 |
|
63550 | 22 |
definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool" |
23 |
where "summable f \<longleftrightarrow> (\<exists>s. f sums s)" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
24 |
|
63550 | 25 |
definition suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" |
26 |
(binder "\<Sum>" 10) |
|
27 |
where "suminf f = (THE s. f sums s)" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
28 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
29 |
lemma sums_def': "f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i = 0..n. f i) \<longlonglongrightarrow> s" |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
30 |
apply (simp add: sums_def) |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
31 |
apply (subst LIMSEQ_Suc_iff [symmetric]) |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
32 |
apply (simp only: lessThan_Suc_atMost atLeast0AtMost) |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
33 |
done |
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
34 |
|
63550 | 35 |
|
60758 | 36 |
subsection \<open>Infinite summability on topological monoids\<close> |
56213 | 37 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
38 |
lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
39 |
by simp |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
40 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
41 |
lemma sums_cong: "(\<And>n. f n = g n) \<Longrightarrow> f sums c \<longleftrightarrow> g sums c" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
42 |
by (drule ext) simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
43 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
44 |
lemma sums_summable: "f sums l \<Longrightarrow> summable f" |
41970 | 45 |
by (simp add: sums_def summable_def, blast) |
14416 | 46 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
47 |
lemma summable_iff_convergent: "summable f \<longleftrightarrow> convergent (\<lambda>n. \<Sum>i<n. f i)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
48 |
by (simp add: summable_def sums_def convergent_def) |
14416 | 49 |
|
63550 | 50 |
lemma summable_iff_convergent': "summable f \<longleftrightarrow> convergent (\<lambda>n. setsum f {..n})" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
51 |
by (simp_all only: summable_iff_convergent convergent_def |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
52 |
lessThan_Suc_atMost [symmetric] LIMSEQ_Suc_iff[of "\<lambda>n. setsum f {..<n}"]) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
53 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
54 |
lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)" |
41970 | 55 |
by (simp add: suminf_def sums_def lim_def) |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
31336
diff
changeset
|
56 |
|
56213 | 57 |
lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0" |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57418
diff
changeset
|
58 |
unfolding sums_def by simp |
56213 | 59 |
|
60 |
lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" |
|
61 |
by (rule sums_zero [THEN sums_summable]) |
|
62 |
||
63 |
lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s" |
|
64 |
apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially) |
|
65 |
apply safe |
|
66 |
apply (erule_tac x=S in allE) |
|
67 |
apply safe |
|
68 |
apply (rule_tac x="N" in exI, safe) |
|
69 |
apply (drule_tac x="n*k" in spec) |
|
70 |
apply (erule mp) |
|
71 |
apply (erule order_trans) |
|
72 |
apply simp |
|
73 |
done |
|
74 |
||
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
75 |
lemma suminf_cong: "(\<And>n. f n = g n) \<Longrightarrow> suminf f = suminf g" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
76 |
by (rule arg_cong[of f g], rule ext) simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
77 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
78 |
lemma summable_cong: |
63550 | 79 |
fixes f g :: "nat \<Rightarrow> 'a::real_normed_vector" |
80 |
assumes "eventually (\<lambda>x. f x = g x) sequentially" |
|
81 |
shows "summable f = summable g" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
82 |
proof - |
63550 | 83 |
from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" |
84 |
by (auto simp: eventually_at_top_linorder) |
|
63040 | 85 |
define C where "C = (\<Sum>k<N. f k - g k)" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
86 |
from eventually_ge_at_top[of N] |
63550 | 87 |
have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
88 |
proof eventually_elim |
63550 | 89 |
case (elim n) |
90 |
then have "{..<n} = {..<N} \<union> {N..<n}" |
|
91 |
by auto |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
92 |
also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
93 |
by (intro setsum.union_disjoint) auto |
63550 | 94 |
also from N have "setsum f {N..<n} = setsum g {N..<n}" |
95 |
by (intro setsum.cong) simp_all |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
96 |
also have "setsum f {..<N} + setsum g {N..<n} = C + (setsum g {..<N} + setsum g {N..<n})" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
97 |
unfolding C_def by (simp add: algebra_simps setsum_subtractf) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
98 |
also have "setsum g {..<N} + setsum g {N..<n} = setsum g ({..<N} \<union> {N..<n})" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
99 |
by (intro setsum.union_disjoint [symmetric]) auto |
63550 | 100 |
also from elim have "{..<N} \<union> {N..<n} = {..<n}" |
101 |
by auto |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
102 |
finally show "setsum f {..<n} = C + setsum g {..<n}" . |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
103 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
104 |
from convergent_cong[OF this] show ?thesis |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
105 |
by (simp add: summable_iff_convergent convergent_add_const_iff) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
106 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
107 |
|
47761 | 108 |
lemma sums_finite: |
63550 | 109 |
assumes [simp]: "finite N" |
110 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" |
|
47761 | 111 |
shows "f sums (\<Sum>n\<in>N. f n)" |
112 |
proof - |
|
63550 | 113 |
have eq: "setsum f {..<n + Suc (Max N)} = setsum f N" for n |
114 |
proof (cases "N = {}") |
|
115 |
case True |
|
116 |
with f have "f = (\<lambda>x. 0)" by auto |
|
117 |
then show ?thesis by simp |
|
118 |
next |
|
119 |
case [simp]: False |
|
120 |
show ?thesis |
|
121 |
proof (safe intro!: setsum.mono_neutral_right f) |
|
122 |
fix i |
|
123 |
assume "i \<in> N" |
|
124 |
then have "i \<le> Max N" by simp |
|
125 |
then show "i < n + Suc (Max N)" by simp |
|
126 |
qed |
|
127 |
qed |
|
128 |
show ?thesis |
|
129 |
unfolding sums_def |
|
47761 | 130 |
by (rule LIMSEQ_offset[of _ "Suc (Max N)"]) |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57418
diff
changeset
|
131 |
(simp add: eq atLeast0LessThan del: add_Suc_right) |
47761 | 132 |
qed |
133 |
||
63550 | 134 |
corollary sums_0: "(\<And>n. f n = 0) \<Longrightarrow> (f sums 0)" |
62217 | 135 |
by (metis (no_types) finite.emptyI setsum.empty sums_finite) |
136 |
||
56213 | 137 |
lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f" |
138 |
by (rule sums_summable) (rule sums_finite) |
|
139 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
140 |
lemma sums_If_finite_set: "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0) sums (\<Sum>r\<in>A. f r)" |
47761 | 141 |
using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp |
142 |
||
56213 | 143 |
lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)" |
144 |
by (rule sums_summable) (rule sums_If_finite_set) |
|
145 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
146 |
lemma sums_If_finite: "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0) sums (\<Sum>r | P r. f r)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
147 |
using sums_If_finite_set[of "{r. P r}"] by simp |
16819 | 148 |
|
56213 | 149 |
lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)" |
150 |
by (rule sums_summable) (rule sums_If_finite) |
|
151 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
152 |
lemma sums_single: "(\<lambda>r. if r = i then f r else 0) sums f i" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
153 |
using sums_If_finite[of "\<lambda>r. r = i"] by simp |
29803
c56a5571f60a
Added derivation lemmas for power series and theorems for the pi, arcus tangens and logarithm series
hoelzl
parents:
29197
diff
changeset
|
154 |
|
56213 | 155 |
lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)" |
156 |
by (rule sums_summable) (rule sums_single) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
157 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
158 |
context |
63550 | 159 |
fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
160 |
begin |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
161 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
162 |
lemma summable_sums[intro]: "summable f \<Longrightarrow> f sums (suminf f)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
163 |
by (simp add: summable_def sums_def suminf_def) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
164 |
(metis convergent_LIMSEQ_iff convergent_def lim_def) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
165 |
|
61969 | 166 |
lemma summable_LIMSEQ: "summable f \<Longrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> suminf f" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
167 |
by (rule summable_sums [unfolded sums_def]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
168 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
169 |
lemma sums_unique: "f sums s \<Longrightarrow> s = suminf f" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
170 |
by (metis limI suminf_eq_lim sums_def) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
171 |
|
63550 | 172 |
lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> suminf f = x" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
173 |
by (metis summable_sums sums_summable sums_unique) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
174 |
|
63550 | 175 |
lemma summable_sums_iff: "summable f \<longleftrightarrow> f sums suminf f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
176 |
by (auto simp: sums_iff summable_sums) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
177 |
|
63550 | 178 |
lemma sums_unique2: "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b" |
179 |
for a b :: 'a |
|
180 |
by (simp add: sums_iff) |
|
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset
|
181 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
182 |
lemma suminf_finite: |
63550 | 183 |
assumes N: "finite N" |
184 |
and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
185 |
shows "suminf f = (\<Sum>n\<in>N. f n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
186 |
using sums_finite[OF assms, THEN sums_unique] by simp |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
187 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
188 |
end |
16819 | 189 |
|
41970 | 190 |
lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
191 |
by (rule sums_zero [THEN sums_unique, symmetric]) |
16819 | 192 |
|
56213 | 193 |
|
60758 | 194 |
subsection \<open>Infinite summability on ordered, topological monoids\<close> |
56213 | 195 |
|
63550 | 196 |
lemma sums_le: "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t" |
197 |
for f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}" |
|
56213 | 198 |
by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def) |
199 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
200 |
context |
63550 | 201 |
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology}" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
202 |
begin |
14416 | 203 |
|
63550 | 204 |
lemma suminf_le: "\<forall>n. f n \<le> g n \<Longrightarrow> summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f \<le> suminf g" |
56213 | 205 |
by (auto dest: sums_summable intro: sums_le) |
206 |
||
207 |
lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f" |
|
208 |
by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto |
|
209 |
||
210 |
lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f" |
|
211 |
using setsum_le_suminf[of 0] by simp |
|
212 |
||
213 |
lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x" |
|
214 |
by (metis LIMSEQ_le_const2 summable_LIMSEQ) |
|
14416 | 215 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
216 |
lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)" |
50999 | 217 |
proof |
218 |
assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n" |
|
61969 | 219 |
then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0" |
56213 | 220 |
using summable_LIMSEQ[of f] by simp |
221 |
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0" |
|
222 |
proof (rule LIMSEQ_le_const) |
|
63550 | 223 |
show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}" for i |
50999 | 224 |
using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto |
225 |
qed |
|
226 |
with pos show "\<forall>n. f n = 0" |
|
227 |
by (auto intro!: antisym) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
228 |
qed (metis suminf_zero fun_eq_iff) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
229 |
|
63550 | 230 |
lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)" |
62377
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
231 |
using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le) |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
232 |
|
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
233 |
lemma suminf_pos2: |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
234 |
assumes "summable f" "\<forall>n. 0 \<le> f n" "0 < f i" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
235 |
shows "0 < suminf f" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
236 |
proof - |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
237 |
have "0 < (\<Sum>n<Suc i. f n)" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
238 |
using assms by (intro setsum_pos2[where i=i]) auto |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
239 |
also have "\<dots> \<le> suminf f" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
240 |
using assms by (intro setsum_le_suminf) auto |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
241 |
finally show ?thesis . |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
242 |
qed |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
243 |
|
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
244 |
lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
245 |
by (intro suminf_pos2[where i=0]) (auto intro: less_imp_le) |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
246 |
|
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
247 |
end |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
248 |
|
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
249 |
context |
63550 | 250 |
fixes f :: "nat \<Rightarrow> 'a::{ordered_cancel_comm_monoid_add,linorder_topology}" |
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
251 |
begin |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
252 |
|
63550 | 253 |
lemma setsum_less_suminf2: |
254 |
"summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> n \<le> i \<Longrightarrow> 0 < f i \<Longrightarrow> setsum f {..<n} < suminf f" |
|
255 |
using setsum_le_suminf[of f "Suc i"] |
|
256 |
and add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"] |
|
257 |
and setsum_mono2[of "{..<i}" "{..<n}" f] |
|
62376
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
258 |
by (auto simp: less_imp_le ac_simps) |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
259 |
|
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
260 |
lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f" |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
261 |
using setsum_less_suminf2[of n n] by (simp add: less_imp_le) |
85f38d5f8807
Rename ordered_comm_monoid_add to ordered_cancel_comm_monoid_add. Introduce ordreed_comm_monoid_add, canonically_ordered_comm_monoid and dioid. Setup nat, entat and ennreal as dioids.
hoelzl
parents:
62368
diff
changeset
|
262 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
263 |
end |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
264 |
|
56213 | 265 |
lemma summableI_nonneg_bounded: |
63550 | 266 |
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add,linorder_topology,conditionally_complete_linorder}" |
267 |
assumes pos[simp]: "\<And>n. 0 \<le> f n" |
|
268 |
and le: "\<And>n. (\<Sum>i<n. f i) \<le> x" |
|
56213 | 269 |
shows "summable f" |
63550 | 270 |
unfolding summable_def sums_def [abs_def] |
62377
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
271 |
proof (rule exI LIMSEQ_incseq_SUP)+ |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
272 |
show "bdd_above (range (\<lambda>n. setsum f {..<n}))" |
56213 | 273 |
using le by (auto simp: bdd_above_def) |
62377
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
274 |
show "incseq (\<lambda>n. setsum f {..<n})" |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
275 |
by (auto simp: mono_def intro!: setsum_mono2) |
56213 | 276 |
qed |
277 |
||
63550 | 278 |
lemma summableI[intro, simp]: "summable f" |
279 |
for f :: "nat \<Rightarrow> 'a::{canonically_ordered_monoid_add,linorder_topology,complete_linorder}" |
|
62377
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
280 |
by (intro summableI_nonneg_bounded[where x=top] zero_le top_greatest) |
ace69956d018
moved more proofs to ordered_comm_monoid_add; introduced strict_ordered_ab_semigroup/comm_monoid_add
hoelzl
parents:
62376
diff
changeset
|
281 |
|
63550 | 282 |
|
62368 | 283 |
subsection \<open>Infinite summability on topological monoids\<close> |
284 |
||
285 |
context |
|
63550 | 286 |
fixes f g :: "nat \<Rightarrow> 'a::{t2_space,topological_comm_monoid_add}" |
62368 | 287 |
begin |
288 |
||
289 |
lemma sums_Suc: |
|
63550 | 290 |
assumes "(\<lambda>n. f (Suc n)) sums l" |
291 |
shows "f sums (l + f 0)" |
|
62368 | 292 |
proof - |
293 |
have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0" |
|
294 |
using assms by (auto intro!: tendsto_add simp: sums_def) |
|
295 |
moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n |
|
63365 | 296 |
unfolding lessThan_Suc_eq_insert_0 |
63550 | 297 |
by (simp add: ac_simps setsum_atLeast1_atMost_eq image_Suc_lessThan) |
62368 | 298 |
ultimately show ?thesis |
63550 | 299 |
by (auto simp: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1]) |
62368 | 300 |
qed |
301 |
||
302 |
lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)" |
|
303 |
unfolding sums_def by (simp add: setsum.distrib tendsto_add) |
|
304 |
||
305 |
lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)" |
|
306 |
unfolding summable_def by (auto intro: sums_add) |
|
307 |
||
308 |
lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)" |
|
309 |
by (intro sums_unique sums_add summable_sums) |
|
310 |
||
311 |
end |
|
312 |
||
313 |
context |
|
63550 | 314 |
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space,topological_comm_monoid_add}" |
315 |
and I :: "'i set" |
|
62368 | 316 |
begin |
317 |
||
318 |
lemma sums_setsum: "(\<And>i. i \<in> I \<Longrightarrow> (f i) sums (x i)) \<Longrightarrow> (\<lambda>n. \<Sum>i\<in>I. f i n) sums (\<Sum>i\<in>I. x i)" |
|
319 |
by (induct I rule: infinite_finite_induct) (auto intro!: sums_add) |
|
320 |
||
321 |
lemma suminf_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> (\<Sum>n. \<Sum>i\<in>I. f i n) = (\<Sum>i\<in>I. \<Sum>n. f i n)" |
|
322 |
using sums_unique[OF sums_setsum, OF summable_sums] by simp |
|
323 |
||
324 |
lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)" |
|
325 |
using sums_summable[OF sums_setsum[OF summable_sums]] . |
|
326 |
||
327 |
end |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
328 |
|
60758 | 329 |
subsection \<open>Infinite summability on real normed vector spaces\<close> |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
330 |
|
62368 | 331 |
context |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
332 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
62368 | 333 |
begin |
334 |
||
335 |
lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
336 |
proof - |
61969 | 337 |
have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
338 |
by (subst LIMSEQ_Suc_iff) (simp add: sums_def) |
61969 | 339 |
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0" |
63365 | 340 |
by (simp add: ac_simps lessThan_Suc_eq_insert_0 image_Suc_lessThan setsum_atLeast1_atMost_eq) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
341 |
also have "\<dots> \<longleftrightarrow> (\<lambda>n. f (Suc n)) sums s" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
342 |
proof |
61969 | 343 |
assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0" |
63550 | 344 |
with tendsto_add[OF this tendsto_const, of "- f 0"] show "(\<lambda>i. f (Suc i)) sums s" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
345 |
by (simp add: sums_def) |
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57418
diff
changeset
|
346 |
qed (auto intro: tendsto_add simp: sums_def) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
347 |
finally show ?thesis .. |
50999 | 348 |
qed |
349 |
||
62368 | 350 |
lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
351 |
proof |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
352 |
assume "summable f" |
63550 | 353 |
then have "f sums suminf f" |
354 |
by (rule summable_sums) |
|
355 |
then have "(\<lambda>n. f (Suc n)) sums (suminf f - f 0)" |
|
356 |
by (simp add: sums_Suc_iff) |
|
357 |
then show "summable (\<lambda>n. f (Suc n))" |
|
358 |
unfolding summable_def by blast |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
359 |
qed (auto simp: sums_Suc_iff summable_def) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
360 |
|
62381
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
361 |
lemma sums_Suc_imp: "f 0 = 0 \<Longrightarrow> (\<lambda>n. f (Suc n)) sums s \<Longrightarrow> (\<lambda>n. f n) sums s" |
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
362 |
using sums_Suc_iff by simp |
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
363 |
|
62368 | 364 |
end |
365 |
||
63550 | 366 |
context (* Separate contexts are necessary to allow general use of the results above, here. *) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
367 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
368 |
begin |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
369 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
370 |
lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
371 |
unfolding sums_def by (simp add: setsum_subtractf tendsto_diff) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
372 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
373 |
lemma summable_diff: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n - g n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
374 |
unfolding summable_def by (auto intro: sums_diff) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
375 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
376 |
lemma suminf_diff: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f - suminf g = (\<Sum>n. f n - g n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
377 |
by (intro sums_unique sums_diff summable_sums) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
378 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
379 |
lemma sums_minus: "f sums a \<Longrightarrow> (\<lambda>n. - f n) sums (- a)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
380 |
unfolding sums_def by (simp add: setsum_negf tendsto_minus) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
381 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
382 |
lemma summable_minus: "summable f \<Longrightarrow> summable (\<lambda>n. - f n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
383 |
unfolding summable_def by (auto intro: sums_minus) |
20692 | 384 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
385 |
lemma suminf_minus: "summable f \<Longrightarrow> (\<Sum>n. - f n) = - (\<Sum>n. f n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
386 |
by (intro sums_unique [symmetric] sums_minus summable_sums) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
387 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
388 |
lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
389 |
proof (induct n arbitrary: s) |
63550 | 390 |
case 0 |
391 |
then show ?case by simp |
|
392 |
next |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
393 |
case (Suc n) |
63550 | 394 |
then have "(\<lambda>i. f (Suc i + n)) sums s \<longleftrightarrow> (\<lambda>i. f (i + n)) sums (s + f n)" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
395 |
by (subst sums_Suc_iff) simp |
63550 | 396 |
with Suc show ?case |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
397 |
by (simp add: ac_simps) |
63550 | 398 |
qed |
20692 | 399 |
|
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
400 |
corollary sums_iff_shift': "(\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i)) \<longleftrightarrow> f sums s" |
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
401 |
by (simp add: sums_iff_shift) |
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
402 |
|
62381
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
403 |
lemma sums_zero_iff_shift: |
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
404 |
assumes "\<And>i. i < n \<Longrightarrow> f i = 0" |
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
405 |
shows "(\<lambda>i. f (i+n)) sums s \<longleftrightarrow> (\<lambda>i. f i) sums s" |
63550 | 406 |
by (simp add: assms sums_iff_shift) |
62381
a6479cb85944
New and revised material for (multivariate) analysis
paulson <lp15@cam.ac.uk>
parents:
62379
diff
changeset
|
407 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
408 |
lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f" |
63550 | 409 |
by (metis diff_add_cancel summable_def sums_iff_shift [abs_def]) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
410 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
411 |
lemma sums_split_initial_segment: "f sums s \<Longrightarrow> (\<lambda>i. f (i + n)) sums (s - (\<Sum>i<n. f i))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
412 |
by (simp add: sums_iff_shift) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
413 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
414 |
lemma summable_ignore_initial_segment: "summable f \<Longrightarrow> summable (\<lambda>n. f(n + k))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
415 |
by (simp add: summable_iff_shift) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
416 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
417 |
lemma suminf_minus_initial_segment: "summable f \<Longrightarrow> (\<Sum>n. f (n + k)) = (\<Sum>n. f n) - (\<Sum>i<k. f i)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
418 |
by (rule sums_unique[symmetric]) (auto simp: sums_iff_shift) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
419 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
420 |
lemma suminf_split_initial_segment: "summable f \<Longrightarrow> suminf f = (\<Sum>n. f(n + k)) + (\<Sum>i<k. f i)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
421 |
by (auto simp add: suminf_minus_initial_segment) |
20692 | 422 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
423 |
lemma suminf_split_head: "summable f \<Longrightarrow> (\<Sum>n. f (Suc n)) = suminf f - f 0" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
424 |
using suminf_split_initial_segment[of 1] by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
425 |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
426 |
lemma suminf_exist_split: |
63550 | 427 |
fixes r :: real |
428 |
assumes "0 < r" and "summable f" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
429 |
shows "\<exists>N. \<forall>n\<ge>N. norm (\<Sum>i. f (i + n)) < r" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
430 |
proof - |
60758 | 431 |
from LIMSEQ_D[OF summable_LIMSEQ[OF \<open>summable f\<close>] \<open>0 < r\<close>] |
63550 | 432 |
obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n} - suminf f) < r" |
433 |
by auto |
|
434 |
then show ?thesis |
|
60758 | 435 |
by (auto simp: norm_minus_commute suminf_minus_initial_segment[OF \<open>summable f\<close>]) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
436 |
qed |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
437 |
|
61969 | 438 |
lemma summable_LIMSEQ_zero: "summable f \<Longrightarrow> f \<longlonglongrightarrow> 0" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
439 |
apply (drule summable_iff_convergent [THEN iffD1]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
440 |
apply (drule convergent_Cauchy) |
63550 | 441 |
apply (simp only: Cauchy_iff LIMSEQ_iff) |
442 |
apply safe |
|
443 |
apply (drule_tac x="r" in spec) |
|
444 |
apply safe |
|
445 |
apply (rule_tac x="M" in exI) |
|
446 |
apply safe |
|
447 |
apply (drule_tac x="Suc n" in spec) |
|
448 |
apply simp |
|
449 |
apply (drule_tac x="n" in spec) |
|
450 |
apply simp |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
451 |
done |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
452 |
|
62368 | 453 |
lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
454 |
by (force dest!: summable_LIMSEQ_zero simp: convergent_def) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
455 |
|
62368 | 456 |
lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
457 |
by (simp add: convergent_imp_Bseq summable_imp_convergent) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
458 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
459 |
end |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
460 |
|
63550 | 461 |
lemma summable_minus_iff: "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f" |
462 |
for f :: "nat \<Rightarrow> 'a::real_normed_vector" |
|
463 |
by (auto dest: summable_minus) (* used two ways, hence must be outside the context above *) |
|
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset
|
464 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
465 |
lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" |
63550 | 466 |
unfolding sums_def by (drule tendsto) (simp only: setsum) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
467 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
468 |
lemma (in bounded_linear) summable: "summable (\<lambda>n. X n) \<Longrightarrow> summable (\<lambda>n. f (X n))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
469 |
unfolding summable_def by (auto intro: sums) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
470 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
471 |
lemma (in bounded_linear) suminf: "summable (\<lambda>n. X n) \<Longrightarrow> f (\<Sum>n. X n) = (\<Sum>n. f (X n))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
472 |
by (intro sums_unique sums summable_sums) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
473 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
474 |
lemmas sums_of_real = bounded_linear.sums [OF bounded_linear_of_real] |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
475 |
lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real] |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
476 |
lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real] |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
477 |
|
57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
478 |
lemmas sums_scaleR_left = bounded_linear.sums[OF bounded_linear_scaleR_left] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
479 |
lemmas summable_scaleR_left = bounded_linear.summable[OF bounded_linear_scaleR_left] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
480 |
lemmas suminf_scaleR_left = bounded_linear.suminf[OF bounded_linear_scaleR_left] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
481 |
|
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
482 |
lemmas sums_scaleR_right = bounded_linear.sums[OF bounded_linear_scaleR_right] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
483 |
lemmas summable_scaleR_right = bounded_linear.summable[OF bounded_linear_scaleR_right] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
484 |
lemmas suminf_scaleR_right = bounded_linear.suminf[OF bounded_linear_scaleR_right] |
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset
|
485 |
|
63550 | 486 |
lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> c = 0" |
487 |
for c :: "'a::real_normed_vector" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
488 |
proof - |
63550 | 489 |
have "\<not> summable (\<lambda>_. c)" if "c \<noteq> 0" |
490 |
proof - |
|
491 |
from that have "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
492 |
by (subst mult.commute) |
63550 | 493 |
(auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially) |
494 |
then have "\<not> convergent (\<lambda>n. norm (\<Sum>k<n. c))" |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
495 |
by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity) |
63550 | 496 |
(simp_all add: setsum_constant_scaleR) |
497 |
then show ?thesis |
|
498 |
unfolding summable_iff_convergent using convergent_norm by blast |
|
499 |
qed |
|
500 |
then show ?thesis by auto |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
501 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
502 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
503 |
|
60758 | 504 |
subsection \<open>Infinite summability on real normed algebras\<close> |
56213 | 505 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
506 |
context |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
507 |
fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
508 |
begin |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
509 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
510 |
lemma sums_mult: "f sums a \<Longrightarrow> (\<lambda>n. c * f n) sums (c * a)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
511 |
by (rule bounded_linear.sums [OF bounded_linear_mult_right]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
512 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
513 |
lemma summable_mult: "summable f \<Longrightarrow> summable (\<lambda>n. c * f n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
514 |
by (rule bounded_linear.summable [OF bounded_linear_mult_right]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
515 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
516 |
lemma suminf_mult: "summable f \<Longrightarrow> suminf (\<lambda>n. c * f n) = c * suminf f" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
517 |
by (rule bounded_linear.suminf [OF bounded_linear_mult_right, symmetric]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
518 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
519 |
lemma sums_mult2: "f sums a \<Longrightarrow> (\<lambda>n. f n * c) sums (a * c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
520 |
by (rule bounded_linear.sums [OF bounded_linear_mult_left]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
521 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
522 |
lemma summable_mult2: "summable f \<Longrightarrow> summable (\<lambda>n. f n * c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
523 |
by (rule bounded_linear.summable [OF bounded_linear_mult_left]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
524 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
525 |
lemma suminf_mult2: "summable f \<Longrightarrow> suminf f * c = (\<Sum>n. f n * c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
526 |
by (rule bounded_linear.suminf [OF bounded_linear_mult_left]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
527 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
528 |
end |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
529 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
530 |
lemma sums_mult_iff: |
63550 | 531 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra,field}" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
532 |
assumes "c \<noteq> 0" |
63550 | 533 |
shows "(\<lambda>n. c * f n) sums (c * d) \<longleftrightarrow> f sums d" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
534 |
using sums_mult[of f d c] sums_mult[of "\<lambda>n. c * f n" "c * d" "inverse c"] |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
535 |
by (force simp: field_simps assms) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
536 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
537 |
lemma sums_mult2_iff: |
63550 | 538 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_algebra,field}" |
539 |
assumes "c \<noteq> 0" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
540 |
shows "(\<lambda>n. f n * c) sums (d * c) \<longleftrightarrow> f sums d" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
541 |
using sums_mult_iff[OF assms, of f d] by (simp add: mult.commute) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
542 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
543 |
lemma sums_of_real_iff: |
63550 | 544 |
"(\<lambda>n. of_real (f n) :: 'a::real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
545 |
by (simp add: sums_def of_real_setsum[symmetric] tendsto_of_real_iff del: of_real_setsum) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
546 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
547 |
|
60758 | 548 |
subsection \<open>Infinite summability on real normed fields\<close> |
56213 | 549 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
550 |
context |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
551 |
fixes c :: "'a::real_normed_field" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
552 |
begin |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
553 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
554 |
lemma sums_divide: "f sums a \<Longrightarrow> (\<lambda>n. f n / c) sums (a / c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
555 |
by (rule bounded_linear.sums [OF bounded_linear_divide]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
556 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
557 |
lemma summable_divide: "summable f \<Longrightarrow> summable (\<lambda>n. f n / c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
558 |
by (rule bounded_linear.summable [OF bounded_linear_divide]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
559 |
|
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
560 |
lemma suminf_divide: "summable f \<Longrightarrow> suminf (\<lambda>n. f n / c) = suminf f / c" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
561 |
by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric]) |
14416 | 562 |
|
63550 | 563 |
lemma sums_mult_D: "(\<lambda>n. c * f n) sums a \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> f sums (a/c)" |
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
564 |
using sums_mult_iff by fastforce |
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
565 |
|
63550 | 566 |
lemma summable_mult_D: "summable (\<lambda>n. c * f n) \<Longrightarrow> c \<noteq> 0 \<Longrightarrow> summable f" |
62379
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
567 |
by (auto dest: summable_divide) |
340738057c8c
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
paulson <lp15@cam.ac.uk>
parents:
62377
diff
changeset
|
568 |
|
63550 | 569 |
|
570 |
text \<open>Sum of a geometric progression.\<close> |
|
14416 | 571 |
|
63550 | 572 |
lemma geometric_sums: |
573 |
assumes less_1: "norm c < 1" |
|
574 |
shows "(\<lambda>n. c^n) sums (1 / (1 - c))" |
|
20692 | 575 |
proof - |
63550 | 576 |
from less_1 have neq_1: "c \<noteq> 1" by auto |
577 |
then have neq_0: "c - 1 \<noteq> 0" by simp |
|
61969 | 578 |
from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0" |
20692 | 579 |
by (rule LIMSEQ_power_zero) |
63550 | 580 |
then have "(\<lambda>n. c ^ n / (c - 1) - 1 / (c - 1)) \<longlonglongrightarrow> 0 / (c - 1) - 1 / (c - 1)" |
44568
e6f291cb5810
discontinue many legacy theorems about LIM and LIMSEQ, in favor of tendsto theorems
huffman
parents:
44289
diff
changeset
|
581 |
using neq_0 by (intro tendsto_intros) |
63550 | 582 |
then have "(\<lambda>n. (c ^ n - 1) / (c - 1)) \<longlonglongrightarrow> 1 / (1 - c)" |
20692 | 583 |
by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) |
63550 | 584 |
then show "(\<lambda>n. c ^ n) sums (1 / (1 - c))" |
20692 | 585 |
by (simp add: sums_def geometric_sum neq_1) |
586 |
qed |
|
587 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
588 |
lemma summable_geometric: "norm c < 1 \<Longrightarrow> summable (\<lambda>n. c^n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
589 |
by (rule geometric_sums [THEN sums_summable]) |
14416 | 590 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
591 |
lemma suminf_geometric: "norm c < 1 \<Longrightarrow> suminf (\<lambda>n. c^n) = 1 / (1 - c)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
592 |
by (rule sums_unique[symmetric]) (rule geometric_sums) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
593 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
594 |
lemma summable_geometric_iff: "summable (\<lambda>n. c ^ n) \<longleftrightarrow> norm c < 1" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
595 |
proof |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
596 |
assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)" |
63550 | 597 |
then have "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
598 |
by (simp add: norm_power [symmetric] tendsto_norm_zero_iff summable_LIMSEQ_zero) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
599 |
from order_tendstoD(2)[OF this zero_less_one] obtain n where "norm c ^ n < 1" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
600 |
by (auto simp: eventually_at_top_linorder) |
63550 | 601 |
then show "norm c < 1" using one_le_power[of "norm c" n] |
602 |
by (cases "norm c \<ge> 1") (linarith, simp) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
603 |
qed (rule summable_geometric) |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
604 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
605 |
end |
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
606 |
|
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
607 |
lemma power_half_series: "(\<lambda>n. (1/2::real)^Suc n) sums 1" |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
608 |
proof - |
63550 | 609 |
have 2: "(\<lambda>n. (1/2::real)^n) sums 2" |
610 |
using geometric_sums [of "1/2::real"] by auto |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
611 |
have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)" |
59741
5b762cd73a8e
Lots of new material on complex-valued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59712
diff
changeset
|
612 |
by (simp add: mult.commute) |
63550 | 613 |
then show ?thesis |
614 |
using sums_divide [OF 2, of 2] by simp |
|
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
615 |
qed |
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset
|
616 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
617 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
618 |
subsection \<open>Telescoping\<close> |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
619 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
620 |
lemma telescope_sums: |
63550 | 621 |
fixes c :: "'a::real_normed_vector" |
622 |
assumes "f \<longlonglongrightarrow> c" |
|
623 |
shows "(\<lambda>n. f (Suc n) - f n) sums (c - f 0)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
624 |
unfolding sums_def |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
625 |
proof (subst LIMSEQ_Suc_iff [symmetric]) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
626 |
have "(\<lambda>n. \<Sum>k<Suc n. f (Suc k) - f k) = (\<lambda>n. f (Suc n) - f 0)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
627 |
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff) |
63550 | 628 |
also have "\<dots> \<longlonglongrightarrow> c - f 0" |
629 |
by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const) |
|
61969 | 630 |
finally show "(\<lambda>n. \<Sum>n<Suc n. f (Suc n) - f n) \<longlonglongrightarrow> c - f 0" . |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
631 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
632 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
633 |
lemma telescope_sums': |
63550 | 634 |
fixes c :: "'a::real_normed_vector" |
635 |
assumes "f \<longlonglongrightarrow> c" |
|
636 |
shows "(\<lambda>n. f n - f (Suc n)) sums (f 0 - c)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
637 |
using sums_minus[OF telescope_sums[OF assms]] by (simp add: algebra_simps) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
638 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
639 |
lemma telescope_summable: |
63550 | 640 |
fixes c :: "'a::real_normed_vector" |
641 |
assumes "f \<longlonglongrightarrow> c" |
|
642 |
shows "summable (\<lambda>n. f (Suc n) - f n)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
643 |
using telescope_sums[OF assms] by (simp add: sums_iff) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
644 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
645 |
lemma telescope_summable': |
63550 | 646 |
fixes c :: "'a::real_normed_vector" |
647 |
assumes "f \<longlonglongrightarrow> c" |
|
648 |
shows "summable (\<lambda>n. f n - f (Suc n))" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
649 |
using summable_minus[OF telescope_summable[OF assms]] by (simp add: algebra_simps) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
650 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
651 |
|
60758 | 652 |
subsection \<open>Infinite summability on Banach spaces\<close> |
56213 | 653 |
|
63550 | 654 |
text \<open>Cauchy-type criterion for convergence of series (c.f. Harrison).\<close> |
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
655 |
|
63550 | 656 |
lemma summable_Cauchy: "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (setsum f {m..<n}) < e)" |
657 |
for f :: "nat \<Rightarrow> 'a::banach" |
|
658 |
apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff) |
|
659 |
apply safe |
|
660 |
apply (drule spec) |
|
661 |
apply (drule (1) mp) |
|
662 |
apply (erule exE) |
|
663 |
apply (rule_tac x="M" in exI) |
|
664 |
apply clarify |
|
665 |
apply (rule_tac x="m" and y="n" in linorder_le_cases) |
|
666 |
apply (frule (1) order_trans) |
|
667 |
apply (drule_tac x="n" in spec) |
|
668 |
apply (drule (1) mp) |
|
669 |
apply (drule_tac x="m" in spec) |
|
670 |
apply (drule (1) mp) |
|
671 |
apply (simp_all add: setsum_diff [symmetric]) |
|
672 |
apply (drule spec) |
|
673 |
apply (drule (1) mp) |
|
674 |
apply (erule exE) |
|
675 |
apply (rule_tac x="N" in exI) |
|
676 |
apply clarify |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
677 |
apply (rule_tac x="m" and y="n" in linorder_le_cases) |
63550 | 678 |
apply (subst norm_minus_commute) |
679 |
apply (simp_all add: setsum_diff [symmetric]) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
680 |
done |
14416 | 681 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
682 |
context |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
683 |
fixes f :: "nat \<Rightarrow> 'a::banach" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
684 |
begin |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
685 |
|
63550 | 686 |
text \<open>Absolute convergence imples normal convergence.\<close> |
20689 | 687 |
|
56194 | 688 |
lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f" |
63550 | 689 |
apply (simp only: summable_Cauchy) |
690 |
apply safe |
|
691 |
apply (drule_tac x="e" in spec) |
|
692 |
apply safe |
|
693 |
apply (rule_tac x="N" in exI) |
|
694 |
apply safe |
|
695 |
apply (drule_tac x="m" in spec) |
|
696 |
apply safe |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
697 |
apply (rule order_le_less_trans [OF norm_setsum]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
698 |
apply (rule order_le_less_trans [OF abs_ge_self]) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
699 |
apply simp |
50999 | 700 |
done |
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
31336
diff
changeset
|
701 |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
702 |
lemma summable_norm: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> norm (suminf f) \<le> (\<Sum>n. norm (f n))" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
703 |
by (auto intro: LIMSEQ_le tendsto_norm summable_norm_cancel summable_LIMSEQ norm_setsum) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
704 |
|
63550 | 705 |
text \<open>Comparison tests.\<close> |
14416 | 706 |
|
56194 | 707 |
lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f" |
63550 | 708 |
apply (simp add: summable_Cauchy) |
709 |
apply safe |
|
710 |
apply (drule_tac x="e" in spec) |
|
711 |
apply safe |
|
712 |
apply (rule_tac x = "N + Na" in exI) |
|
713 |
apply safe |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
714 |
apply (rotate_tac 2) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
715 |
apply (drule_tac x = m in spec) |
63550 | 716 |
apply auto |
717 |
apply (rotate_tac 2) |
|
718 |
apply (drule_tac x = n in spec) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
719 |
apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans) |
63550 | 720 |
apply (rule norm_setsum) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
721 |
apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans) |
63550 | 722 |
apply (auto intro: setsum_mono simp add: abs_less_iff) |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
723 |
done |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
724 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
725 |
lemma summable_comparison_test_ev: |
63550 | 726 |
"eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
727 |
by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
728 |
|
63550 | 729 |
text \<open>A better argument order.\<close> |
730 |
lemma summable_comparison_test': "summable g \<Longrightarrow> (\<And>n. n \<ge> N \<Longrightarrow> norm (f n) \<le> g n) \<Longrightarrow> summable f" |
|
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
731 |
by (rule summable_comparison_test) auto |
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56213
diff
changeset
|
732 |
|
63550 | 733 |
|
60758 | 734 |
subsection \<open>The Ratio Test\<close> |
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset
|
735 |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
736 |
lemma summable_ratio_test: |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
737 |
assumes "c < 1" "\<And>n. n \<ge> N \<Longrightarrow> norm (f (Suc n)) \<le> c * norm (f n)" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
738 |
shows "summable f" |
63550 | 739 |
proof (cases "0 < c") |
740 |
case True |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
741 |
show "summable f" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
742 |
proof (rule summable_comparison_test) |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
743 |
show "\<exists>N'. \<forall>n\<ge>N'. norm (f n) \<le> (norm (f N) / (c ^ N)) * c ^ n" |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
744 |
proof (intro exI allI impI) |
63550 | 745 |
fix n |
746 |
assume "N \<le> n" |
|
747 |
then show "norm (f n) \<le> (norm (f N) / (c ^ N)) * c ^ n" |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
748 |
proof (induct rule: inc_induct) |
63550 | 749 |
case base |
750 |
with True show ?case by simp |
|
751 |
next |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
752 |
case (step m) |
63550 | 753 |
have "norm (f (Suc m)) / c ^ Suc m * c ^ n \<le> norm (f m) / c ^ m * c ^ n" |
60758 | 754 |
using \<open>0 < c\<close> \<open>c < 1\<close> assms(2)[OF \<open>N \<le> m\<close>] by (simp add: field_simps) |
63550 | 755 |
with step show ?case by simp |
756 |
qed |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
757 |
qed |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
758 |
show "summable (\<lambda>n. norm (f N) / c ^ N * c ^ n)" |
60758 | 759 |
using \<open>0 < c\<close> \<open>c < 1\<close> by (intro summable_mult summable_geometric) simp |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
760 |
qed |
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
761 |
next |
63550 | 762 |
case False |
763 |
have "f (Suc n) = 0" if "n \<ge> N" for n |
|
764 |
proof - |
|
765 |
from that have "norm (f (Suc n)) \<le> c * norm (f n)" |
|
766 |
by (rule assms(2)) |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
767 |
also have "\<dots> \<le> 0" |
63550 | 768 |
using False by (simp add: not_less mult_nonpos_nonneg) |
769 |
finally show ?thesis |
|
770 |
by auto |
|
771 |
qed |
|
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
772 |
then show "summable f" |
56194 | 773 |
by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_eq2) |
56178 | 774 |
qed |
775 |
||
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
776 |
end |
14416 | 777 |
|
63550 | 778 |
|
779 |
text \<open>Relations among convergence and absolute convergence for power series.\<close> |
|
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
780 |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
781 |
lemma Abel_lemma: |
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
782 |
fixes a :: "nat \<Rightarrow> 'a::real_normed_vector" |
63550 | 783 |
assumes r: "0 \<le> r" |
784 |
and r0: "r < r0" |
|
785 |
and M: "\<And>n. norm (a n) * r0^n \<le> M" |
|
786 |
shows "summable (\<lambda>n. norm (a n) * r^n)" |
|
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
787 |
proof (rule summable_comparison_test') |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
788 |
show "summable (\<lambda>n. M * (r / r0) ^ n)" |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
789 |
using assms |
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
790 |
by (auto simp add: summable_mult summable_geometric) |
63550 | 791 |
show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" for n |
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
792 |
using r r0 M [of n] |
60867 | 793 |
apply (auto simp add: abs_mult field_simps) |
63550 | 794 |
apply (cases "r = 0") |
795 |
apply simp |
|
796 |
apply (cases n) |
|
797 |
apply auto |
|
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
798 |
done |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
799 |
qed |
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
800 |
|
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset
|
801 |
|
63550 | 802 |
text \<open>Summability of geometric series for real algebras.\<close> |
23084 | 803 |
|
804 |
lemma complete_algebra_summable_geometric: |
|
31017 | 805 |
fixes x :: "'a::{real_normed_algebra_1,banach}" |
63550 | 806 |
assumes "norm x < 1" |
807 |
shows "summable (\<lambda>n. x ^ n)" |
|
23084 | 808 |
proof (rule summable_comparison_test) |
809 |
show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n" |
|
810 |
by (simp add: norm_power_ineq) |
|
63550 | 811 |
from assms show "summable (\<lambda>n. norm x ^ n)" |
23084 | 812 |
by (simp add: summable_geometric) |
813 |
qed |
|
814 |
||
63550 | 815 |
|
60758 | 816 |
subsection \<open>Cauchy Product Formula\<close> |
23111 | 817 |
|
60758 | 818 |
text \<open> |
54703 | 819 |
Proof based on Analysis WebNotes: Chapter 07, Class 41 |
820 |
@{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"} |
|
60758 | 821 |
\<close> |
23111 | 822 |
|
823 |
lemma Cauchy_product_sums: |
|
824 |
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}" |
|
825 |
assumes a: "summable (\<lambda>k. norm (a k))" |
|
63550 | 826 |
and b: "summable (\<lambda>k. norm (b k))" |
56213 | 827 |
shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))" |
23111 | 828 |
proof - |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
829 |
let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}" |
23111 | 830 |
let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}" |
831 |
have S1_mono: "\<And>m n. m \<le> n \<Longrightarrow> ?S1 m \<subseteq> ?S1 n" by auto |
|
832 |
have S2_le_S1: "\<And>n. ?S2 n \<subseteq> ?S1 n" by auto |
|
833 |
have S1_le_S2: "\<And>n. ?S1 (n div 2) \<subseteq> ?S2 n" by auto |
|
834 |
have finite_S1: "\<And>n. finite (?S1 n)" by simp |
|
835 |
with S2_le_S1 have finite_S2: "\<And>n. finite (?S2 n)" by (rule finite_subset) |
|
836 |
||
837 |
let ?g = "\<lambda>(i,j). a i * b j" |
|
838 |
let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)" |
|
63550 | 839 |
have f_nonneg: "\<And>x. 0 \<le> ?f x" by auto |
840 |
then have norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A" |
|
23111 | 841 |
unfolding real_norm_def |
842 |
by (simp only: abs_of_nonneg setsum_nonneg [rule_format]) |
|
843 |
||
61969 | 844 |
have "(\<lambda>n. (\<Sum>k<n. a k) * (\<Sum>k<n. b k)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
845 |
by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b]) |
63550 | 846 |
then have 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)" |
57418 | 847 |
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) |
23111 | 848 |
|
61969 | 849 |
have "(\<lambda>n. (\<Sum>k<n. norm (a k)) * (\<Sum>k<n. norm (b k))) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset
|
850 |
using a b by (intro tendsto_mult summable_LIMSEQ) |
63550 | 851 |
then have "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" |
57418 | 852 |
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) |
63550 | 853 |
then have "convergent (\<lambda>n. setsum ?f (?S1 n))" |
23111 | 854 |
by (rule convergentI) |
63550 | 855 |
then have Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))" |
23111 | 856 |
by (rule convergent_Cauchy) |
36657 | 857 |
have "Zfun (\<lambda>n. setsum ?f (?S1 n - ?S2 n)) sequentially" |
858 |
proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f) |
|
23111 | 859 |
fix r :: real |
860 |
assume r: "0 < r" |
|
861 |
from CauchyD [OF Cauchy r] obtain N |
|
63550 | 862 |
where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m) - setsum ?f (?S1 n)) < r" .. |
863 |
then have "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> norm (setsum ?f (?S1 m - ?S1 n)) < r" |
|
23111 | 864 |
by (simp only: setsum_diff finite_S1 S1_mono) |
63550 | 865 |
then have N: "\<And>m n. N \<le> n \<Longrightarrow> n \<le> m \<Longrightarrow> setsum ?f (?S1 m - ?S1 n) < r" |
23111 | 866 |
by (simp only: norm_setsum_f) |
867 |
show "\<exists>N. \<forall>n\<ge>N. setsum ?f (?S1 n - ?S2 n) < r" |
|
868 |
proof (intro exI allI impI) |
|
63550 | 869 |
fix n |
870 |
assume "2 * N \<le> n" |
|
871 |
then have n: "N \<le> n div 2" by simp |
|
23111 | 872 |
have "setsum ?f (?S1 n - ?S2 n) \<le> setsum ?f (?S1 n - ?S1 (n div 2))" |
63550 | 873 |
by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg Diff_mono subset_refl S1_le_S2) |
23111 | 874 |
also have "\<dots> < r" |
875 |
using n div_le_dividend by (rule N) |
|
876 |
finally show "setsum ?f (?S1 n - ?S2 n) < r" . |
|
877 |
qed |
|
878 |
qed |
|
63550 | 879 |
then have "Zfun (\<lambda>n. setsum ?g (?S1 n - ?S2 n)) sequentially" |
36657 | 880 |
apply (rule Zfun_le [rule_format]) |
23111 | 881 |
apply (simp only: norm_setsum_f) |
882 |
apply (rule order_trans [OF norm_setsum setsum_mono]) |
|
883 |
apply (auto simp add: norm_mult_ineq) |
|
884 |
done |
|
63550 | 885 |
then have 2: "(\<lambda>n. setsum ?g (?S1 n) - setsum ?g (?S2 n)) \<longlonglongrightarrow> 0" |
36660
1cc4ab4b7ff7
make (X ----> L) an abbreviation for (X ---> L) sequentially
huffman
parents:
36657
diff
changeset
|
886 |
unfolding tendsto_Zfun_iff diff_0_right |
36657 | 887 |
by (simp only: setsum_diff finite_S1 S2_le_S1) |
61969 | 888 |
with 1 have "(\<lambda>n. setsum ?g (?S2 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)" |
60141
833adf7db7d8
New material, mostly about limits. Consolidation.
paulson <lp15@cam.ac.uk>
parents:
59741
diff
changeset
|
889 |
by (rule Lim_transform2) |
63550 | 890 |
then show ?thesis |
891 |
by (simp only: sums_def setsum_triangle_reindex) |
|
23111 | 892 |
qed |
893 |
||
894 |
lemma Cauchy_product: |
|
895 |
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}" |
|
63550 | 896 |
assumes "summable (\<lambda>k. norm (a k))" |
897 |
and "summable (\<lambda>k. norm (b k))" |
|
56213 | 898 |
shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))" |
63550 | 899 |
using assms by (rule Cauchy_product_sums [THEN sums_unique]) |
56213 | 900 |
|
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61969
diff
changeset
|
901 |
lemma summable_Cauchy_product: |
63550 | 902 |
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}" |
903 |
assumes "summable (\<lambda>k. norm (a k))" |
|
904 |
and "summable (\<lambda>k. norm (b k))" |
|
905 |
shows "summable (\<lambda>k. \<Sum>i\<le>k. a i * b (k - i))" |
|
62087
44841d07ef1d
revisions to limits and derivatives, plus new lemmas
paulson
parents:
62049
diff
changeset
|
906 |
using Cauchy_product_sums[OF assms] by (simp add: sums_iff) |
62049
b0f941e207cf
Added lots of material on infinite sums, convergence radii, harmonic numbers, Gamma function
eberlm
parents:
61969
diff
changeset
|
907 |
|
63550 | 908 |
|
60758 | 909 |
subsection \<open>Series on @{typ real}s\<close> |
56213 | 910 |
|
63550 | 911 |
lemma summable_norm_comparison_test: |
912 |
"\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))" |
|
56213 | 913 |
by (rule summable_comparison_test) auto |
914 |
||
63550 | 915 |
lemma summable_rabs_comparison_test: "\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)" |
916 |
for f :: "nat \<Rightarrow> real" |
|
56213 | 917 |
by (rule summable_comparison_test) auto |
918 |
||
63550 | 919 |
lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> summable f" |
920 |
for f :: "nat \<Rightarrow> real" |
|
56213 | 921 |
by (rule summable_norm_cancel) simp |
922 |
||
63550 | 923 |
lemma summable_rabs: "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)" |
924 |
for f :: "nat \<Rightarrow> real" |
|
56213 | 925 |
by (fold real_norm_def) (rule summable_norm) |
23111 | 926 |
|
63550 | 927 |
lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a::{comm_ring_1,topological_space})" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
928 |
proof - |
63550 | 929 |
have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" |
930 |
by (intro ext) (simp add: zero_power) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
931 |
moreover have "summable \<dots>" by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
932 |
ultimately show ?thesis by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
933 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
934 |
|
63550 | 935 |
lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a::{ring_1,topological_space})" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
936 |
proof - |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
937 |
have "(\<lambda>n. f n * 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then f 0 * 0^0 else 0)" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
938 |
by (intro ext) (simp add: zero_power) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
939 |
moreover have "summable \<dots>" by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
940 |
ultimately show ?thesis by simp |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
941 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
942 |
|
59000 | 943 |
lemma summable_power_series: |
944 |
fixes z :: real |
|
63550 | 945 |
assumes le_1: "\<And>i. f i \<le> 1" |
946 |
and nonneg: "\<And>i. 0 \<le> f i" |
|
947 |
and z: "0 \<le> z" "z < 1" |
|
59000 | 948 |
shows "summable (\<lambda>i. f i * z^i)" |
949 |
proof (rule summable_comparison_test[OF _ summable_geometric]) |
|
63550 | 950 |
show "norm z < 1" |
951 |
using z by (auto simp: less_imp_le) |
|
59000 | 952 |
show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na" |
63550 | 953 |
using z |
954 |
by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1) |
|
59000 | 955 |
qed |
956 |
||
63550 | 957 |
lemma summable_0_powser: "summable (\<lambda>n. f n * 0 ^ n :: 'a::real_normed_div_algebra)" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
958 |
proof - |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
959 |
have A: "(\<lambda>n. f n * 0 ^ n) = (\<lambda>n. if n = 0 then f n else 0)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
960 |
by (intro ext) auto |
63550 | 961 |
then show ?thesis |
962 |
by (subst A) simp_all |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
963 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
964 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
965 |
lemma summable_powser_split_head: |
63550 | 966 |
"summable (\<lambda>n. f (Suc n) * z ^ n :: 'a::real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
967 |
proof - |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
968 |
have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)" |
63550 | 969 |
(is "?lhs \<longleftrightarrow> ?rhs") |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
970 |
proof |
63550 | 971 |
show ?rhs if ?lhs |
972 |
using summable_mult2[OF that, of z] |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
973 |
by (simp add: power_commutes algebra_simps) |
63550 | 974 |
show ?lhs if ?rhs |
975 |
using summable_mult2[OF that, of "inverse z"] |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
976 |
by (cases "z \<noteq> 0", subst (asm) power_Suc2) (simp_all add: algebra_simps) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
977 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
978 |
also have "\<dots> \<longleftrightarrow> summable (\<lambda>n. f n * z ^ n)" by (rule summable_Suc_iff) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
979 |
finally show ?thesis . |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
980 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
981 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
982 |
lemma powser_split_head: |
63550 | 983 |
fixes f :: "nat \<Rightarrow> 'a::{real_normed_div_algebra,banach}" |
984 |
assumes "summable (\<lambda>n. f n * z ^ n)" |
|
985 |
shows "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" |
|
986 |
and "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" |
|
987 |
and "summable (\<lambda>n. f (Suc n) * z ^ n)" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
988 |
proof - |
63550 | 989 |
from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" |
990 |
by (subst summable_powser_split_head) |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
991 |
from suminf_mult2[OF this, of z] |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
992 |
have "(\<Sum>n. f (Suc n) * z ^ n) * z = (\<Sum>n. f (Suc n) * z ^ Suc n)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
993 |
by (simp add: power_commutes algebra_simps) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
994 |
also from assms have "\<dots> = suminf (\<lambda>n. f n * z ^ n) - f 0" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
995 |
by (subst suminf_split_head) simp_all |
63550 | 996 |
finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" |
997 |
by simp |
|
998 |
then show "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n) - f 0" |
|
999 |
by simp |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1000 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1001 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1002 |
lemma summable_partial_sum_bound: |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1003 |
fixes f :: "nat \<Rightarrow> 'a :: banach" |
63550 | 1004 |
and e :: real |
1005 |
assumes summable: "summable f" |
|
1006 |
and e: "e > 0" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1007 |
obtains N where "\<And>m n. m \<ge> N \<Longrightarrow> norm (\<Sum>k=m..n. f k) < e" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1008 |
proof - |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1009 |
from summable have "Cauchy (\<lambda>n. \<Sum>k<n. f k)" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1010 |
by (simp add: Cauchy_convergent_iff summable_iff_convergent) |
63550 | 1011 |
from CauchyD [OF this e] obtain N |
1012 |
where N: "\<And>m n. m \<ge> N \<Longrightarrow> n \<ge> N \<Longrightarrow> norm ((\<Sum>k<m. f k) - (\<Sum>k<n. f k)) < e" |
|
1013 |
by blast |
|
1014 |
have "norm (\<Sum>k=m..n. f k) < e" if m: "m \<ge> N" for m n |
|
1015 |
proof (cases "n \<ge> m") |
|
1016 |
case True |
|
1017 |
with m have "norm ((\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k)) < e" |
|
1018 |
by (intro N) simp_all |
|
1019 |
also from True have "(\<Sum>k<Suc n. f k) - (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)" |
|
1020 |
by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus) |
|
1021 |
finally show ?thesis . |
|
1022 |
next |
|
1023 |
case False |
|
1024 |
with e show ?thesis by simp_all |
|
1025 |
qed |
|
1026 |
then show ?thesis by (rule that) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1027 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1028 |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1029 |
lemma powser_sums_if: |
63550 | 1030 |
"(\<lambda>n. (if n = m then (1 :: 'a::{ring_1,topological_space}) else 0) * z^n) sums z^m" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1031 |
proof - |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1032 |
have "(\<lambda>n. (if n = m then 1 else 0) * z^n) = (\<lambda>n. if n = m then z^n else 0)" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1033 |
by (intro ext) auto |
63550 | 1034 |
then show ?thesis |
1035 |
by (simp add: sums_single) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1036 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1037 |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1038 |
lemma |
63550 | 1039 |
fixes f :: "nat \<Rightarrow> real" |
1040 |
assumes "summable f" |
|
1041 |
and "inj g" |
|
1042 |
and pos: "\<And>x. 0 \<le> f x" |
|
1043 |
shows summable_reindex: "summable (f \<circ> g)" |
|
1044 |
and suminf_reindex_mono: "suminf (f \<circ> g) \<le> suminf f" |
|
1045 |
and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f" |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1046 |
proof - |
63550 | 1047 |
from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A" |
1048 |
by (rule subset_inj_on) simp |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1049 |
|
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1050 |
have smaller: "\<forall>n. (\<Sum>i<n. (f \<circ> g) i) \<le> suminf f" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1051 |
proof |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1052 |
fix n |
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1053 |
have "\<forall> n' \<in> (g ` {..<n}). n' < Suc (Max (g ` {..<n}))" |
63550 | 1054 |
by (metis Max_ge finite_imageI finite_lessThan not_le not_less_eq) |
1055 |
then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m" |
|
1056 |
by blast |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1057 |
|
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1058 |
have "(\<Sum>i<n. f (g i)) = setsum f (g ` {..<n})" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1059 |
by (simp add: setsum.reindex) |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1060 |
also have "\<dots> \<le> (\<Sum>i<m. f i)" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1061 |
by (rule setsum_mono3) (auto simp add: pos n[rule_format]) |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1062 |
also have "\<dots> \<le> suminf f" |
63550 | 1063 |
using \<open>summable f\<close> by (rule setsum_le_suminf) (simp add: pos) |
1064 |
finally show "(\<Sum>i<n. (f \<circ> g) i) \<le> suminf f" |
|
1065 |
by simp |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1066 |
qed |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1067 |
|
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1068 |
have "incseq (\<lambda>n. \<Sum>i<n. (f \<circ> g) i)" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1069 |
by (rule incseq_SucI) (auto simp add: pos) |
61969 | 1070 |
then obtain L where L: "(\<lambda> n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> L" |
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1071 |
using smaller by(rule incseq_convergent) |
63550 | 1072 |
then have "(f \<circ> g) sums L" |
1073 |
by (simp add: sums_def) |
|
1074 |
then show "summable (f \<circ> g)" |
|
1075 |
by (auto simp add: sums_iff) |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1076 |
|
63550 | 1077 |
then have "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> suminf (f \<circ> g)" |
1078 |
by (rule summable_LIMSEQ) |
|
1079 |
then show le: "suminf (f \<circ> g) \<le> suminf f" |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1080 |
by(rule LIMSEQ_le_const2)(blast intro: smaller[rule_format]) |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1081 |
|
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1082 |
assume f: "\<And>x. x \<notin> range g \<Longrightarrow> f x = 0" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1083 |
|
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1084 |
from \<open>summable f\<close> have "suminf f \<le> suminf (f \<circ> g)" |
63550 | 1085 |
proof (rule suminf_le_const) |
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1086 |
fix n |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1087 |
have "\<forall> n' \<in> (g -` {..<n}). n' < Suc (Max (g -` {..<n}))" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1088 |
by(auto intro: Max_ge simp add: finite_vimageI less_Suc_eq_le) |
63550 | 1089 |
then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m" |
1090 |
by blast |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1091 |
have "(\<Sum>i<n. f i) = (\<Sum>i\<in>{..<n} \<inter> range g. f i)" |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1092 |
using f by(auto intro: setsum.mono_neutral_cong_right) |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1093 |
also have "\<dots> = (\<Sum>i\<in>g -` {..<n}. (f \<circ> g) i)" |
63550 | 1094 |
by (rule setsum.reindex_cong[where l=g])(auto) |
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1095 |
also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)" |
63550 | 1096 |
by (rule setsum_mono3)(auto simp add: pos n) |
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1097 |
also have "\<dots> \<le> suminf (f \<circ> g)" |
63550 | 1098 |
using \<open>summable (f \<circ> g)\<close> by (rule setsum_le_suminf) (simp add: pos) |
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1099 |
finally show "setsum f {..<n} \<le> suminf (f \<circ> g)" . |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1100 |
qed |
63550 | 1101 |
with le show "suminf (f \<circ> g) = suminf f" |
1102 |
by (rule antisym) |
|
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1103 |
qed |
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset
|
1104 |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1105 |
lemma sums_mono_reindex: |
63550 | 1106 |
assumes subseq: "subseq g" |
1107 |
and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0" |
|
1108 |
shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c" |
|
1109 |
unfolding sums_def |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1110 |
proof |
61969 | 1111 |
assume lim: "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1112 |
have "(\<lambda>n. \<Sum>k<n. f (g k)) = (\<lambda>n. \<Sum>k<g n. f k)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1113 |
proof |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1114 |
fix n :: nat |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1115 |
from subseq have "(\<Sum>k<n. f (g k)) = (\<Sum>k\<in>g`{..<n}. f k)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1116 |
by (subst setsum.reindex) (auto intro: subseq_imp_inj_on) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1117 |
also from subseq have "\<dots> = (\<Sum>k<g n. f k)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1118 |
by (intro setsum.mono_neutral_left ballI zero) |
63550 | 1119 |
(auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq) |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1120 |
finally show "(\<Sum>k<n. f (g k)) = (\<Sum>k<g n. f k)" . |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1121 |
qed |
63550 | 1122 |
also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" |
1123 |
by (simp only: o_def) |
|
61969 | 1124 |
finally show "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" . |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1125 |
next |
61969 | 1126 |
assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" |
63040 | 1127 |
define g_inv where "g_inv n = (LEAST m. g m \<ge> n)" for n |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1128 |
from filterlim_subseq[OF subseq] have g_inv_ex: "\<exists>m. g m \<ge> n" for n |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1129 |
by (auto simp: filterlim_at_top eventually_at_top_linorder) |
63550 | 1130 |
then have g_inv: "g (g_inv n) \<ge> n" for n |
1131 |
unfolding g_inv_def by (rule LeastI_ex) |
|
1132 |
have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n |
|
1133 |
using that unfolding g_inv_def by (rule Least_le) |
|
1134 |
have g_inv_least': "g m < n" if "m < g_inv n" for m n |
|
1135 |
using that g_inv_least[of n m] by linarith |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1136 |
have "(\<lambda>n. \<Sum>k<n. f k) = (\<lambda>n. \<Sum>k<g_inv n. f (g k))" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1137 |
proof |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1138 |
fix n :: nat |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1139 |
{ |
63550 | 1140 |
fix k |
1141 |
assume k: "k \<in> {..<n} - g`{..<g_inv n}" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1142 |
have "k \<notin> range g" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1143 |
proof (rule notI, elim imageE) |
63550 | 1144 |
fix l |
1145 |
assume l: "k = g l" |
|
1146 |
have "g l < g (g_inv n)" |
|
1147 |
by (rule less_le_trans[OF _ g_inv]) (use k l in simp_all) |
|
1148 |
with subseq have "l < g_inv n" |
|
1149 |
by (simp add: subseq_strict_mono strict_mono_less) |
|
1150 |
with k l show False |
|
1151 |
by simp |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1152 |
qed |
63550 | 1153 |
then have "f k = 0" |
1154 |
by (rule zero) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1155 |
} |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1156 |
with g_inv_least' g_inv have "(\<Sum>k<n. f k) = (\<Sum>k\<in>g`{..<g_inv n}. f k)" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1157 |
by (intro setsum.mono_neutral_right) auto |
63550 | 1158 |
also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" |
1159 |
using subseq_imp_inj_on by (subst setsum.reindex) simp_all |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1160 |
finally show "(\<Sum>k<n. f k) = (\<Sum>k<g_inv n. f (g k))" . |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1161 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1162 |
also { |
63550 | 1163 |
fix K n :: nat |
1164 |
assume "g K \<le> n" |
|
1165 |
also have "n \<le> g (g_inv n)" |
|
1166 |
by (rule g_inv) |
|
1167 |
finally have "K \<le> g_inv n" |
|
1168 |
using subseq by (simp add: strict_mono_less_eq subseq_strict_mono) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1169 |
} |
63550 | 1170 |
then have "filterlim g_inv at_top sequentially" |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1171 |
by (auto simp: filterlim_at_top eventually_at_top_linorder) |
63550 | 1172 |
with lim have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) \<longlonglongrightarrow> c" |
1173 |
by (rule filterlim_compose) |
|
61969 | 1174 |
finally show "(\<lambda>n. \<Sum>k<n. f k) \<longlonglongrightarrow> c" . |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1175 |
qed |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1176 |
|
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1177 |
lemma summable_mono_reindex: |
63550 | 1178 |
assumes subseq: "subseq g" |
1179 |
and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0" |
|
1180 |
shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1181 |
using sums_mono_reindex[of g f, OF assms] by (simp add: summable_def) |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1182 |
|
61609
77b453bd616f
Coercion "real" now has type nat => real only and is no longer overloaded. Type class "real_of" is gone. Many duplicate theorems removed.
paulson <lp15@cam.ac.uk>
parents:
61531
diff
changeset
|
1183 |
lemma suminf_mono_reindex: |
63550 | 1184 |
fixes f :: "nat \<Rightarrow> 'a::{t2_space,comm_monoid_add}" |
1185 |
assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1186 |
shows "suminf (\<lambda>n. f (g n)) = suminf f" |
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1187 |
proof (cases "summable f") |
63550 | 1188 |
case True |
1189 |
with sums_mono_reindex [of g f, OF assms] |
|
1190 |
and summable_mono_reindex [of g f, OF assms] |
|
1191 |
show ?thesis |
|
1192 |
by (simp add: sums_iff) |
|
1193 |
next |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1194 |
case False |
63550 | 1195 |
then have "\<not>(\<exists>c. f sums c)" |
1196 |
unfolding summable_def by blast |
|
1197 |
then have "suminf f = The (\<lambda>_. False)" |
|
1198 |
by (simp add: suminf_def) |
|
1199 |
moreover from False have "\<not> summable (\<lambda>n. f (g n))" |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1200 |
using summable_mono_reindex[of g f, OF assms] by simp |
63550 | 1201 |
then have "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" |
1202 |
unfolding summable_def by blast |
|
1203 |
then have "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" |
|
1204 |
by (simp add: suminf_def) |
|
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1205 |
ultimately show ?thesis by simp |
63550 | 1206 |
qed |
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset
|
1207 |
|
14416 | 1208 |
end |