src/HOL/Series.thy
changeset 62368 106569399cd6
parent 62217 527488dc8b90
child 62376 85f38d5f8807
     1.1 --- a/src/HOL/Series.thy	Mon Feb 08 17:18:13 2016 +0100
     1.2 +++ b/src/HOL/Series.thy	Mon Feb 08 19:53:49 2016 +0100
     1.3 @@ -271,12 +271,59 @@
     1.4        by (auto intro: le_less_trans simp: eventually_sequentially) }
     1.5  qed
     1.6  
     1.7 +subsection \<open>Infinite summability on topological monoids\<close>
     1.8 +
     1.9 +lemma Zero_notin_Suc: "0 \<notin> Suc ` A"
    1.10 +  by auto
    1.11 +
    1.12 +context
    1.13 +  fixes f g :: "nat \<Rightarrow> 'a :: {t2_space, topological_comm_monoid_add}"
    1.14 +begin
    1.15 +
    1.16 +lemma sums_Suc:
    1.17 +  assumes "(\<lambda>n. f (Suc n)) sums l" shows "f sums (l + f 0)"
    1.18 +proof  -
    1.19 +  have "(\<lambda>n. (\<Sum>i<n. f (Suc i)) + f 0) \<longlonglongrightarrow> l + f 0"
    1.20 +    using assms by (auto intro!: tendsto_add simp: sums_def)
    1.21 +  moreover have "(\<Sum>i<n. f (Suc i)) + f 0 = (\<Sum>i<Suc n. f i)" for n
    1.22 +    unfolding lessThan_Suc_eq_insert_0 by (simp add: Zero_notin_Suc ac_simps setsum.reindex)
    1.23 +  ultimately show ?thesis
    1.24 +    by (auto simp add: sums_def simp del: setsum_lessThan_Suc intro: LIMSEQ_Suc_iff[THEN iffD1])
    1.25 +qed
    1.26 +
    1.27 +lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
    1.28 +  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
    1.29 +
    1.30 +lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
    1.31 +  unfolding summable_def by (auto intro: sums_add)
    1.32 +
    1.33 +lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
    1.34 +  by (intro sums_unique sums_add summable_sums)
    1.35 +
    1.36 +end
    1.37 +
    1.38 +context
    1.39 +  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::{t2_space, topological_comm_monoid_add}" and I :: "'i set"
    1.40 +begin
    1.41 +
    1.42 +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)"
    1.43 +  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
    1.44 +
    1.45 +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)"
    1.46 +  using sums_unique[OF sums_setsum, OF summable_sums] by simp
    1.47 +
    1.48 +lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
    1.49 +  using sums_summable[OF sums_setsum[OF summable_sums]] .
    1.50 +
    1.51 +end
    1.52  
    1.53  subsection \<open>Infinite summability on real normed vector spaces\<close>
    1.54  
    1.55 -lemma sums_Suc_iff:
    1.56 +context
    1.57    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.58 -  shows "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
    1.59 +begin
    1.60 +
    1.61 +lemma sums_Suc_iff: "(\<lambda>n. f (Suc n)) sums s \<longleftrightarrow> f sums (s + f 0)"
    1.62  proof -
    1.63    have "f sums (s + f 0) \<longleftrightarrow> (\<lambda>i. \<Sum>j<Suc i. f j) \<longlonglongrightarrow> s + f 0"
    1.64      by (subst LIMSEQ_Suc_iff) (simp add: sums_def)
    1.65 @@ -292,7 +339,7 @@
    1.66    finally show ?thesis ..
    1.67  qed
    1.68  
    1.69 -lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n) :: 'a :: real_normed_vector) = summable f"
    1.70 +lemma summable_Suc_iff: "summable (\<lambda>n. f (Suc n)) = summable f"
    1.71  proof
    1.72    assume "summable f"
    1.73    hence "f sums suminf f" by (rule summable_sums)
    1.74 @@ -300,19 +347,12 @@
    1.75    thus "summable (\<lambda>n. f (Suc n))" unfolding summable_def by blast
    1.76  qed (auto simp: sums_Suc_iff summable_def)
    1.77  
    1.78 +end
    1.79 +
    1.80  context
    1.81    fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
    1.82  begin
    1.83  
    1.84 -lemma sums_add: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n + g n) sums (a + b)"
    1.85 -  unfolding sums_def by (simp add: setsum.distrib tendsto_add)
    1.86 -
    1.87 -lemma summable_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> summable (\<lambda>n. f n + g n)"
    1.88 -  unfolding summable_def by (auto intro: sums_add)
    1.89 -
    1.90 -lemma suminf_add: "summable f \<Longrightarrow> summable g \<Longrightarrow> suminf f + suminf g = (\<Sum>n. f n + g n)"
    1.91 -  by (intro sums_unique sums_add summable_sums)
    1.92 -
    1.93  lemma sums_diff: "f sums a \<Longrightarrow> g sums b \<Longrightarrow> (\<lambda>n. f n - g n) sums (a - b)"
    1.94    unfolding sums_def by (simp add: setsum_subtractf tendsto_diff)
    1.95  
    1.96 @@ -331,9 +371,6 @@
    1.97  lemma suminf_minus: "summable f \<Longrightarrow> (\<Sum>n. - f n) = - (\<Sum>n. f n)"
    1.98    by (intro sums_unique [symmetric] sums_minus summable_sums)
    1.99  
   1.100 -lemma sums_Suc: "(\<lambda> n. f (Suc n)) sums l \<Longrightarrow> f sums (l + f 0)"
   1.101 -  by (simp add: sums_Suc_iff)
   1.102 -
   1.103  lemma sums_iff_shift: "(\<lambda>i. f (i + n)) sums s \<longleftrightarrow> f sums (s + (\<Sum>i<n. f i))"
   1.104  proof (induct n arbitrary: s)
   1.105    case (Suc n)
   1.106 @@ -381,12 +418,10 @@
   1.107    apply (drule_tac x="n" in spec, simp)
   1.108    done
   1.109  
   1.110 -lemma summable_imp_convergent:
   1.111 -  "summable (f :: nat \<Rightarrow> 'a) \<Longrightarrow> convergent f"
   1.112 +lemma summable_imp_convergent: "summable f \<Longrightarrow> convergent f"
   1.113    by (force dest!: summable_LIMSEQ_zero simp: convergent_def)
   1.114  
   1.115 -lemma summable_imp_Bseq:
   1.116 -  "summable f \<Longrightarrow> Bseq (f :: nat \<Rightarrow> 'a :: real_normed_vector)"
   1.117 +lemma summable_imp_Bseq: "summable f \<Longrightarrow> Bseq f"
   1.118    by (simp add: convergent_imp_Bseq summable_imp_convergent)
   1.119  
   1.120  end
   1.121 @@ -396,22 +431,6 @@
   1.122    shows "summable (\<lambda>n. - f n) \<longleftrightarrow> summable f"
   1.123    by (auto dest: summable_minus) \<comment>\<open>used two ways, hence must be outside the context above\<close>
   1.124  
   1.125 -
   1.126 -context
   1.127 -  fixes f :: "'i \<Rightarrow> nat \<Rightarrow> 'a::real_normed_vector" and I :: "'i set"
   1.128 -begin
   1.129 -
   1.130 -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)"
   1.131 -  by (induct I rule: infinite_finite_induct) (auto intro!: sums_add)
   1.132 -
   1.133 -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)"
   1.134 -  using sums_unique[OF sums_setsum, OF summable_sums] by simp
   1.135 -
   1.136 -lemma summable_setsum: "(\<And>i. i \<in> I \<Longrightarrow> summable (f i)) \<Longrightarrow> summable (\<lambda>n. \<Sum>i\<in>I. f i n)"
   1.137 -  using sums_summable[OF sums_setsum[OF summable_sums]] .
   1.138 -
   1.139 -end
   1.140 -
   1.141  lemma (in bounded_linear) sums: "(\<lambda>n. X n) sums a \<Longrightarrow> (\<lambda>n. f (X n)) sums (f a)"
   1.142    unfolding sums_def by (drule tendsto, simp only: setsum)
   1.143  
   1.144 @@ -923,7 +942,7 @@
   1.145     fixes f :: "nat \<Rightarrow> real"
   1.146     assumes "summable f"
   1.147     and "inj g"
   1.148 -   and pos: "!!x. 0 \<le> f x"
   1.149 +   and pos: "\<And>x. 0 \<le> f x"
   1.150     shows summable_reindex: "summable (f o g)"
   1.151     and suminf_reindex_mono: "suminf (f o g) \<le> suminf f"
   1.152     and suminf_reindex: "(\<And>x. x \<notin> range g \<Longrightarrow> f x = 0) \<Longrightarrow> suminf (f \<circ> g) = suminf f"