src/HOL/Probability/Caratheodory.thy
changeset 41023 9118eb4eb8dc
parent 40859 de0b30e6c2d2
child 41689 3e39b0e730d6
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Dec 06 19:18:02 2010 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Fri Dec 03 15:25:14 2010 +0100
     1.3 @@ -1,14 +1,14 @@
     1.4  header {*Caratheodory Extension Theorem*}
     1.5  
     1.6  theory Caratheodory
     1.7 -  imports Sigma_Algebra Positive_Infinite_Real
     1.8 +  imports Sigma_Algebra Positive_Extended_Real
     1.9  begin
    1.10  
    1.11  text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    1.12  
    1.13  subsection {* Measure Spaces *}
    1.14  
    1.15 -definition "positive f \<longleftrightarrow> f {} = (0::pinfreal)" -- "Positive is enforced by the type"
    1.16 +definition "positive f \<longleftrightarrow> f {} = (0::pextreal)" -- "Positive is enforced by the type"
    1.17  
    1.18  definition
    1.19    additive  where
    1.20 @@ -58,7 +58,7 @@
    1.21       {r . \<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> X \<subseteq> (\<Union>i. A i) \<and> (\<Sum>\<^isub>\<infinity> i. f (A i)) = r}"
    1.22  
    1.23  locale measure_space = sigma_algebra +
    1.24 -  fixes \<mu> :: "'a set \<Rightarrow> pinfreal"
    1.25 +  fixes \<mu> :: "'a set \<Rightarrow> pextreal"
    1.26    assumes empty_measure [simp]: "\<mu> {} = 0"
    1.27        and ca: "countably_additive M \<mu>"
    1.28  
    1.29 @@ -148,7 +148,7 @@
    1.30    by (simp add:  lambda_system_def)
    1.31  
    1.32  lemma (in algebra) lambda_system_Compl:
    1.33 -  fixes f:: "'a set \<Rightarrow> pinfreal"
    1.34 +  fixes f:: "'a set \<Rightarrow> pextreal"
    1.35    assumes x: "x \<in> lambda_system M f"
    1.36    shows "space M - x \<in> lambda_system M f"
    1.37    proof -
    1.38 @@ -161,7 +161,7 @@
    1.39    qed
    1.40  
    1.41  lemma (in algebra) lambda_system_Int:
    1.42 -  fixes f:: "'a set \<Rightarrow> pinfreal"
    1.43 +  fixes f:: "'a set \<Rightarrow> pextreal"
    1.44    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
    1.45    shows "x \<inter> y \<in> lambda_system M f"
    1.46    proof -
    1.47 @@ -196,7 +196,7 @@
    1.48  
    1.49  
    1.50  lemma (in algebra) lambda_system_Un:
    1.51 -  fixes f:: "'a set \<Rightarrow> pinfreal"
    1.52 +  fixes f:: "'a set \<Rightarrow> pextreal"
    1.53    assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
    1.54    shows "x \<union> y \<in> lambda_system M f"
    1.55  proof -
    1.56 @@ -295,7 +295,7 @@
    1.57    by (auto simp add: countably_subadditive_def o_def)
    1.58  
    1.59  lemma (in algebra) increasing_additive_bound:
    1.60 -  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pinfreal"
    1.61 +  fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pextreal"
    1.62    assumes f: "positive f" and ad: "additive M f"
    1.63        and inc: "increasing M f"
    1.64        and A: "range A \<subseteq> sets M"
    1.65 @@ -315,7 +315,7 @@
    1.66    by (simp add: increasing_def lambda_system_def)
    1.67  
    1.68  lemma (in algebra) lambda_system_strong_sum:
    1.69 -  fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal"
    1.70 +  fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pextreal"
    1.71    assumes f: "positive f" and a: "a \<in> sets M"
    1.72        and A: "range A \<subseteq> lambda_system M f"
    1.73        and disj: "disjoint_family A"
    1.74 @@ -497,7 +497,7 @@
    1.75    assumes posf: "positive f" and ca: "countably_additive M f"
    1.76        and s: "s \<in> sets M"
    1.77    shows "Inf (measure_set M f s) = f s"
    1.78 -  unfolding Inf_pinfreal_def
    1.79 +  unfolding Inf_pextreal_def
    1.80  proof (safe intro!: Greatest_equality)
    1.81    fix z
    1.82    assume z: "z \<in> measure_set M f s"
    1.83 @@ -608,8 +608,8 @@
    1.84    shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
    1.85                    (\<lambda>x. Inf (measure_set M f x))"
    1.86    unfolding countably_subadditive_def o_def
    1.87 -proof (safe, simp, rule pinfreal_le_epsilon)
    1.88 -  fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal
    1.89 +proof (safe, simp, rule pextreal_le_epsilon)
    1.90 +  fix A :: "nat \<Rightarrow> 'a set" and e :: pextreal
    1.91  
    1.92    let "?outer n" = "Inf (measure_set M f (A n))"
    1.93    assume A: "range A \<subseteq> Pow (space M)"
    1.94 @@ -688,8 +688,8 @@
    1.95      by blast
    1.96    have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
    1.97          \<le> Inf (measure_set M f s)"
    1.98 -    proof (rule pinfreal_le_epsilon)
    1.99 -      fix e :: pinfreal
   1.100 +    proof (rule pextreal_le_epsilon)
   1.101 +      fix e :: pextreal
   1.102        assume e: "0 < e"
   1.103        from inf_measure_close [of f, OF posf e s]
   1.104        obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   1.105 @@ -760,7 +760,7 @@
   1.106  
   1.107  theorem (in algebra) caratheodory:
   1.108    assumes posf: "positive f" and ca: "countably_additive M f"
   1.109 -  shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma M) \<mu>"
   1.110 +  shows "\<exists>\<mu> :: 'a set \<Rightarrow> pextreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma M) \<mu>"
   1.111    proof -
   1.112      have inc: "increasing M f"
   1.113        by (metis additive_increasing ca countably_additive_additive posf)