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.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.23    assumes f: "positive M f" and cs: "countably_subadditive M f"
1.24    shows  "subadditive M f"
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.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.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.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
```