author  wenzelm 
Tue, 29 Dec 2015 23:04:53 +0100  
changeset 61969  e01015e49041 
parent 61799  4cf66f21b764 
child 62049  b0f941e207cf 
permissions  rwrr 
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 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

18 
definition 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

19 
sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

20 
(infixr "sums" 80) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

21 
where 
61969  22 
"f sums s \<longleftrightarrow> (\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> s" 
14416  23 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

24 
definition summable :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> bool" where 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

25 
"summable f \<longleftrightarrow> (\<exists>s. f sums s)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

26 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

27 
definition 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

28 
suminf :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

29 
(binder "\<Sum>" 10) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

30 
where 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

31 
"suminf f = (THE s. f sums s)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

32 

60758  33 
subsection \<open>Infinite summability on topological monoids\<close> 
56213  34 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

35 
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

36 
by simp 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

37 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

38 
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

39 
by (drule ext) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

40 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

41 
lemma sums_summable: "f sums l \<Longrightarrow> summable f" 
41970  42 
by (simp add: sums_def summable_def, blast) 
14416  43 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

44 
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

45 
by (simp add: summable_def sums_def convergent_def) 
14416  46 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

47 
lemma summable_iff_convergent': 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

48 
"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

49 
by (simp_all only: summable_iff_convergent convergent_def 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

50 
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

51 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

52 
lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)" 
41970  53 
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

54 

56213  55 
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

56 
unfolding sums_def by simp 
56213  57 

58 
lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)" 

59 
by (rule sums_zero [THEN sums_summable]) 

60 

61 
lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s" 

62 
apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially) 

63 
apply safe 

64 
apply (erule_tac x=S in allE) 

65 
apply safe 

66 
apply (rule_tac x="N" in exI, safe) 

67 
apply (drule_tac x="n*k" in spec) 

68 
apply (erule mp) 

69 
apply (erule order_trans) 

70 
apply simp 

71 
done 

72 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

73 
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

74 
by (rule arg_cong[of f g], rule ext) simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

75 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

76 
lemma summable_cong: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

77 
assumes "eventually (\<lambda>x. f x = (g x :: 'a :: real_normed_vector)) sequentially" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

78 
shows "summable f = summable g" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

79 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

80 
from assms obtain N where N: "\<forall>n\<ge>N. f n = g n" by (auto simp: eventually_at_top_linorder) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

81 
def C \<equiv> "(\<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

82 
from eventually_ge_at_top[of N] 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

83 
have "eventually (\<lambda>n. setsum f {..<n} = C + setsum g {..<n}) sequentially" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

84 
proof eventually_elim 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

85 
fix n assume n: "n \<ge> N" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

86 
from n have "{..<n} = {..<N} \<union> {N..<n}" by auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

87 
also have "setsum f ... = setsum f {..<N} + setsum f {N..<n}" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

88 
by (intro setsum.union_disjoint) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

89 
also from N have "setsum f {N..<n} = setsum g {N..<n}" 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

90 
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

91 
unfolding C_def by (simp add: algebra_simps setsum_subtractf) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

92 
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

93 
by (intro setsum.union_disjoint [symmetric]) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

94 
also from n have "{..<N} \<union> {N..<n} = {..<n}" by auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

95 
finally show "setsum f {..<n} = C + setsum g {..<n}" . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

96 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

97 
from convergent_cong[OF this] show ?thesis 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

98 
by (simp add: summable_iff_convergent convergent_add_const_iff) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

99 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

100 

47761  101 
lemma sums_finite: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

102 
assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" 
47761  103 
shows "f sums (\<Sum>n\<in>N. f n)" 
104 
proof  

105 
{ fix n 

106 
have "setsum f {..<n + Suc (Max N)} = setsum f N" 

107 
proof cases 

108 
assume "N = {}" 

109 
with f have "f = (\<lambda>x. 0)" by auto 

110 
then show ?thesis by simp 

111 
next 

112 
assume [simp]: "N \<noteq> {}" 

113 
show ?thesis 

57418  114 
proof (safe intro!: setsum.mono_neutral_right f) 
47761  115 
fix i assume "i \<in> N" 
116 
then have "i \<le> Max N" by simp 

117 
then show "i < n + Suc (Max N)" by simp 

118 
qed 

119 
qed } 

120 
note eq = this 

121 
show ?thesis unfolding sums_def 

122 
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

123 
(simp add: eq atLeast0LessThan del: add_Suc_right) 
47761  124 
qed 
125 

56213  126 
lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f" 
127 
by (rule sums_summable) (rule sums_finite) 

128 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

129 
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  130 
using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp 
131 

56213  132 
lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)" 
133 
by (rule sums_summable) (rule sums_If_finite_set) 

134 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

135 
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

136 
using sums_If_finite_set[of "{r. P r}"] by simp 
16819  137 

56213  138 
lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)" 
139 
by (rule sums_summable) (rule sums_If_finite) 

140 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

141 
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

142 
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

143 

56213  144 
lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)" 
145 
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

146 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

147 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

148 
fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

149 
begin 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

150 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

151 
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

152 
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

153 
(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

154 

61969  155 
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

156 
by (rule summable_sums [unfolded sums_def]) 
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 
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

159 
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

160 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

161 
lemma sums_iff: "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

162 
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

163 

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

164 
lemma summable_sums_iff: 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

165 
"summable (f :: nat \<Rightarrow> 'a :: {comm_monoid_add,t2_space}) \<longleftrightarrow> f sums suminf f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

166 
by (auto simp: sums_iff summable_sums) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

167 

59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

168 
lemma sums_unique2: 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

169 
fixes a b :: "'a::{comm_monoid_add,t2_space}" 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

170 
shows "f sums a \<Longrightarrow> f sums b \<Longrightarrow> a = b" 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

171 
by (simp add: sums_iff) 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

172 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

173 
lemma suminf_finite: 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

174 
assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

175 
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

176 
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

177 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

178 
end 
16819  179 

41970  180 
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

181 
by (rule sums_zero [THEN sums_unique, symmetric]) 
16819  182 

56213  183 

60758  184 
subsection \<open>Infinite summability on ordered, topological monoids\<close> 
56213  185 

186 
lemma sums_le: 

187 
fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}" 

