# HG changeset patch
# User hoelzl
# Date 1335374760 -7200
# Node ID dfe747e72fa8739b8a4720aa4bda4caa85e7e717
# Parent  b9840d8fca43adaec14bce4bf40e1da871aa9637
moved lemmas to appropriate places

diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Library/FuncSet.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -63,6 +63,9 @@
 lemma Pi_mem: "[|f: Pi A B; x \<in> A|] ==> f x \<in> B x"
   by (simp add: Pi_def)
 
+lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
+  unfolding Pi_def by auto
+
 lemma PiE [elim]:
   "f : Pi A B ==> (f x : B x ==> Q) ==> (x ~: A ==> Q) ==> Q"
 by(auto simp: Pi_def)
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy
--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -1129,22 +1129,6 @@
     using assms real by (simp add: ereal_le_minus)
 qed (insert assms, auto)
 
-lemma sums_finite:
-  assumes "\<forall>N\<ge>n. f N = 0"
-  shows "f sums (\<Sum>N<n. f N)"
-proof -
-  { fix i have "(\<Sum>N<i + n. f N) = (\<Sum>N<n. f N)"
-      by (induct i) (insert assms, auto) }
-  note this[simp]
-  show ?thesis unfolding sums_def
-    by (rule LIMSEQ_offset[of _ n]) (auto simp add: atLeast0LessThan intro: tendsto_const)
-qed
-
-lemma suminf_finite:
-  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}" assumes "\<forall>N\<ge>n. f N = 0"
-  shows "suminf f = (\<Sum>N<n. f N)"
-  using sums_finite[OF assms, THEN sums_unique] by simp
-
 lemma suminf_upper:
   fixes f :: "nat \<Rightarrow> ereal" assumes "\<And>n. 0 \<le> f n"
   shows "(\<Sum>n<N. f n) \<le> (\<Sum>n. f n)"
@@ -1294,4 +1278,13 @@
     apply (subst SUP_commute) ..
 qed
 
+lemma suminf_setsum_ereal:
+  fixes f :: "_ \<Rightarrow> _ \<Rightarrow> ereal"
+  assumes nonneg: "\<And>i a. a \<in> A \<Longrightarrow> 0 \<le> f i a"
+  shows "(\<Sum>i. \<Sum>a\<in>A. f i a) = (\<Sum>a\<in>A. \<Sum>i. f i a)"
+proof cases
+  assume "finite A" from this nonneg show ?thesis
+    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
+qed simp
+
 end
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Probability/Borel_Space.thy
--- a/src/HOL/Probability/Borel_Space.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Borel_Space.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -943,6 +943,28 @@
   using measurable_comp[OF f borel_measurable_borel_log[OF `1 < b`]]
   by (simp add: comp_def)
 
+lemma borel_measurable_real_floor:
+  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
+  unfolding borel_measurable_iff_ge
+proof (intro allI)
+  fix a :: real
+  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
+      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
+      unfolding real_eq_of_int by simp }
+  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
+  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
+qed
+
+lemma borel_measurable_real_natfloor[intro, simp]:
+  assumes "f \<in> borel_measurable M"
+  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
+proof -
+  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
+    by (auto simp: max_def natfloor_def)
+  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
+  show ?thesis by (simp add: comp_def)
+qed
+
 subsection "Borel space on the extended reals"
 
 lemma borel_measurable_ereal_borel:
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -357,7 +357,7 @@
 proof -
   let ?A = "\<lambda>i::nat. (if i = 0 then b else {})"
   have "(\<Sum>i. f (?A i)) = (\<Sum>i<1::nat. f (?A i))"
-    by (rule suminf_finite) (simp add: f[unfolded positive_def])
+    by (rule suminf_finite) (simp_all add: f[unfolded positive_def])
   also have "... = f b"
     by simp
   finally show ?thesis using assms
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Probability/Finite_Product_Measure.thy
--- a/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Finite_Product_Measure.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -11,9 +11,6 @@
 lemma split_const: "(\<lambda>(i, j). c) = (\<lambda>_. c)"
   by auto
 
-lemma Pi_iff: "f \<in> Pi I X \<longleftrightarrow> (\<forall>i\<in>I. f i \<in> X i)"
-  unfolding Pi_def by auto
-
 abbreviation
   "Pi\<^isub>E A B \<equiv> Pi A B \<inter> extensional A"
 
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Probability/Lebesgue_Integration.thy
--- a/src/HOL/Probability/Lebesgue_Integration.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Lebesgue_Integration.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -32,16 +32,6 @@
     by (intro tendsto_add assms tendsto_divide tendsto_norm tendsto_diff) auto
 qed
 
-lemma measure_Union:
-  assumes "finite S" "S \<subseteq> sets M" "\<And>A B. A \<in> S \<Longrightarrow> B \<in> S \<Longrightarrow> A \<noteq> B \<Longrightarrow> A \<inter> B = {}"
-  shows "setsum (emeasure M) S = (emeasure M) (\<Union>S)"
-proof -
-  have "setsum (emeasure M) S = (emeasure M) (\<Union>i\<in>S. i)"
-    using assms by (intro setsum_emeasure[OF _ _ `finite S`]) (auto simp: disjoint_family_on_def)
-  also have "\<dots> = (emeasure M) (\<Union>S)" by (auto intro!: arg_cong[where f="emeasure M"])
-  finally show ?thesis .
-qed
-
 lemma measurable_sets2[intro]:
   assumes "f \<in> measurable M M'" "g \<in> measurable M M''"
   and "A \<in> sets M'" "B \<in> sets M''"
