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.33  definition additive where "additive M f \<longleftrightarrow>
    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.42    by (simp add: lambda_system_def)
    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.71  lemma (in algebra) increasing_additive_bound:
    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.74    assumes f: "positive M f" and ad: "additive M f"
    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.141 -        by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff)
   1.142 +        by (subst suminf_add_ereal) (auto simp add: ereal_zero_le_0_iff)
   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.181          by (subst add[THEN additiveD, symmetric])
   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