src/HOL/Probability/Measure.thy
author wenzelm
Thu Feb 11 23:00:22 2010 +0100 (2010-02-11)
changeset 35115 446c5063e4fd
parent 33657 a4179bf442d1
child 35582 b16d99a72dc9
permissions -rw-r--r--
modernized translations;
formal markup of @{syntax_const} and @{const_syntax};
minor tuning;
paulson@33271
     1
header {*Measures*}
paulson@33271
     2
paulson@33271
     3
theory Measure
paulson@33271
     4
  imports Caratheodory FuncSet
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
definition prod_sets where
paulson@33271
    10
  "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
paulson@33271
    11
paulson@33271
    12
lemma prod_setsI: "x \<in> A \<Longrightarrow> y \<in> B \<Longrightarrow> (x \<times> y) \<in> prod_sets A B"
paulson@33271
    13
  by (auto simp add: prod_sets_def) 
paulson@33271
    14
paulson@33271
    15
definition
paulson@33271
    16
  closed_cdi  where
paulson@33271
    17
  "closed_cdi M \<longleftrightarrow>
paulson@33271
    18
   sets M \<subseteq> Pow (space M) &
paulson@33271
    19
   (\<forall>s \<in> sets M. space M - s \<in> sets M) &
paulson@33271
    20
   (\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow>
paulson@33271
    21
        (\<Union>i. A i) \<in> sets M) &
paulson@33271
    22
   (\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
paulson@33271
    23
paulson@33271
    24
paulson@33271
    25
inductive_set
paulson@33271
    26
  smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set"
paulson@33271
    27
  for M
paulson@33271
    28
  where
paulson@33271
    29
    Basic [intro]: 
paulson@33271
    30
      "a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M"
paulson@33271
    31
  | Compl [intro]:
paulson@33271
    32
      "a \<in> smallest_ccdi_sets M \<Longrightarrow> space M - a \<in> smallest_ccdi_sets M"
paulson@33271
    33
  | Inc:
paulson@33271
    34
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n))
paulson@33271
    35
       \<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M"
paulson@33271
    36
  | Disj:
paulson@33271
    37
      "range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A
paulson@33271
    38
       \<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M"
paulson@33271
    39
  monos Pow_mono
paulson@33271
    40
paulson@33271
    41
paulson@33271
    42
definition
paulson@33271
    43
  smallest_closed_cdi  where
paulson@33271
    44
  "smallest_closed_cdi M = (|space = space M, sets = smallest_ccdi_sets M|)"
paulson@33271
    45
paulson@33271
    46
definition
paulson@33271
    47
  measurable  where
paulson@33271
    48
  "measurable a b = {f . sigma_algebra a & sigma_algebra b &
wenzelm@33536
    49
                         f \<in> (space a -> space b) &
wenzelm@33536
    50
                         (\<forall>y \<in> sets b. (f -` y) \<inter> (space a) \<in> sets a)}"
paulson@33271
    51
paulson@33271
    52
definition
paulson@33271
    53
  measure_preserving  where
paulson@33271
    54
  "measure_preserving m1 m2 =
paulson@33271
    55
     measurable m1 m2 \<inter> 
paulson@33271
    56
     {f . measure_space m1 & measure_space m2 &
paulson@33271
    57
          (\<forall>y \<in> sets m2. measure m1 ((f -` y) \<inter> (space m1)) = measure m2 y)}"
paulson@33271
    58
paulson@33271
    59
lemma space_smallest_closed_cdi [simp]:
paulson@33271
    60
     "space (smallest_closed_cdi M) = space M"
paulson@33271
    61
  by (simp add: smallest_closed_cdi_def)
paulson@33271
    62
paulson@33271
    63
paulson@33271
    64
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)"
paulson@33271
    65
  by (auto simp add: smallest_closed_cdi_def) 
paulson@33271
    66
paulson@33271
    67
lemma (in algebra) smallest_ccdi_sets:
paulson@33271
    68
     "smallest_ccdi_sets M \<subseteq> Pow (space M)"
paulson@33271
    69
  apply (rule subsetI) 
paulson@33271
    70
  apply (erule smallest_ccdi_sets.induct) 
paulson@33271
    71
  apply (auto intro: range_subsetD dest: sets_into_space)
paulson@33271
    72
  done
paulson@33271
    73
paulson@33271
    74
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)"
paulson@33271
    75
  apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets)
paulson@33271
    76
  apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) +
paulson@33271
    77
  done
paulson@33271
    78
paulson@33271
    79
lemma (in algebra) smallest_closed_cdi3:
paulson@33271
    80
     "sets (smallest_closed_cdi M) \<subseteq> Pow (space M)"
paulson@33271
    81
  by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 
paulson@33271
    82
paulson@33271
    83
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)"
paulson@33271
    84
  by (simp add: closed_cdi_def) 
paulson@33271
    85
paulson@33271
    86
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M - s \<in> sets M"
paulson@33271
    87
  by (simp add: closed_cdi_def) 
paulson@33271
    88
paulson@33271
    89
lemma closed_cdi_Inc:
paulson@33271
    90
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow>
paulson@33271
    91
        (\<Union>i. A i) \<in> sets M"
paulson@33271
    92
  by (simp add: closed_cdi_def) 
paulson@33271
    93
paulson@33271
    94
lemma closed_cdi_Disj:
paulson@33271
    95
     "closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M"
paulson@33271
    96
  by (simp add: closed_cdi_def) 
paulson@33271
    97
paulson@33271
    98
lemma closed_cdi_Un:
paulson@33271
    99
  assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M"
paulson@33271
   100
      and A: "A \<in> sets M" and B: "B \<in> sets M"
paulson@33271
   101
      and disj: "A \<inter> B = {}"
paulson@33271
   102
    shows "A \<union> B \<in> sets M"
paulson@33271
   103
proof -
paulson@33271
   104
  have ra: "range (binaryset A B) \<subseteq> sets M"
paulson@33271
   105
   by (simp add: range_binaryset_eq empty A B) 
paulson@33271
   106
 have di:  "disjoint_family (binaryset A B)" using disj
paulson@33271
   107
   by (simp add: disjoint_family_def binaryset_def Int_commute) 
paulson@33271
   108
 from closed_cdi_Disj [OF cdi ra di]
paulson@33271
   109
 show ?thesis
paulson@33271
   110
   by (simp add: UN_binaryset_eq) 
paulson@33271
   111
qed
paulson@33271
   112
paulson@33271
   113
lemma (in algebra) smallest_ccdi_sets_Un:
paulson@33271
   114
  assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M"
paulson@33271
   115
      and disj: "A \<inter> B = {}"
paulson@33271
   116
    shows "A \<union> B \<in> smallest_ccdi_sets M"
paulson@33271
   117
proof -
paulson@33271
   118
  have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
paulson@33271
   119
    by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
paulson@33271
   120
  have di:  "disjoint_family (binaryset A B)" using disj
paulson@33271
   121
    by (simp add: disjoint_family_def binaryset_def Int_commute) 
paulson@33271
   122
  from Disj [OF ra di]
paulson@33271
   123
  show ?thesis
paulson@33271
   124
    by (simp add: UN_binaryset_eq) 
paulson@33271
   125
qed
paulson@33271
   126
paulson@33271
   127
paulson@33271
   128
paulson@33271
   129
lemma (in algebra) smallest_ccdi_sets_Int1:
paulson@33271
   130
  assumes a: "a \<in> sets M"
paulson@33271
   131
  shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
paulson@33271
   132
proof (induct rule: smallest_ccdi_sets.induct)
paulson@33271
   133
  case (Basic x)
paulson@33271
   134
  thus ?case
