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.10  definition subadditive where "subadditive M f \<longleftrightarrow>
    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.24    by (auto simp add: subadditive_def)
    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.35    by (simp add: measure_space_def positive_def countably_additive_def)
    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>"