src/HOL/Probability/Caratheodory.thy
author hoelzl
Mon Aug 23 19:35:57 2010 +0200 (2010-08-23)
changeset 38656 d5d342611edb
parent 37591 d3daea901123
child 39096 111756225292
permissions -rw-r--r--
Rewrite the Probability theory.

Introduced pinfreal as real numbers with infinity.
Use pinfreal as value for measures.
Introduces Lebesgue Measure based on the integral in Multivariate Analysis.
Proved Radon Nikodym for arbitrary sigma finite measure spaces.
     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 
   449 lemma (in algebra) inf_measure_nonempty:
   450   assumes f: "positive f" and b: "b \<in> sets M" and a: "a \<subseteq> b"
   451   shows "f b \<in> measure_set M f a"
   452 proof -
   453   have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = setsum (f \<circ> (\<lambda>i. {})(0 := b)) {..<1::nat}"
   454     by (rule psuminf_finite) (simp add: f[unfolded positive_def])
   455   also have "... = f b"
   456     by simp
   457   finally have "psuminf (f \<circ> (\<lambda>i. {})(0 := b)) = f b" .
   458   thus ?thesis using a b
   459     by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
   460              simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
   461 qed
   462 
   463 lemma (in algebra) additive_increasing:
   464   assumes posf: "positive f" and addf: "additive M f"
   465   shows "increasing M f"
   466 proof (auto simp add: increasing_def)
   467   fix x y
   468   assume xy: "x \<in> sets M" "y \<in> sets M" "x \<subseteq> y"
   469   have "f x \<le> f x + f (y-x)" ..
   470   also have "... = f (x \<union> (y-x))" using addf
   471     by (auto simp add: additive_def) (metis Diff_disjoint Un_Diff_cancel Diff xy(1,2))
   472   also have "... = f y"
   473     by (metis Un_Diff_cancel Un_absorb1 xy(3))
   474   finally show "f x \<le> f y" .
   475 qed
   476 
   477 lemma (in algebra) countably_additive_additive:
   478   assumes posf: "positive f" and ca: "countably_additive M f"
   479   shows "additive M f"
   480 proof (auto simp add: additive_def)
   481   fix x y
   482   assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
   483   hence "disjoint_family (binaryset x y)"
   484     by (auto simp add: disjoint_family_on_def binaryset_def)
   485   hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
   486          (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
   487          f (\<Union>i. binaryset x y i) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   488     using ca
   489     by (simp add: countably_additive_def)
   490   hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
   491          f (x \<union> y) = (\<Sum>\<^isub>\<infinity> n. f (binaryset x y n))"
   492     by (simp add: range_binaryset_eq UN_binaryset_eq)
   493   thus "f (x \<union> y) = f x + f y" using posf x y
   494     by (auto simp add: Un binaryset_psuminf positive_def)
   495 qed
   496 
   497 lemma (in algebra) inf_measure_agrees:
   498   assumes posf: "positive f" and ca: "countably_additive M f"
   499       and s: "s \<in> sets M"
   500   shows "Inf (measure_set M f s) = f s"
   501   unfolding Inf_pinfreal_def
   502 proof (safe intro!: Greatest_equality)
   503   fix z
   504   assume z: "z \<in> measure_set M f s"
   505   from this obtain A where
   506     A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   507     and "s \<subseteq> (\<Union>x. A x)" and si: "psuminf (f \<circ> A) = z"
   508     by (auto simp add: measure_set_def comp_def)
   509   hence seq: "s = (\<Union>i. A i \<inter> s)" by blast
   510   have inc: "increasing M f"
   511     by (metis additive_increasing ca countably_additive_additive posf)
   512   have sums: "psuminf (\<lambda>i. f (A i \<inter> s)) = f (\<Union>i. A i \<inter> s)"
   513     proof (rule countably_additiveD [OF ca])
   514       show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   515         by blast
   516       show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   517         by (auto simp add: disjoint_family_on_def)
   518       show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   519         by (metis UN_extend_simps(4) s seq)
   520     qed
   521   hence "f s = psuminf (\<lambda>i. f (A i \<inter> s))"
   522     using seq [symmetric] by (simp add: sums_iff)
   523   also have "... \<le> psuminf (f \<circ> A)"
   524     proof (rule psuminf_le)
   525       fix n show "f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
   526         by (force intro: increasingD [OF inc])
   527     qed
   528   also have "... = z" by (rule si)
   529   finally show "f s \<le> z" .
   530 next
   531   fix y
   532   assume y: "\<forall>u \<in> measure_set M f s. y \<le> u"
   533   thus "y \<le> f s"
   534     by (blast intro: inf_measure_nonempty [of f, OF posf s subset_refl])
   535 qed
   536 
   537 lemma (in algebra) inf_measure_empty:
   538   assumes posf: "positive f"
   539   shows "Inf (measure_set M f {}) = 0"
   540 proof (rule antisym)
   541   show "Inf (measure_set M f {}) \<le> 0"
   542     by (metis complete_lattice_class.Inf_lower empty_sets inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
   543 qed simp
   544 
   545 lemma (in algebra) inf_measure_positive:
   546   "positive f \<Longrightarrow>
   547    positive (\<lambda>x. Inf (measure_set M f x))"
   548   by (simp add: positive_def inf_measure_empty) 
   549 
   550 lemma (in algebra) inf_measure_increasing:
   551   assumes posf: "positive f"
   552   shows "increasing (| space = space M, sets = Pow (space M) |)
   553                     (\<lambda>x. Inf (measure_set M f x))"
   554 apply (auto simp add: increasing_def)
   555 apply (rule complete_lattice_class.Inf_greatest)
   556 apply (rule complete_lattice_class.Inf_lower)
   557 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
   558 done
   559 
   560 
   561 lemma (in algebra) inf_measure_le:
   562   assumes posf: "positive f" and inc: "increasing M f"
   563       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}"
   564   shows "Inf (measure_set M f s) \<le> x"
   565 proof -
   566   from x
   567   obtain A where A: "range A \<subseteq> sets M" and ss: "s \<subseteq> (\<Union>i. A i)"
   568              and xeq: "psuminf (f \<circ> A) = x"
   569     by auto
   570   have dA: "range (disjointed A) \<subseteq> sets M"
   571     by (metis A range_disjointed_sets)
   572   have "\<forall>n.(f o disjointed A) n \<le> (f \<circ> A) n" unfolding comp_def
   573     by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A comp_def)
   574   hence sda: "psuminf (f o disjointed A) \<le> psuminf (f \<circ> A)"
   575     by (blast intro: psuminf_le)
   576   hence ley: "psuminf (f o disjointed A) \<le> x"
   577     by (metis xeq)
   578   hence y: "psuminf (f o disjointed A) \<in> measure_set M f s"
   579     apply (auto simp add: measure_set_def)
   580     apply (rule_tac x="disjointed A" in exI)
   581     apply (simp add: disjoint_family_disjointed UN_disjointed_eq ss dA comp_def)
   582     done
   583   show ?thesis
   584     by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
   585 qed
   586 
   587 lemma (in algebra) inf_measure_close:
   588   assumes posf: "positive f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
   589   shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
   590                psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
   591 proof (cases "Inf (measure_set M f s) = \<omega>")
   592   case False
   593   obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
   594     using Inf_close[OF False e] by auto
   595   thus ?thesis
   596     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
   597 next
   598   case True
   599   have "measure_set M f s \<noteq> {}"
   600     by (metis emptyE ss inf_measure_nonempty [of f, OF posf top])
   601   then obtain l where "l \<in> measure_set M f s" by auto
   602   moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
   603   ultimately show ?thesis
   604     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
   605 qed
   606 
   607 lemma (in algebra) inf_measure_countably_subadditive:
   608   assumes posf: "positive f" and inc: "increasing M f"
   609   shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
   610                   (\<lambda>x. Inf (measure_set M f x))"
   611   unfolding countably_subadditive_def o_def
   612 proof (safe, simp, rule pinfreal_le_epsilon)
   613   fix A :: "nat \<Rightarrow> 'a set" and e :: pinfreal
   614 
   615   let "?outer n" = "Inf (measure_set M f (A n))"
   616   assume A: "range A \<subseteq> Pow (space M)"
   617      and disj: "disjoint_family A"
   618      and sb: "(\<Union>i. A i) \<subseteq> space M"
   619      and e: "0 < e"
   620   hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   621                    A n \<subseteq> (\<Union>i. BB n i) \<and>
   622                    psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
   623     apply (safe intro!: choice inf_measure_close [of f, OF posf _])
   624     using e sb by (cases e, auto simp add: not_le mult_pos_pos)
   625   then obtain BB
   626     where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
   627       and disjBB: "\<And>n. disjoint_family (BB n)"
   628       and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
   629       and BBle: "\<And>n. psuminf (f o BB n) \<le> ?outer n + e * (1/2)^(Suc n)"
   630     by auto blast
   631   have sll: "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> psuminf ?outer + e"
   632     proof -
   633       have "(\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n)) \<le> (\<Sum>\<^isub>\<infinity> n. ?outer n + e*(1/2) ^ Suc n)"
   634         by (rule psuminf_le[OF BBle])
   635       also have "... = psuminf ?outer + e"
   636         using psuminf_half_series by simp
   637       finally show ?thesis .
   638     qed
   639   def C \<equiv> "(split BB) o prod_decode"
   640   have C: "!!n. C n \<in> sets M"
   641     apply (rule_tac p="prod_decode n" in PairE)
   642     apply (simp add: C_def)
   643     apply (metis BB subsetD rangeI)
   644     done
   645   have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   646     proof (auto simp add: C_def)
   647       fix x i
   648       assume x: "x \<in> A i"
   649       with sbBB [of i] obtain j where "x \<in> BB i j"
   650         by blast
   651       thus "\<exists>i. x \<in> split BB (prod_decode i)"
   652         by (metis prod_encode_inverse prod.cases)
   653     qed
   654   have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   655     by (rule ext)  (auto simp add: C_def)
   656   moreover have "psuminf ... = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" using BBle
   657     by (force intro!: psuminf_2dimen simp: o_def)
   658   ultimately have Csums: "psuminf (f \<circ> C) = (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))" by simp
   659   have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>\<^isub>\<infinity> n. psuminf (f o BB n))"
   660     apply (rule inf_measure_le [OF posf(1) inc], auto)
   661     apply (rule_tac x="C" in exI)
   662     apply (auto simp add: C sbC Csums)
   663     done
   664   also have "... \<le> (\<Sum>\<^isub>\<infinity>n. Inf (measure_set M f (A n))) + e" using sll
   665     by blast
   666   finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> psuminf ?outer + e" .
   667 qed
   668 
   669 lemma (in algebra) inf_measure_outer:
   670   "\<lbrakk> positive f ; increasing M f \<rbrakk>
   671    \<Longrightarrow> outer_measure_space (| space = space M, sets = Pow (space M) |)
   672                           (\<lambda>x. Inf (measure_set M f x))"
   673   by (simp add: outer_measure_space_def inf_measure_empty
   674                 inf_measure_increasing inf_measure_countably_subadditive positive_def)
   675 
   676 (*MOVE UP*)
   677 
   678 lemma (in algebra) algebra_subset_lambda_system:
   679   assumes posf: "positive f" and inc: "increasing M f"
   680       and add: "additive M f"
   681   shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
   682                                 (\<lambda>x. Inf (measure_set M f x))"
   683 proof (auto dest: sets_into_space
   684             simp add: algebra.lambda_system_eq [OF algebra_Pow])
   685   fix x s
   686   assume x: "x \<in> sets M"
   687      and s: "s \<subseteq> space M"
   688   have [simp]: "!!x. x \<in> sets M \<Longrightarrow> s \<inter> (space M - x) = s-x" using s
   689     by blast
   690   have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   691         \<le> Inf (measure_set M f s)"
   692     proof (rule pinfreal_le_epsilon)
   693       fix e :: pinfreal
   694       assume e: "0 < e"
   695       from inf_measure_close [of f, OF posf e s]
   696       obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   697                  and sUN: "s \<subseteq> (\<Union>i. A i)"
   698                  and l: "psuminf (f \<circ> A) \<le> Inf (measure_set M f s) + e"
   699         by auto
   700       have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   701                       (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   702         by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   703       have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   704         by (subst additiveD [OF add, symmetric])
   705            (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   706       { fix u
   707         assume u: "u \<in> sets M"
   708         have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
   709           by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
   710         have 2: "Inf (measure_set M f (s \<inter> u)) \<le> psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A)"
   711           proof (rule complete_lattice_class.Inf_lower)
   712             show "psuminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
   713               apply (simp add: measure_set_def)
   714               apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
   715               apply (auto simp add: disjoint_family_subset [OF disj] o_def)
   716               apply (blast intro: u range_subsetD [OF A])
   717               apply (blast dest: subsetD [OF sUN])
   718               done
   719           qed
   720       } note lesum = this
   721       have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> psuminf (f o (\<lambda>z. z\<inter>x) o A)"
   722         and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
   723                    \<le> psuminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   724         by (metis Diff lesum top x)+
   725       hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   726            \<le> psuminf (f o (\<lambda>s. s\<inter>x) o A) + psuminf (f o (\<lambda>s. s-x) o A)"
   727         by (simp add: x add_mono)
   728       also have "... \<le> psuminf (f o A)"
   729         by (simp add: x psuminf_add[symmetric] o_def)
   730       also have "... \<le> Inf (measure_set M f s) + e"
   731         by (rule l)
   732       finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   733         \<le> Inf (measure_set M f s) + e" .
   734     qed
   735   moreover
   736   have "Inf (measure_set M f s)
   737        \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   738     proof -
   739     have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
   740       by (metis Un_Diff_Int Un_commute)
   741     also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   742       apply (rule subadditiveD)
   743       apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow
   744                inf_measure_positive inf_measure_countably_subadditive posf inc)
   745       apply (auto simp add: subsetD [OF s])
   746       done
   747     finally show ?thesis .
   748     qed
   749   ultimately
   750   show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   751         = Inf (measure_set M f s)"
   752     by (rule order_antisym)
   753 qed
   754 
   755 lemma measure_down:
   756      "measure_space N \<mu> \<Longrightarrow> sigma_algebra M \<Longrightarrow> sets M \<subseteq> sets N \<Longrightarrow>
   757       (\<nu> = \<mu>) \<Longrightarrow> measure_space M \<nu>"
   758   by (simp add: measure_space_def measure_space_axioms_def positive_def
   759                 countably_additive_def)
   760      blast
   761 
   762 theorem (in algebra) caratheodory:
   763   assumes posf: "positive f" and ca: "countably_additive M f"
   764   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>"
   765   proof -
   766     have inc: "increasing M f"
   767       by (metis additive_increasing ca countably_additive_additive posf)
   768     let ?infm = "(\<lambda>x. Inf (measure_set M f x))"
   769     def ls \<equiv> "lambda_system (|space = space M, sets = Pow (space M)|) ?infm"
   770     have mls: "measure_space \<lparr>space = space M, sets = ls\<rparr> ?infm"
   771       using sigma_algebra.caratheodory_lemma
   772               [OF sigma_algebra_Pow  inf_measure_outer [OF posf inc]]
   773       by (simp add: ls_def)
   774     hence sls: "sigma_algebra (|space = space M, sets = ls|)"
   775       by (simp add: measure_space_def)
   776     have "sets M \<subseteq> ls"
   777       by (simp add: ls_def)
   778          (metis ca posf inc countably_additive_additive algebra_subset_lambda_system)
   779     hence sgs_sb: "sigma_sets (space M) (sets M) \<subseteq> ls"
   780       using sigma_algebra.sigma_sets_subset [OF sls, of "sets M"]
   781       by simp
   782     have "measure_space (sigma (space M) (sets M)) ?infm"
   783       unfolding sigma_def
   784       by (rule measure_down [OF mls], rule sigma_algebra_sigma_sets)
   785          (simp_all add: sgs_sb space_closed)
   786     thus ?thesis using inf_measure_agrees [OF posf ca] by (auto intro!: exI[of _ ?infm])
   787   qed
   788 
   789 end