paulson@33271
   135
    by (metis a Int smallest_ccdi_sets.Basic)
paulson@33271
   136
next
paulson@33271
   137
  case (Compl x)
paulson@33271
   138
  have "a \<inter> (space M - x) = space M - ((space M - a) \<union> (a \<inter> x))"
paulson@33271
   139
    by blast
paulson@33271
   140
  also have "... \<in> smallest_ccdi_sets M" 
paulson@33271
   141
    by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2
paulson@33271
   142
           Diff_disjoint Int_Diff Int_empty_right Un_commute
paulson@33271
   143
           smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl
paulson@33271
   144
           smallest_ccdi_sets_Un) 
paulson@33271
   145
  finally show ?case .
paulson@33271
   146
next
paulson@33271
   147
  case (Inc A)
paulson@33271
   148
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
paulson@33271
   149
    by blast
paulson@33271
   150
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc
paulson@33271
   151
    by blast
paulson@33271
   152
  moreover have "(\<lambda>i. a \<inter> A i) 0 = {}"
paulson@33271
   153
    by (simp add: Inc) 
paulson@33271
   154
  moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc
paulson@33271
   155
    by blast
paulson@33271
   156
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
paulson@33271
   157
    by (rule smallest_ccdi_sets.Inc) 
paulson@33271
   158
  show ?case
paulson@33271
   159
    by (metis 1 2)
paulson@33271
   160
next
paulson@33271
   161
  case (Disj A)
paulson@33271
   162
  have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)"
paulson@33271
   163
    by blast
paulson@33271
   164
  have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
paulson@33271
   165
    by blast
paulson@33271
   166
  moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
paulson@33271
   167
    by (auto simp add: disjoint_family_def) 
paulson@33271
   168
  ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
paulson@33271
   169
    by (rule smallest_ccdi_sets.Disj) 
paulson@33271
   170
  show ?case
paulson@33271
   171
    by (metis 1 2)
paulson@33271
   172
qed
paulson@33271
   173
paulson@33271
   174
paulson@33271
   175
lemma (in algebra) smallest_ccdi_sets_Int:
paulson@33271
   176
  assumes b: "b \<in> smallest_ccdi_sets M"
paulson@33271
   177
  shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M"
paulson@33271
   178
proof (induct rule: smallest_ccdi_sets.induct)
paulson@33271
   179
  case (Basic x)
paulson@33271
   180
  thus ?case
paulson@33271
   181
    by (metis b smallest_ccdi_sets_Int1)
paulson@33271
   182
next
paulson@33271
   183
  case (Compl x)
paulson@33271
   184
  have "(space M - x) \<inter> b = space M - (x \<inter> b \<union> (space M - b))"
paulson@33271
   185
    by blast
paulson@33271
   186
  also have "... \<in> smallest_ccdi_sets M"
paulson@33271
   187
    by (metis Compl(2) Diff_disjoint Int_Diff Int_commute Int_empty_right b 
paulson@33271
   188
           smallest_ccdi_sets.Compl smallest_ccdi_sets_Un) 
paulson@33271
   189
  finally show ?case .
paulson@33271
   190
next
paulson@33271
   191
  case (Inc A)
paulson@33271
   192
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
paulson@33271
   193
    by blast
paulson@33271
   194
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Inc
paulson@33271
   195
    by blast
paulson@33271
   196
  moreover have "(\<lambda>i. A i \<inter> b) 0 = {}"
paulson@33271
   197
    by (simp add: Inc) 
paulson@33271
   198
  moreover have "!!n. (\<lambda>i. A i \<inter> b) n \<subseteq> (\<lambda>i. A i \<inter> b) (Suc n)" using Inc
paulson@33271
   199
    by blast
paulson@33271
   200
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
paulson@33271
   201
    by (rule smallest_ccdi_sets.Inc) 
paulson@33271
   202
  show ?case
paulson@33271
   203
    by (metis 1 2)
paulson@33271
   204
next
paulson@33271
   205
  case (Disj A)
paulson@33271
   206
  have 1: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) = (\<Union>i. A i) \<inter> b"
paulson@33271
   207
    by blast
paulson@33271
   208
  have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
paulson@33271
   209
    by blast
paulson@33271
   210
  moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
paulson@33271
   211
    by (auto simp add: disjoint_family_def) 
paulson@33271
   212
  ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
paulson@33271
   213
    by (rule smallest_ccdi_sets.Disj) 
paulson@33271
   214
  show ?case
paulson@33271
   215
    by (metis 1 2)
paulson@33271
   216
qed
paulson@33271
   217
paulson@33271
   218
lemma (in algebra) sets_smallest_closed_cdi_Int:
paulson@33271
   219
   "a \<in> sets (smallest_closed_cdi M) \<Longrightarrow> b \<in> sets (smallest_closed_cdi M)
paulson@33271
   220
    \<Longrightarrow> a \<inter> b \<in> sets (smallest_closed_cdi M)"
paulson@33271
   221
  by (simp add: smallest_ccdi_sets_Int smallest_closed_cdi_def) 
paulson@33271
   222
paulson@33271
   223
lemma algebra_iff_Int:
paulson@33271
   224
     "algebra M \<longleftrightarrow> 
paulson@33271
   225
       sets M \<subseteq> Pow (space M) & {} \<in> sets M & 
paulson@33271
   226
       (\<forall>a \<in> sets M. space M - a \<in> sets M) &
paulson@33271
   227
       (\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
paulson@33271
   228
proof (auto simp add: algebra.Int, auto simp add: algebra_def)
paulson@33271
   229
  fix a b
paulson@33271
   230
  assume ab: "sets M \<subseteq> Pow (space M)"
paulson@33271
   231
             "\<forall>a\<in>sets M. space M - a \<in> sets M" 
paulson@33271
   232
             "\<forall>a\<in>sets M. \<forall>b\<in>sets M. a \<inter> b \<in> sets M"
paulson@33271
   233
             "a \<in> sets M" "b \<in> sets M"
paulson@33271
   234
  hence "a \<union> b = space M - ((space M - a) \<inter> (space M - b))"
paulson@33271
   235
    by blast
paulson@33271
   236
  also have "... \<in> sets M"
paulson@33271
   237
    by (metis ab)
paulson@33271
   238
  finally show "a \<union> b \<in> sets M" .
paulson@33271
   239
qed
paulson@33271
   240
paulson@33271
   241
lemma (in algebra) sigma_property_disjoint_lemma:
paulson@33271
   242
  assumes sbC: "sets M \<subseteq> C"
paulson@33271
   243
      and ccdi: "closed_cdi (|space = space M, sets = C|)"
paulson@33271
   244
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
paulson@33271
   245
proof -
paulson@33271
   246
  have "smallest_ccdi_sets M \<in> {B . sets M \<subseteq> B \<and> sigma_algebra (|space = space M, sets = B|)}"
paulson@33271
   247
    apply (auto simp add: sigma_algebra_disjoint_iff algebra_iff_Int 
paulson@33271
   248
            smallest_ccdi_sets_Int)
paulson@33271
   249
    apply (metis Union_Pow_eq Union_upper subsetD smallest_ccdi_sets) 
paulson@33271
   250
    apply (blast intro: smallest_ccdi_sets.Disj) 
paulson@33271
   251
    done
paulson@33271
   252
  hence "sigma_sets (space M) (sets M) \<subseteq> smallest_ccdi_sets M"
paulson@33271
   253
    by auto 
paulson@33271
   254
       (metis sigma_algebra.sigma_sets_subset algebra.simps(1) 
paulson@33271
   255
          algebra.simps(2) subsetD) 
paulson@33271
   256
  also have "...  \<subseteq> C"
paulson@33271
   257
    proof
paulson@33271
   258
      fix x
paulson@33271
   259
      assume x: "x \<in> smallest_ccdi_sets M"
paulson@33271
   260
      thus "x \<in> C"
wenzelm@33536
   261
        proof (induct rule: smallest_ccdi_sets.induct)
wenzelm@33536
   262
          case (Basic x)
wenzelm@33536
   263
          thus ?case
wenzelm@33536
   264
            by (metis Basic subsetD sbC)
wenzelm@33536
   265
        next
wenzelm@33536
   266
          case (Compl x)
wenzelm@33536
   267
          thus ?case
wenzelm@33536
   268
            by (blast intro: closed_cdi_Compl [OF ccdi, simplified])
wenzelm@33536
   269
        next
wenzelm@33536
   270
          case (Inc A)
wenzelm@33536
   271
          thus ?case
wenzelm@33536
   272
               by (auto intro: closed_cdi_Inc [OF ccdi, simplified]) 
wenzelm@33536
   273
        next
wenzelm@33536
   274
          case (Disj A)
wenzelm@33536
   275
          thus ?case
wenzelm@33536
   276
               by (auto intro: closed_cdi_Disj [OF ccdi, simplified]) 
wenzelm@33536
   277
        qed
paulson@33271
   278
    qed
paulson@33271
   279
  finally show ?thesis .
paulson@33271
   280
qed
paulson@33271
   281
paulson@33271
   282
lemma (in algebra) sigma_property_disjoint:
paulson@33271
   283
  assumes sbC: "sets M \<subseteq> C"
paulson@33271
   284
      and compl: "!!s. s \<in> C \<inter> sigma_sets (space M) (sets M) \<Longrightarrow> space M - s \<in> C"
paulson@33271
   285
      and inc: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
paulson@33271
   286
                     \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) 
