src/HOL/Probability/Caratheodory.thy
 changeset 43920 cedb5cb948fd parent 42950 6e5c2a3c69da child 44106 0e018cbcc0de
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Jul 19 14:35:44 2011 +0200
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Jul 19 14:36:12 2011 +0200
1.3 @@ -19,8 +19,8 @@
1.4    Originally from the Hurd/Coble measure theory development, translated by Lawrence Paulson.
1.5  *}
1.6
1.7 -lemma suminf_extreal_2dimen:
1.8 -  fixes f:: "nat \<times> nat \<Rightarrow> extreal"
1.9 +lemma suminf_ereal_2dimen:
1.10 +  fixes f:: "nat \<times> nat \<Rightarrow> ereal"
1.11    assumes pos: "\<And>p. 0 \<le> f p"
1.12    assumes "\<And>m. g m = (\<Sum>n. f (m,n))"
1.13    shows "(\<Sum>i. f (prod_decode i)) = suminf g"
1.14 @@ -47,21 +47,21 @@
1.15    ultimately
1.16    show ?thesis unfolding g_def using pos
1.17      by (auto intro!: SUPR_eq  simp: setsum_cartesian_product reindex le_SUPI2
1.18 -                     setsum_nonneg suminf_extreal_eq_SUPR SUPR_pair
1.19 -                     SUPR_extreal_setsum[symmetric] incseq_setsumI setsum_nonneg)
1.20 +                     setsum_nonneg suminf_ereal_eq_SUPR SUPR_pair
1.21 +                     SUPR_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
1.22  qed
1.23
1.24  subsection {* Measure Spaces *}
1.25
1.26  record 'a measure_space = "'a algebra" +
1.27 -  measure :: "'a set \<Rightarrow> extreal"
1.28 +  measure :: "'a set \<Rightarrow> ereal"
1.29
1.30 -definition positive where "positive M f \<longleftrightarrow> f {} = (0::extreal) \<and> (\<forall>A\<in>sets M. 0 \<le> f A)"
1.31 +definition positive where "positive M f \<longleftrightarrow> f {} = (0::ereal) \<and> (\<forall>A\<in>sets M. 0 \<le> f A)"
1.32
1.34    (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) = f x + f y)"
1.35
1.36 -definition countably_additive :: "('a, 'b) algebra_scheme \<Rightarrow> ('a set \<Rightarrow> extreal) \<Rightarrow> bool" where
1.37 +definition countably_additive :: "('a, 'b) algebra_scheme \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
1.38    "countably_additive M f \<longleftrightarrow> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow>
1.39      (\<Sum>i. f (A i)) = f (\<Union>i. A i))"
1.40
1.41 @@ -168,7 +168,7 @@
1.43
1.44  lemma (in algebra) lambda_system_Compl:
1.45 -  fixes f:: "'a set \<Rightarrow> extreal"
1.46 +  fixes f:: "'a set \<Rightarrow> ereal"
1.47    assumes x: "x \<in> lambda_system M f"
1.48    shows "space M - x \<in> lambda_system M f"
1.49  proof -
1.50 @@ -181,7 +181,7 @@
1.51  qed
1.52
1.53  lemma (in algebra) lambda_system_Int:
1.54 -  fixes f:: "'a set \<Rightarrow> extreal"
1.55 +  fixes f:: "'a set \<Rightarrow> ereal"
1.56    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.57    shows "x \<inter> y \<in> lambda_system M f"
1.58  proof -
1.59 @@ -215,7 +215,7 @@
1.60  qed
1.61
1.62  lemma (in algebra) lambda_system_Un:
1.63 -  fixes f:: "'a set \<Rightarrow> extreal"
1.64 +  fixes f:: "'a set \<Rightarrow> ereal"
1.65    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
1.66    shows "x \<union> y \<in> lambda_system M f"
1.67  proof -
1.68 @@ -321,7 +321,7 @@
1.69  qed
1.70
1.72 -  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> extreal"
1.73 +  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> ereal"
1.75        and inc: "increasing M f"
1.76        and A: "range A \<subseteq> sets M"
1.77 @@ -346,7 +346,7 @@
1.78    by (simp add: positive_def lambda_system_def)
1.79
1.80  lemma (in algebra) lambda_system_strong_sum:
1.81 -  fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> extreal"
1.82 +  fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> ereal"
1.83    assumes f: "positive M f" and a: "a \<in> sets M"
1.84        and A: "range A \<subseteq> lambda_system M f"
1.85        and disj: "disjoint_family A"
1.86 @@ -537,7 +537,7 @@
1.87    assumes posf: "positive M f" and ca: "countably_additive M f"
1.88        and s: "s \<in> sets M"
1.89    shows "Inf (measure_set M f s) = f s"
1.90 -  unfolding Inf_extreal_def
1.91 +  unfolding Inf_ereal_def
1.92  proof (safe intro!: Greatest_equality)
1.93    fix z
1.94    assume z: "z \<in> measure_set M f s"
1.95 @@ -648,7 +648,7 @@
1.96  qed
1.97
1.98  lemma (in ring_of_sets) inf_measure_close:
1.99 -  fixes e :: extreal
1.100 +  fixes e :: ereal
1.101    assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
1.102    shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
1.103                 (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
1.104 @@ -656,7 +656,7 @@
1.105    from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
1.106      using inf_measure_pos[OF posf, of s] by auto
1.107    obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
1.108 -    using Inf_extreal_close[OF fin e] by auto
1.109 +    using Inf_ereal_close[OF fin e] by auto
1.110    thus ?thesis
1.111      by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
1.112  qed
1.113 @@ -672,11 +672,11 @@
1.114       and disj: "disjoint_family A"
1.115       and sb: "(\<Union>i. A i) \<subseteq> space M"
1.116
1.117 -  { fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
1.118 +  { fix e :: ereal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
1.119      hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
1.120          A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
1.121        apply (safe intro!: choice inf_measure_close [of f, OF posf])
1.122 -      using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def)
1.123 +      using e sb by (auto simp: ereal_zero_less_0_iff one_ereal_def)
1.124      then obtain BB
1.125        where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
1.126        and disjBB: "\<And>n. disjoint_family (BB n)"
1.127 @@ -686,15 +686,15 @@
1.128      have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
1.129      proof -
1.130        have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
1.131 -        using suminf_half_series_extreal e
1.132 -        by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal)
1.133 +        using suminf_half_series_ereal e
1.134 +        by (simp add: ereal_zero_le_0_iff zero_le_divide_ereal suminf_cmult_ereal)
1.135        have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
1.136        then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
1.137        then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
1.138          by (rule suminf_le_pos[OF BBle])
1.139        also have "... = (\<Sum>n. ?outer (A n)) + e"
1.140          using sum_eq_1 inf_measure_pos[OF posf] e
1.143        finally show ?thesis .
1.144      qed
1.145      def C \<equiv> "(split BB) o prod_decode"
1.146 @@ -716,7 +716,7 @@
1.147        by (rule ext)  (auto simp add: C_def)
1.148      moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
1.149        using BB posf[unfolded positive_def]
1.150 -      by (force intro!: suminf_extreal_2dimen simp: o_def)
1.151 +      by (force intro!: suminf_ereal_2dimen simp: o_def)
1.152      ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
1.153      have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
1.154        apply (rule inf_measure_le [OF posf(1) inc], auto)
1.155 @@ -732,7 +732,7 @@
1.156    proof cases
1.157      assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
1.158      with for_finite_Inf show ?thesis
1.159 -      by (intro extreal_le_epsilon) auto
1.160 +      by (intro ereal_le_epsilon) auto
1.161    next
1.162      assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
1.163      then have "\<exists>i. ?outer (A i) = \<infinity>"
1.164 @@ -771,7 +771,7 @@
1.165    next
1.166      assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
1.167      then have "measure_set M f s \<noteq> {}"
1.168 -      by (auto simp: top_extreal_def)
1.169 +      by (auto simp: top_ereal_def)
1.170      show ?thesis
1.171      proof (rule complete_lattice_class.Inf_greatest)
1.172        fix r assume "r \<in> measure_set M f s"
1.173 @@ -793,7 +793,7 @@
1.174        ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
1.175            (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
1.176        also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
1.177 -        using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def)
1.178 +        using A(2) x posf by (subst suminf_add_ereal) (auto simp: positive_def)
1.179        also have "\<dots> = (\<Sum>i. f (A i))"
1.180          using A x
1.182 @@ -830,7 +830,7 @@
1.183
1.184  theorem (in ring_of_sets) caratheodory:
1.185    assumes posf: "positive M f" and ca: "countably_additive M f"
1.186 -  shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
1.187 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
1.188              measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
1.189  proof -
1.190    have inc: "increasing M f"
1.191 @@ -873,7 +873,7 @@
1.192      by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
1.193    moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
1.194      using f(1)[unfolded positive_def] dA
1.195 -    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_extreal_pos)
1.196 +    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_ereal_pos)
1.197    from LIMSEQ_Suc[OF this]
1.198    have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
1.199      unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
1.200 @@ -936,13 +936,13 @@
1.201      show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> sets M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
1.202        using A by auto
1.203    qed
1.204 -  from INF_Lim_extreal[OF decseq_f this]
1.205 +  from INF_Lim_ereal[OF decseq_f this]
1.206    have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
1.207    moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
1.208      by auto
1.209    ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
1.210      using A(4) f_fin f_Int_fin
1.211 -    by (subst INFI_extreal_add) (auto simp: decseq_f)
1.212 +    by (subst INFI_ereal_add) (auto simp: decseq_f)
1.213    moreover {
1.214      fix n
1.215      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.216 @@ -952,7 +952,7 @@
1.217      finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
1.218    ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
1.219      by simp
1.220 -  with LIMSEQ_extreal_INFI[OF decseq_fA]
1.221 +  with LIMSEQ_ereal_INFI[OF decseq_fA]
1.222    show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
1.223  qed
1.224
1.225 @@ -965,9 +965,9 @@
1.226    assumes A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
1.227    shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
1.228  proof -
1.229 -  have "\<forall>A\<in>sets M. \<exists>x. f A = extreal x"
1.230 +  have "\<forall>A\<in>sets M. \<exists>x. f A = ereal x"
1.231    proof
1.232 -    fix A assume "A \<in> sets M" with f show "\<exists>x. f A = extreal x"
1.233 +    fix A assume "A \<in> sets M" with f show "\<exists>x. f A = ereal x"
1.234        unfolding positive_def by (cases "f A") auto
1.235    qed
1.236    from bchoice[OF this] guess f' .. note f' = this[rule_format]
1.237 @@ -981,10 +981,10 @@
1.238        by auto
1.239      finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
1.240        using A by (subst (asm) (1 2 3) f') auto
1.241 -    then have "f ((\<Union>i. A i) - A i) = extreal (f' (\<Union>i. A i) - f' (A i))"
1.242 +    then have "f ((\<Union>i. A i) - A i) = ereal (f' (\<Union>i. A i) - f' (A i))"
1.243        using A f' by auto }
1.244    ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
1.245 -    by (simp add: zero_extreal_def)
1.246 +    by (simp add: zero_ereal_def)
1.247    then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
1.248      by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
1.249    then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
1.250 @@ -1002,7 +1002,7 @@
1.251  lemma (in ring_of_sets) caratheodory_empty_continuous:
1.252    assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> sets M \<Longrightarrow> f A \<noteq> \<infinity>"
1.253    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.254 -  shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
1.255 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
1.256              measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
1.257  proof (intro caratheodory empty_continuous_imp_countably_additive f)
1.258    show "\<forall>A\<in>sets M. f A \<noteq> \<infinity>" using fin by auto
```