src/HOL/Probability/Caratheodory.thy
 changeset 56994 8d5e5ec1cac3 parent 56212 3253aaf73a01 child 57418 6ab1c7cb0b8d
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon May 19 12:04:45 2014 +0200
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon May 19 13:44:13 2014 +0200
1.3 @@ -45,7 +45,7 @@
1.4                       SUP_ereal_setsum[symmetric] incseq_setsumI setsum_nonneg)
1.5  qed
1.6
1.7 -subsection {* Measure Spaces *}
1.8 +subsection {* Characterizations of Measures *}
1.9
1.11    (\<forall>x\<in>M. \<forall>y\<in>M. x \<inter> y = {} \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
1.12 @@ -54,9 +54,6 @@
1.13    (\<forall>A. range A \<subseteq> M \<longrightarrow> disjoint_family A \<longrightarrow> (\<Union>i. A i) \<in> M \<longrightarrow>
1.14      (f (\<Union>i. A i) \<le> (\<Sum>i. f (A i))))"
1.15
1.16 -definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
1.17 -  \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
1.18 -
1.19  definition outer_measure_space where "outer_measure_space M f \<longleftrightarrow>
1.20    positive M f \<and> increasing M f \<and> countably_subadditive M f"
1.21
1.22 @@ -67,7 +64,10 @@
1.23    "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x \<in> M \<Longrightarrow> y \<in> M \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
1.25
1.26 -subsection {* Lambda Systems *}
1.27 +subsubsection {* Lambda Systems *}
1.28 +
1.29 +definition lambda_system where "lambda_system \<Omega> M f = {l \<in> M.
1.30 +  \<forall>x \<in> M. f (l \<inter> x) + f ((\<Omega> - l) \<inter> x) = f x}"
1.31
1.32  lemma (in algebra) lambda_system_eq:
1.33    shows "lambda_system \<Omega> M f = {l \<in> M. \<forall>x \<in> M. f (x \<inter> l) + f (x - l) = f x}"
1.34 @@ -643,6 +643,8 @@
1.36       blast
1.37
1.38 +subsection {* Caratheodory's theorem *}
1.39 +
1.40  theorem (in ring_of_sets) caratheodory':
1.41    assumes posf: "positive M f" and ca: "countably_additive M f"
1.42    shows "\<exists>\<mu> :: 'a set \<Rightarrow> ereal. (\<forall>s \<in> M. \<mu> s = f s) \<and> measure_space \<Omega> (sigma_sets \<Omega> M) \<mu>"
1.43 @@ -670,8 +672,6 @@
1.44      by (intro exI[of _ ?infm]) auto
1.45  qed
1.46
1.47 -subsubsection {*Alternative instances of caratheodory*}
1.48 -
1.49  lemma (in ring_of_sets) caratheodory_empty_continuous:
1.50    assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> M \<Longrightarrow> f A \<noteq> \<infinity>"
1.51    assumes cont: "\<And>A. range A \<subseteq> M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
1.52 @@ -680,7 +680,7 @@
1.53    show "\<forall>A\<in>M. f A \<noteq> \<infinity>" using fin by auto
1.54  qed (rule cont)
1.55
1.56 -section {* Volumes *}
1.57 +subsection {* Volumes *}
1.58
1.59  definition volume :: "'a set set \<Rightarrow> ('a set \<Rightarrow> ereal) \<Rightarrow> bool" where
1.60    "volume M f \<longleftrightarrow>
1.61 @@ -818,7 +818,7 @@
1.62    qed
1.63  qed
1.64
1.65 -section {* Caratheodory on semirings *}
1.66 +subsubsection {* Caratheodory on semirings *}
1.67
1.68  theorem (in semiring_of_sets) caratheodory:
1.69    assumes pos: "positive M \<mu>" and ca: "countably_additive M \<mu>"
```