paulson@33271
   287
                     \<Longrightarrow> (\<Union>i. A i) \<in> C"
paulson@33271
   288
      and disj: "!!A. range A \<subseteq> C \<inter> sigma_sets (space M) (sets M) 
paulson@33271
   289
                      \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> C"
paulson@33271
   290
  shows "sigma_sets (space M) (sets M) \<subseteq> C"
paulson@33271
   291
proof -
paulson@33271
   292
  have "sigma_sets (space M) (sets M) \<subseteq> C \<inter> sigma_sets (space M) (sets M)" 
paulson@33271
   293
    proof (rule sigma_property_disjoint_lemma) 
paulson@33271
   294
      show "sets M \<subseteq> C \<inter> sigma_sets (space M) (sets M)"
wenzelm@33536
   295
        by (metis Int_greatest Set.subsetI sbC sigma_sets.Basic)
paulson@33271
   296
    next
paulson@33271
   297
      show "closed_cdi \<lparr>space = space M, sets = C \<inter> sigma_sets (space M) (sets M)\<rparr>"
wenzelm@33536
   298
        by (simp add: closed_cdi_def compl inc disj)
paulson@33271
   299
           (metis PowI Set.subsetI le_infI2 sigma_sets_into_sp space_closed
wenzelm@33536
   300
             IntE sigma_sets.Compl range_subsetD sigma_sets.Union)
paulson@33271
   301
    qed
paulson@33271
   302
  thus ?thesis
paulson@33271
   303
    by blast
paulson@33271
   304
qed
paulson@33271
   305
paulson@33271
   306
paulson@33271
   307
(* or just countably_additiveD [OF measure_space.ca] *)
paulson@33271
   308
lemma (in measure_space) measure_countably_additive:
paulson@33271
   309
    "range A \<subseteq> sets M
paulson@33271
   310
     \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i. A i) \<in> sets M
paulson@33271
   311
     \<Longrightarrow> (measure M o A)  sums  measure M (\<Union>i. A i)"
paulson@33271
   312
  by (insert ca) (simp add: countably_additive_def o_def) 
paulson@33271
   313
paulson@33271
   314
lemma (in measure_space) additive:
paulson@33271
   315
     "additive M (measure M)"
paulson@33271
   316
proof (rule algebra.countably_additive_additive [OF _ _ ca]) 
paulson@33271
   317
  show "algebra M"
paulson@33271
   318
    by (blast intro: sigma_algebra.axioms local.sigma_algebra_axioms)
paulson@33271
   319
  show "positive M (measure M)"
paulson@33271
   320
    by (simp add: positive_def empty_measure positive) 
paulson@33271
   321
qed
paulson@33271
   322
 
paulson@33271
   323
lemma (in measure_space) measure_additive:
paulson@33271
   324
     "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {} 
paulson@33271
   325
      \<Longrightarrow> measure M a + measure M b = measure M (a \<union> b)"
paulson@33271
   326
  by (metis additiveD additive)
paulson@33271
   327
paulson@33271
   328
lemma (in measure_space) measure_compl:
paulson@33271
   329
  assumes s: "s \<in> sets M"
paulson@33271
   330
  shows "measure M (space M - s) = measure M (space M) - measure M s"
paulson@33271
   331
proof -
paulson@33271
   332
  have "measure M (space M) = measure M (s \<union> (space M - s))" using s
paulson@33271
   333
    by (metis Un_Diff_cancel Un_absorb1 s sets_into_space)
paulson@33271
   334
  also have "... = measure M s + measure M (space M - s)"
paulson@33271
   335
    by (rule additiveD [OF additive]) (auto simp add: s) 
paulson@33271
   336
  finally have "measure M (space M) = measure M s + measure M (space M - s)" .
paulson@33271
   337
  thus ?thesis
paulson@33271
   338
    by arith
paulson@33271
   339
qed
paulson@33271
   340
paulson@33271
   341
lemma disjoint_family_Suc:
paulson@33271
   342
  assumes Suc: "!!n. A n \<subseteq> A (Suc n)"
paulson@33271
   343
  shows "disjoint_family (\<lambda>i. A (Suc i) - A i)"
paulson@33271
   344
proof -
paulson@33271
   345
  {
paulson@33271
   346
    fix m
paulson@33271
   347
    have "!!n. A n \<subseteq> A (m+n)" 
paulson@33271
   348
    proof (induct m)
paulson@33271
   349
      case 0 show ?case by simp
paulson@33271
   350
    next
paulson@33271
   351
      case (Suc m) thus ?case
wenzelm@33536
   352
        by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans)
paulson@33271
   353
    qed
paulson@33271
   354
  }
paulson@33271
   355
  hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
paulson@33271
   356
    by (metis add_commute le_add_diff_inverse nat_less_le)
paulson@33271
   357
  thus ?thesis
paulson@33271
   358
    by (auto simp add: disjoint_family_def)