@@ -57,55 +47,6 @@
   assume "\<forall>n. f n \<le> f (Suc n)" then show "incseq f" by (auto intro!: incseq_SucI)
 qed (auto simp: incseq_def)
 
-lemma borel_measurable_real_floor:
-  "(\<lambda>x::real. real \<lfloor>x\<rfloor>) \<in> borel_measurable borel"
-  unfolding borel_measurable_iff_ge
-proof (intro allI)
-  fix a :: real
-  { fix x have "a \<le> real \<lfloor>x\<rfloor> \<longleftrightarrow> real \<lceil>a\<rceil> \<le> x"
-      using le_floor_eq[of "\<lceil>a\<rceil>" x] ceiling_le_iff[of a "\<lfloor>x\<rfloor>"]
-      unfolding real_eq_of_int by simp }
-  then have "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} = {real \<lceil>a\<rceil>..}" by auto
-  then show "{w::real \<in> space borel. a \<le> real \<lfloor>w\<rfloor>} \<in> sets borel" by auto
-qed
-
-lemma borel_measurable_real_natfloor[intro, simp]:
-  assumes "f \<in> borel_measurable M"
-  shows "(\<lambda>x. real (natfloor (f x))) \<in> borel_measurable M"
-proof -
-  have "\<And>x. real (natfloor (f x)) = max 0 (real \<lfloor>f x\<rfloor>)"
-    by (auto simp: max_def natfloor_def)
-  with borel_measurable_max[OF measurable_comp[OF assms borel_measurable_real_floor] borel_measurable_const]
-  show ?thesis by (simp add: comp_def)
-qed
-
-lemma AE_not_in:
-  assumes N: "N \<in> null_sets M" shows "AE x in M. x \<notin> N"
-  using N by (rule AE_I') auto
-
-lemma sums_If_finite:
-  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
-  assumes finite: "finite {r. P r}"
-  shows "(\<lambda>r. if P r then f r else 0) sums (\<Sum>r\<in>{r. P r}. f r)" (is "?F sums _")
-proof cases
-  assume "{r. P r} = {}" hence "\<And>r. \<not> P r" by auto
-  thus ?thesis by (simp add: sums_zero)
-next
-  assume not_empty: "{r. P r} \<noteq> {}"
-  have "?F sums (\<Sum>r = 0..< Suc (Max {r. P r}). ?F r)"
-    by (rule series_zero)
-       (auto simp add: Max_less_iff[OF finite not_empty] less_eq_Suc_le[symmetric])
-  also have "(\<Sum>r = 0..< Suc (Max {r. P r}). ?F r) = (\<Sum>r\<in>{r. P r}. f r)"
-    by (subst setsum_cases)
-       (auto intro!: setsum_cong simp: Max_ge_iff[OF finite not_empty] less_Suc_eq_le)
-  finally show ?thesis .
-qed
-
-lemma sums_single:
-  fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
-  shows "(\<lambda>r. if r = i then f r else 0) sums f i"
-  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
-
 section "Simple function"
 
 text {*
@@ -526,7 +467,7 @@
   { fix x assume "x \<in> space M"
     have "\<Union>(?sub (f x)) = (f -` {f x} \<inter> space M)" by auto
     with sets have "(emeasure M) (f -` {f x} \<inter> space M) = setsum (emeasure M) (?sub (f x))"
-      by (subst measure_Union) auto }
+      by (subst setsum_emeasure) (auto simp: disjoint_family_on_def) }
   hence "integral\<^isup>S M f = (\<Sum>(x,A)\<in>?SIGMA. x * (emeasure M) A)"
     unfolding simple_integral_def using f sets
     by (subst setsum_Sigma[symmetric])
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Probability/Measure_Space.thy
--- a/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Probability/Measure_Space.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -12,22 +12,6 @@
   "~~/src/HOL/Multivariate_Analysis/Extended_Real_Limits"
 begin
 
-lemma suminf_eq_setsum:
-  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add, t2_space}"
-  assumes "finite {i. f i \<noteq> 0}" (is "finite ?P")
-  shows "(\<Sum>i. f i) = (\<Sum>i | f i \<noteq> 0. f i)"
-proof cases
-  assume "?P \<noteq> {}"
-  have [dest!]: "\<And>i. Suc (Max ?P) \<le> i \<Longrightarrow> f i = 0"
-    using `finite ?P` `?P \<noteq> {}` by (auto simp: Suc_le_eq) 
-  have "(\<Sum>i. f i) = (\<Sum>i<Suc (Max ?P). f i)"
-    by (rule suminf_finite) auto
-  also have "\<dots> = (\<Sum>i | f i \<noteq> 0. f i)"
-    using `finite ?P` `?P \<noteq> {}`
-    by (intro setsum_mono_zero_right) (auto simp: less_Suc_eq_le)
-  finally show ?thesis .
-qed simp
-
 lemma suminf_cmult_indicator:
   fixes f :: "nat \<Rightarrow> ereal"
   assumes "disjoint_family A" "x \<in> A i" "\<And>i. 0 \<le> f i"
