--- 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)
--- 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
--- 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:
--- 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
--- 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"
--- 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])
--- 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))"
--- 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))"