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.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.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.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.58
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.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.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"