nipkow@33657
   359
      (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
paulson@33271
   360
qed
paulson@33271
   361
paulson@33271
   362
paulson@33271
   363
lemma (in measure_space) measure_countable_increasing:
paulson@33271
   364
  assumes A: "range A \<subseteq> sets M"
paulson@33271
   365
      and A0: "A 0 = {}"
paulson@33271
   366
      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
paulson@33271
   367
  shows "(measure M o A) ----> measure M (\<Union>i. A i)"
paulson@33271
   368
proof -
paulson@33271
   369
  {
paulson@33271
   370
    fix n
paulson@33271
   371
    have "(measure M \<circ> A) n =
paulson@33271
   372
          setsum (measure M \<circ> (\<lambda>i. A (Suc i) - A i)) {0..<n}"
paulson@33271
   373
      proof (induct n)
wenzelm@33536
   374
        case 0 thus ?case by (auto simp add: A0 empty_measure)
paulson@33271
   375
      next
wenzelm@33536
   376
        case (Suc m) 
wenzelm@33536
   377
        have "A (Suc m) = A m \<union> (A (Suc m) - A m)"
wenzelm@33536
   378
          by (metis ASuc Un_Diff_cancel Un_absorb1)
wenzelm@33536
   379
        hence "measure M (A (Suc m)) =
paulson@33271
   380
               measure M (A m) + measure M (A (Suc m) - A m)" 
wenzelm@33536
   381
          by (subst measure_additive) 
paulson@33271
   382
             (auto simp add: measure_additive range_subsetD [OF A]) 
wenzelm@33536
   383
        with Suc show ?case
wenzelm@33536
   384
          by simp
paulson@33271
   385
      qed
paulson@33271
   386
  }
paulson@33271
   387
  hence Meq: "measure M o A = (\<lambda>n. setsum (measure M o (\<lambda>i. A(Suc i) - A i)) {0..<n})"
paulson@33271
   388
    by (blast intro: ext) 
paulson@33271
   389
  have Aeq: "(\<Union>i. A (Suc i) - A i) = (\<Union>i. A i)"
paulson@33271
   390
    proof (rule UN_finite2_eq [where k=1], simp) 
paulson@33271
   391
      fix i
paulson@33271
   392
      show "(\<Union>i\<in>{0..<i}. A (Suc i) - A i) = (\<Union>i\<in>{0..<Suc i}. A i)"
wenzelm@33536
   393
        proof (induct i)
wenzelm@33536
   394
          case 0 thus ?case by (simp add: A0)
wenzelm@33536
   395
        next
wenzelm@33536
   396
          case (Suc i) 
wenzelm@33536
   397
          thus ?case
wenzelm@33536
   398
            by (auto simp add: atLeastLessThanSuc intro: subsetD [OF ASuc])
wenzelm@33536
   399
        qed
paulson@33271
   400
    qed
paulson@33271
   401
  have A1: "\<And>i. A (Suc i) - A i \<in> sets M"
paulson@33271
   402
    by (metis A Diff range_subsetD)
paulson@33271
   403
  have A2: "(\<Union>i. A (Suc i) - A i) \<in> sets M"
paulson@33271
   404
    by (blast intro: countable_UN range_subsetD [OF A])  
paulson@33271
   405
  have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A (Suc i) - A i)"
paulson@33271
   406
    by (rule measure_countably_additive) 
paulson@33271
   407
       (auto simp add: disjoint_family_Suc ASuc A1 A2)
paulson@33271
   408
  also have "... =  measure M (\<Union>i. A i)"
paulson@33271
   409
    by (simp add: Aeq) 
paulson@33271
   410
  finally have "(measure M o (\<lambda>i. A (Suc i) - A i)) sums measure M (\<Union>i. A i)" .
paulson@33271
   411
  thus ?thesis
paulson@33271
   412
    by (auto simp add: sums_iff Meq dest: summable_sumr_LIMSEQ_suminf) 
paulson@33271
   413
qed
paulson@33271
   414
paulson@33271
   415
lemma (in measure_space) monotone_convergence:
paulson@33271
   416
  assumes A: "range A \<subseteq> sets M"
paulson@33271
   417
      and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
paulson@33271
   418
  shows "(measure M \<circ> A) ----> measure M (\<Union>i. A i)"
paulson@33271
   419
proof -
paulson@33271
   420
  have ueq: "(\<Union>i. nat_case {} A i) = (\<Union>i. A i)" 
paulson@33271
   421
    by (auto simp add: split: nat.splits) 
paulson@33271
   422
  have meq: "measure M \<circ> A = (\<lambda>n. (measure M \<circ> nat_case {} A) (Suc n))"
paulson@33271
   423
    by (rule ext) simp
paulson@33271
   424
  have "(measure M \<circ> nat_case {} A) ----> measure M (\<Union>i. nat_case {} A i)" 
paulson@33271
   425
    by (rule measure_countable_increasing) 
paulson@33271
   426
       (auto simp add: range_subsetD [OF A] subsetD [OF ASuc] split: nat.splits) 
paulson@33271
   427
  also have "... = measure M (\<Union>i. A i)" 
paulson@33271
   428
    by (simp add: ueq) 
paulson@33271
   429
  finally have "(measure M \<circ> nat_case {} A) ---->  measure M (\<Union>i. A i)" .
paulson@33271
   430
  thus ?thesis using meq
paulson@33271
   431
    by (metis LIMSEQ_Suc)
paulson@33271
   432
qed
paulson@33271
   433
paulson@33271
   434
lemma measurable_sigma_preimages:
paulson@33271
   435
  assumes a: "sigma_algebra a" and b: "sigma_algebra b"
paulson@33271
   436
      and f: "f \<in> space a -> space b"
paulson@33271
   437
      and ba: "!!y. y \<in> sets b ==> f -` y \<in> sets a"
paulson@33271
   438
  shows "sigma_algebra (|space = space a, sets = (vimage f) ` (sets b) |)"
paulson@33271
   439
proof (simp add: sigma_algebra_iff2, intro conjI) 
paulson@33271
   440
  show "op -` f ` sets b \<subseteq> Pow (space a)"
paulson@33271
   441
    by auto (metis IntE a algebra.Int_space_eq1 ba sigma_algebra_iff vimageI) 
paulson@33271
   442
next
paulson@33271
   443
  show "{} \<in> op -` f ` sets b"
paulson@33271
   444
    by (metis algebra.empty_sets b image_iff sigma_algebra_iff vimage_empty)
paulson@33271
   445
next
paulson@33271
   446
  { fix y
paulson@33271
   447
    assume y: "y \<in> sets b"
paulson@33271
   448
    with a b f
paulson@33271
   449
    have "space a - f -` y = f -` (space b - y)"
paulson@33271
   450
      by (auto simp add: sigma_algebra_iff2) (blast intro: ba) 
paulson@33271
   451
    hence "space a - (f -` y) \<in> (vimage f) ` sets b"
paulson@33271
   452
      by auto
paulson@33271
   453
         (metis b y subsetD equalityE imageI sigma_algebra.sigma_sets_eq
paulson@33271
   454
                sigma_sets.Compl) 
paulson@33271
   455
  } 
paulson@33271
   456
  thus "\<forall>s\<in>sets b. space a - f -` s \<in> (vimage f) ` sets b"
paulson@33271
   457
    by blast
paulson@33271
   458
next
paulson@33271
   459
  {
paulson@33271
   460
    fix A:: "nat \<Rightarrow> 'a set"
paulson@33271
   461
    assume A: "range A \<subseteq> (vimage f) ` (sets b)"
paulson@33271
   462
    have  "(\<Union>i. A i) \<in> (vimage f) ` (sets b)"
paulson@33271
   463
      proof -
wenzelm@33536
   464
        def B \<equiv> "\<lambda>i. @v. v \<in> sets b \<and> f -` v = A i"
wenzelm@33536
   465
        { 
wenzelm@33536
   466
          fix i
wenzelm@33536
   467
          have "A i \<in> (vimage f) ` (sets b)" using A
wenzelm@33536
   468
            by blast
wenzelm@33536
   469
          hence "\<exists>v. v \<in> sets b \<and> f -` v = A i"
wenzelm@33536
   470
            by blast
wenzelm@33536
   471
          hence "B i \<in> sets b \<and> f -` B i = A i" 
wenzelm@33536
   472
            by (simp add: B_def) (erule someI_ex)
wenzelm@33536
   473
        } note B = this
wenzelm@33536
   474
        show ?thesis
wenzelm@33536
   475
          proof
wenzelm@33536
   476
            show "(\<Union>i. A i) = f -` (\<Union>i. B i)"
wenzelm@33536
   477
              by (simp add: vimage_UN B) 
wenzelm@33536
   478
           show "(\<Union>i. B i) \<in> sets b" using B
wenzelm@33536
   479
             by (auto intro: sigma_algebra.countable_UN [OF b]) 
wenzelm@33536
   480
          qed
paulson@33271
   481
      qed
paulson@33271
   482
  }