@@ -246,7 +230,7 @@
     using disj by (auto simp: disjoint_family_on_def)
 
   from fin_not_0 have "(\<Sum>i. \<mu> (F i)) = (\<Sum>i | \<mu> (F i) \<noteq> 0. \<mu> (F i))"
-    by (rule suminf_eq_setsum)
+    by (rule suminf_finite) auto
   also have "\<dots> = (\<Sum>i | F i \<noteq> {}. \<mu> (F i))"
     using fin_not_empty F_subset by (rule setsum_mono_zero_left) auto
   also have "\<dots> = \<mu> (\<Union>i\<in>{i. F i \<noteq> {}}. F i)"
@@ -791,6 +775,10 @@
   using Int_absorb1[OF sets_into_space, of N M]
   by (subst AE_iff_null) (auto simp: Int_def[symmetric])
 
+lemma AE_not_in:
+  "N \<in> null_sets M \<Longrightarrow> AE x in M. x \<notin> N"
+  by (metis AE_iff_null_sets null_setsD2)
+
 lemma AE_iff_measurable:
   "N \<in> sets M \<Longrightarrow> {x\<in>space M. \<not> P x} = N \<Longrightarrow> (AE x in M. P x) \<longleftrightarrow> emeasure M N = 0"
   using AE_iff_null[of _ P] by auto
@@ -1357,7 +1345,7 @@
           with finite_F have "finite {i. ?M (F i) \<noteq> 0} "
             by (simp add: fin_eq)
           then have "(\<Sum>i. ?M (F i)) = (\<Sum>i | ?M (F i) \<noteq> 0. ?M (F i))"
-            by (rule suminf_eq_setsum)
+            by (rule suminf_finite) auto
           also have "\<dots> = ereal (\<Sum>i | F i \<noteq> {}. card (F i))"
             using finite_F by simp
           also have "\<dots> = ereal (card (\<Union>i \<in> {i. F i \<noteq> {}}. F i))"
diff -r b9840d8fca43 -r dfe747e72fa8 src/HOL/Series.thy
--- a/src/HOL/Series.thy	Wed Apr 25 17:15:10 2012 +0200
+++ b/src/HOL/Series.thy	Wed Apr 25 19:26:00 2012 +0200
@@ -120,6 +120,50 @@
   shows "f sums x \<longleftrightarrow> summable f \<and> (suminf f = x)"
   by (metis summable_sums sums_summable sums_unique)
 
+lemma sums_finite:
+  assumes [simp]: "finite N"
+  assumes f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
+  shows "f sums (\<Sum>n\<in>N. f n)"
+proof -
+  { fix n
+    have "setsum f {..<n + Suc (Max N)} = setsum f N"
+    proof cases
+      assume "N = {}"
+      with f have "f = (\<lambda>x. 0)" by auto
+      then show ?thesis by simp
+    next
+      assume [simp]: "N \<noteq> {}"
+      show ?thesis
+      proof (safe intro!: setsum_mono_zero_right f)
+        fix i assume "i \<in> N"
+        then have "i \<le> Max N" by simp
+        then show "i < n + Suc (Max N)" by simp
+      qed
+    qed }
+  note eq = this
+  show ?thesis unfolding sums_def
+    by (rule LIMSEQ_offset[of _ "Suc (Max N)"])
+       (simp add: eq atLeast0LessThan tendsto_const del: add_Suc_right)
+qed
+
+lemma suminf_finite:
+  fixes f :: "nat \<Rightarrow> 'a::{comm_monoid_add,t2_space}"
+  assumes N: "finite N" and f: "\<And>n. n \<notin> N \<Longrightarrow> f n = 0"
+  shows "suminf f = (\<Sum>n\<in>N. f n)"
+  using sums_finite[OF assms, THEN sums_unique] by simp
+
+lemma sums_If_finite_set:
+  "finite A \<Longrightarrow> (\<lambda>r. if r \<in> A then f r else 0 :: 'a::{comm_monoid_add,t2_space}) 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 sums_If_finite:
+  "finite {r. P r} \<Longrightarrow> (\<lambda>r. if P r then f r else 0 :: 'a::{comm_monoid_add,t2_space}) sums (\<Sum>r | P r. f r)"
+  using sums_If_finite_set[of "{r. P r}" f] by simp
+
+lemma sums_single:
+  "(\<lambda>r. if r = i then f r else 0::'a::{comm_monoid_add,t2_space}) sums f i"
+  using sums_If_finite[of "\<lambda>r. r = i" f] by simp
+
 lemma sums_split_initial_segment:
   fixes f :: "nat \<Rightarrow> 'a::real_normed_vector"
   shows "f sums s ==> (\<lambda>n. f(n + k)) sums (s - (SUM i = 0..< k. f i))"