src/HOL/Probability/Caratheodory.thy
author hoelzl
Thu Sep 02 17:28:00 2010 +0200 (2010-09-02)
changeset 39096 111756225292
parent 38656 d5d342611edb
child 40859 de0b30e6c2d2
permissions -rw-r--r--
merged
     1 header {*Caratheodory Extension Theorem*}
     2 
     3 theory Caratheodory
     4   imports Sigma_Algebra Positive_Infinite_Real
     5 begin
     6 
     7 text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
     8 
     9 subsection {* Measure Spaces *}
    10 
    11 definition "positive f \<longleftrightarrow> f {} = (0::pinfreal)" -- "Positive is enforced by the type"
    12 
    13 definition
    14   additive  where
    15   "additive M f \<longleftrightarrow>
    16     (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
    17     \<longrightarrow> f (x \<union> y) = f x + f y)"
    18 
    19 definition
    20   countably_additive  where
    21   "countably_additive M f \<longleftrightarrow>
    22     (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
    23          disjoint_family A \<longrightarrow>
    24          (\<Union>i. A i) \<in> sets M \<longrightarrow>
    25          (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i))"
    26 
    27 definition
    28   increasing  where
    29   "increasing M f \<longleftrightarrow> (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<subseteq> y \<longrightarrow> f x \<le> f y)"
    30 
    31 definition
    32   subadditive  where
    33   "subadditive M f \<longleftrightarrow>
    34     (\<forall>x \<in> sets M. \<forall>y \<in> sets M. x \<inter> y = {}
    35     \<longrightarrow> f (x \<union> y) \<le> f x + f y)"
    36 
    37 definition
    38   countably_subadditive  where
    39   "countably_subadditive M f \<longleftrightarrow>
    40     (\<forall>A. range A \<subseteq> sets M \<longrightarrow>
    41          disjoint_family A \<longrightarrow>
    42          (\<Union>i. A i) \<in> sets M \<longrightarrow>
    43          f (\<Union>i. A i) \<le> psuminf (\<lambda>n. f (A n)))"
    44 
    45 definition
    46   lambda_system where
    47   "lambda_system M f =
    48     {l. l \<in> sets M & (\<forall>x \<in> sets M. f (l \<inter> x) + f ((space M - l) \<inter> x) = f x)}"
    49 
    50 definition
    51   outer_measure_space where
    52   "outer_measure_space M f  \<longleftrightarrow>
    53      positive f \<and> increasing M f \<and> countably_subadditive M f"
    54 
    55 definition
    56   measure_set where
    57   "measure_set M f X =
    58      {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}"
    59 
    60 locale measure_space = sigma_algebra +
    61   fixes \<mu> :: "'a set \<Rightarrow> pinfreal"
    62   assumes empty_measure [simp]: "\<mu> {} = 0"
    63       and ca: "countably_additive M \<mu>"
    64 
    65 lemma increasingD:
    66      "increasing M f \<Longrightarrow> x \<subseteq> y \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M \<Longrightarrow> f x \<le> f y"
    67   by (auto simp add: increasing_def)
    68 
    69 lemma subadditiveD:
    70      "subadditive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
    71       \<Longrightarrow> f (x \<union> y) \<le> f x + f y"
    72   by (auto simp add: subadditive_def)
    73 
    74 lemma additiveD:
    75      "additive M f \<Longrightarrow> x \<inter> y = {} \<Longrightarrow> x\<in>sets M \<Longrightarrow> y\<in>sets M
    76       \<Longrightarrow> f (x \<union> y) = f x + f y"
    77   by (auto simp add: additive_def)
    78 
    79 lemma countably_additiveD:
    80   "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
    81    \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<Sum>\<^isub>\<infinity> n. f (A n)) = f (\<Union>i. A i)"
    82   by (simp add: countably_additive_def)
    83 
    84 section "Extend binary sets"
    85 
    86 lemma LIMSEQ_binaryset:
    87   assumes f: "f {} = 0"
    88   shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
    89 proof -
    90   have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
    91     proof
    92       fix n
    93       show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
    94         by (induct n)  (auto simp add: binaryset_def f)
    95     qed
    96   moreover
    97   have "... ----> f A + f B" by (rule LIMSEQ_const)
    98   ultimately
    99   have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
   100     by metis
   101   hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
   102     by simp
   103   thus ?thesis by (rule LIMSEQ_offset [where k=2])
   104 qed
   105 
   106 lemma binaryset_sums:
   107   assumes f: "f {} = 0"
   108   shows  "(\<lambda>n. f (binaryset A B n)) sums (f A + f B)"
   109     by (simp add: sums_def LIMSEQ_binaryset [where f=f, OF f])
   110 
   111 lemma suminf_binaryset_eq:
   112      "f {} = 0 \<Longrightarrow> suminf (\<lambda>n. f (binaryset A B n)) = f A + f B"
   113   by (metis binaryset_sums sums_unique)
   114 
   115 lemma binaryset_psuminf:
   116   assumes "f {} = 0"
   117   shows "(\<Sum>\<^isub>\<infinity> n. f (binaryset A B n)) = f A + f B" (is "?suminf = ?sum")
   118 proof -
   119   have *: "{..<2} = {0, 1::nat}" by auto
   120   have "\<forall>n\<ge>2. f (binaryset A B n) = 0"
   121     unfolding binaryset_def
   122     using assms by auto
   123   hence "?suminf = (\<Sum>N<2. f (binaryset A B N))"
   124     by (rule psuminf_finite)
   125   also have "... = ?sum" unfolding * binaryset_def
   126     by simp
   127   finally show ?thesis .
   128 qed
   129 
   130 subsection {* Lambda Systems *}
   131 
   132 lemma (in algebra) lambda_system_eq:
   133     "lambda_system M f =
   134         {l. l \<in> sets M & (\<forall>x \<in> sets M. f (x \<inter> l) + f (x - l) = f x)}"
   135 proof -
   136   have [simp]: "!!l x. l \<in> sets M \<Longrightarrow> x \<in> sets M \<Longrightarrow> (space M - l) \<inter> x = x - l"
   137     by (metis Int_Diff Int_absorb1 Int_commute sets_into_space)
   138   show ?thesis
   139     by (auto simp add: lambda_system_def) (metis Int_commute)+
   140 qed
   141 
   142 lemma (in algebra) lambda_system_empty:
   143   "positive f \<Longrightarrow> {} \<in> lambda_system M f"
   144   by (auto simp add: positive_def lambda_system_eq)
   145 
   146 lemma lambda_system_sets:
   147     "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
   148   by (simp add:  lambda_system_def)
   149 
   150 lemma (in algebra) lambda_system_Compl:
   151   fixes f:: "'a set \<Rightarrow> pinfreal"
   152   assumes x: "x \<in> lambda_system M f"
   153   shows "space M - x \<in> lambda_system M f"
   154   proof -
   155     have "x \<subseteq> space M"
   156       by (metis sets_into_space lambda_system_sets x)
   157     hence "space M - (space M - x) = x"
   158       by (metis double_diff equalityE)
   159     with x show ?thesis
   160       by (force simp add: lambda_system_def ac_simps)
   161   qed
   162 
   163 lemma (in algebra) lambda_system_Int:
   164   fixes f:: "'a set \<Rightarrow> pinfreal"
   165   assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   166   shows "x \<inter> y \<in> lambda_system M f"
   167   proof -
   168     from xl yl show ?thesis
   169       proof (auto simp add: positive_def lambda_system_eq Int)
   170         fix u
   171         assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
   172            and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
   173            and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
   174         have "u - x \<inter> y \<in> sets M"
   175           by (metis Diff Diff_Int Un u x y)
   176         moreover
   177         have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
   178         moreover
   179         have "u - x \<inter> y - y = u - y" by blast
   180         ultimately
   181         have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
   182           by force
   183         have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y)
   184               = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
   185           by (simp add: ey ac_simps)
   186         also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
   187           by (simp add: Int_ac)
   188         also have "... = f (u \<inter> y) + f (u - y)"
   189           using fx [THEN bspec, of "u \<inter> y"] Int y u
   190           by force
   191         also have "... = f u"
   192           by (metis fy u)
   193         finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
   194       qed
   195   qed
   196 
   197 
   198 lemma (in algebra) lambda_system_Un:
   199   fixes f:: "'a set \<Rightarrow> pinfreal"
   200   assumes xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   201   shows "x \<union> y \<in> lambda_system M f"
   202 proof -
   203   have "(space M - x) \<inter> (space M - y) \<in> sets M"
   204     by (metis Diff_Un Un compl_sets lambda_system_sets xl yl)
   205   moreover
   206   have "x \<union> y = space M - ((space M - x) \<inter> (space M - y))"
   207     by auto  (metis subsetD lambda_system_sets sets_into_space xl yl)+
   208   ultimately show ?thesis
   209     by (metis lambda_system_Compl lambda_system_Int xl yl)
   210 qed
   211 
   212 lemma (in algebra) lambda_system_algebra:
   213   "positive f \<Longrightarrow> algebra (M (|sets := lambda_system M f|))"
   214   apply (auto simp add: algebra_def)
   215   apply (metis lambda_system_sets set_mp sets_into_space)
   216   apply (metis lambda_system_empty)
   217   apply (metis lambda_system_Compl)
   218   apply (metis lambda_system_Un)
   219   done
   220 
   221 lemma (in algebra) lambda_system_strong_additive:
   222   assumes z: "z \<in> sets M" and disj: "x \<inter> y = {}"
   223       and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   224   shows "f (z \<inter> (x \<union> y)) = f (z \<inter> x) + f (z \<inter> y)"
   225   proof -
   226     have "z \<inter> x = (z \<inter> (x \<union> y)) \<inter> x" using disj by blast
   227     moreover
   228     have "z \<inter> y = (z \<inter> (x \<union> y)) - x" using disj by blast
   229     moreover
   230     have "(z \<inter> (x \<union> y)) \<in> sets M"
   231       by (metis Int Un lambda_system_sets xl yl z)
   232     ultimately show ?thesis using xl yl
   233       by (simp add: lambda_system_eq)
   234   qed
   235 
   236 lemma (in algebra) lambda_system_additive:
   237      "additive (M (|sets := lambda_system M f|)) f"
   238   proof (auto simp add: additive_def)
   239     fix x and y
   240     assume disj: "x \<inter> y = {}"
   241        and xl: "x \<in> lambda_system M f" and yl: "y \<in> lambda_system M f"
   242     hence  "x \<in> sets M" "y \<in> sets M" by (blast intro: lambda_system_sets)+
   243     thus "f (x \<union> y) = f x + f y"
   244       using lambda_system_strong_additive [OF top disj xl yl]
   245       by (simp add: Un)
   246   qed
   247 
   248 
   249 lemma (in algebra) countably_subadditive_subadditive:
   250   assumes f: "positive f" and cs: "countably_subadditive M f"
   251   shows  "subadditive M f"
   252 proof (auto simp add: subadditive_def)
   253   fix x y
   254   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   255   hence "disjoint_family (binaryset x y)"
   256     by (auto simp add: disjoint_family_on_def binaryset_def)
   257   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
   258          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
   259          f (\<Union>i. binaryset x y i) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   260     using cs by (simp add: countably_subadditive_def)
   261   hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
   262          f (x \<union> y) \<le> (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   263     by (simp add: range_binaryset_eq UN_binaryset_eq)
   264   thus "f (x \<union> y) \<le>  f x + f y" using f x y
   265     by (auto simp add: Un o_def binaryset_psuminf positive_def)
   266 qed
   267 
   268 lemma (in algebra) additive_sum:
   269   fixes A:: "nat \<Rightarrow> 'a set"
   270   assumes f: "positive f" and ad: "additive M f"
   271       and A: "range A \<subseteq> sets M"
   272       and disj: "disjoint_family A"
   273   shows  "setsum (f \<circ> A) {0..<n} = f (\<Union>i\<in>{0..<n}. A i)"
   274 proof (induct n)
   275   case 0 show ?case using f by (simp add: positive_def)
   276 next
   277   case (Suc n)
   278   have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
   279     by (auto simp add: disjoint_family_on_def neq_iff) blast
   280   moreover
   281   have "A n \<in> sets M" using A by blast
   282   moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   283     by (metis A UNION_in_sets atLeast0LessThan)
   284   moreover
   285   ultimately have "f (A n \<union> (\<Union>i\<in>{0..<n}. A i)) = f (A n) + f(\<Union>i\<in>{0..<n}. A i)"
   286     using ad UNION_in_sets A by (auto simp add: additive_def)
   287   with Suc.hyps show ?case using ad
   288     by (auto simp add: atLeastLessThanSuc additive_def)
   289 qed
   290 
   291 
   292 lemma countably_subadditiveD:
   293   "countably_subadditive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow>
   294    (\<Union>i. A i) \<in> sets M \<Longrightarrow> f (\<Union>i. A i) \<le> psuminf (f o A)"
   295   by (auto simp add: countably_subadditive_def o_def)
   296 
   297 lemma (in algebra) increasing_additive_bound:
   298   fixes A:: "nat \<Rightarrow> 'a set" and  f :: "'a set \<Rightarrow> pinfreal"
   299   assumes f: "positive f" and ad: "additive M f"
   300       and inc: "increasing M f"
   301       and A: "range A \<subseteq> sets M"
   302       and disj: "disjoint_family A"
   303   shows  "psuminf (f \<circ> A) \<le> f (space M)"
   304 proof (safe intro!: psuminf_bound)
   305   fix N
   306   have "setsum (f \<circ> A) {0..<N} = f (\<Union>i\<in>{0..<N}. A i)"
   307     by (rule additive_sum [OF f ad A disj])
   308   also have "... \<le> f (space M)" using space_closed A
   309     by (blast intro: increasingD [OF inc] UNION_in_sets top)
   310   finally show "setsum (f \<circ> A) {..<N} \<le> f (space M)" by (simp add: atLeast0LessThan)
   311 qed
   312 
   313 lemma lambda_system_increasing:
   314    "increasing M f \<Longrightarrow> increasing (M (|sets := lambda_system M f|)) f"
   315   by (simp add: increasing_def lambda_system_def)
   316 
   317 lemma (in algebra) lambda_system_strong_sum:
   318   fixes A:: "nat \<Rightarrow> 'a set" and f :: "'a set \<Rightarrow> pinfreal"
   319   assumes f: "positive f" and a: "a \<in> sets M"
   320       and A: "range A \<subseteq> lambda_system M f"
   321       and disj: "disjoint_family A"
   322   shows  "(\<Sum>i = 0..<n. f (a \<inter>A i)) = f (a \<inter> (\<Union>i\<in>{0..<n}. A i))"
   323 proof (induct n)
   324   case 0 show ?case using f by (simp add: positive_def)
   325 next
   326   case (Suc n)
   327   have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
   328     by (force simp add: disjoint_family_on_def neq_iff)
   329   have 3: "A n \<in> lambda_system M f" using A
   330     by blast
   331   have 4: "UNION {0..<n} A \<in> lambda_system M f"
   332     using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
   333     by simp
   334   from Suc.hyps show ?case
   335     by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
   336 qed
   337 
   338 
   339 lemma (in sigma_algebra) lambda_system_caratheodory:
   340   assumes oms: "outer_measure_space M f"
   341       and A: "range A \<subseteq> lambda_system M f"
   342       and disj: "disjoint_family A"
   343   shows  "(\<Union>i. A i) \<in> lambda_system M f \<and> psuminf (f \<circ> A) = f (\<Union>i. A i)"
   344 proof -
   345   have pos: "positive f" and inc: "increasing M f"
   346    and csa: "countably_subadditive M f"
   347     by (metis oms outer_measure_space_def)+
   348   have sa: "subadditive M f"
   349     by (metis countably_subadditive_subadditive csa pos)
   350   have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
   351     by simp
   352   have alg_ls: "algebra (M(|sets := lambda_system M f|))"
   353     by (rule lambda_system_algebra) (rule pos)
   354   have A'': "range A \<subseteq> sets M"
   355      by (metis A image_subset_iff lambda_system_sets)
   356 
   357   have U_in: "(\<Union>i. A i) \<in> sets M"
   358     by (metis A'' countable_UN)
   359   have U_eq: "f (\<Union>i. A i) = psuminf (f o A)"
   360     proof (rule antisym)
   361       show "f (\<Union>i. A i) \<le> psuminf (f \<circ> A)"
   362         by (rule countably_subadditiveD [OF csa A'' disj U_in])
   363       show "psuminf (f \<circ> A) \<le> f (\<Union>i. A i)"
   364         by (rule psuminf_bound, unfold atLeast0LessThan[symmetric])
   365            (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
   366                   lambda_system_additive subset_Un_eq increasingD [OF inc]
   367                   A' A'' UNION_in_sets U_in)
   368     qed
   369   {
   370     fix a
   371     assume a [iff]: "a \<in> sets M"
   372     have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
   373     proof -
   374       show ?thesis
   375       proof (rule antisym)
   376         have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
   377           by blast
   378         moreover
   379         have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   380           by (auto simp add: disjoint_family_on_def)
   381         moreover
   382         have "a \<inter> (\<Union>i. A i) \<in> sets M"
   383           by (metis Int U_in a)
   384         ultimately
   385         have "f (a \<inter> (\<Union>i. A i)) \<le> psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
   386           using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"]
   387           by (simp add: o_def)
   388         hence "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le>
   389             psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i))"
   390           by (rule add_right_mono)
   391         moreover
   392         have "psuminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) + f (a - (\<Union>i. A i)) \<le> f a"
   393           proof (safe intro!: psuminf_bound_add)
   394             fix n
   395             have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   396               by (metis A'' UNION_in_sets)
   397             have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   398               by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
   399             have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
   400               using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
   401               by (simp add: A)
   402             hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
   403               by (simp add: lambda_system_eq UNION_in)
   404             have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   405               by (blast intro: increasingD [OF inc] UNION_eq_Union_image
   406                                UNION_in U_in)
   407             thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {..<n} + f (a - (\<Union>i. A i)) \<le> f a"
   408               by (simp add: lambda_system_strong_sum pos A disj eq_fa add_left_mono atLeast0LessThan[symmetric])
   409           qed
   410         ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a"
   411           by (rule order_trans)
   412       next
   413         have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))"
   414           by (blast intro:  increasingD [OF inc] U_in)
   415         also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   416           by (blast intro: subadditiveD [OF sa] U_in)
   417         finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   418         qed
   419      qed
   420   }
   421   thus  ?thesis
   422     by (simp add: lambda_system_eq sums_iff U_eq U_in)
   423 qed
   424 
   425 lemma (in sigma_algebra) caratheodory_lemma:
   426   assumes oms: "outer_measure_space M f"
   427   shows "measure_space (|space = space M, sets = lambda_system M f|) f"
   428 proof -
   429   have pos: "positive f"
   430     by (metis oms outer_measure_space_def)
   431   have alg: "algebra (|space = space M, sets = lambda_system M f|)"
   432     using lambda_system_algebra [of f, OF pos]
   433     by (simp add: algebra_def)
   434   then moreover
   435   have "sigma_algebra (|space = space M, sets = lambda_system M f|)"
   436     using lambda_system_caratheodory [OF oms]
   437     by (simp add: sigma_algebra_disjoint_iff)
   438   moreover
   439   have "measure_space_axioms (|space = space M, sets = lambda_system M f|) f"
   440     using pos lambda_system_caratheodory [OF oms]
   441     by (simp add: measure_space_axioms_def positive_def lambda_system_sets
   442                   countably_additive_def o_def)
   443   ultimately
   444   show ?thesis
   445     by intro_locales (auto simp add: sigma_algebra_def)
   446 qed
   447 
   448 lemma (in algebra) additive_increasing:
   449   assumes posf: "positive f" and addf: "additive M f"
   450   shows "increasing M f"
   451 proof (auto simp add: increasing_def)
   452   fix x y
   453   assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
   454   have "f x \<le> f x + f (y-x)" ..
   455   also have "... = f (x \<union> (y-x))" using addf
   456     by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
   457   also have "... = f y"
   458     by (metis Un_Diff_cancel Un_absorb1 xy(3))
   459   finally show "f x \<le> f y" .
   460 qed
   461 
   462 lemma (in algebra) countably_additive_additive:
   463   assumes posf: "positive f" and ca: "countably_additive M f"
   464   shows "additive M f"
   465 proof (auto simp add: additive_def)
   466   fix x y
   467   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   468   hence "disjoint_family (binaryset x y)"
   469     by (auto simp add: disjoint_family_on_def binaryset_def)
   470   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
   471          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
   472          f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   473     using ca
   474     by (simp add: countably_additive_def)
   475   hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
   476          f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   477     by (simp add: range_binaryset_eq UN_binaryset_eq)
   478   thus "f (x \<union> y) = f x + f y" using posf x y
   479     by (auto simp add: Un binaryset_psuminf positive_def)
   480 qed
   481 
   482 lemma inf_measure_nonempty:
   483   assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b" "{} \<in> sets M"
   484   shows "f b \<in> measure_set M f a"
   485 proof -
   486   have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
   487     by (rule psuminf_finite) (simp add: f[unfolded positive_def])
   488   also have "... = f b"
   489     by simp
   490   finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
   491   thus ?thesis using assms
   492     by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
   493              simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
   494 qed
   495 
   496 lemma (in algebra) inf_measure_agrees:
   497   assumes posf: "positive f" and ca: "countably_additive M f"
   498       and s: "s \<in> sets M"
   499   shows "Inf (measure_set M f s) = f s"
   500   unfolding Inf_pinfreal_def
   501 proof (safe intro!: Greatest_equality)
   502   fix z
   503   assume z: "z \<in> measure_set M f s"
   504   from this obtain A where
   505     A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   506     and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z"
   507     by (auto simp add: measure_set_def comp_def)
   508   hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
   509   have inc: "increasing M f"
   510     by (metis additive_increasing ca countably_additive_additive posf)
   511   have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
   512     proof (rule countably_additiveD [OF ca])
   513       show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   514         by blast
   515       show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   516         by (auto simp add: disjoint_family_on_def)
   517       show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   518         by (metis UN_extend_simps(4) s seq)
   519     qed
   520   hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))"
   521     using seq [symmetric] by (simp add: sums_iff)
   522   also have "... \<le> psuminf (f \<circ> A)"
   523     proof (rule psuminf_le)
   524       fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
   525         by (force intro: increasingD [OF inc])
   526     qed
   527   also have "... = z" by (rule si)
   528   finally show "f s \<le> z" .
   529 next
   530   fix y
   531   assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
   532   thus "y \<le> f s"
   533     by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl])
   534 qed
   535 
   536 lemma (in algebra) inf_measure_empty:
   537   assumes posf: "positive f"  "{} \<in> sets M"
   538   shows "Inf (measure_set M f {}) = 0"
   539 proof (rule antisym)
   540   show "Inf (measure_set M f {}) \<le> 0"
   541     by (metis complete_lattice_class.Inf_lower `{} \<in> sets M` inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
   542 qed simp
   543 
   544 lemma (in algebra) inf_measure_positive:
   545   "positive f \<Longrightarrow>
   546    positive (\<lambda>x. Inf (measure_set M f x))"
   547   by (simp add: positive_def inf_measure_empty) 
   548 
   549 lemma (in algebra) inf_measure_increasing:
   550   assumes posf: "positive f"
   551   shows "increasing (| space = space M, sets = Pow (space M) |)
   552                     (\<lambda>x. Inf (measure_set M f x))"
   553 apply (auto simp add: increasing_def)
   554 apply (rule complete_lattice_class.Inf_greatest)
   555 apply (rule complete_lattice_class.Inf_lower)
   556 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
   557 done
   558 
   559 
   560 lemma (in algebra) inf_measure_le:
   561   assumes posf: "positive f" and inc: "increasing M f"
   562       and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> psuminf (f \<circ> A) = r}"
   563   shows "Inf (measure_set M f s) \<le> x"
   564 proof -
   565   from x
   566   obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
   567              and xeq: "psuminf (f \<circ> A) = x"
   568     by auto
   569   have dA: "range (disjointed A) \<subseteq> sets M"
   570     by (metis A range_disjointed_sets)
   571   have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def
   572     by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
   573   hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)"
   574     by (blast intro: psuminf_le)
   575   hence ley: "psuminf (f o disjointed A) \<le> x"
   576     by (metis xeq)
   577   hence y: "psuminf (f o disjointed A) \<in> measure_set M f s"
   578     apply (auto simp add: measure_set_def)
   579     apply (rule_tac x="disjointed A" in exI)
   580     apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
   581     done
   582   show ?thesis
   583     by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
   584 qed
   585 
   586 lemma (in algebra) inf_measure_close:
   587   assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
   588   shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
   589                psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
   590 proof (cases "Inf (measure_set M f s) = \<omega>")
   591   case False
   592   obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
   593     using Inf_close[OF False e] by auto
   594   thus ?thesis
   595     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
   596 next
   597   case True
   598   have "measure_set M f s \<noteq> {}"
   599     by (metis emptyE ss inf_measure_nonempty [of f, OF posf top _ empty_sets])
   600   then obtain l where "l \<in> measure_set M f s" by auto
   601   moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
   602   ultimately show ?thesis
   603     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
   604 qed
   605 
   606 lemma (in algebra) inf_measure_countably_subadditive:
   607   assumes posf: "positive f" and inc: "increasing M f"
   608   shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
   609                   (\<lambda>x. Inf (measure_set M f x))"
   610   unfolding countably_subadditive_def o_def
   611 proof (safe, simp, rule pinfreal_le_epsilon)
   612   fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal
   613 
   614   let "?outer n" = "Inf (measure_set M f (A n))"
   615   assume A: "range A \<subseteq> Pow (space M)"
   616      and disj: "disjoint_family A"
   617      and sb: "(\<Union>i. A i) \<subseteq> space M"
   618      and e: "0 < e"
   619   hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   620                    A n \<subseteq> (\<Union>i. BB n i) \<and>
   621                    psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
   622     apply (safe intro!: choice inf_measure_close [of f, OF posf _])
   623     using e sb by (cases e, auto simp add: not_le mult_pos_pos)
   624   then obtain BB
   625     where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
   626       and disjBB: "\<And>n. disjoint_family (BB n)"
   627       and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
   628       and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
   629     by auto blast
   630   have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e"
   631     proof -
   632       have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)"
   633         by (rule psuminf_le[OF BBle])
   634       also have "... = psuminf ?outer + e"
   635         using psuminf_half_series by simp
   636       finally show ?thesis .
   637     qed
   638   def C \<equiv> "(split BB) o prod_decode"
   639   have C: "!!n. C n \<in> sets M"
   640     apply (rule_tac p="prod_decode n" in PairE)
   641     apply (simp add: C_def)
   642     apply (metis BB subsetD rangeI)
   643     done
   644   have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   645     proof (auto simp add: C_def)
   646       fix x i
   647       assume x: "x \<in> A i"
   648       with sbBB [of i] obtain j where "x \<in> BB i j"
   649         by blast
   650       thus "\<exists>i. x \<in> split BB (prod_decode i)"
   651         by (metis prod_encode_inverse prod.cases)
   652     qed
   653   have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   654     by (rule ext)  (auto simp add: C_def)
   655   moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle
   656     by (force intro!: psuminf_2dimen simp: o_def)
   657   ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp
   658   have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))"
   659     apply (rule inf_measure_le [OF posf(1) inc], auto)
   660     apply (rule_tac x="C" in exI)
   661     apply (auto simp add: C sbC Csums)
   662     done
   663   also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll
   664     by blast
   665   finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" .
   666 qed
   667 
   668 lemma (in algebra) inf_measure_outer:
   669   "\<lbrakk> positive f ; increasing M f \<rbrakk>
   670    \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
   671                           (\<lambda>x. Inf (measure_set M f x))"
   672   by (simp add: outer_measure_space_def inf_measure_empty
   673                 inf_measure_increasing inf_measure_countably_subadditive positive_def)
   674 
   675 (*MOVE UP*)
   676 
   677 lemma (in algebra) algebra_subset_lambda_system:
   678   assumes posf: "positive f" and inc: "increasing M f"
   679       and add: "additive M f"
   680   shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
   681                                 (\<lambda>x. Inf (measure_set M f x))"
   682 proof (auto dest: sets_into_space
   683             simp add: algebra.lambda_system_eq [OF algebra_Pow])
   684   fix x s
   685   assume x: "x \<in> sets M"
   686      and s: "s \<subseteq> space M"
   687   have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
   688     by blast
   689   have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   690         \<le> Inf (measure_set M f s)"
   691     proof (rule pinfreal_le_epsilon)
   692       fix e :: pinfreal
   693       assume e: "0 < e"
   694       from inf_measure_close [of f, OF posf e s]
   695       obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   696                  and sUN: "s \<subseteq> (\<Union>i. A i)"
   697                  and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
   698         by auto
   699       have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   700                       (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   701         by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   702       have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   703         by (subst additiveD [OF add, symmetric])
   704            (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   705       { fix u
   706         assume u: "u \<in> sets M"
   707         have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
   708           by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
   709         have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)"
   710           proof (rule complete_lattice_class.Inf_lower)
   711             show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
   712               apply (simp add: measure_set_def)
   713               apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
   714               apply (auto simp add: disjoint_family_subset [OF disj] o_def)
   715               apply (blast intro: u range_subsetD [OF A])
   716               apply (blast dest: subsetD [OF sUN])
   717               done
   718           qed
   719       } note lesum = this
   720       have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)"
   721         and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
   722                    \<le> psuminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   723         by (metis Diff lesum top x)+
   724       hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   725            \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)"
   726         by (simp add: x add_mono)
   727       also have "... \<le> psuminf (f o A)"
   728         by (simp add: x psuminf_add[symmetric] o_def)
   729       also have "... \<le> Inf (measure_set M f s) + e"
   730         by (rule l)
   731       finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   732         \<le> Inf (measure_set M f s) + e" .
   733     qed
   734   moreover
   735   have "Inf (measure_set M f s)
   736        \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   737     proof -
   738     have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
   739       by (metis Un_Diff_Int Un_commute)
   740     also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   741       apply (rule subadditiveD)
   742       apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
   743                inf_measure_positive inf_measure_countably_subadditive posf inc)
   744       apply (auto simp add: subsetD [OF s])
   745       done
   746     finally show ?thesis .
   747     qed
   748   ultimately
   749   show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   750         = Inf (measure_set M f s)"
   751     by (rule order_antisym)
   752 qed
   753 
   754 lemma measure_down:
   755      "measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
   756       (\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>"
   757   by (simp add: measure_space_def measure_space_axioms_def positive_def
   758                 countably_additive_def)
   759      blast
   760 
   761 theorem (in algebra) caratheodory:
   762   assumes posf: "positive f" and ca: "countably_additive M f"
   763   shows "\<exists>\<mu> :: 'a set \<Rightarrow> pinfreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and> measure_space (sigma (space M) (sets M)) \<mu>"
   764   proof -
   765     have inc: "increasing M f"
   766       by (metis additive_increasing ca countably_additive_additive posf)
   767     let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
   768     def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
   769     have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm"
   770       using sigma_algebra.caratheodory_lemma
   771               [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
   772       by (simp add: ls_def)
   773     hence sls: "sigma_algebra (|space = space M, sets = ls|)"
   774       by (simp add: measure_space_def)
   775     have "sets M \<subseteq> ls"
   776       by (simp add: ls_def)
   777          (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
   778     hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
   779       using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
   780       by simp
   781     have "measure_space (sigma (space M) (sets M)) ?infm"
   782       unfolding sigma_def
   783       by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
   784          (simp_all add: sgs_sb space_closed)
   785     thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm])
   786   qed
   787 
   788 end