paulson@33271
   483
  thus "\<forall>A::nat \<Rightarrow> 'a set.
paulson@33271
   484
           range A \<subseteq> (vimage f) ` sets b \<longrightarrow> (\<Union>i. A i) \<in> (vimage f) ` sets b"
paulson@33271
   485
    by blast
paulson@33271
   486
qed
paulson@33271
   487
paulson@33271
   488
lemma (in sigma_algebra) measurable_sigma:
paulson@33271
   489
  assumes B: "B \<subseteq> Pow X" 
paulson@33271
   490
      and f: "f \<in> space M -> X"
paulson@33271
   491
      and ba: "!!y. y \<in> B ==> (f -` y) \<inter> space M \<in> sets M"
paulson@33271
   492
  shows "f \<in> measurable M (sigma X B)"
paulson@33271
   493
proof -
paulson@33271
   494
  have "sigma_sets X B \<subseteq> {y . (f -` y) \<inter> space M \<in> sets M & y \<subseteq> X}"
paulson@33271
   495
    proof clarify
paulson@33271
   496
      fix x
paulson@33271
   497
      assume "x \<in> sigma_sets X B"
paulson@33271
   498
      thus "f -` x \<inter> space M \<in> sets M \<and> x \<subseteq> X"
wenzelm@33536
   499
        proof induct
wenzelm@33536
   500
          case (Basic a)
wenzelm@33536
   501
          thus ?case
wenzelm@33536
   502
            by (auto simp add: ba) (metis B subsetD PowD) 
paulson@33271
   503
        next
wenzelm@33536
   504
          case Empty
wenzelm@33536
   505
          thus ?case
wenzelm@33536
   506
            by auto
paulson@33271
   507
        next
wenzelm@33536
   508
          case (Compl a)
wenzelm@33536
   509
          have [simp]: "f -` X \<inter> space M = space M"
wenzelm@33536
   510
            by (auto simp add: funcset_mem [OF f]) 
wenzelm@33536
   511
          thus ?case
wenzelm@33536
   512
            by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl)
wenzelm@33536
   513
        next
wenzelm@33536
   514
          case (Union a)
wenzelm@33536
   515
          thus ?case
wenzelm@33536
   516
            by (simp add: vimage_UN, simp only: UN_extend_simps(4))
wenzelm@33536
   517
               (blast intro: countable_UN)
wenzelm@33536
   518
        qed
paulson@33271
   519
    qed
paulson@33271
   520
  thus ?thesis
paulson@33271
   521
    by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 
paulson@33271
   522
       (auto simp add: sigma_def) 
paulson@33271
   523
qed
paulson@33271
   524
paulson@33271
   525
lemma measurable_subset:
paulson@33271
   526
     "measurable a b \<subseteq> measurable a (sigma (space b) (sets b))"
paulson@33271
   527
  apply clarify
paulson@33271
   528
  apply (rule sigma_algebra.measurable_sigma) 
paulson@33271
   529
  apply (auto simp add: measurable_def)
paulson@33271
   530
  apply (metis algebra.sets_into_space subsetD sigma_algebra_iff) 
paulson@33271
   531
  done
paulson@33271
   532
paulson@33271
   533
lemma measurable_eqI: 
paulson@33271
   534
     "space m1 = space m1' \<Longrightarrow> space m2 = space m2'
paulson@33271
   535
      \<Longrightarrow> sets m1 = sets m1' \<Longrightarrow> sets m2 = sets m2'
paulson@33271
   536
      \<Longrightarrow> measurable m1 m2 = measurable m1' m2'"
paulson@33271
   537
  by (simp add: measurable_def sigma_algebra_iff2) 
paulson@33271
   538
paulson@33271
   539
lemma measure_preserving_lift:
paulson@33271
   540
  fixes f :: "'a1 \<Rightarrow> 'a2" 
paulson@33271
   541
    and m1 :: "('a1, 'b1) measure_space_scheme"
paulson@33271
   542
    and m2 :: "('a2, 'b2) measure_space_scheme"
paulson@33271
   543
  assumes m1: "measure_space m1" and m2: "measure_space m2" 
paulson@33271
   544
  defines "m x \<equiv> (|space = space m2, sets = x, measure = measure m2, ... = more m2|)"
paulson@33271
   545
  assumes setsm2: "sets m2 = sigma_sets (space m2) a"
paulson@33271
   546
      and fmp: "f \<in> measure_preserving m1 (m a)"
paulson@33271
   547
  shows "f \<in> measure_preserving m1 m2"
paulson@33271
   548
proof -
paulson@33271
   549
  have [simp]: "!!x. space (m x) = space m2 & sets (m x) = x & measure (m x) = measure m2"
paulson@33271
   550
    by (simp add: m_def) 
paulson@33271
   551
  have sa1: "sigma_algebra m1" using m1 
paulson@33271
   552
    by (simp add: measure_space_def) 
paulson@33271
   553
  show ?thesis using fmp
paulson@33271
   554
    proof (clarsimp simp add: measure_preserving_def m1 m2) 
paulson@33271
   555
      assume fm: "f \<in> measurable m1 (m a)" 
wenzelm@33536
   556
         and mam: "measure_space (m a)"
wenzelm@33536
   557
         and meq: "\<forall>y\<in>a. measure m1 (f -` y \<inter> space m1) = measure m2 y"
paulson@33271
   558
      have "f \<in> measurable m1 (sigma (space (m a)) (sets (m a)))"
wenzelm@33536
   559
        by (rule subsetD [OF measurable_subset fm]) 
paulson@33271
   560
      also have "... = measurable m1 m2"
wenzelm@33536
   561
        by (rule measurable_eqI) (simp_all add: m_def setsm2 sigma_def) 
paulson@33271
   562
      finally have f12: "f \<in> measurable m1 m2" .
paulson@33271
   563
      hence ffn: "f \<in> space m1 \<rightarrow> space m2"
wenzelm@33536
   564
        by (simp add: measurable_def) 
paulson@33271
   565
      have "space m1 \<subseteq> f -` (space m2)"
wenzelm@33536
   566
        by auto (metis PiE ffn)
paulson@33271
   567
      hence fveq [simp]: "(f -` (space m2)) \<inter> space m1 = space m1"
wenzelm@33536
   568
        by blast
