src/HOL/Series.thy
 changeset 56213 e5720d3c18f0 parent 56194 9ffbb4004c81 child 56217 dc429a5b13c4
```     1.1 --- a/src/HOL/Series.thy	Tue Mar 18 22:11:46 2014 +0100
1.2 +++ b/src/HOL/Series.thy	Wed Mar 19 15:34:57 2014 +0100
1.3 @@ -7,12 +7,14 @@
1.5  *)
1.6
1.7 -header {* Finite Summation and Infinite Series *}
1.8 +header {* Infinite Series *}
1.9
1.10  theory Series
1.11  imports Limits
1.12  begin
1.13
1.14 +subsection {* Definition of infinite summability *}
1.15 +
1.16  definition
1.17    sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
1.18    (infixr "sums" 80)
1.19 @@ -28,6 +30,8 @@
1.20  where
1.21    "suminf f = (THE s. f sums s)"
1.22
1.23 +subsection {* Infinite summability on topological monoids *}
1.24 +
1.25  lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
1.26    by simp
1.27
1.28 @@ -40,6 +44,24 @@
1.29  lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
1.30    by (simp add: suminf_def sums_def lim_def)
1.31
1.32 +lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
1.33 +  unfolding sums_def by (simp add: tendsto_const)
1.34 +
1.35 +lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
1.36 +  by (rule sums_zero [THEN sums_summable])
1.37 +
1.38 +lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
1.39 +  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
1.40 +  apply safe
1.41 +  apply (erule_tac x=S in allE)
1.42 +  apply safe
1.43 +  apply (rule_tac x="N" in exI, safe)
1.44 +  apply (drule_tac x="n*k" in spec)
1.45 +  apply (erule mp)
1.46 +  apply (erule order_trans)
1.47 +  apply simp
1.48 +  done
1.49 +
1.50  lemma sums_finite:
1.51    assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
1.52    shows "f sums (\<Sum>n\<in>N. f n)"
1.53 @@ -65,36 +87,26 @@
1.55  qed
1.56
1.57 +lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
1.58 +  by (rule sums_summable) (rule sums_finite)
1.59 +
1.60  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)"
1.61    using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
1.62
1.63 +lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)"
1.64 +  by (rule sums_summable) (rule sums_If_finite_set)
1.65 +
1.66  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)"
1.67    using sums_If_finite_set[of "{r. P r}"] by simp
1.68
1.69 +lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)"
1.70 +  by (rule sums_summable) (rule sums_If_finite)
1.71 +
1.72  lemma sums_single: "(\<lambda>r. if r = i then f r else 0) sums f i"
1.73    using sums_If_finite[of "\<lambda>r. r = i"] by simp
1.74
1.75 -lemma series_zero: (* REMOVE *)
1.76 -  "(\<And>m. n \<le> m \<Longrightarrow> f m = 0) \<Longrightarrow> f sums (\<Sum>i<n. f i)"
1.77 -  by (rule sums_finite) auto
1.78 -
1.79 -lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
1.80 -  unfolding sums_def by (simp add: tendsto_const)
1.81 -
1.82 -lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
1.83 -  by (rule sums_zero [THEN sums_summable])
1.84 -
1.85 -lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
1.86 -  apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
1.87 -  apply safe
1.88 -  apply (erule_tac x=S in allE)
1.89 -  apply safe
1.90 -  apply (rule_tac x="N" in exI, safe)
1.91 -  apply (drule_tac x="n*k" in spec)
1.92 -  apply (erule mp)
1.93 -  apply (erule order_trans)
1.94 -  apply simp
1.95 -  done
1.96 +lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)"
1.97 +  by (rule sums_summable) (rule sums_single)
1.98
1.99  context
1.100    fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
1.101 @@ -123,26 +135,53 @@
1.102  lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0"
1.103    by (rule sums_zero [THEN sums_unique, symmetric])
1.104
1.105 +
1.106 +subsection {* Infinite summability on ordered, topological monoids *}
1.107 +
1.108 +lemma sums_le:
1.109 +  fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
1.110 +  shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
1.111 +  by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
1.112 +
1.113  context
1.114    fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
1.115  begin
1.116
1.117 -lemma series_pos_le: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
1.118 -  apply (rule LIMSEQ_le_const[OF summable_LIMSEQ])
1.119 -  apply assumption
1.120 -  apply (intro exI[of _ n])
1.121 -  apply (auto intro!: setsum_mono2 simp: not_le[symmetric])
1.122 -  done
1.123 +lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
1.124 +  by (auto dest: sums_summable intro: sums_le)
1.125 +
1.126 +lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
1.127 +  by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
1.128 +
1.129 +lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
1.130 +  using setsum_le_suminf[of 0] by simp
1.131 +
1.132 +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"
1.133 +  using
1.134 +    setsum_le_suminf[of "Suc i"]
1.135 +    add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
1.136 +    setsum_mono2[of "{..<i}" "{..<n}" f]
1.137 +  by (auto simp: less_imp_le ac_simps)
1.138 +
1.139 +lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
1.140 +  using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
1.141 +
1.142 +lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
1.143 +  using setsum_less_suminf2[of 0 i] by simp
1.144 +
1.145 +lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
1.146 +  using suminf_pos2[of 0] by (simp add: less_imp_le)
1.147 +
1.148 +lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
1.149 +  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
1.150
1.151  lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
1.152  proof
1.153    assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
1.154 -  then have "f sums 0"
1.155 -    by (simp add: sums_iff)
1.156    then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
1.157 -    by (simp add: sums_def atLeast0LessThan)
1.158 -  have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
1.159 -  proof (rule LIMSEQ_le_const[OF f])
1.160 +    using summable_LIMSEQ[of f] by simp
1.161 +  then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
1.162 +  proof (rule LIMSEQ_le_const)
1.163      fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
1.164        using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
1.165    qed
1.166 @@ -150,33 +189,34 @@
1.167      by (auto intro!: antisym)
1.168  qed (metis suminf_zero fun_eq_iff)
1.169
1.170 -lemma suminf_gt_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
1.171 -  using series_pos_le[of 0] suminf_eq_zero_iff by (simp add: less_le)
1.172 -
1.173 -lemma suminf_gt_zero: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
1.174 -  using suminf_gt_zero_iff by (simp add: less_imp_le)
1.175 -
1.176 -lemma suminf_ge_zero: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
1.177 -  by (drule_tac n="0" in series_pos_le) simp_all
1.178 -
1.179 -lemma suminf_le: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
1.180 -  by (metis LIMSEQ_le_const2 summable_LIMSEQ)
1.181 -
1.182 -lemma summable_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
1.183 -  by (rule LIMSEQ_le) (auto intro: setsum_mono summable_LIMSEQ)
1.184 +lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
1.185 +  using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
1.186
1.187  end
1.188
1.189 -lemma series_pos_less:
1.191 -  shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {..<n} < suminf f"
1.192 -  apply simp
1.193 -  apply (rule_tac y="setsum f {..<Suc n}" in order_less_le_trans)
1.194 -  using add_less_cancel_left [of "setsum f {..<n}" 0 "f n"]
1.195 -  apply simp
1.196 -  apply (erule series_pos_le)
1.197 -  apply (simp add: order_less_imp_le)
1.198 -  done
1.199 +lemma summableI_nonneg_bounded:
1.200 +  fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}"
1.201 +  assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
1.202 +  shows "summable f"
1.203 +  unfolding summable_def sums_def[abs_def]
1.204 +proof (intro exI order_tendstoI)
1.205 +  have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
1.206 +    using le by (auto simp: bdd_above_def)
1.207 +  { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
1.208 +    then obtain n where "a < (\<Sum>i<n. f i)"
1.209 +      by (auto simp add: less_cSUP_iff)
1.210 +    then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
1.211 +      by (rule less_le_trans) (auto intro!: setsum_mono2)
1.212 +    then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
1.213 +      by (auto simp: eventually_sequentially) }
1.214 +  { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
1.215 +    moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
1.216 +      by (auto intro: cSUP_upper)
1.217 +    ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
1.218 +      by (auto intro: le_less_trans simp: eventually_sequentially) }
1.219 +qed
1.220 +
1.221 +subsection {* Infinite summability on real normed vector spaces *}
1.222
1.223  lemma sums_Suc_iff:
1.224    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
1.225 @@ -289,6 +329,8 @@
1.226  lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
1.227  lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
1.228
1.229 +subsection {* Infinite summability on real normed algebras *}
1.230 +
1.231  context
1.232    fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra"
1.233  begin
1.234 @@ -313,6 +355,8 @@
1.235
1.236  end
1.237
1.238 +subsection {* Infinite summability on real normed fields *}
1.239 +
1.240  context
1.241    fixes c :: "'a::real_normed_field"
1.242  begin
1.243 @@ -361,6 +405,8 @@
1.244      by simp
1.245  qed
1.246
1.247 +subsection {* Infinite summability on Banach spaces *}
1.248 +
1.249  text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
1.250
1.251  lemma summable_Cauchy:
1.252 @@ -452,12 +498,6 @@
1.253
1.254  end
1.255
1.256 -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))"
1.257 -  by (rule summable_comparison_test) auto
1.258 -
1.259 -lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
1.260 -  by (rule summable_norm_cancel) simp
1.261 -
1.262  text{*Summability of geometric series for real algebras*}
1.263
1.264  lemma complete_algebra_summable_geometric:
1.265 @@ -470,34 +510,6 @@
1.267  qed
1.268
1.269 -
1.270 -text{*A summable series of positive terms has limit that is at least as
1.271 -great as any partial sum.*}
1.272 -
1.273 -lemma pos_summable:
1.274 -  fixes f:: "nat \<Rightarrow> real"
1.275 -  assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {..<n} \<le> x"
1.276 -  shows "summable f"
1.277 -proof -
1.278 -  have "convergent (\<lambda>n. setsum f {..<n})"
1.279 -  proof (rule Bseq_mono_convergent)
1.280 -    show "Bseq (\<lambda>n. setsum f {..<n})"
1.281 -      by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
1.282 -  qed (auto intro: setsum_mono2 pos)
1.283 -  thus ?thesis
1.284 -    by (force simp add: summable_def sums_def convergent_def)
1.285 -qed
1.286 -
1.287 -lemma summable_rabs_comparison_test:
1.288 -  fixes f :: "nat \<Rightarrow> real"
1.289 -  shows "\<lbrakk>\<exists>N. \<forall>n\<ge>N. \<bar>f n\<bar> \<le> g n; summable g\<rbrakk> \<Longrightarrow> summable (\<lambda>n. \<bar>f n\<bar>)"
1.290 -  by (rule summable_comparison_test) auto
1.291 -
1.292 -lemma summable_rabs:
1.293 -  fixes f :: "nat \<Rightarrow> real"
1.294 -  shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
1.295 -by (fold real_norm_def, rule summable_norm)
1.296 -
1.297  subsection {* Cauchy Product Formula *}
1.298
1.299  text {*
1.300 @@ -507,14 +519,14 @@
1.301
1.302  lemma setsum_triangle_reindex:
1.303    fixes n :: nat
1.304 -  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i=0..k. f i (k - i))"
1.305 +  shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
1.306  proof -
1.307    have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
1.308 -    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {0..k}). f i (k - i))"
1.309 +    (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
1.310    proof (rule setsum_reindex_cong)
1.311 -    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {0..k})"
1.312 +    show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
1.313        by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
1.314 -    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {0..k})"
1.315 +    show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
1.316        by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
1.317      show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
1.318        by clarify
1.319 @@ -526,7 +538,7 @@
1.320    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
1.321    assumes a: "summable (\<lambda>k. norm (a k))"
1.322    assumes b: "summable (\<lambda>k. norm (b k))"
1.323 -  shows "(\<lambda>k. \<Sum>i=0..k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
1.324 +  shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
1.325  proof -
1.326    let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}"
1.327    let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}"
1.328 @@ -598,8 +610,22 @@
1.329    fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
1.330    assumes a: "summable (\<lambda>k. norm (a k))"
1.331    assumes b: "summable (\<lambda>k. norm (b k))"
1.332 -  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
1.333 -using a b
1.334 -by (rule Cauchy_product_sums [THEN sums_unique])
1.335 +  shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))"
1.336 +  using a b
1.337 +  by (rule Cauchy_product_sums [THEN sums_unique])
1.338 +
1.339 +subsection {* Series on @{typ real}s *}
1.340 +
1.341 +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))"
1.342 +  by (rule summable_comparison_test) auto
1.343 +
1.344 +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>)"
1.345 +  by (rule summable_comparison_test) auto
1.346 +
1.347 +lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
1.348 +  by (rule summable_norm_cancel) simp
1.349 +
1.350 +lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
1.351 +  by (fold real_norm_def) (rule summable_norm)
1.352
1.353  end
```