src/HOL/Probability/Caratheodory.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
parent 39096 111756225292
child 41023 9118eb4eb8dc
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
     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 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 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