src/HOL/Probability/Caratheodory.thy
changeset 42145 8448713d48b7
parent 42067 66c8281349ec
child 42950 6e5c2a3c69da
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Mar 28 23:49:53 2011 +0200
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 29 14:27:31 2011 +0200
     1.3 @@ -258,7 +258,21 @@
     1.4      by (simp add: Un)
     1.5  qed
     1.6  
     1.7 -lemma (in algebra) countably_subadditive_subadditive:
     1.8 +lemma (in ring_of_sets) disjointed_additive:
     1.9 +  assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> sets M" "incseq A"
    1.10 +  shows "(\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
    1.11 +proof (induct n)
    1.12 +  case (Suc n)
    1.13 +  then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
    1.14 +    by simp
    1.15 +  also have "\<dots> = f (A n \<union> disjointed A (Suc n))"
    1.16 +    using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq)
    1.17 +  also have "A n \<union> disjointed A (Suc n) = A (Suc n)"
    1.18 +    using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq)
    1.19 +  finally show ?case .
    1.20 +qed simp
    1.21 +
    1.22 +lemma (in ring_of_sets) countably_subadditive_subadditive:
    1.23    assumes f: "positive M f" and cs: "countably_subadditive M f"
    1.24    shows  "subadditive M f"
    1.25  proof (auto simp add: subadditive_def)
    1.26 @@ -277,7 +291,7 @@
    1.27      by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
    1.28  qed
    1.29  
    1.30 -lemma (in algebra) additive_sum:
    1.31 +lemma (in ring_of_sets) additive_sum:
    1.32    fixes A:: "nat \<Rightarrow> 'a set"
    1.33    assumes f: "positive M f" and ad: "additive M f" and "finite S"
    1.34        and A: "range A \<subseteq> sets M"
    1.35 @@ -785,17 +799,17 @@
    1.36    moreover
    1.37    have "Inf (measure_set M f s)
    1.38         \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
    1.39 -    proof -
    1.40 +  proof -
    1.41      have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
    1.42        by (metis Un_Diff_Int Un_commute)
    1.43      also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
    1.44        apply (rule subadditiveD)
    1.45 -      apply (rule algebra.countably_subadditive_subadditive[OF algebra_Pow])
    1.46 +      apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
    1.47        apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf])
    1.48        apply (rule inf_measure_countably_subadditive)
    1.49        using s by (auto intro!: posf inc)
    1.50      finally show ?thesis .
    1.51 -    qed
    1.52 +  qed
    1.53    ultimately
    1.54    show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
    1.55          = Inf (measure_set M f s)"
    1.56 @@ -837,4 +851,183 @@
    1.57      by (intro exI[of _ ?infm]) auto
    1.58  qed
    1.59  
    1.60 +subsubsection {*Alternative instances of caratheodory*}
    1.61 +
    1.62 +lemma sums_def2:
    1.63 +  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
    1.64 +  unfolding sums_def
    1.65 +  apply (subst LIMSEQ_Suc_iff[symmetric])
    1.66 +  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
    1.67 +
    1.68 +lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
    1.69 +  assumes f: "positive M f" "additive M f"
    1.70 +  shows "countably_additive M f \<longleftrightarrow>
    1.71 +    (\<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))"
    1.72 +  unfolding countably_additive_def
    1.73 +proof safe
    1.74 +  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)"
    1.75 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
    1.76 +  then have dA: "range (disjointed A) \<subseteq> sets M" by (auto simp: range_disjointed_sets)
    1.77 +  with count_sum[THEN spec, of "disjointed A"] A(3)
    1.78 +  have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
    1.79 +    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
    1.80 +  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.81 +    using f(1)[unfolded positive_def] dA
    1.82 +    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_extreal_pos)
    1.83 +  from LIMSEQ_Suc[OF this]
    1.84 +  have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
    1.85 +    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
    1.86 +  moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
    1.87 +    using disjointed_additive[OF f A(1,2)] .
    1.88 +  ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
    1.89 +next
    1.90 +  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)"
    1.91 +  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" "(\<Union>i. A i) \<in> sets M"
    1.92 +  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
    1.93 +  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
    1.94 +  proof (unfold *[symmetric], intro cont[rule_format])
    1.95 +    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> sets M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> sets M"
    1.96 +      using A * by auto
    1.97 +  qed (force intro!: incseq_SucI)
    1.98 +  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
    1.99 +    using A
   1.100 +    by (intro additive_sum[OF f, of _ A, symmetric])
   1.101 +       (auto intro: disjoint_family_on_mono[where B=UNIV])
   1.102 +  ultimately
   1.103 +  have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
   1.104 +    unfolding sums_def2 by simp
   1.105 +  from sums_unique[OF this]
   1.106 +  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
   1.107 +qed
   1.108 +
   1.109 +lemma uminus_extreal_add_uminus_uminus:
   1.110 +  fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
   1.111 +  by (cases rule: extreal2_cases[of a b]) auto
   1.112 +
   1.113 +lemma INFI_extreal_add:
   1.114 +  assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
   1.115 +  shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
   1.116 +proof -
   1.117 +  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
   1.118 +    using assms unfolding INF_less_iff by auto
   1.119 +  { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
   1.120 +      by (rule uminus_extreal_add_uminus_uminus) }
   1.121 +  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
   1.122 +    by simp
   1.123 +  also have "\<dots> = INFI UNIV f + INFI UNIV g"
   1.124 +    unfolding extreal_INFI_uminus
   1.125 +    using assms INF_less
   1.126 +    by (subst SUPR_extreal_add)
   1.127 +       (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
   1.128 +  finally show ?thesis .
   1.129 +qed
   1.130 +
   1.131 +lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
   1.132 +  assumes f: "positive M f" "additive M f"
   1.133 +  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))
   1.134 +     \<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)"
   1.135 +proof safe
   1.136 +  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))"
   1.137 +  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>"
   1.138 +  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
   1.139 +    using `positive M f`[unfolded positive_def] by auto
   1.140 +next
   1.141 +  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"
   1.142 +  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>"
   1.143 +
   1.144 +  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"
   1.145 +    using additive_increasing[OF f] unfolding increasing_def by simp
   1.146 +
   1.147 +  have decseq_fA: "decseq (\<lambda>i. f (A i))"
   1.148 +    using A by (auto simp: decseq_def intro!: f_mono)
   1.149 +  have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
   1.150 +    using A by (auto simp: decseq_def)
   1.151 +  then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
   1.152 +    using A unfolding decseq_def by (auto intro!: f_mono Diff)
   1.153 +  have "f (\<Inter>x. A x) \<le> f (A 0)"
   1.154 +    using A by (auto intro!: f_mono)
   1.155 +  then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
   1.156 +    using A by auto
   1.157 +  { fix i
   1.158 +    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
   1.159 +    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
   1.160 +      using A by auto }
   1.161 +  note f_fin = this
   1.162 +  have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
   1.163 +  proof (intro cont[rule_format, OF _ decseq _ f_fin])
   1.164 +    show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> sets M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
   1.165 +      using A by auto
   1.166 +  qed
   1.167 +  from INF_Lim_extreal[OF decseq_f this]
   1.168 +  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
   1.169 +  moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
   1.170 +    by auto
   1.171 +  ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
   1.172 +    using A(4) f_fin f_Int_fin
   1.173 +    by (subst INFI_extreal_add) (auto simp: decseq_f)
   1.174 +  moreover {
   1.175 +    fix n
   1.176 +    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))"
   1.177 +      using A by (subst f(2)[THEN additiveD]) auto
   1.178 +    also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
   1.179 +      by auto
   1.180 +    finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
   1.181 +  ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
   1.182 +    by simp
   1.183 +  with LIMSEQ_extreal_INFI[OF decseq_fA]
   1.184 +  show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
   1.185 +qed
   1.186 +
   1.187 +lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
   1.188 +lemma positiveD2: "positive M f \<Longrightarrow> A \<in> sets M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
   1.189 +
   1.190 +lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
   1.191 +  assumes f: "positive M f" "additive M f" "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
   1.192 +  assumes cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.193 +  assumes A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
   1.194 +  shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.195 +proof -
   1.196 +  have "\<forall>A\<in>sets M. \<exists>x. f A = extreal x"
   1.197 +  proof
   1.198 +    fix A assume "A \<in> sets M" with f show "\<exists>x. f A = extreal x"
   1.199 +      unfolding positive_def by (cases "f A") auto
   1.200 +  qed
   1.201 +  from bchoice[OF this] guess f' .. note f' = this[rule_format]
   1.202 +  from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
   1.203 +    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
   1.204 +  moreover
   1.205 +  { fix i
   1.206 +    have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
   1.207 +      using A by (intro f(2)[THEN additiveD, symmetric]) auto
   1.208 +    also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
   1.209 +      by auto
   1.210 +    finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
   1.211 +      using A by (subst (asm) (1 2 3) f') auto
   1.212 +    then have "f ((\<Union>i. A i) - A i) = extreal (f' (\<Union>i. A i) - f' (A i))"
   1.213 +      using A f' by auto }
   1.214 +  ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
   1.215 +    by (simp add: zero_extreal_def)
   1.216 +  then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
   1.217 +    by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
   1.218 +  then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
   1.219 +    using A by (subst (1 2) f') auto
   1.220 +qed
   1.221 +
   1.222 +lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
   1.223 +  assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
   1.224 +  assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.225 +  shows "countably_additive M f"
   1.226 +  using countably_additive_iff_continuous_from_below[OF f]
   1.227 +  using empty_continuous_imp_continuous_from_below[OF f fin] cont
   1.228 +  by blast
   1.229 +
   1.230 +lemma (in ring_of_sets) caratheodory_empty_continuous:
   1.231 +  assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> sets M \<Longrightarrow> f A \<noteq> \<infinity>"
   1.232 +  assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
   1.233 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
   1.234 +            measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
   1.235 +proof (intro caratheodory empty_continuous_imp_countably_additive f)
   1.236 +  show "\<forall>A\<in>sets M. f A \<noteq> \<infinity>" using fin by auto
   1.237 +qed (rule cont)
   1.238 +
   1.239  end