src/HOL/Probability/Caratheodory.thy

 header {*Caratheodory Extension Theorem*}
 
 theory Caratheodory
   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.
 *}
 

     by (intro exI[of _ ?infm]) auto
 qed
 
 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"
   shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
 proof (intro caratheodory' empty_continuous_imp_countably_additive f)