author hoelzl Mon, 14 Mar 2011 14:37:44 +0100 changeset 41977 dbfc073c310d parent 41976 3fdbc7d5b525 child 41978 656298577a33
introduce setsum on extreal
```--- a/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:42 2011 +0100
+++ b/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:44 2011 +0100
@@ -3076,4 +3076,51 @@
"[| (a::extreal) <= x; c <= x |] ==> max a c <= x"
by (metis sup_extreal_def sup_least)

+subsection {* Sums *}
+
+lemma setsum_extreal[simp]:
+  "(\<Sum>x\<in>A. extreal (f x)) = extreal (\<Sum>x\<in>A. f x)"
+proof cases
+  assume "finite A" then show ?thesis by induct auto
+qed simp
+
+lemma setsum_Pinfty: "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
+proof safe
+  assume *: "setsum f P = \<infinity>"
+  show "finite P"
+  proof (rule ccontr) assume "infinite P" with * show False by auto qed
+  show "\<exists>i\<in>P. f i = \<infinity>"
+  proof (rule ccontr)
+    assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
+    from `finite P` this have "setsum f P \<noteq> \<infinity>"
+      by induct auto
+    with * show False by auto
+  qed
+next
+  fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
+  thus "setsum f P = \<infinity>"
+  proof induct
+    case (insert x A)
+    show ?case using insert by (cases "x = i") auto
+  qed simp
+qed
+
+lemma setsum_of_pextreal:
+  assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
+  shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
+proof -
+  have "\<forall>x\<in>S. \<exists>r. f x = extreal r"
+  proof
+    fix x assume "x \<in> S"
+    from assms[OF this] show "\<exists>r. f x = extreal r" by (cases "f x") auto
+  qed
+  from bchoice[OF this] guess r ..
+  then show ?thesis by simp
+qed
+
+lemma setsum_0:
+  fixes f :: "'a \<Rightarrow> pextreal" assumes "finite A"
+  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
+  using assms by induct auto
+
end```