188 
shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t" 

189 
by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def) 

190 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

191 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

192 
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

193 
begin 
14416  194 

56213  195 
lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g" 
196 
by (auto dest: sums_summable intro: sums_le) 

197 

198 
lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f" 

199 
by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto 

200 

201 
lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f" 

202 
using setsum_le_suminf[of 0] by simp 

203 

204 
lemma setsum_less_suminf2: "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" 

205 
using 

206 
setsum_le_suminf[of "Suc i"] 

207 
add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"] 

208 
setsum_mono2[of "{..<i}" "{..<n}" f] 

209 
by (auto simp: less_imp_le ac_simps) 

210 

211 
lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f" 

212 
using setsum_less_suminf2[of n n] by (simp add: less_imp_le) 

213 

214 
lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f" 

215 
using setsum_less_suminf2[of 0 i] by simp 

216 

217 
lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f" 

218 
using suminf_pos2[of 0] by (simp add: less_imp_le) 

219 

220 
lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x" 

221 
by (metis LIMSEQ_le_const2 summable_LIMSEQ) 

14416  222 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

223 
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  224 
proof 
225 
assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n" 

61969  226 
then have f: "(\<lambda>n. \<Sum>i<n. f i) \<longlonglongrightarrow> 0" 
56213  227 
using summable_LIMSEQ[of f] by simp 
228 
then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0" 

229 
proof (rule LIMSEQ_le_const) 

50999  230 
fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}" 
231 
using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto 

232 
qed 

233 
with pos show "\<forall>n. f n = 0" 

234 
by (auto intro!: antisym) 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

235 
qed (metis suminf_zero fun_eq_iff) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

236 

56213  237 
lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)" 
238 
using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le) 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

239 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

240 
end 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

241 

56213  242 
lemma summableI_nonneg_bounded: 
243 
fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}" 

244 
assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x" 

245 
shows "summable f" 

246 
unfolding summable_def sums_def[abs_def] 

247 
proof (intro exI order_tendstoI) 

248 
have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))" 

249 
using le by (auto simp: bdd_above_def) 

250 
{ fix a assume "a < (SUP n. \<Sum>i<n. f i)" 

251 
then obtain n where "a < (\<Sum>i<n. f i)" 

252 
by (auto simp add: less_cSUP_iff) 

253 
then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)" 

254 
by (rule less_le_trans) (auto intro!: setsum_mono2) 

255 
then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially" 

256 
by (auto simp: eventually_sequentially) } 

257 
{ fix a assume "(SUP n. \<Sum>i<n. f i) < a" 

258 
moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)" 

259 
by (auto intro: cSUP_upper) 

260 
ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially" 

261 
by (auto intro: le_less_trans simp: eventually_sequentially) } 

262 
qed 

263 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

264 

60758  265 
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

266 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

267 
lemma sums_Suc_iff: 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

268 
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

269 
shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

270 
proof  
61969  271 
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

272 
by (subst LIMSEQ_Suc_iff) (simp add: sums_def) 
61969  273 
also have "\<dots> \<longleftrightarrow> (\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0" 
57418  274 
by (simp add: ac_simps setsum.reindex image_iff lessThan_Suc_eq_insert_0) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

275 
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

276 
proof 
61969  277 
assume "(\<lambda>i. (\<Sum>j<i. f (Suc j)) + f 0) \<longlonglongrightarrow> s + f 0" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

278 
with tendsto_add[OF this tendsto_const, of " f 0"] 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

279 
show "(\<lambda>i. f (Suc i)) sums s" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

280 
by (simp add: sums_def) 
58729
e8ecc79aee43
add tendsto_const and tendsto_ident_at as simp and intro rules
hoelzl
parents:
57418
diff
changeset

281 
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

282 
finally show ?thesis .. 
50999  283 
qed 
284 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

285 
lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

286 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

287 
assume "summable f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

288 
hence "f sums suminf f" by (rule summable_sums) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

289 
hence "(\<lambda>n. f (Suc n)) sums (suminf f  f 0)" by (simp add: sums_Suc_iff) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

290 
thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

291 
qed (auto simp: sums_Suc_iff summable_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

292 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

293 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

294 
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

295 
begin 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

296 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

297 
lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)" 
57418  298 
unfolding sums_def by (simp add: setsum.distrib tendsto_add) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

299 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

300 
lemma summable_add: "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

301 
unfolding summable_def by (auto intro: sums_add) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

302 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

303 
lemma suminf_add: "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

304 
by (intro sums_unique sums_add summable_sums) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

305 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

306 
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

307 
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

308 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

309 
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

310 
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

311 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

312 
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

313 
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

314 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

315 
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

316 
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

317 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

318 
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

319 
unfolding summable_def by (auto intro: sums_minus) 
20692  320 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

321 
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

322 
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

323 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

324 
lemma sums_Suc: "(\<lambda> n. f (Suc n)) sums l \<Longrightarrow> f sums (l + f 0)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

325 
by (simp add: sums_Suc_iff) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

326 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

327 
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

328 
proof (induct n arbitrary: s) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

329 
case (Suc n) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

330 
moreover have "(\<lambda>i. f (Suc i + n)) sums s \<longleftrightarrow> (\<lambda>i. f (i + n)) sums (s + f n)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

331 
by (subst sums_Suc_iff) simp 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

332 
ultimately show ?case 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

333 
by (simp add: ac_simps) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

334 
qed simp 
20692  335 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

336 
lemma summable_iff_shift: "summable (\<lambda>n. f (n + k)) \<longleftrightarrow> summable f" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

337 
by (metis diff_add_cancel summable_def sums_iff_shift[abs_def]) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

338 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

339 
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

340 
by (simp add: sums_iff_shift) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

341 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

342 
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

343 
by (simp add: summable_iff_shift) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

344 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

345 
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

346 
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

347 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

348 
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

