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

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