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