--- a/src/HOL/Probability/Caratheodory.thy Mon Mar 28 23:49:53 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Tue Mar 29 14:27:31 2011 +0200
@@ -258,7 +258,21 @@
by (simp add: Un)
qed
-lemma (in algebra) countably_subadditive_subadditive:
+lemma (in ring_of_sets) disjointed_additive:
+ assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> sets M" "incseq A"
+ shows "(\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
+proof (induct n)
+ case (Suc n)
+ then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
+ by simp
+ also have "\<dots> = f (A n \<union> disjointed A (Suc n))"
+ using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq)
+ also have "A n \<union> disjointed A (Suc n) = A (Suc n)"
+ using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq)
+ finally show ?case .
+qed simp
+
+lemma (in ring_of_sets) countably_subadditive_subadditive:
assumes f: "positive M f" and cs: "countably_subadditive M f"
shows "subadditive M f"
proof (auto simp add: subadditive_def)
@@ -277,7 +291,7 @@
by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
qed
-lemma (in algebra) additive_sum:
+lemma (in ring_of_sets) additive_sum:
fixes A:: "nat \<Rightarrow> 'a set"
assumes f: "positive M f" and ad: "additive M f" and "finite S"
and A: "range A \<subseteq> sets M"
@@ -785,17 +799,17 @@
moreover
have "Inf (measure_set M f s)
\<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
- proof -
+ proof -
have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
by (metis Un_Diff_Int Un_commute)
also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
apply (rule subadditiveD)
- apply (rule algebra.countably_subadditive_subadditive[OF algebra_Pow])
+ apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf])
apply (rule inf_measure_countably_subadditive)
using s by (auto intro!: posf inc)
finally show ?thesis .
- qed
+ qed
ultimately
show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
= Inf (measure_set M f s)"
@@ -837,4 +851,183 @@
by (intro exI[of _ ?infm]) auto
qed
+subsubsection {*Alternative instances of caratheodory*}
+
+lemma sums_def2:
+ "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
+ unfolding sums_def
+ apply (subst LIMSEQ_Suc_iff[symmetric])
+ unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
+
+lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
+ assumes f: "positive M f" "additive M f"
+ shows "countably_additive M f \<longleftrightarrow>
+ (\<forall>A. range A \<subseteq> sets M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i))"
+ unfolding countably_additive_def
+proof safe
+ assume count_sum: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> sets M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
+ then have dA: "range (disjointed A) \<subseteq> sets M" by (auto simp: range_disjointed_sets)
+ with count_sum[THEN spec, of "disjointed A"] A(3)
+ have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
+ by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
+ moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+ using f(1)[unfolded positive_def] dA
+ by (auto intro!: summable_sumr_LIMSEQ_suminf summable_extreal_pos)
+ from LIMSEQ_Suc[OF this]
+ have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+ unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
+ moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
+ using disjointed_additive[OF f A(1,2)] .
+ ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
+next
+ assume cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" "(\<Union>i. A i) \<in> sets M"
+ have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
+ have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
+ proof (unfold *[symmetric], intro cont[rule_format])
+ show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> sets M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> sets M"
+ using A * by auto
+ qed (force intro!: incseq_SucI)
+ moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
+ using A
+ by (intro additive_sum[OF f, of _ A, symmetric])
+ (auto intro: disjoint_family_on_mono[where B=UNIV])
+ ultimately
+ have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
+ unfolding sums_def2 by simp
+ from sums_unique[OF this]
+ show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
+qed
+
+lemma uminus_extreal_add_uminus_uminus:
+ fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
+ by (cases rule: extreal2_cases[of a b]) auto
+
+lemma INFI_extreal_add:
+ assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+ shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
+proof -
+ have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+ using assms unfolding INF_less_iff by auto
+ { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
+ by (rule uminus_extreal_add_uminus_uminus) }
+ then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+ by simp
+ also have "\<dots> = INFI UNIV f + INFI UNIV g"
+ unfolding extreal_INFI_uminus
+ using assms INF_less
+ by (subst SUPR_extreal_add)
+ (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
+ finally show ?thesis .
+qed
+
+lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
+ assumes f: "positive M f" "additive M f"
+ shows "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
+ \<longleftrightarrow> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0)"
+proof safe
+ assume cont: "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))"
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
+ with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
+ using `positive M f`[unfolded positive_def] by auto
+next
+ assume cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "decseq A" "(\<Inter>i. A i) \<in> sets M" "\<forall>i. f (A i) \<noteq> \<infinity>"
+
+ have f_mono: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
+ using additive_increasing[OF f] unfolding increasing_def by simp
+
+ have decseq_fA: "decseq (\<lambda>i. f (A i))"
+ using A by (auto simp: decseq_def intro!: f_mono)
+ have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
+ using A by (auto simp: decseq_def)
+ then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
+ using A unfolding decseq_def by (auto intro!: f_mono Diff)
+ have "f (\<Inter>x. A x) \<le> f (A 0)"
+ using A by (auto intro!: f_mono)
+ then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
+ using A by auto
+ { fix i
+ have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
+ then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
+ using A by auto }
+ note f_fin = this
+ have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
+ proof (intro cont[rule_format, OF _ decseq _ f_fin])
+ show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> sets M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
+ using A by auto
+ qed
+ from INF_Lim_extreal[OF decseq_f this]
+ have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
+ moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
+ by auto
+ ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
+ using A(4) f_fin f_Int_fin
+ by (subst INFI_extreal_add) (auto simp: decseq_f)
+ moreover {
+ fix n
+ have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
+ using A by (subst f(2)[THEN additiveD]) auto
+ also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
+ by auto
+ finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
+ ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
+ by simp
+ with LIMSEQ_extreal_INFI[OF decseq_fA]
+ show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
+qed
+
+lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
+lemma positiveD2: "positive M f \<Longrightarrow> A \<in> sets M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
+
+lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
+ assumes f: "positive M f" "additive M f" "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
+ assumes cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ assumes A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
+ shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+proof -
+ have "\<forall>A\<in>sets M. \<exists>x. f A = extreal x"
+ proof
+ fix A assume "A \<in> sets M" with f show "\<exists>x. f A = extreal x"
+ unfolding positive_def by (cases "f A") auto
+ qed
+ from bchoice[OF this] guess f' .. note f' = this[rule_format]
+ from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
+ by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
+ moreover
+ { fix i
+ have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
+ using A by (intro f(2)[THEN additiveD, symmetric]) auto
+ also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
+ by auto
+ finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
+ using A by (subst (asm) (1 2 3) f') auto
+ then have "f ((\<Union>i. A i) - A i) = extreal (f' (\<Union>i. A i) - f' (A i))"
+ using A f' by auto }
+ ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
+ by (simp add: zero_extreal_def)
+ then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
+ by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
+ then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+ using A by (subst (1 2) f') auto
+qed
+
+lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
+ assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
+ assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ shows "countably_additive M f"
+ using countably_additive_iff_continuous_from_below[OF f]
+ using empty_continuous_imp_continuous_from_below[OF f fin] cont
+ by blast
+
+lemma (in ring_of_sets) caratheodory_empty_continuous:
+ assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> sets M \<Longrightarrow> f A \<noteq> \<infinity>"
+ assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+ shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
+ measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
+proof (intro caratheodory empty_continuous_imp_countably_additive f)
+ show "\<forall>A\<in>sets M. f A \<noteq> \<infinity>" using fin by auto
+qed (rule cont)
+
end
--- a/src/HOL/Probability/Sigma_Algebra.thy Mon Mar 28 23:49:53 2011 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy Tue Mar 29 14:27:31 2011 +0200
@@ -9,7 +9,7 @@
theory Sigma_Algebra
imports
- Main
+ Complex_Main
"~~/src/HOL/Library/Countable"
"~~/src/HOL/Library/FuncSet"
"~~/src/HOL/Library/Indicator_Function"
@@ -195,13 +195,17 @@
ultimately show ?thesis by metis
qed
+lemma ring_of_sets_Pow:
+ "ring_of_sets \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
+ by default auto
+
lemma algebra_Pow:
- "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
- by (auto simp add: algebra_iff_Un)
+ "algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
+ by default auto
lemma sigma_algebra_Pow:
"sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>"
- by (auto simp add: sigma_algebra_def sigma_algebra_axioms_def algebra_Pow)
+ by default auto
lemma sigma_algebra_iff:
"sigma_algebra M \<longleftrightarrow>
@@ -714,6 +718,18 @@
"range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M"
using range_disjointed_sets .
+lemma disjointed_0[simp]: "disjointed A 0 = A 0"
+ by (simp add: disjointed_def)
+
+lemma incseq_Un:
+ "incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n"
+ unfolding incseq_def by auto
+
+lemma disjointed_incseq:
+ "incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n) - A n"
+ using incseq_Un[of A]
+ by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost)
+
lemma sigma_algebra_disjoint_iff:
"sigma_algebra M \<longleftrightarrow>
algebra M &