349 
by (auto simp add: suminf_minus_initial_segment) 
20692  350 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

351 
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

352 
using suminf_split_initial_segment[of 1] by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

353 

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

354 
lemma suminf_exist_split: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

355 
fixes r :: real assumes "0 < r" and "summable f" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

356 
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

357 
proof  
60758  358 
from LIMSEQ_D[OF summable_LIMSEQ[OF \<open>summable f\<close>] \<open>0 < r\<close>] 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

359 
obtain N :: nat where "\<forall> n \<ge> N. norm (setsum f {..<n}  suminf f) < r" by auto 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

360 
thus ?thesis 
60758  361 
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

362 
qed 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

363 

61969  364 
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

365 
apply (drule summable_iff_convergent [THEN iffD1]) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

366 
apply (drule convergent_Cauchy) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

367 
apply (simp only: Cauchy_iff LIMSEQ_iff, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

368 
apply (drule_tac x="r" in spec, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

369 
apply (rule_tac x="M" in exI, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

370 
apply (drule_tac x="Suc n" in spec, simp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

371 
apply (drule_tac x="n" in spec, simp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

372 
done 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

373 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

374 
lemma summable_imp_convergent: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

375 
"summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

376 
by (force dest!: summable_LIMSEQ_zero simp: convergent_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

377 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

378 
lemma summable_imp_Bseq: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

379 
"summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

380 
by (simp add: convergent_imp_Bseq summable_imp_convergent) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

381 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

382 
end 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

383 

59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

384 
lemma summable_minus_iff: 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

385 
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector" 
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

386 
shows "summable (\<lambda>n.  f n) \<longleftrightarrow> summable f" 
61799  387 
by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close> 
59613
7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

388 

7103019278f0
The function frac. Various lemmas about limits, series, the exp function, etc.
paulson <lp15@cam.ac.uk>
parents:
59025
diff
changeset

389 

57025  390 
context 
391 
fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set" 

392 
begin 

393 

394 
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)" 

395 
by (induct I rule: infinite_finite_induct) (auto intro!: sums_add) 

396 

397 
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)" 

398 
using sums_unique[OF sums_setsum, OF summable_sums] by simp 

399 

400 
lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)" 

401 
using sums_summable[OF sums_setsum[OF summable_sums]] . 

402 

403 
end 

404 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

405 
lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

406 
unfolding sums_def by (drule tendsto, simp only: setsum) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

407 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

408 
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

409 
unfolding summable_def by (auto intro: sums) 
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 (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

412 
by (intro sums_unique sums summable_sums) 
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 
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

415 
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

416 
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

417 

57275
0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset

418 
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

419 
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

420 
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

421 

0ddb5b755cdc
moved lemmas from the proof of the Central Limit Theorem by Jeremy Avigad and Luke Serafin
hoelzl
parents:
57129
diff
changeset

422 
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

423 
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

424 
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

425 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

426 
lemma summable_const_iff: "summable (\<lambda>_. c) \<longleftrightarrow> (c :: 'a :: real_normed_vector) = 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

427 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

428 
{ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

429 
assume "c \<noteq> 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

430 
hence "filterlim (\<lambda>n. of_nat n * norm c) at_top sequentially" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

431 
by (subst mult.commute) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

432 
(auto intro!: filterlim_tendsto_pos_mult_at_top filterlim_real_sequentially) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

433 
hence "\<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

434 
by (intro filterlim_at_infinity_imp_not_convergent filterlim_at_top_imp_at_infinity) 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

435 
(simp_all add: setsum_constant_scaleR) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

436 
hence "\<not>summable (\<lambda>_. c)" unfolding summable_iff_convergent using convergent_norm by blast 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

437 
} 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

438 
thus ?thesis by auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

439 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

440 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

441 

60758  442 
subsection \<open>Infinite summability on real normed algebras\<close> 
56213  443 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

444 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

445 
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

446 
begin 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

447 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

448 
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

449 
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

450 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

451 
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

452 
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

453 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

454 
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

455 
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

456 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

457 
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

458 
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

459 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

460 
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

461 
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

462 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

463 
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

464 
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

465 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

466 
end 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

467 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

468 
lemma sums_mult_iff: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

469 
assumes "c \<noteq> 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

470 
shows "(\<lambda>n. c * f n :: 'a :: {real_normed_algebra,field}) sums (c * d) \<longleftrightarrow> f sums d" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

471 
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

472 
by (force simp: field_simps assms) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

473 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

474 
lemma sums_mult2_iff: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

475 
assumes "c \<noteq> (0 :: 'a :: {real_normed_algebra, field})" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

476 
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

477 
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

478 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

479 
lemma sums_of_real_iff: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

480 
"(\<lambda>n. of_real (f n) :: 'a :: real_normed_div_algebra) sums of_real c \<longleftrightarrow> f sums c" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

481 
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

482 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

483 

60758  484 
subsection \<open>Infinite summability on real normed fields\<close> 
56213  485 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

486 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

487 
fixes c :: "'a::real_normed_field" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

488 
begin 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

489 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

490 
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

491 
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

492 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

493 
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

494 
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

495 

c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

496 
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

497 
by (rule bounded_linear.suminf [OF bounded_linear_divide, symmetric]) 
14416  498 

60758  499 
text\<open>Sum of a geometric progression.\<close> 
14416  500 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

501 
lemma geometric_sums: "norm c < 1 \<Longrightarrow> (\<lambda>n. c^n) sums (1 / (1  c))" 
20692  502 
proof  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

503 
assume less_1: "norm c < 1" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

504 
hence neq_1: "c \<noteq> 1" by auto 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

505 
hence neq_0: "c  1 \<noteq> 0" by simp 
61969  506 
from less_1 have lim_0: "(\<lambda>n. c^n) \<longlonglongrightarrow> 0" 
20692  507 
by (rule LIMSEQ_power_zero) 
61969  508 
hence "(\<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

509 
using neq_0 by (intro tendsto_intros) 
61969  510 
hence "(\<lambda>n. (c ^ n  1) / (c  1)) \<longlonglongrightarrow> 1 / (1  c)" 
20692  511 
by (simp add: nonzero_minus_divide_right [OF neq_0] diff_divide_distrib) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

512 
thus "(\<lambda>n. c ^ n) sums (1 / (1  c))" 
20692  513 
by (simp add: sums_def geometric_sum neq_1) 
514 
qed 

515 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

516 
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

517 
by (rule geometric_sums [THEN sums_summable]) 
14416  518 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

519 
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

520 
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

521 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

522 
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

523 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

524 
assume "summable (\<lambda>n. c ^ n :: 'a :: real_normed_field)" 
61969  525 
hence "(\<lambda>n. norm c ^ n) \<longlonglongrightarrow> 0" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

526 
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

527 
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

528 
by (auto simp: eventually_at_top_linorder) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

529 
thus "norm c < 1" using one_le_power[of "norm c" n] by (cases "norm c \<ge> 1") (linarith, simp) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

530 
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

531 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

532 
end 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

533 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

534 
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

535 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

536 
have 2: "(\<lambda>n. (1/2::real)^n) sums 2" using geometric_sums [of "1/2::real"] 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

537 
by auto 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

538 
have "(\<lambda>n. (1/2::real)^Suc n) = (\<lambda>n. (1 / 2) ^ n / 2)" 
59741
5b762cd73a8e
Lots of new material on complexvalued functions. Modified simplification of (x/n)^k
paulson <lp15@cam.ac.uk>
parents:
59712
diff
changeset

539 
by (simp add: mult.commute) 
44282
f0de18b62d63
remove bounded_(bi)linear locale interpretations, to avoid duplicating so many lemmas
huffman
parents:
41970
diff
changeset

540 
thus ?thesis using sums_divide [OF 2, of 2] 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

541 
by simp 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

542 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
32877
diff
changeset

543 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

544 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

545 
subsection \<open>Telescoping\<close> 
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 
lemma telescope_sums: 
61969  548 
assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

549 
shows "(\<lambda>n. f (Suc n)  f n) sums (c  f 0)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

550 
unfolding sums_def 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

551 
proof (subst LIMSEQ_Suc_iff [symmetric]) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

552 
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

553 
by (simp add: lessThan_Suc_atMost atLeast0AtMost [symmetric] setsum_Suc_diff) 
61969  554 
also have "\<dots> \<longlonglongrightarrow> c  f 0" by (intro tendsto_diff LIMSEQ_Suc[OF assms] tendsto_const) 
555 
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

556 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

557 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

558 
lemma telescope_sums': 
61969  559 
assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

560 
shows "(\<lambda>n. f n  f (Suc n)) sums (f 0  c)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

561 
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

562 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

563 
lemma telescope_summable: 
61969  564 
assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

565 
shows "summable (\<lambda>n. f (Suc n)  f n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

566 
using telescope_sums[OF assms] by (simp add: sums_iff) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

567 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

568 
lemma telescope_summable': 
61969  569 
assumes "f \<longlonglongrightarrow> (c :: 'a :: real_normed_vector)" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

570 
shows "summable (\<lambda>n. f n  f (Suc n))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

571 
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

572 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

573 

60758  574 
subsection \<open>Infinite summability on Banach spaces\<close> 
56213  575 

60758  576 
text\<open>Cauchytype 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

577 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

578 
lemma summable_Cauchy: 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

579 
fixes f :: "nat \<Rightarrow> 'a::banach" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

580 
shows "summable f \<longleftrightarrow> (\<forall>e>0. \<exists>N. \<forall>m\<ge>N. \<forall>n. norm (setsum f {m..<n}) < e)" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

581 
apply (simp only: summable_iff_convergent Cauchy_convergent_iff [symmetric] Cauchy_iff, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

582 
apply (drule spec, drule (1) mp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

583 
apply (erule exE, rule_tac x="M" in exI, clarify) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

584 
apply (rule_tac x="m" and y="n" in linorder_le_cases) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

585 
apply (frule (1) order_trans) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

586 
apply (drule_tac x="n" in spec, drule (1) mp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

587 
apply (drule_tac x="m" in spec, drule (1) mp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

588 
apply (simp_all add: setsum_diff [symmetric]) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

589 
apply (drule spec, drule (1) mp) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

590 
apply (erule exE, rule_tac x="N" in exI, clarify) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

591 
apply (rule_tac x="m" and y="n" in linorder_le_cases) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

592 
apply (subst norm_minus_commute) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

593 
apply (simp_all add: setsum_diff [symmetric]) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

594 
done 
14416  595 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

596 
context 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

597 
fixes f :: "nat \<Rightarrow> 'a::banach" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

598 
begin 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

599 

60758  600 
text\<open>Absolute convergence imples normal convergence\<close> 
20689  601 

56194  602 
lemma summable_norm_cancel: "summable (\<lambda>n. norm (f n)) \<Longrightarrow> summable f" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

603 
apply (simp only: summable_Cauchy, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

604 
apply (drule_tac x="e" in spec, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

605 
apply (rule_tac x="N" in exI, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

606 
apply (drule_tac x="m" in spec, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

607 
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

608 
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

609 
apply simp 
50999  610 
done 
32707
836ec9d0a0c8
New lemmas involving the real numbers, especially limits and series
paulson
parents:
31336
diff
changeset

611 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

612 
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

613 
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

614 

60758  615 
text \<open>Comparison tests\<close> 
14416  616 

56194  617 
lemma summable_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable f" 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

618 
apply (simp add: summable_Cauchy, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

619 
apply (drule_tac x="e" in spec, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

620 
apply (rule_tac x = "N + Na" in exI, safe) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

621 
apply (rotate_tac 2) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

622 
apply (drule_tac x = m in spec) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

623 
apply (auto, rotate_tac 2, drule_tac x = n in spec) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

624 
apply (rule_tac y = "\<Sum>k=m..<n. norm (f k)" in order_le_less_trans) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

625 
apply (rule norm_setsum) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

626 
apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

627 
apply (auto intro: setsum_mono simp add: abs_less_iff) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

628 
done 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

629 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

630 
lemma summable_comparison_test_ev: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

631 
shows "eventually (\<lambda>n. norm (f n) \<le> g n) sequentially \<Longrightarrow> summable g \<Longrightarrow> summable f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

632 
by (rule summable_comparison_test) (auto simp: eventually_at_top_linorder) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

633 

56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56213
diff
changeset

634 
(*A better argument order*) 
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56213
diff
changeset

635 
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

636 
by (rule summable_comparison_test) auto 
56217
dc429a5b13c4
Some rationalisation of basic lemmas
paulson <lp15@cam.ac.uk>
parents:
56213
diff
changeset

637 

60758  638 
subsection \<open>The Ratio Test\<close> 
15085
5693a977a767
removed some [iff] declarations from RealDef.thy, concerning inequalities
paulson
parents:
15053
diff
changeset

639 

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

640 
lemma summable_ratio_test: 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

641 
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

642 
shows "summable f" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

643 
proof cases 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

644 
assume "0 < c" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

645 
show "summable f" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

646 
proof (rule summable_comparison_test) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

647 
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

648 
proof (intro exI allI impI) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

649 
fix n assume "N \<le> n" then show "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

650 
proof (induct rule: inc_induct) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

651 
case (step m) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

652 
moreover have "norm (f (Suc m)) / c ^ Suc m * c ^ n \<le> norm (f m) / c ^ m * c ^ n" 
60758  653 
using \<open>0 < c\<close> \<open>c < 1\<close> assms(2)[OF \<open>N \<le> m\<close>] by (simp add: field_simps) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

654 
ultimately show ?case by simp 
60758  655 
qed (insert \<open>0 < c\<close>, simp) 
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

656 
qed 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

657 
show "summable (\<lambda>n. norm (f N) / c ^ N * c ^ n)" 
60758  658 
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

659 
qed 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

660 
next 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

661 
assume c: "\<not> 0 < c" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

662 
{ fix n assume "n \<ge> N" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

663 
then have "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

664 
by fact 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

665 
also have "\<dots> \<le> 0" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

666 
using c by (simp add: not_less mult_nonpos_nonneg) 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

667 
finally have "f (Suc n) = 0" 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

668 
by auto } 
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

669 
then show "summable f" 
56194  670 
by (intro sums_summable[OF sums_finite, of "{.. Suc N}"]) (auto simp: not_le Suc_less_eq2) 
56178  671 
qed 
672 

56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

673 
end 
14416  674 

60758  675 
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

676 

2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

677 
lemma abel_lemma: 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

678 
fixes a :: "nat \<Rightarrow> 'a::real_normed_vector" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

679 
assumes r: "0 \<le> r" and r0: "r < r0" and M: "\<And>n. norm (a n) * r0^n \<le> M" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

680 
shows "summable (\<lambda>n. norm (a n) * r^n)" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

681 
proof (rule summable_comparison_test') 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

682 
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

683 
using assms 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

684 
by (auto simp add: summable_mult summable_geometric) 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

685 
next 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

686 
fix n 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

687 
show "norm (norm (a n) * r ^ n) \<le> M * (r / r0) ^ n" 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

688 
using r r0 M [of n] 
60867  689 
apply (auto simp add: abs_mult field_simps) 
56369
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

690 
apply (cases "r=0", simp) 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

691 
apply (cases n, auto) 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

692 
done 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

693 
qed 
2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

694 

2704ca85be98
moved generic theorems from Complex_Analysis_Basic; fixed some theorem names
hoelzl
parents:
56217
diff
changeset

695 

60758  696 
text\<open>Summability of geometric series for real algebras\<close> 
23084  697 

698 
lemma complete_algebra_summable_geometric: 

31017  699 
fixes x :: "'a::{real_normed_algebra_1,banach}" 
23084  700 
shows "norm x < 1 \<Longrightarrow> summable (\<lambda>n. x ^ n)" 
701 
proof (rule summable_comparison_test) 

702 
show "\<exists>N. \<forall>n\<ge>N. norm (x ^ n) \<le> norm x ^ n" 

703 
by (simp add: norm_power_ineq) 

704 
show "norm x < 1 \<Longrightarrow> summable (\<lambda>n. norm x ^ n)" 

705 
by (simp add: summable_geometric) 

706 
qed 

707 

60758  708 
subsection \<open>Cauchy Product Formula\<close> 
23111  709 

60758  710 
text \<open> 
54703  711 
Proof based on Analysis WebNotes: Chapter 07, Class 41 
712 
@{url "http://www.math.unl.edu/~webnotes/classes/class41/prp77.htm"} 

60758  713 
\<close> 
23111  714 

715 
lemma Cauchy_product_sums: 

716 
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}" 

717 
assumes a: "summable (\<lambda>k. norm (a k))" 

718 
assumes b: "summable (\<lambda>k. norm (b k))" 

56213  719 
shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k  i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))" 
23111  720 
proof  
56193
c726ecfb22b6
cleanup Series: sorted according to typeclass hierarchy, use {..<_} instead of {0..<_}
hoelzl
parents:
56178
diff
changeset

721 
let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}" 
23111  722 
let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}" 
723 
have S1_mono: "\<And>m n. m \<le> n \<Longrightarrow> ?S1 m \<subseteq> ?S1 n" by auto 

724 
have S2_le_S1: "\<And>n. ?S2 n \<subseteq> ?S1 n" by auto 

725 
have S1_le_S2: "\<And>n. ?S1 (n div 2) \<subseteq> ?S2 n" by auto 

726 
have finite_S1: "\<And>n. finite (?S1 n)" by simp 

727 
with S2_le_S1 have finite_S2: "\<And>n. finite (?S2 n)" by (rule finite_subset) 

728 

729 
let ?g = "\<lambda>(i,j). a i * b j" 

730 
let ?f = "\<lambda>(i,j). norm (a i) * norm (b j)" 

56536  731 
have f_nonneg: "\<And>x. 0 \<le> ?f x" by (auto) 
23111  732 
hence norm_setsum_f: "\<And>A. norm (setsum ?f A) = setsum ?f A" 
733 
unfolding real_norm_def 

734 
by (simp only: abs_of_nonneg setsum_nonneg [rule_format]) 

735 

61969  736 
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

737 
by (intro tendsto_mult summable_LIMSEQ summable_norm_cancel [OF a] summable_norm_cancel [OF b]) 
61969  738 
hence 1: "(\<lambda>n. setsum ?g (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. a k) * (\<Sum>k. b k)" 
57418  739 
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) 
23111  740 

61969  741 
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

742 
using a b by (intro tendsto_mult summable_LIMSEQ) 
61969  743 
hence "(\<lambda>n. setsum ?f (?S1 n)) \<longlonglongrightarrow> (\<Sum>k. norm (a k)) * (\<Sum>k. norm (b k))" 
57418  744 
by (simp only: setsum_product setsum.Sigma [rule_format] finite_lessThan) 
23111  745 
hence "convergent (\<lambda>n. setsum ?f (?S1 n))" 
746 
by (rule convergentI) 

747 
hence Cauchy: "Cauchy (\<lambda>n. setsum ?f (?S1 n))" 

748 
by (rule convergent_Cauchy) 

36657  749 
have "Zfun (\<lambda>n. setsum ?f (?S1 n  ?S2 n)) sequentially" 
750 
proof (rule ZfunI, simp only: eventually_sequentially norm_setsum_f) 

23111  751 
fix r :: real 
752 
assume r: "0 < r" 

753 
from CauchyD [OF Cauchy r] obtain N 

754 
where "\<forall>m\<ge>N. \<forall>n\<ge>N. norm (setsum ?f (?S1 m)  setsum ?f (?S1 n)) < r" .. 

755 
hence "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> norm (setsum ?f (?S1 m  ?S1 n)) < r" 

756 
by (simp only: setsum_diff finite_S1 S1_mono) 

757 
hence N: "\<And>m n. \<lbrakk>N \<le> n; n \<le> m\<rbrakk> \<Longrightarrow> setsum ?f (?S1 m  ?S1 n) < r" 

758 
by (simp only: norm_setsum_f) 

759 
show "\<exists>N. \<forall>n\<ge>N. setsum ?f (?S1 n  ?S2 n) < r" 

760 
proof (intro exI allI impI) 

761 
fix n assume "2 * N \<le> n" 

762 
hence n: "N \<le> n div 2" by simp 

763 
have "setsum ?f (?S1 n  ?S2 n) \<le> setsum ?f (?S1 n  ?S1 (n div 2))" 

764 
by (intro setsum_mono2 finite_Diff finite_S1 f_nonneg 

765 
Diff_mono subset_refl S1_le_S2) 

766 
also have "\<dots> < r" 

767 
using n div_le_dividend by (rule N) 

768 
finally show "setsum ?f (?S1 n  ?S2 n) < r" . 

769 
qed 

770 
qed 

36657  771 
hence "Zfun (\<lambda>n. setsum ?g (?S1 n  ?S2 n)) sequentially" 
772 
apply (rule Zfun_le [rule_format]) 

23111  773 
apply (simp only: norm_setsum_f) 
774 
apply (rule order_trans [OF norm_setsum setsum_mono]) 

775 
apply (auto simp add: norm_mult_ineq) 

776 
done 

61969  777 
hence 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

778 
unfolding tendsto_Zfun_iff diff_0_right 
36657  779 
by (simp only: setsum_diff finite_S1 S2_le_S1) 
23111  780 

61969  781 
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

782 
by (rule Lim_transform2) 
23111  783 
thus ?thesis by (simp only: sums_def setsum_triangle_reindex) 
784 
qed 

785 

786 
lemma Cauchy_product: 

787 
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}" 

788 
assumes a: "summable (\<lambda>k. norm (a k))" 

789 
assumes b: "summable (\<lambda>k. norm (b k))" 

56213  790 
shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k  i))" 
791 
using a b 

792 
by (rule Cauchy_product_sums [THEN sums_unique]) 

793 

60758  794 
subsection \<open>Series on @{typ real}s\<close> 
56213  795 

796 
lemma summable_norm_comparison_test: "\<exists>N. \<forall>n\<ge>N. norm (f n) \<le> g n \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. norm (f n))" 

797 
by (rule summable_comparison_test) auto 

798 

799 
lemma summable_rabs_comparison_test: "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n :: real\<bar>)" 

800 
by (rule summable_comparison_test) auto 

801 

802 
lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f" 

803 
by (rule summable_norm_cancel) simp 

804 

805 
lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)" 

806 
by (fold real_norm_def) (rule summable_norm) 

23111  807 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

808 
lemma summable_zero_power [simp]: "summable (\<lambda>n. 0 ^ n :: 'a :: {comm_ring_1,topological_space})" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

809 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

810 
have "(\<lambda>n. 0 ^ n :: 'a) = (\<lambda>n. if n = 0 then 0^0 else 0)" by (intro ext) (simp add: zero_power) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

811 
moreover have "summable \<dots>" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

812 
ultimately show ?thesis by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

813 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

814 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

815 
lemma summable_zero_power' [simp]: "summable (\<lambda>n. f n * 0 ^ n :: 'a :: {ring_1,topological_space})" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

816 
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

817 
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

818 
by (intro ext) (simp add: zero_power) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

819 
moreover have "summable \<dots>" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

820 
ultimately show ?thesis by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

821 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

822 

59000  823 
lemma summable_power_series: 
824 
fixes z :: real 

825 
assumes le_1: "\<And>i. f i \<le> 1" and nonneg: "\<And>i. 0 \<le> f i" and z: "0 \<le> z" "z < 1" 

826 
shows "summable (\<lambda>i. f i * z^i)" 

827 
proof (rule summable_comparison_test[OF _ summable_geometric]) 

828 
show "norm z < 1" using z by (auto simp: less_imp_le) 

829 
show "\<And>n. \<exists>N. \<forall>na\<ge>N. norm (f na * z ^ na) \<le> z ^ na" 

830 
using z by (auto intro!: exI[of _ 0] mult_left_le_one_le simp: abs_mult nonneg power_abs less_imp_le le_1) 

831 
qed 

832 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

833 
lemma summable_0_powser: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

834 
"summable (\<lambda>n. f n * 0 ^ n :: 'a :: real_normed_div_algebra)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

835 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

836 
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

837 
by (intro ext) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

838 
thus ?thesis by (subst A) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

839 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

840 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

841 
lemma summable_powser_split_head: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

842 
"summable (\<lambda>n. f (Suc n) * z ^ n :: 'a :: real_normed_div_algebra) = summable (\<lambda>n. f n * z ^ n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

843 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

844 
have "summable (\<lambda>n. f (Suc n) * z ^ n) \<longleftrightarrow> summable (\<lambda>n. f (Suc n) * z ^ Suc n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

845 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

846 
assume "summable (\<lambda>n. f (Suc n) * z ^ 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

847 
from summable_mult2[OF this, of z] show "summable (\<lambda>n. f (Suc n) * z ^ Suc n)" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

848 
by (simp add: power_commutes algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

849 
next 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

850 
assume "summable (\<lambda>n. f (Suc n) * z ^ Suc n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

851 
from summable_mult2[OF this, of "inverse z"] show "summable (\<lambda>n. f (Suc n) * z ^ n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

852 
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

853 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

854 
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

855 
finally show ?thesis . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

856 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

857 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

858 
lemma powser_split_head: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

859 
assumes "summable (\<lambda>n. f n * z ^ n :: 'a :: {real_normed_div_algebra,banach})" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

860 
shows "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

861 
"suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n)  f 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

862 
"summable (\<lambda>n. f (Suc n) * z ^ n)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

863 
proof  
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

864 
from assms show "summable (\<lambda>n. f (Suc n) * z ^ n)" by (subst summable_powser_split_head) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

865 

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

866 
from suminf_mult2[OF this, of z] 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

867 
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

868 
by (simp add: power_commutes algebra_simps) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

869 
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

870 
by (subst suminf_split_head) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

871 
finally show "suminf (\<lambda>n. f n * z ^ n) = f 0 + suminf (\<lambda>n. f (Suc n) * z ^ n) * z" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

872 
thus "suminf (\<lambda>n. f (Suc n) * z ^ n) * z = suminf (\<lambda>n. f n * z ^ n)  f 0" by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

873 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

874 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

875 
lemma summable_partial_sum_bound: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

876 
fixes f :: "nat \<Rightarrow> 'a :: banach" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

877 
assumes summable: "summable f" and e: "e > (0::real)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

878 
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

879 
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

880 
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

881 
by (simp add: Cauchy_convergent_iff summable_iff_convergent) 
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

882 
from CauchyD[OF this e] obtain N 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

883 
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" by blast 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

884 
{ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

885 
fix m n :: nat assume m: "m \<ge> N" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

886 
have "norm (\<Sum>k=m..n. f k) < e" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

887 
proof (cases "n \<ge> m") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

888 
assume n: "n \<ge> m" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

889 
with m have "norm ((\<Sum>k<Suc n. f k)  (\<Sum>k<m. f k)) < e" by (intro N) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

890 
also from n have "(\<Sum>k<Suc n. f k)  (\<Sum>k<m. f k) = (\<Sum>k=m..n. f k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

891 
by (subst setsum_diff [symmetric]) (simp_all add: setsum_last_plus) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

892 
finally show ?thesis . 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

893 
qed (insert e, simp_all) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

894 
} 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

895 
thus ?thesis by (rule that) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

896 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

897 

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

898 
lemma powser_sums_if: 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

899 
"(\<lambda>n. (if n = m then (1 :: 'a :: {ring_1,topological_space}) else 0) * z^n) sums z^m" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

900 
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

901 
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

902 
by (intro ext) auto 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

903 
thus ?thesis by (simp add: sums_single) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

904 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

905 

59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

906 
lemma 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

907 
fixes f :: "nat \<Rightarrow> real" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

908 
assumes "summable f" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

909 
and "inj g" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

910 
and pos: "!!x. 0 \<le> f x" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

911 
shows summable_reindex: "summable (f o g)" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

912 
and suminf_reindex_mono: "suminf (f o g) \<le> suminf f" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

913 
and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

914 
proof  
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

915 
from \<open>inj g\<close> have [simp]: "\<And>A. inj_on g A" by(rule subset_inj_on) simp 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

916 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

917 
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

918 
proof 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

919 
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

920 
have "\<forall> n' \<in> (g ` {..<n}). n' < Suc (Max (g ` {..<n}))" 
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

921 
by(metis Max_ge finite_imageI finite_lessThan not_le not_less_eq) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

922 
then obtain m where n: "\<And>n'. n' < n \<Longrightarrow> g n' < m" by blast 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

923 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

924 
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

925 
by (simp add: setsum.reindex) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

926 
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

927 
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

928 
also have "\<dots> \<le> suminf f" 
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

929 
using \<open>summable f\<close> 
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

930 
by (rule setsum_le_suminf) (simp add: pos) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

931 
finally show "(\<Sum>i<n. (f \<circ> g) i) \<le> suminf f" by simp 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

932 
qed 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

933 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

934 
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

935 
by (rule incseq_SucI) (auto simp add: pos) 
61969  936 
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

937 
using smaller by(rule incseq_convergent) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

938 
hence "(f \<circ> g) sums L" by (simp add: sums_def) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

939 
thus "summable (f o g)" by (auto simp add: sums_iff) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

940 

61969  941 
hence "(\<lambda>n. \<Sum>i<n. (f \<circ> g) i) \<longlonglongrightarrow> suminf (f \<circ> g)" 
59025
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

942 
by(rule summable_LIMSEQ) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

943 
thus le: "suminf (f \<circ> g) \<le> suminf f" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

944 
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

945 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

946 
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

947 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

948 
from \<open>summable f\<close> have "suminf f \<le> suminf (f \<circ> g)" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

949 
proof(rule suminf_le_const) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

950 
fix n 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

951 
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

952 
by(auto intro: Max_ge simp add: finite_vimageI less_Suc_eq_le) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

953 
then obtain m where n: "\<And>n'. g n' < n \<Longrightarrow> n' < m" by blast 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

954 

d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

955 
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

956 
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

957 
also have "\<dots> = (\<Sum>i\<in>g ` {..<n}. (f \<circ> g) i)" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

958 
by(rule setsum.reindex_cong[where l=g])(auto) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

959 
also have "\<dots> \<le> (\<Sum>i<m. (f \<circ> g) i)" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

960 
by(rule setsum_mono3)(auto simp add: pos n) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

961 
also have "\<dots> \<le> suminf (f \<circ> g)" 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

962 
using \<open>summable (f o g)\<close> 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

963 
by(rule setsum_le_suminf)(simp add: pos) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

964 
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

965 
qed 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

966 
with le show "suminf (f \<circ> g) = suminf f" by(rule antisym) 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

967 
qed 
d885cff91200
add lemma following a proof suggestion by Joachim Breitner
Andreas Lochbihler
parents:
59000
diff
changeset

968 

61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

969 
lemma sums_mono_reindex: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

970 
assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

971 
shows "(\<lambda>n. f (g n)) sums c \<longleftrightarrow> f sums c" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

972 
unfolding sums_def 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

973 
proof 
61969  974 
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

975 
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

976 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

977 
fix n :: nat 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

978 
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

979 
by (subst setsum.reindex) (auto intro: subseq_imp_inj_on) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

980 
also from subseq have "\<dots> = (\<Sum>k<g n. f k)" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

981 
by (intro setsum.mono_neutral_left ballI zero) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

982 
(auto dest: subseq_strict_mono simp: strict_mono_less strict_mono_less_eq) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

983 
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

984 
qed 
61969  985 
also from LIMSEQ_subseq_LIMSEQ[OF lim subseq] have "\<dots> \<longlonglongrightarrow> c" unfolding o_def . 
986 
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

987 
next 
61969  988 
assume lim: "(\<lambda>n. \<Sum>k<n. f (g k)) \<longlonglongrightarrow> c" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

989 
def g_inv \<equiv> "\<lambda>n. LEAST m. g m \<ge> n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

990 
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

991 
by (auto simp: filterlim_at_top eventually_at_top_linorder) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

992 
hence g_inv: "g (g_inv n) \<ge> n" for n unfolding g_inv_def by (rule LeastI_ex) 
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

993 
have g_inv_least: "m \<ge> g_inv n" if "g m \<ge> n" for m n using that 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

994 
unfolding g_inv_def by (rule Least_le) 
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

995 
have g_inv_least': "g m < n" if "m < g_inv n" for m n using that g_inv_least[of n m] by linarith 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

996 
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

997 
proof 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

998 
fix n :: nat 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

999 
{ 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1000 
fix k assume k: "k \<in> {..<n}  g`{..<g_inv n}" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1001 
have "k \<notin> range g" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1002 
proof (rule notI, elim imageE) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1003 
fix l assume l: "k = g l" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1004 
have "g l < g (g_inv n)" by (rule less_le_trans[OF _ g_inv]) (insert k l, simp_all) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1005 
with subseq have "l < g_inv n" by (simp add: subseq_strict_mono strict_mono_less) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1006 
with k l show False by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1007 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1008 
hence "f k = 0" by (rule zero) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1009 
} 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1010 
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

1011 
by (intro setsum.mono_neutral_right) auto 
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

1012 
also from subseq have "\<dots> = (\<Sum>k<g_inv n. f (g k))" using subseq_imp_inj_on 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1013 
by (subst setsum.reindex) simp_all 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1014 
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

1015 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1016 
also { 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1017 
fix K n :: nat assume "g K \<le> n" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1018 
also have "n \<le> g (g_inv n)" by (rule g_inv) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1019 
finally have "K \<le> g_inv n" using subseq by (simp add: strict_mono_less_eq subseq_strict_mono) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1020 
} 
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

1021 
hence "filterlim g_inv at_top sequentially" 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1022 
by (auto simp: filterlim_at_top eventually_at_top_linorder) 
61969  1023 
from lim and this have "(\<lambda>n. \<Sum>k<g_inv n. f (g k)) \<longlonglongrightarrow> c" by (rule filterlim_compose) 
1024 
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

1025 
qed 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1026 

ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1027 
lemma summable_mono_reindex: 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1028 
assumes subseq: "subseq g" and zero: "\<And>n. n \<notin> range g \<Longrightarrow> f n = 0" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1029 
shows "summable (\<lambda>n. f (g n)) \<longleftrightarrow> summable f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1030 
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

1031 

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 
lemma suminf_mono_reindex: 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1033 
assumes "subseq g" "\<And>n. n \<notin> range g \<Longrightarrow> f n = (0 :: 'a :: {t2_space,comm_monoid_add})" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1034 
shows "suminf (\<lambda>n. f (g n)) = suminf f" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1035 
proof (cases "summable f") 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1036 
case False 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1037 
hence "\<not>(\<exists>c. f sums c)" unfolding summable_def by blast 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1038 
hence "suminf f = The (\<lambda>_. False)" by (simp add: suminf_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1039 
moreover from False have "\<not>summable (\<lambda>n. f (g n))" 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1040 
using summable_mono_reindex[of g f, OF assms] by simp 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1041 
hence "\<not>(\<exists>c. (\<lambda>n. f (g n)) sums c)" unfolding summable_def by blast 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1042 
hence "suminf (\<lambda>n. f (g n)) = The (\<lambda>_. False)" by (simp add: suminf_def) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1043 
ultimately show ?thesis by simp 
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

1044 
qed (insert sums_mono_reindex[of g f, OF assms] summable_mono_reindex[of g f, OF assms], 
61531
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1045 
simp_all add: sums_iff) 
ab2e862263e7
Rounding function, uniform limits, cotangent, binomial identities
eberlm
parents:
60867
diff
changeset

1046 

14416  1047 
end 