--- a/src/HOL/Probability/Lebesgue_Integration.thy Tue Mar 18 22:11:46 2014 +0100
+++ b/src/HOL/Probability/Lebesgue_Integration.thy Wed Mar 19 15:34:57 2014 +0100
@@ -2239,7 +2239,7 @@
proof eventually_elim
fix j x assume [simp]: "x \<in> space M"
have "\<bar>\<Sum>i<j. f i x\<bar> \<le> (\<Sum>i<j. \<bar>f i x\<bar>)" by (rule setsum_abs)
- also have "\<dots> \<le> w x" using w[of x] series_pos_le[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
+ also have "\<dots> \<le> w x" using w[of x] setsum_le_suminf[of "\<lambda>i. \<bar>f i x\<bar>"] unfolding sums_iff by auto
finally show "\<bar>\<Sum>i<j. f i x\<bar> \<le> ?w x" by simp
qed
--- a/src/HOL/Series.thy Tue Mar 18 22:11:46 2014 +0100
+++ b/src/HOL/Series.thy Wed Mar 19 15:34:57 2014 +0100
@@ -7,12 +7,14 @@
Additional contributions by Jeremy Avigad
*)
-header {* Finite Summation and Infinite Series *}
+header {* Infinite Series *}
theory Series
imports Limits
begin
+subsection {* Definition of infinite summability *}
+
definition
sums :: "(nat \<Rightarrow> 'a::{topological_space, comm_monoid_add}) \<Rightarrow> 'a \<Rightarrow> bool"
(infixr "sums" 80)
@@ -28,6 +30,8 @@
where
"suminf f = (THE s. f sums s)"
+subsection {* Infinite summability on topological monoids *}
+
lemma sums_subst[trans]: "f = g \<Longrightarrow> g sums z \<Longrightarrow> f sums z"
by simp
@@ -40,6 +44,24 @@
lemma suminf_eq_lim: "suminf f = lim (\<lambda>n. \<Sum>i<n. f i)"
by (simp add: suminf_def sums_def lim_def)
+lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
+ unfolding sums_def by (simp add: tendsto_const)
+
+lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
+ by (rule sums_zero [THEN sums_summable])
+
+lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
+ apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
+ apply safe
+ apply (erule_tac x=S in allE)
+ apply safe
+ apply (rule_tac x="N" in exI, safe)
+ apply (drule_tac x="n*k" in spec)
+ apply (erule mp)
+ apply (erule order_trans)
+ apply simp
+ done
+
lemma sums_finite:
assumes [simp]: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
shows "f sums (\<Sum>n\<in>N. f n)"
@@ -65,36 +87,26 @@
(simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
qed
+lemma summable_finite: "finite N \<Longrightarrow> (\<And>n. n \<notin> N \<Longrightarrow> f n = 0) \<Longrightarrow> summable f"
+ by (rule sums_summable) (rule sums_finite)
+
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)"
using sums_finite[of A "(\<lambda>r. if r \<in> A then f r else 0)"] by simp
+lemma summable_If_finite_set[simp, intro]: "finite A \<Longrightarrow> summable (\<lambda>r. if r \<in> A then f r else 0)"
+ by (rule sums_summable) (rule sums_If_finite_set)
+
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)"
using sums_If_finite_set[of "{r. P r}"] by simp
+lemma summable_If_finite[simp, intro]: "finite {r. P r} \<Longrightarrow> summable (\<lambda>r. if P r then f r else 0)"
+ by (rule sums_summable) (rule sums_If_finite)
+
lemma sums_single: "(\<lambda>r. if r = i then f r else 0) sums f i"
using sums_If_finite[of "\<lambda>r. r = i"] by simp
-lemma series_zero: (* REMOVE *)
- "(\<And>m. n \<le> m \<Longrightarrow> f m = 0) \<Longrightarrow> f sums (\<Sum>i<n. f i)"
- by (rule sums_finite) auto
-
-lemma sums_zero[simp, intro]: "(\<lambda>n. 0) sums 0"
- unfolding sums_def by (simp add: tendsto_const)
-
-lemma summable_zero[simp, intro]: "summable (\<lambda>n. 0)"
- by (rule sums_zero [THEN sums_summable])
-
-lemma sums_group: "f sums s \<Longrightarrow> 0 < k \<Longrightarrow> (\<lambda>n. setsum f {n * k ..< n * k + k}) sums s"
- apply (simp only: sums_def setsum_nat_group tendsto_def eventually_sequentially)
- apply safe
- apply (erule_tac x=S in allE)
- apply safe
- apply (rule_tac x="N" in exI, safe)
- apply (drule_tac x="n*k" in spec)
- apply (erule mp)
- apply (erule order_trans)
- apply simp
- done
+lemma summable_single[simp, intro]: "summable (\<lambda>r. if r = i then f r else 0)"
+ by (rule sums_summable) (rule sums_single)
context
fixes f :: "nat \<Rightarrow> 'a::{t2_space, comm_monoid_add}"
@@ -123,26 +135,53 @@
lemma suminf_zero[simp]: "suminf (\<lambda>n. 0::'a::{t2_space, comm_monoid_add}) = 0"
by (rule sums_zero [THEN sums_unique, symmetric])
+
+subsection {* Infinite summability on ordered, topological monoids *}
+
+lemma sums_le:
+ fixes f g :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
+ shows "\<forall>n. f n \<le> g n \<Longrightarrow> f sums s \<Longrightarrow> g sums t \<Longrightarrow> s \<le> t"
+ by (rule LIMSEQ_le) (auto intro: setsum_mono simp: sums_def)
+
context
fixes f :: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology}"
begin
-lemma series_pos_le: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
- apply (rule LIMSEQ_le_const[OF summable_LIMSEQ])
- apply assumption
- apply (intro exI[of _ n])
- apply (auto intro!: setsum_mono2 simp: not_le[symmetric])
- done
+lemma suminf_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
+ by (auto dest: sums_summable intro: sums_le)
+
+lemma setsum_le_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 \<le> f m \<Longrightarrow> setsum f {..<n} \<le> suminf f"
+ by (rule sums_le[OF _ sums_If_finite_set summable_sums]) auto
+
+lemma suminf_nonneg: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
+ using setsum_le_suminf[of 0] by simp
+
+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"
+ using
+ setsum_le_suminf[of "Suc i"]
+ add_strict_increasing[of "f i" "setsum f {..<n}" "setsum f {..<i}"]
+ setsum_mono2[of "{..<i}" "{..<n}" f]
+ by (auto simp: less_imp_le ac_simps)
+
+lemma setsum_less_suminf: "summable f \<Longrightarrow> \<forall>m\<ge>n. 0 < f m \<Longrightarrow> setsum f {..<n} < suminf f"
+ using setsum_less_suminf2[of n n] by (simp add: less_imp_le)
+
+lemma suminf_pos2: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < f i \<Longrightarrow> 0 < suminf f"
+ using setsum_less_suminf2[of 0 i] by simp
+
+lemma suminf_pos: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
+ using suminf_pos2[of 0] by (simp add: less_imp_le)
+
+lemma suminf_le_const: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
+ by (metis LIMSEQ_le_const2 summable_LIMSEQ)
lemma suminf_eq_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> suminf f = 0 \<longleftrightarrow> (\<forall>n. f n = 0)"
proof
assume "summable f" "suminf f = 0" and pos: "\<forall>n. 0 \<le> f n"
- then have "f sums 0"
- by (simp add: sums_iff)
then have f: "(\<lambda>n. \<Sum>i<n. f i) ----> 0"
- by (simp add: sums_def atLeast0LessThan)
- have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
- proof (rule LIMSEQ_le_const[OF f])
+ using summable_LIMSEQ[of f] by simp
+ then have "\<And>i. (\<Sum>n\<in>{i}. f n) \<le> 0"
+ proof (rule LIMSEQ_le_const)
fix i show "\<exists>N. \<forall>n\<ge>N. (\<Sum>n\<in>{i}. f n) \<le> setsum f {..<n}"
using pos by (intro exI[of _ "Suc i"] allI impI setsum_mono2) auto
qed
@@ -150,33 +189,34 @@
by (auto intro!: antisym)
qed (metis suminf_zero fun_eq_iff)
-lemma suminf_gt_zero_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
- using series_pos_le[of 0] suminf_eq_zero_iff by (simp add: less_le)
-
-lemma suminf_gt_zero: "summable f \<Longrightarrow> \<forall>n. 0 < f n \<Longrightarrow> 0 < suminf f"
- using suminf_gt_zero_iff by (simp add: less_imp_le)
-
-lemma suminf_ge_zero: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 \<le> suminf f"
- by (drule_tac n="0" in series_pos_le) simp_all
-
-lemma suminf_le: "summable f \<Longrightarrow> (\<And>n. setsum f {..<n} \<le> x) \<Longrightarrow> suminf f \<le> x"
- by (metis LIMSEQ_le_const2 summable_LIMSEQ)
-
-lemma summable_le: "\<lbrakk>\<forall>n. f n \<le> g n; summable f; summable g\<rbrakk> \<Longrightarrow> suminf f \<le> suminf g"
- by (rule LIMSEQ_le) (auto intro: setsum_mono summable_LIMSEQ)
+lemma suminf_pos_iff: "summable f \<Longrightarrow> \<forall>n. 0 \<le> f n \<Longrightarrow> 0 < suminf f \<longleftrightarrow> (\<exists>i. 0 < f i)"
+ using setsum_le_suminf[of 0] suminf_eq_zero_iff by (simp add: less_le)
end
-lemma series_pos_less:
- fixes f :: "nat \<Rightarrow> 'a::{ordered_ab_semigroup_add_imp_le, ordered_comm_monoid_add, linorder_topology}"
- shows "\<lbrakk>summable f; \<forall>m\<ge>n. 0 < f m\<rbrakk> \<Longrightarrow> setsum f {..<n} < suminf f"
- apply simp
- apply (rule_tac y="setsum f {..<Suc n}" in order_less_le_trans)
- using add_less_cancel_left [of "setsum f {..<n}" 0 "f n"]
- apply simp
- apply (erule series_pos_le)
- apply (simp add: order_less_imp_le)
- done
+lemma summableI_nonneg_bounded:
+ fixes f:: "nat \<Rightarrow> 'a::{ordered_comm_monoid_add, linorder_topology, conditionally_complete_linorder}"
+ assumes pos[simp]: "\<And>n. 0 \<le> f n" and le: "\<And>n. (\<Sum>i<n. f i) \<le> x"
+ shows "summable f"
+ unfolding summable_def sums_def[abs_def]
+proof (intro exI order_tendstoI)
+ have [simp, intro]: "bdd_above (range (\<lambda>n. \<Sum>i<n. f i))"
+ using le by (auto simp: bdd_above_def)
+ { fix a assume "a < (SUP n. \<Sum>i<n. f i)"
+ then obtain n where "a < (\<Sum>i<n. f i)"
+ by (auto simp add: less_cSUP_iff)
+ then have "\<And>m. n \<le> m \<Longrightarrow> a < (\<Sum>i<m. f i)"
+ by (rule less_le_trans) (auto intro!: setsum_mono2)
+ then show "eventually (\<lambda>n. a < (\<Sum>i<n. f i)) sequentially"
+ by (auto simp: eventually_sequentially) }
+ { fix a assume "(SUP n. \<Sum>i<n. f i) < a"
+ moreover have "\<And>n. (\<Sum>i<n. f i) \<le> (SUP n. \<Sum>i<n. f i)"
+ by (auto intro: cSUP_upper)
+ ultimately show "eventually (\<lambda>n. (\<Sum>i<n. f i) < a) sequentially"
+ by (auto intro: le_less_trans simp: eventually_sequentially) }
+qed
+
+subsection {* Infinite summability on real normed vector spaces *}
lemma sums_Suc_iff:
fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
@@ -289,6 +329,8 @@
lemmas summable_of_real = bounded_linear.summable [OF bounded_linear_of_real]
lemmas suminf_of_real = bounded_linear.suminf [OF bounded_linear_of_real]
+subsection {* Infinite summability on real normed algebras *}
+
context
fixes f :: "nat \<Rightarrow> 'a::real_normed_algebra"
begin
@@ -313,6 +355,8 @@
end
+subsection {* Infinite summability on real normed fields *}
+
context
fixes c :: "'a::real_normed_field"
begin
@@ -361,6 +405,8 @@
by simp
qed
+subsection {* Infinite summability on Banach spaces *}
+
text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
lemma summable_Cauchy:
@@ -452,12 +498,6 @@
end
-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))"
- by (rule summable_comparison_test) auto
-
-lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
- by (rule summable_norm_cancel) simp
-
text{*Summability of geometric series for real algebras*}
lemma complete_algebra_summable_geometric:
@@ -470,34 +510,6 @@
by (simp add: summable_geometric)
qed
-
-text{*A summable series of positive terms has limit that is at least as
-great as any partial sum.*}
-
-lemma pos_summable:
- fixes f:: "nat \<Rightarrow> real"
- assumes pos: "\<And>n. 0 \<le> f n" and le: "\<And>n. setsum f {..<n} \<le> x"
- shows "summable f"
-proof -
- have "convergent (\<lambda>n. setsum f {..<n})"
- proof (rule Bseq_mono_convergent)
- show "Bseq (\<lambda>n. setsum f {..<n})"
- by (intro BseqI'[of _ x]) (auto simp add: setsum_nonneg pos intro: le)
- qed (auto intro: setsum_mono2 pos)
- thus ?thesis
- by (force simp add: summable_def sums_def convergent_def)
-qed
-
-lemma summable_rabs_comparison_test:
- fixes f :: "nat \<Rightarrow> real"
- 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>)"
- by (rule summable_comparison_test) auto
-
-lemma summable_rabs:
- fixes f :: "nat \<Rightarrow> real"
- shows "summable (\<lambda>n. \<bar>f n\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
-by (fold real_norm_def, rule summable_norm)
-
subsection {* Cauchy Product Formula *}
text {*
@@ -507,14 +519,14 @@
lemma setsum_triangle_reindex:
fixes n :: nat
- shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i=0..k. f i (k - i))"
+ shows "(\<Sum>(i,j)\<in>{(i,j). i+j < n}. f i j) = (\<Sum>k<n. \<Sum>i\<le>k. f i (k - i))"
proof -
have "(\<Sum>(i, j)\<in>{(i, j). i + j < n}. f i j) =
- (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {0..k}). f i (k - i))"
+ (\<Sum>(k, i)\<in>(SIGMA k:{..<n}. {..k}). f i (k - i))"
proof (rule setsum_reindex_cong)
- show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {0..k})"
+ show "inj_on (\<lambda>(k,i). (i, k - i)) (SIGMA k:{..<n}. {..k})"
by (rule inj_on_inverseI [where g="\<lambda>(i,j). (i+j, i)"], auto)
- show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {0..k})"
+ show "{(i,j). i + j < n} = (\<lambda>(k,i). (i, k - i)) ` (SIGMA k:{..<n}. {..k})"
by (safe, rule_tac x="(a+b,a)" in image_eqI, auto)
show "\<And>a. (\<lambda>(k, i). f i (k - i)) a = split f ((\<lambda>(k, i). (i, k - i)) a)"
by clarify
@@ -526,7 +538,7 @@
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
assumes a: "summable (\<lambda>k. norm (a k))"
assumes b: "summable (\<lambda>k. norm (b k))"
- shows "(\<lambda>k. \<Sum>i=0..k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
+ shows "(\<lambda>k. \<Sum>i\<le>k. a i * b (k - i)) sums ((\<Sum>k. a k) * (\<Sum>k. b k))"
proof -
let ?S1 = "\<lambda>n::nat. {..<n} \<times> {..<n}"
let ?S2 = "\<lambda>n::nat. {(i,j). i + j < n}"
@@ -598,8 +610,22 @@
fixes a b :: "nat \<Rightarrow> 'a::{real_normed_algebra,banach}"
assumes a: "summable (\<lambda>k. norm (a k))"
assumes b: "summable (\<lambda>k. norm (b k))"
- shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i=0..k. a i * b (k - i))"
-using a b
-by (rule Cauchy_product_sums [THEN sums_unique])
+ shows "(\<Sum>k. a k) * (\<Sum>k. b k) = (\<Sum>k. \<Sum>i\<le>k. a i * b (k - i))"
+ using a b
+ by (rule Cauchy_product_sums [THEN sums_unique])
+
+subsection {* Series on @{typ real}s *}
+
+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))"
+ by (rule summable_comparison_test) auto
+
+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>)"
+ by (rule summable_comparison_test) auto
+
+lemma summable_rabs_cancel: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> summable f"
+ by (rule summable_norm_cancel) simp
+
+lemma summable_rabs: "summable (\<lambda>n. \<bar>f n :: real\<bar>) \<Longrightarrow> \<bar>suminf f\<bar> \<le> (\<Sum>n. \<bar>f n\<bar>)"
+ by (fold real_norm_def) (rule summable_norm)
end
--- a/src/HOL/Transcendental.thy Tue Mar 18 22:11:46 2014 +0100
+++ b/src/HOL/Transcendental.thy Wed Mar 19 15:34:57 2014 +0100
@@ -552,7 +552,7 @@
hence "norm (suminf (g h)) \<le> (\<Sum>n. norm (g h n))"
by (rule summable_norm)
also from A C B have "(\<Sum>n. norm (g h n)) \<le> (\<Sum>n. f n * norm h)"
- by (rule summable_le)
+ by (rule suminf_le)
also from f have "(\<Sum>n. f n * norm h) = suminf f * norm h"
by (rule suminf_mult2 [symmetric])
finally show "norm (suminf (g h)) \<le> suminf f * norm h" .
@@ -737,7 +737,7 @@
using `x \<noteq> 0` by auto }
note 1 = this and 2 = summable_rabs_comparison_test[OF _ ign[OF `summable L`]]
then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> (\<Sum> i. L (i + ?N))"
- by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] summable_le[OF _ 2 ign[OF `summable L`]]])
+ by (metis (lifting) abs_idempotent order_trans[OF summable_rabs[OF 2] suminf_le[OF _ 2 ign[OF `summable L`]]])
then have "\<bar> \<Sum> i. ?diff (i + ?N) x \<bar> \<le> r / 3" (is "?L_part \<le> r/3")
using L_estimate by auto
@@ -1006,22 +1006,17 @@
shows "(\<Sum>n. f n * 0 ^ n) = f 0"
proof -
have "(\<Sum>n<1. f n * 0 ^ n) = (\<Sum>n. f n * 0 ^ n)"
- by (rule sums_unique [OF series_zero], simp add: power_0_left)
+ by (subst suminf_finite[where N="{0}"]) (auto simp: power_0_left)
thus ?thesis unfolding One_nat_def by simp
qed
lemma exp_zero [simp]: "exp 0 = 1"
unfolding exp_def by (simp add: scaleR_conv_of_real powser_zero)
-lemma setsum_cl_ivl_Suc2:
- "(\<Sum>i=m..Suc n. f i) = (if Suc n < m then 0 else f m + (\<Sum>i=m..n. f (Suc i)))"
- by (simp add: setsum_head_Suc setsum_shift_bounds_cl_Suc_ivl
- del: setsum_cl_ivl_Suc)
-
lemma exp_series_add:
fixes x y :: "'a::{real_field}"
defines S_def: "S \<equiv> \<lambda>x n. x ^ n /\<^sub>R real (fact n)"
- shows "S (x + y) n = (\<Sum>i=0..n. S x i * S y (n - i))"
+ shows "S (x + y) n = (\<Sum>i\<le>n. S x i * S y (n - i))"
proof (induct n)
case 0
show ?case
@@ -1035,32 +1030,32 @@
have "real (Suc n) *\<^sub>R S (x + y) (Suc n) = (x + y) * S (x + y) n"
by (simp only: times_S)
- also have "\<dots> = (x + y) * (\<Sum>i=0..n. S x i * S y (n-i))"
+ also have "\<dots> = (x + y) * (\<Sum>i\<le>n. S x i * S y (n-i))"
by (simp only: Suc)
- also have "\<dots> = x * (\<Sum>i=0..n. S x i * S y (n-i))
- + y * (\<Sum>i=0..n. S x i * S y (n-i))"
+ also have "\<dots> = x * (\<Sum>i\<le>n. S x i * S y (n-i))
+ + y * (\<Sum>i\<le>n. S x i * S y (n-i))"
by (rule distrib_right)
- also have "\<dots> = (\<Sum>i=0..n. (x * S x i) * S y (n-i))
- + (\<Sum>i=0..n. S x i * (y * S y (n-i)))"
+ also have "\<dots> = (\<Sum>i\<le>n. (x * S x i) * S y (n-i))
+ + (\<Sum>i\<le>n. S x i * (y * S y (n-i)))"
by (simp only: setsum_right_distrib mult_ac)
- also have "\<dots> = (\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
- + (\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
+ also have "\<dots> = (\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i)))
+ + (\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
by (simp add: times_S Suc_diff_le)
- also have "(\<Sum>i=0..n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
- (\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
- by (subst setsum_cl_ivl_Suc2, simp)
- also have "(\<Sum>i=0..n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
- (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
- by (subst setsum_cl_ivl_Suc, simp)
- also have "(\<Sum>i=0..Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
- (\<Sum>i=0..Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
- (\<Sum>i=0..Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
+ also have "(\<Sum>i\<le>n. real (Suc i) *\<^sub>R (S x (Suc i) * S y (n-i))) =
+ (\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i)))"
+ by (subst setsum_atMost_Suc_shift) simp
+ also have "(\<Sum>i\<le>n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+ (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i)))"
+ by simp
+ also have "(\<Sum>i\<le>Suc n. real i *\<^sub>R (S x i * S y (Suc n-i))) +
+ (\<Sum>i\<le>Suc n. real (Suc n-i) *\<^sub>R (S x i * S y (Suc n-i))) =
+ (\<Sum>i\<le>Suc n. real (Suc n) *\<^sub>R (S x i * S y (Suc n-i)))"
by (simp only: setsum_addf [symmetric] scaleR_left_distrib [symmetric]
- real_of_nat_add [symmetric], simp)
- also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i=0..Suc n. S x i * S y (Suc n-i))"
+ real_of_nat_add [symmetric]) simp
+ also have "\<dots> = real (Suc n) *\<^sub>R (\<Sum>i\<le>Suc n. S x i * S y (Suc n-i))"
by (simp only: scaleR_right.setsum)
finally show
- "S (x + y) (Suc n) = (\<Sum>i=0..Suc n. S x i * S y (Suc n - i))"
+ "S (x + y) (Suc n) = (\<Sum>i\<le>Suc n. S x i * S y (Suc n - i))"
by (simp del: setsum_cl_ivl_Suc)
qed
@@ -1128,7 +1123,7 @@
have "1+x \<le> (\<Sum>n<2. inverse (real (fact n)) * x ^ n)"
by (auto simp add: numeral_2_eq_2)
also have "... \<le> (\<Sum>n. inverse (real (fact n)) * x ^ n)"
- apply (rule series_pos_le [OF summable_exp])
+ apply (rule setsum_le_suminf [OF summable_exp])
using `0 < x`
apply (auto simp add: zero_le_mult_iff)
done
@@ -1412,7 +1407,7 @@
proof -
have "suminf (\<lambda>n. inverse(fact (n+2)) * (x ^ (n+2))) <=
suminf (\<lambda>n. (x\<^sup>2/2) * ((1/2)^n))"
- apply (rule summable_le)
+ apply (rule suminf_le)
apply (rule allI, rule aux1)
apply (rule summable_exp [THEN summable_ignore_initial_segment])
by (rule sums_summable, rule aux2)
@@ -2388,7 +2383,7 @@
show "0 < sin x"
unfolding sums_unique [OF sums]
using sums_summable [OF sums] pos
- by (rule suminf_gt_zero)
+ by (rule suminf_pos)
qed
lemma cos_double_less_one: "0 < x \<Longrightarrow> x < 2 \<Longrightarrow> cos (2 * x) < 1"
@@ -2427,7 +2422,7 @@
apply (frule sums_unique)
apply (drule sums_summable)
apply simp
-apply (erule suminf_gt_zero)
+apply (erule suminf_pos)
apply (simp add: add_ac)
done
--- a/src/HOL/ex/HarmonicSeries.thy Tue Mar 18 22:11:46 2014 +0100
+++ b/src/HOL/ex/HarmonicSeries.thy Wed Mar 19 15:34:57 2014 +0100
@@ -268,8 +268,8 @@
text {* The final theorem shows that as we take more and more elements
(see @{thm [source] harmonic_aux3}) we get an ever increasing sum. By assuming
-the sum converges, the lemma @{thm [source] series_pos_less} ( @{thm
-series_pos_less} ) states that each sum is bounded above by the
+the sum converges, the lemma @{thm [source] setsum_less_suminf} ( @{thm
+setsum_less_suminf} ) states that each sum is bounded above by the
series' limit. This contradicts our first statement and thus we prove
that the harmonic series is divergent. *}
@@ -284,7 +284,7 @@
proof -
have "\<forall>n. 0 \<le> ?f n" by simp
with sf have "?s \<ge> 0"
- by - (rule suminf_ge_zero, simp_all)
+ by (rule suminf_nonneg)
then have cgt0: "\<lceil>2*?s\<rceil> \<ge> 0" by simp
from ndef have "n = nat \<lceil>(2*?s)\<rceil>" .
@@ -298,11 +298,9 @@
obtain j where jdef: "j = (2::nat)^n" by simp
have "\<forall>m\<ge>j. 0 < ?f m" by simp
- with sf have "(\<Sum>i\<in>{0..<j}. ?f i) < ?s" unfolding atLeast0LessThan by (rule series_pos_less)
- then have "(\<Sum>i\<in>{1..<Suc j}. 1/(real i)) < ?s"
- apply -
- apply (subst(asm) setsum_shift_bounds_Suc_ivl [symmetric])
- by simp
+ with sf have "(\<Sum>i<j. ?f i) < ?s" by (rule setsum_less_suminf)
+ then have "(\<Sum>i\<in>{Suc 0..<Suc j}. 1/(real i)) < ?s"
+ unfolding setsum_shift_bounds_Suc_ivl by (simp add: atLeast0LessThan)
with jdef have
"(\<Sum>i\<in>{1..< Suc ((2::nat)^n)}. 1 / (real i)) < ?s" by simp
then have