--- a/src/HOL/Probability/Caratheodory.thy Wed Oct 10 12:12:14 2012 +0200
+++ b/src/HOL/Probability/Caratheodory.thy Wed Oct 10 12:12:15 2012 +0200
@@ -9,12 +9,6 @@
imports Measure_Space
begin
-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 ..
-
text {*
Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
*}
@@ -684,146 +678,6 @@
subsubsection {*Alternative instances of caratheodory*}
-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> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> 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> M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
- fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
- then have dA: "range (disjointed A) \<subseteq> 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_ereal_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> M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
- fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> M" "disjoint_family A" "(\<Union>i. A i) \<in> 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> M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> 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 (in ring_of_sets) continuous_from_above_iff_empty_continuous:
- assumes f: "positive M f" "additive M f"
- shows "(\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> 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> 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> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> 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> 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> 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> M" "decseq A" "(\<Inter>i. A i) \<in> M" "\<forall>i. f (A i) \<noteq> \<infinity>"
-
- have f_mono: "\<And>a b. a \<in> M \<Longrightarrow> b \<in> 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> M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
- using A by auto
- qed
- from INF_Lim_ereal[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_ereal_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_ereal_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> 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>M. f A \<noteq> \<infinity>"
- assumes cont: "\<forall>A. range A \<subseteq> M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
- assumes A: "range A \<subseteq> M" "incseq A" "(\<Union>i. A i) \<in> M"
- shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
-proof -
- have "\<forall>A\<in>M. \<exists>x. f A = ereal x"
- proof
- fix A assume "A \<in> M" with f show "\<exists>x. f A = ereal 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) = ereal (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_ereal_def)
- then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
- by (rule LIMSEQ_diff_approach_zero2[OF tendsto_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>M. f A \<noteq> \<infinity>"
- assumes cont: "\<And>A. range A \<subseteq> 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> M \<Longrightarrow> f A \<noteq> \<infinity>"
assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"