paulson@33271
   569
      {
wenzelm@33536
   570
        fix y
wenzelm@33536
   571
        assume y: "y \<in> sets m2" 
wenzelm@33536
   572
        have ama: "algebra (m a)"  using mam
wenzelm@33536
   573
          by (simp add: measure_space_def sigma_algebra_iff) 
wenzelm@33536
   574
        have spa: "space m2 \<in> a" using algebra.top [OF ama]
wenzelm@33536
   575
          by (simp add: m_def) 
wenzelm@33536
   576
        have "sigma_sets (space m2) a = sigma_sets (space (m a)) (sets (m a))"
wenzelm@33536
   577
          by (simp add: m_def) 
wenzelm@33536
   578
        also have "... \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}"
wenzelm@33536
   579
          proof (rule algebra.sigma_property_disjoint, auto simp add: ama) 
wenzelm@33536
   580
            fix x
wenzelm@33536
   581
            assume x: "x \<in> a"
wenzelm@33536
   582
            thus "measure m1 (f -` x \<inter> space m1) = measure m2 x"
wenzelm@33536
   583
              by (simp add: meq)
wenzelm@33536
   584
          next
wenzelm@33536
   585
            fix s
wenzelm@33536
   586
            assume eq: "measure m1 (f -` s \<inter> space m1) = measure m2 s"
wenzelm@33536
   587
               and s: "s \<in> sigma_sets (space m2) a"
wenzelm@33536
   588
            hence s2: "s \<in> sets m2"
wenzelm@33536
   589
              by (simp add: setsm2) 
wenzelm@33536
   590
            thus "measure m1 (f -` (space m2 - s) \<inter> space m1) =
paulson@33271
   591
                  measure m2 (space m2 - s)" using f12
wenzelm@33536
   592
              by (simp add: vimage_Diff Diff_Int_distrib2 eq m1 m2
wenzelm@33536
   593
                    measure_space.measure_compl measurable_def)  
wenzelm@33536
   594
                 (metis fveq meq spa) 
wenzelm@33536
   595
          next
wenzelm@33536
   596
            fix A
wenzelm@33536
   597
              assume A0: "A 0 = {}"
wenzelm@33536
   598
                 and ASuc: "!!n.  A n \<subseteq> A (Suc n)"
wenzelm@33536
   599
                 and rA1: "range A \<subseteq> 
wenzelm@33536
   600
                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
wenzelm@33536
   601
                 and "range A \<subseteq> sigma_sets (space m2) a"
wenzelm@33536
   602
              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
wenzelm@33536
   603
              have eq1: "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
wenzelm@33536
   604
                using rA1 by blast
wenzelm@33536
   605
              have "(measure m2 \<circ> A) = measure m1 o (\<lambda>i. (f -` A i \<inter> space m1))" 
wenzelm@33536
   606
                by (simp add: o_def eq1) 
wenzelm@33536
   607
              also have "... ----> measure m1 (\<Union>i. f -` A i \<inter> space m1)"
wenzelm@33536
   608
                proof (rule measure_space.measure_countable_increasing [OF m1])
wenzelm@33536
   609
                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
wenzelm@33536
   610
                    using f12 rA2 by (auto simp add: measurable_def)
wenzelm@33536
   611
                  show "f -` A 0 \<inter> space m1 = {}" using A0
wenzelm@33536
   612
                    by blast
wenzelm@33536
   613
                  show "\<And>n. f -` A n \<inter> space m1 \<subseteq> f -` A (Suc n) \<inter> space m1"
wenzelm@33536
   614
                    using ASuc by auto
wenzelm@33536
   615
                qed
wenzelm@33536
   616
              also have "... = measure m1 (f -` (\<Union>i. A i) \<inter> space m1)"
wenzelm@33536
   617
                by (simp add: vimage_UN)
wenzelm@33536
   618
              finally have "(measure m2 \<circ> A) ----> measure m1 (f -` (\<Union>i. A i) \<inter> space m1)" .
wenzelm@33536
   619
              moreover
wenzelm@33536
   620
              have "(measure m2 \<circ> A) ----> measure m2 (\<Union>i. A i)"
wenzelm@33536
   621
                by (rule measure_space.measure_countable_increasing 
wenzelm@33536
   622
                          [OF m2 rA2, OF A0 ASuc])
wenzelm@33536
   623
              ultimately 
wenzelm@33536
   624
              show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
paulson@33271
   625
                    measure m2 (\<Union>i. A i)"
wenzelm@33536
   626
                by (rule LIMSEQ_unique) 
wenzelm@33536
   627
          next
wenzelm@33536
   628
            fix A :: "nat => 'a2 set"
wenzelm@33536
   629
              assume dA: "disjoint_family A"
wenzelm@33536
   630
                 and rA1: "range A \<subseteq> 
wenzelm@33536
   631
                           {s. measure m1 (f -` s \<inter> space m1) = measure m2 s}"
wenzelm@33536
   632
                 and "range A \<subseteq> sigma_sets (space m2) a"
wenzelm@33536
   633
              hence rA2: "range A \<subseteq> sets m2" by (metis setsm2)
wenzelm@33536
   634
              hence Um2: "(\<Union>i. A i) \<in> sets m2"
wenzelm@33536
   635
                by (metis range_subsetD setsm2 sigma_sets.Union)
wenzelm@33536
   636
              have "!!i. measure m1 (f -` A i \<inter> space m1) = measure m2 (A i)"
wenzelm@33536
   637
                using rA1 by blast
wenzelm@33536
   638
              hence "measure m2 o A = measure m1 o (\<lambda>i. f -` A i \<inter> space m1)"
wenzelm@33536
   639
                by (simp add: o_def) 
wenzelm@33536
   640
              also have "... sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" 
wenzelm@33536
   641
                proof (rule measure_space.measure_countably_additive [OF m1] )
wenzelm@33536
   642
                  show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
wenzelm@33536
   643
                    using f12 rA2 by (auto simp add: measurable_def)
wenzelm@33536
   644
                  show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
wenzelm@33536
   645
                    by (auto simp add: disjoint_family_def) 
wenzelm@33536
   646
                  show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
wenzelm@33536
   647
                    proof (rule sigma_algebra.countable_UN [OF sa1])
wenzelm@33536
   648
                      show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
wenzelm@33536
   649
                        by (auto simp add: measurable_def) 
wenzelm@33536
   650
                    qed
wenzelm@33536
   651
                qed
wenzelm@33536
   652
              finally have "(measure m2 o A) sums measure m1 (\<Union>i. f -` A i \<inter> space m1)" .
wenzelm@33536
   653
              with measure_space.measure_countably_additive [OF m2 rA2 dA Um2] 
wenzelm@33536
   654
              have "measure m1 (\<Union>i. f -` A i \<inter> space m1) = measure m2 (\<Union>i. A i)"
wenzelm@33536
   655
                by (metis sums_unique) 
paulson@33271
   656
wenzelm@33536
   657
              moreover have "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) = measure m1 (\<Union>i. f -` A i \<inter> space m1)"
wenzelm@33536
   658
                by (simp add: vimage_UN)
wenzelm@33536
   659
              ultimately show "measure m1 (f -` (\<Union>i. A i) \<inter> space m1) =
paulson@33271
   660
                    measure m2 (\<Union>i. A i)" 
wenzelm@33536
   661
                by metis
wenzelm@33536
   662
          qed
wenzelm@33536
   663
        finally have "sigma_sets (space m2) a 
paulson@33271
   664
              \<subseteq> {s . measure m1 ((f -` s) \<inter> space m1) = measure m2 s}" .
wenzelm@33536
   665
        hence "measure m1 (f -` y \<inter> space m1) = measure m2 y" using y
wenzelm@33536
   666
          by (force simp add: setsm2) 
paulson@33271
   667
      }
paulson@33271
   668
      thus "f \<in> measurable m1 m2 \<and>
paulson@33271
   669
       (\<forall>y\<in>sets m2.
paulson@33271
   670
           measure m1 (f -` y \<inter> space m1) = measure m2 y)"
wenzelm@33536
   671
        by (blast intro: f12) 
paulson@33271
   672
    qed
paulson@33271
   673
qed
paulson@33271
   674
paulson@33271
   675
lemma measurable_ident:
paulson@33271
   676
     "sigma_algebra M ==> id \<in> measurable M M"
paulson@33271
   677
  apply (simp add: measurable_def)
paulson@33271
   678
  apply (auto simp add: sigma_algebra_def algebra.Int algebra.top)
paulson@33271
   679
  done
paulson@33271
   680
paulson@33271
   681
lemma measurable_comp:
paulson@33271
   682
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
paulson@33271
   683
  shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c"
paulson@33271
   684
  apply (auto simp add: measurable_def vimage_compose) 
paulson@33271
   685
  apply (subgoal_tac "f -` g -` y \<inter> space a = f -` (g -` y \<inter> space b) \<inter> space a")
paulson@33271
   686
  apply force+
paulson@33271
   687
  done
paulson@33271
   688
paulson@33271
   689
 lemma measurable_strong:
paulson@33271
   690
  fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 
paulson@33271
   691
  assumes f: "f \<in> measurable a b" and g: "g \<in> (space b -> space c)"
paulson@33271
   692
      and c: "sigma_algebra c"
paulson@33271
   693
      and t: "f ` (space a) \<subseteq> t"
paulson@33271
   694
      and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g -` s) \<inter> t \<in> sets b"
paulson@33271
   695
  shows "(g o f) \<in> measurable a c"
paulson@33271
   696
proof -
paulson@33271
   697
  have a: "sigma_algebra a" and b: "sigma_algebra b"
paulson@33271
   698
   and fab: "f \<in> (space a -> space b)"
paulson@33271
   699
   and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f -` y) \<inter> (space a) \<in> sets a" using f
paulson@33271
   700
     by (auto simp add: measurable_def)
paulson@33271
   701
  have eq: "f -` g -` y \<inter> space a = f -` (g -` y \<inter> t) \<inter> space a" using t
paulson@33271
   702
    by force
paulson@33271
   703
  show ?thesis
paulson@33271
   704
    apply (auto simp add: measurable_def vimage_compose a c) 
paulson@33271
   705
    apply (metis funcset_mem fab g) 
paulson@33271
   706
    apply (subst eq, metis ba cb) 
paulson@33271
   707
    done
paulson@33271
   708
qed
paulson@33271
   709
 
paulson@33271
   710
lemma measurable_mono1:
paulson@33271
   711
     "a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr>
paulson@33271
   712
      \<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c"
paulson@33271
   713
  by (auto simp add: measurable_def) 
paulson@33271
   714
paulson@33271
   715
lemma measurable_up_sigma:
paulson@33271
   716
   "measurable a b \<subseteq> measurable (sigma (space a) (sets a)) b"
paulson@33271
   717
  apply (auto simp add: measurable_def) 
paulson@33271
   718
  apply (metis sigma_algebra_iff2 sigma_algebra_sigma)
paulson@33271
   719
  apply (metis algebra.simps(2) sigma_algebra.sigma_sets_eq sigma_def) 
paulson@33271
   720
  done
paulson@33271
   721
paulson@33271
   722
lemma measure_preserving_up:
paulson@33271
   723
   "f \<in> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 \<Longrightarrow>
paulson@33271
   724
    measure_space m1 \<Longrightarrow> sigma_algebra m1 \<Longrightarrow> a \<subseteq> sets m1 
paulson@33271
   725
    \<Longrightarrow> f \<in> measure_preserving m1 m2"
paulson@33271
   726
  by (auto simp add: measure_preserving_def measurable_def) 
paulson@33271
   727
paulson@33271
   728
lemma measure_preserving_up_sigma:
paulson@33271
   729
   "measure_space m1 \<Longrightarrow> (sets m1 = sets (sigma (space m1) a))
paulson@33271
   730
    \<Longrightarrow> measure_preserving \<lparr>space = space m1, sets = a, measure = measure m1\<rparr> m2 
paulson@33271
   731
        \<subseteq> measure_preserving m1 m2"
paulson@33271
   732
  apply (rule subsetI) 
paulson@33271
   733
  apply (rule measure_preserving_up) 
paulson@33271
   734
  apply (simp_all add: measure_space_def sigma_def) 
paulson@33271
   735
  apply (metis sigma_algebra.sigma_sets_eq subsetI sigma_sets.Basic) 
paulson@33271
   736
  done
paulson@33271
   737
paulson@33271
   738
lemma (in sigma_algebra) measurable_prod_sigma:
paulson@33271
   739
  assumes 1: "(fst o f) \<in> measurable M a1" and 2: "(snd o f) \<in> measurable M a2"
paulson@33271
   740
  shows "f \<in> measurable M (sigma ((space a1) \<times> (space a2)) 
paulson@33271
   741
                          (prod_sets (sets a1) (sets a2)))"
paulson@33271
   742
proof -
paulson@33271
   743
  from 1 have sa1: "sigma_algebra a1" and fn1: "fst \<circ> f \<in> space M \<rightarrow> space a1"
paulson@33271
   744
     and q1: "\<forall>y\<in>sets a1. (fst \<circ> f) -` y \<inter> space M \<in> sets M"
paulson@33271
   745
    by (auto simp add: measurable_def) 
paulson@33271
   746
  from 2 have sa2: "sigma_algebra a2" and fn2: "snd \<circ> f \<in> space M \<rightarrow> space a2"
paulson@33271
   747
     and q2: "\<forall>y\<in>sets a2. (snd \<circ> f) -` y \<inter> space M \<in> sets M"
paulson@33271
   748
    by (auto simp add: measurable_def) 
paulson@33271
   749
  show ?thesis
paulson@33271
   750
    proof (rule measurable_sigma) 
paulson@33271
   751
      show "prod_sets (sets a1) (sets a2) \<subseteq> Pow (space a1 \<times> space a2)" using sa1 sa2
paulson@33271
   752
        by (force simp add: prod_sets_def sigma_algebra_iff algebra_def) 
paulson@33271
   753
    next
paulson@33271
   754
      show "f \<in> space M \<rightarrow> space a1 \<times> space a2" 
paulson@33271
   755
        by (rule prod_final [OF fn1 fn2])
paulson@33271
   756
    next
paulson@33271
   757
      fix z
paulson@33271
   758
      assume z: "z \<in> prod_sets (sets a1) (sets a2)" 
paulson@33271
   759
      thus "f -` z \<inter> space M \<in> sets M"
paulson@33271
   760
        proof (auto simp add: prod_sets_def vimage_Times) 
paulson@33271
   761
          fix x y
paulson@33271
   762
          assume x: "x \<in> sets a1" and y: "y \<in> sets a2"
paulson@33271
   763
          have "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M = 
paulson@33271
   764
                ((fst \<circ> f) -` x \<inter> space M) \<inter> ((snd \<circ> f) -` y \<inter> space M)"
paulson@33271
   765
            by blast
paulson@33271
   766
          also have "...  \<in> sets M" using x y q1 q2
paulson@33271
   767
            by blast
paulson@33271
   768
          finally show "(fst \<circ> f) -` x \<inter> (snd \<circ> f) -` y \<inter> space M \<in> sets M" .
paulson@33271
   769
        qed
paulson@33271
   770
    qed
paulson@33271
   771
qed
paulson@33271
   772
paulson@33271
   773
paulson@33271
   774
lemma (in measure_space) measurable_range_reduce:
paulson@33271
   775
   "f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> \<Longrightarrow>
paulson@33271
   776
    s \<noteq> {} 
paulson@33271
   777
    \<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>"
paulson@33271
   778
  by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast
paulson@33271
   779
paulson@33271
   780
lemma (in measure_space) measurable_Pow_to_Pow:
paulson@33271
   781
   "(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>"
paulson@33271
   782
  by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def)
paulson@33271
   783
paulson@33271
   784
lemma (in measure_space) measurable_Pow_to_Pow_image:
paulson@33271
   785
   "sets M = Pow (space M)
paulson@33271
   786
    \<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>"
paulson@33271
   787
  by (simp add: measurable_def sigma_algebra_Pow) intro_locales
paulson@33271
   788
paulson@33271
   789
lemma (in measure_space) measure_real_sum_image:
paulson@33271
   790
  assumes s: "s \<in> sets M"
paulson@33271
   791
      and ssets: "\<And>x. x \<in> s ==> {x} \<in> sets M"
paulson@33271
   792
      and fin: "finite s"
paulson@33271
   793
  shows "measure M s = (\<Sum>x\<in>s. measure M {x})"
paulson@33271
   794
proof -
paulson@33271
   795
  {
paulson@33271
   796
    fix u
paulson@33271
   797
    assume u: "u \<subseteq> s & u \<in> sets M"
paulson@33271
   798
    hence "finite u"
paulson@33271
   799
      by (metis fin finite_subset) 
paulson@33271
   800
    hence "measure M u = (\<Sum>x\<in>u. measure M {x})" using u
paulson@33271
   801
      proof (induct u)
paulson@33271
   802
        case empty
paulson@33271
   803
        thus ?case by simp
paulson@33271
   804
      next
paulson@33271
   805
        case (insert x t)
paulson@33271
   806
        hence x: "x \<in> s" and t: "t \<subseteq> s" 
paulson@33271
   807
          by (simp_all add: insert_subset) 
paulson@33271
   808
        hence ts: "t \<in> sets M"  using insert
paulson@33271
   809
          by (metis Diff_insert_absorb Diff ssets)
paulson@33271
   810
        have "measure M (insert x t) = measure M ({x} \<union> t)"
paulson@33271
   811
          by simp
paulson@33271
   812
        also have "... = measure M {x} + measure M t" 
paulson@33271
   813
          by (simp add: measure_additive insert insert_disjoint ssets x ts 
paulson@33271
   814
                  del: Un_insert_left)
paulson@33271
   815
        also have "... = (\<Sum>x\<in>insert x t. measure M {x})" 
paulson@33271
   816
          by (simp add: x t ts insert) 
paulson@33271
   817
        finally show ?case .
paulson@33271
   818
      qed
paulson@33271
   819
    }
paulson@33271
   820
  thus ?thesis
paulson@33271
   821
    by (metis subset_refl s)
paulson@33271
   822
qed
paulson@33271
   823
  
paulson@33271
   824
lemma (in sigma_algebra) sigma_algebra_extend:
paulson@33271
   825
     "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
paulson@33273
   826
   by unfold_locales (auto intro!: space_closed)
paulson@33271
   827
paulson@33271
   828
lemma (in sigma_algebra) finite_additivity_sufficient:
paulson@33271
   829
  assumes fin: "finite (space M)"
paulson@33271
   830
      and posf: "positive M f" and addf: "additive M f" 
paulson@33271
   831
  defines "Mf \<equiv> \<lparr>space = space M, sets = sets M, measure = f\<rparr>"
paulson@33271
   832
  shows "measure_space Mf" 
paulson@33271
   833
proof -
paulson@33271
   834
  have [simp]: "f {} = 0" using posf
paulson@33271
   835
    by (simp add: positive_def) 
paulson@33271
   836
  have "countably_additive Mf f"
paulson@33271
   837
    proof (auto simp add: countably_additive_def positive_def) 
paulson@33271
   838
      fix A :: "nat \<Rightarrow> 'a set"
paulson@33271
   839
      assume A: "range A \<subseteq> sets Mf"
paulson@33271
   840
         and disj: "disjoint_family A"
paulson@33271
   841
         and UnA: "(\<Union>i. A i) \<in> sets Mf"
paulson@33271
   842
      def I \<equiv> "{i. A i \<noteq> {}}"
paulson@33271
   843
      have "Union (A ` I) \<subseteq> space M" using A
paulson@33271
   844
        by (auto simp add: Mf_def) (metis range_subsetD subsetD sets_into_space) 
paulson@33271
   845
      hence "finite (A ` I)"
paulson@33271
   846
        by (metis finite_UnionD finite_subset fin) 
paulson@33271
   847
      moreover have "inj_on A I" using disj
paulson@33271
   848
        by (auto simp add: I_def disjoint_family_def inj_on_def) 
paulson@33271
   849
      ultimately have finI: "finite I"
paulson@33271
   850
        by (metis finite_imageD)
paulson@33271
   851
      hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
paulson@33271
   852
        proof (cases "I = {}")
paulson@33271
   853
          case True thus ?thesis by (simp add: I_def) 
paulson@33271
   854
        next
paulson@33271
   855
          case False
paulson@33271
   856
          hence "\<forall>i\<in>I. i < Suc(Max I)"
paulson@33271
   857
            by (simp add: Max_less_iff [symmetric] finI) 
paulson@33271
   858
          hence "\<forall>m \<ge> Suc(Max I). A m = {}"
paulson@33271
   859
            by (simp add: I_def) (metis less_le_not_le) 
paulson@33271
   860
          thus ?thesis
paulson@33271
   861
            by blast
paulson@33271
   862
        qed
paulson@33271
   863
      then obtain N where N: "\<forall>m\<ge>N. A m = {}" by blast
paulson@33271
   864
      hence "\<forall>m\<ge>N. (f o A) m = 0"
paulson@33271
   865
        by simp 
paulson@33271
   866
      hence "(\<lambda>n. f (A n)) sums setsum (f o A) {0..<N}" 
paulson@33271
   867
        by (simp add: series_zero o_def) 
paulson@33271
   868
      also have "... = f (\<Union>i<N. A i)"
paulson@33271
   869
        proof (induct N)
paulson@33271
   870
          case 0 thus ?case by simp
paulson@33271
   871
        next
paulson@33271
   872
          case (Suc n) 
paulson@33271
   873
          have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
paulson@33271
   874
            proof (rule Caratheodory.additiveD [OF addf])
paulson@33271
   875
              show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
paulson@33271
   876
                by (auto simp add: disjoint_family_def nat_less_le) blast
paulson@33271
   877
              show "A n \<in> sets M" using A 
paulson@33271
   878
                by (force simp add: Mf_def) 
paulson@33271
   879
              show "(\<Union>i<n. A i) \<in> sets M"
paulson@33271
   880
                proof (induct n)
paulson@33271
   881
                  case 0 thus ?case by simp
paulson@33271
   882
                next
paulson@33271
   883
                  case (Suc n) thus ?case using A
paulson@33271
   884
                    by (simp add: lessThan_Suc Mf_def Un range_subsetD) 
paulson@33271
   885
                qed
paulson@33271
   886
            qed
paulson@33271
   887
          thus ?case using Suc
paulson@33271
   888
            by (simp add: lessThan_Suc) 
paulson@33271
   889
        qed
paulson@33271
   890
      also have "... = f (\<Union>i. A i)" 
paulson@33271
   891
        proof -
paulson@33271
   892
          have "(\<Union> i<N. A i) = (\<Union>i. A i)" using N
paulson@33271
   893
            by auto (metis Int_absorb N disjoint_iff_not_equal lessThan_iff not_leE)
paulson@33271
   894
          thus ?thesis by simp
paulson@33271
   895
        qed
paulson@33271
   896
      finally show "(\<lambda>n. f (A n)) sums f (\<Union>i. A i)" .
paulson@33271
   897
    qed
paulson@33271
   898
  thus ?thesis using posf 
paulson@33271
   899
    by (simp add: Mf_def measure_space_def measure_space_axioms_def sigma_algebra_extend positive_def) 
paulson@33271
   900
qed
paulson@33271
   901
paulson@33271
   902
lemma finite_additivity_sufficient:
paulson@33271
   903
     "sigma_algebra M 
paulson@33271
   904
      \<Longrightarrow> finite (space M) 
paulson@33271
   905
      \<Longrightarrow> positive M (measure M) \<Longrightarrow> additive M (measure M) 
paulson@33271
   906
      \<Longrightarrow> measure_space M"
paulson@33271
   907
  by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
paulson@33271
   908
paulson@33271
   909
end
paulson@33271
   910