src/HOL/Probability/Complete_Measure.thy
author hoelzl
Tue Mar 22 18:53:05 2011 +0100 (2011-03-22)
changeset 42066 6db76c88907a
parent 41983 2dc6e382a58b
child 42146 5b52c6a9c627
permissions -rw-r--r--
generalized Caratheodory from algebra to ring_of_sets
wenzelm@41983
     1
(*  Title:      HOL/Probability/Complete_Measure.thy
hoelzl@40859
     2
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
hoelzl@40859
     3
*)
wenzelm@41983
     4
hoelzl@40859
     5
theory Complete_Measure
hoelzl@40859
     6
imports Product_Measure
hoelzl@40859
     7
begin
hoelzl@40859
     8
hoelzl@40859
     9
locale completeable_measure_space = measure_space
hoelzl@40859
    10
hoelzl@41689
    11
definition (in completeable_measure_space)
hoelzl@41689
    12
  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
hoelzl@41689
    13
    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
hoelzl@41689
    14
hoelzl@41689
    15
definition (in completeable_measure_space)
hoelzl@41689
    16
  "main_part A = fst (Eps (split_completion A))"
hoelzl@41689
    17
hoelzl@41689
    18
definition (in completeable_measure_space)
hoelzl@41689
    19
  "null_part A = snd (Eps (split_completion A))"
hoelzl@41689
    20
hoelzl@41689
    21
abbreviation (in completeable_measure_space) "\<mu>' A \<equiv> \<mu> (main_part A)"
hoelzl@41689
    22
hoelzl@41689
    23
definition (in completeable_measure_space) completion :: "('a, 'b) measure_space_scheme" where
hoelzl@40859
    24
  "completion = \<lparr> space = space M,
hoelzl@41689
    25
                  sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' },
hoelzl@41689
    26
                  measure = \<mu>',
hoelzl@41689
    27
                  \<dots> = more M \<rparr>"
hoelzl@41689
    28
hoelzl@40859
    29
hoelzl@40859
    30
lemma (in completeable_measure_space) space_completion[simp]:
hoelzl@40859
    31
  "space completion = space M" unfolding completion_def by simp
hoelzl@40859
    32
hoelzl@40859
    33
lemma (in completeable_measure_space) sets_completionE:
hoelzl@40859
    34
  assumes "A \<in> sets completion"
hoelzl@40859
    35
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
hoelzl@40859
    36
  using assms unfolding completion_def by auto
hoelzl@40859
    37
hoelzl@40859
    38
lemma (in completeable_measure_space) sets_completionI:
hoelzl@40859
    39
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
hoelzl@40859
    40
  shows "A \<in> sets completion"
hoelzl@40859
    41
  using assms unfolding completion_def by auto
hoelzl@40859
    42
hoelzl@40859
    43
lemma (in completeable_measure_space) sets_completionI_sets[intro]:
hoelzl@40859
    44
  "A \<in> sets M \<Longrightarrow> A \<in> sets completion"
hoelzl@40859
    45
  unfolding completion_def by force
hoelzl@40859
    46
hoelzl@40859
    47
lemma (in completeable_measure_space) null_sets_completion:
hoelzl@40859
    48
  assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
hoelzl@40859
    49
  apply(rule sets_completionI[of N "{}" N N'])
hoelzl@40859
    50
  using assms by auto
hoelzl@40859
    51
hoelzl@40859
    52
sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
hoelzl@40859
    53
proof (unfold sigma_algebra_iff2, safe)
hoelzl@40859
    54
  fix A x assume "A \<in> sets completion" "x \<in> A"
hoelzl@40859
    55
  with sets_into_space show "x \<in> space completion"
hoelzl@40859
    56
    by (auto elim!: sets_completionE)
hoelzl@40859
    57
next
hoelzl@40859
    58
  fix A assume "A \<in> sets completion"
hoelzl@40859
    59
  from this[THEN sets_completionE] guess S N N' . note A = this
hoelzl@40859
    60
  let ?C = "space completion"
hoelzl@40859
    61
  show "?C - A \<in> sets completion" using A
hoelzl@40859
    62
    by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
hoelzl@40859
    63
       auto
hoelzl@40859
    64
next
hoelzl@40859
    65
  fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
hoelzl@40859
    66
  then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N'"
hoelzl@40859
    67
    unfolding completion_def by (auto simp: image_subset_iff)
hoelzl@40859
    68
  from choice[OF this] guess S ..
hoelzl@40859
    69
  from choice[OF this] guess N ..
hoelzl@40859
    70
  from choice[OF this] guess N' ..
hoelzl@40859
    71
  then show "UNION UNIV A \<in> sets completion"
hoelzl@40859
    72
    using null_sets_UN[of N']
hoelzl@40859
    73
    by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
hoelzl@40859
    74
       auto
hoelzl@40859
    75
qed auto
hoelzl@40859
    76
hoelzl@40859
    77
lemma (in completeable_measure_space) split_completion:
hoelzl@40859
    78
  assumes "A \<in> sets completion"
hoelzl@40859
    79
  shows "split_completion A (main_part A, null_part A)"
hoelzl@40859
    80
  unfolding main_part_def null_part_def
hoelzl@40859
    81
proof (rule someI2_ex)
hoelzl@40859
    82
  from assms[THEN sets_completionE] guess S N N' . note A = this
hoelzl@40859
    83
  let ?P = "(S, N - S)"
hoelzl@40859
    84
  show "\<exists>p. split_completion A p"
hoelzl@40859
    85
    unfolding split_completion_def using A
hoelzl@40859
    86
  proof (intro exI conjI)
hoelzl@40859
    87
    show "A = fst ?P \<union> snd ?P" using A by auto
hoelzl@40859
    88
    show "snd ?P \<subseteq> N'" using A by auto
hoelzl@40859
    89
  qed auto
hoelzl@40859
    90
qed auto
hoelzl@40859
    91
hoelzl@40859
    92
lemma (in completeable_measure_space)
hoelzl@40859
    93
  assumes "S \<in> sets completion"
hoelzl@40859
    94
  shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
hoelzl@40859
    95
    and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
hoelzl@40859
    96
    and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
hoelzl@40859
    97
  using split_completion[OF assms] by (auto simp: split_completion_def)
hoelzl@40859
    98
hoelzl@40859
    99
lemma (in completeable_measure_space) null_part:
hoelzl@40859
   100
  assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
hoelzl@40859
   101
  using split_completion[OF assms] by (auto simp: split_completion_def)
hoelzl@40859
   102
hoelzl@40859
   103
lemma (in completeable_measure_space) null_part_sets[intro, simp]:
hoelzl@40859
   104
  assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
hoelzl@40859
   105
proof -
hoelzl@40859
   106
  have S: "S \<in> sets completion" using assms by auto
hoelzl@40859
   107
  have "S - main_part S \<in> sets M" using assms by auto
hoelzl@40859
   108
  moreover
hoelzl@40859
   109
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
hoelzl@40859
   110
  have "S - main_part S = null_part S" by auto
hoelzl@40859
   111
  ultimately show sets: "null_part S \<in> sets M" by auto
hoelzl@40859
   112
  from null_part[OF S] guess N ..
hoelzl@40859
   113
  with measure_eq_0[of N "null_part S"] sets
hoelzl@40859
   114
  show "\<mu> (null_part S) = 0" by auto
hoelzl@40859
   115
qed
hoelzl@40859
   116
hoelzl@40859
   117
lemma (in completeable_measure_space) \<mu>'_set[simp]:
hoelzl@40859
   118
  assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
hoelzl@40859
   119
proof -
hoelzl@40859
   120
  have S: "S \<in> sets completion" using assms by auto
hoelzl@40859
   121
  then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
hoelzl@41689
   122
  also have "\<dots> = \<mu>' S"
hoelzl@40859
   123
    using S assms measure_additive[of "main_part S" "null_part S"]
hoelzl@40859
   124
    by (auto simp: measure_additive)
hoelzl@41689
   125
  finally show ?thesis by simp
hoelzl@40859
   126
qed
hoelzl@40859
   127
hoelzl@40859
   128
lemma (in completeable_measure_space) sets_completionI_sub:
hoelzl@40859
   129
  assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
hoelzl@40859
   130
  shows "N \<in> sets completion"
hoelzl@40859
   131
  using assms by (intro sets_completionI[of _ "{}" N N']) auto
hoelzl@40859
   132
hoelzl@40859
   133
lemma (in completeable_measure_space) \<mu>_main_part_UN:
hoelzl@40859
   134
  fixes S :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   135
  assumes "range S \<subseteq> sets completion"
hoelzl@40859
   136
  shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
hoelzl@40859
   137
proof -
hoelzl@40859
   138
  have S: "\<And>i. S i \<in> sets completion" using assms by auto
hoelzl@40859
   139
  then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
hoelzl@40859
   140
  have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
hoelzl@40859
   141
    using null_part[OF S] by auto
hoelzl@40859
   142
  from choice[OF this] guess N .. note N = this
hoelzl@40859
   143
  then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
hoelzl@40859
   144
  have "(\<Union>i. S i) \<in> sets completion" using S by auto
hoelzl@40859
   145
  from null_part[OF this] guess N' .. note N' = this
hoelzl@40859
   146
  let ?N = "(\<Union>i. N i) \<union> N'"
hoelzl@40859
   147
  have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
hoelzl@40859
   148
  have "main_part (\<Union>i. S i) \<union> ?N = (main_part (\<Union>i. S i) \<union> null_part (\<Union>i. S i)) \<union> ?N"
hoelzl@40859
   149
    using N' by auto
hoelzl@40859
   150
  also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
hoelzl@40859
   151
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
hoelzl@40859
   152
  also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
hoelzl@40859
   153
    using N by auto
hoelzl@40859
   154
  finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
hoelzl@40859
   155
  have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
hoelzl@40859
   156
    using null_set UN by (intro measure_Un_null_set[symmetric]) auto
hoelzl@40859
   157
  also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
hoelzl@40859
   158
    unfolding * ..
hoelzl@40859
   159
  also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
hoelzl@40859
   160
    using null_set S by (intro measure_Un_null_set) auto
hoelzl@41689
   161
  finally show ?thesis .
hoelzl@40859
   162
qed
hoelzl@40859
   163
hoelzl@40859
   164
lemma (in completeable_measure_space) \<mu>_main_part_Un:
hoelzl@40859
   165
  assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
hoelzl@40859
   166
  shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
hoelzl@40859
   167
proof -
hoelzl@40859
   168
  have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
hoelzl@40859
   169
    unfolding binary_def by (auto split: split_if_asm)
hoelzl@40859
   170
  show ?thesis
hoelzl@40859
   171
    using \<mu>_main_part_UN[of "binary S T"] assms
hoelzl@40859
   172
    unfolding range_binary_eq Un_range_binary UN by auto
hoelzl@40859
   173
qed
hoelzl@40859
   174
hoelzl@41689
   175
sublocale completeable_measure_space \<subseteq> completion!: measure_space completion
hoelzl@41689
   176
  where "measure completion = \<mu>'"
hoelzl@41689
   177
proof -
hoelzl@41689
   178
  show "measure_space completion"
hoelzl@41689
   179
  proof
hoelzl@41981
   180
    show "positive completion (measure completion)"
hoelzl@41981
   181
      by (auto simp: completion_def positive_def)
hoelzl@41689
   182
  next
hoelzl@41689
   183
    show "countably_additive completion (measure completion)"
hoelzl@41689
   184
    proof (intro countably_additiveI)
hoelzl@41689
   185
      fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
hoelzl@41689
   186
      have "disjoint_family (\<lambda>i. main_part (A i))"
hoelzl@41689
   187
      proof (intro disjoint_family_on_bisimulation[OF A(2)])
hoelzl@41689
   188
        fix n m assume "A n \<inter> A m = {}"
hoelzl@41689
   189
        then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
hoelzl@41689
   190
          using A by (subst (1 2) main_part_null_part_Un) auto
hoelzl@41689
   191
        then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
hoelzl@41689
   192
      qed
hoelzl@41981
   193
      then have "(\<Sum>n. measure completion (A n)) = \<mu> (\<Union>i. main_part (A i))"
hoelzl@41689
   194
        unfolding completion_def using A by (auto intro!: measure_countably_additive)
hoelzl@41981
   195
      then show "(\<Sum>n. measure completion (A n)) = measure completion (UNION UNIV A)"
hoelzl@41689
   196
        by (simp add: completion_def \<mu>_main_part_UN[OF A(1)])
hoelzl@40859
   197
    qed
hoelzl@40859
   198
  qed
hoelzl@41689
   199
  show "measure completion = \<mu>'" unfolding completion_def by simp
hoelzl@40859
   200
qed
hoelzl@40859
   201
hoelzl@40859
   202
lemma (in completeable_measure_space) completion_ex_simple_function:
hoelzl@41689
   203
  assumes f: "simple_function completion f"
hoelzl@41689
   204
  shows "\<exists>f'. simple_function M f' \<and> (AE x. f x = f' x)"
hoelzl@40859
   205
proof -
hoelzl@40859
   206
  let "?F x" = "f -` {x} \<inter> space M"
hoelzl@40859
   207
  have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
hoelzl@40871
   208
    using completion.simple_functionD[OF f]
hoelzl@40859
   209
      completion.simple_functionD[OF f] by simp_all
hoelzl@40859
   210
  have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
hoelzl@40859
   211
    using F null_part by auto
hoelzl@40859
   212
  from choice[OF this] obtain N where
hoelzl@40859
   213
    N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
hoelzl@40859
   214
  let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
hoelzl@40859
   215
  have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
hoelzl@40859
   216
  show ?thesis unfolding simple_function_def
hoelzl@40859
   217
  proof (safe intro!: exI[of _ ?f'])
hoelzl@40859
   218
    have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
hoelzl@40859
   219
    from finite_subset[OF this] completion.simple_functionD(1)[OF f]
hoelzl@40859
   220
    show "finite (?f' ` space M)" by auto
hoelzl@40859
   221
  next
hoelzl@40859
   222
    fix x assume "x \<in> space M"
hoelzl@40859
   223
    have "?f' -` {?f' x} \<inter> space M =
hoelzl@40859
   224
      (if x \<in> ?N then ?F undefined \<union> ?N
hoelzl@40859
   225
       else if f x = undefined then ?F (f x) \<union> ?N
hoelzl@40859
   226
       else ?F (f x) - ?N)"
hoelzl@40859
   227
      using N(2) sets_into_space by (auto split: split_if_asm)
hoelzl@40859
   228
    moreover { fix y have "?F y \<union> ?N \<in> sets M"
hoelzl@40859
   229
      proof cases
hoelzl@40859
   230
        assume y: "y \<in> f`space M"
hoelzl@40859
   231
        have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
hoelzl@40859
   232
          using main_part_null_part_Un[OF F] by auto
hoelzl@40859
   233
        also have "\<dots> = main_part (?F y) \<union> ?N"
hoelzl@40859
   234
          using y N by auto
hoelzl@40859
   235
        finally show ?thesis
hoelzl@40859
   236
          using F sets by auto
hoelzl@40859
   237
      next
hoelzl@40859
   238
        assume "y \<notin> f`space M" then have "?F y = {}" by auto
hoelzl@40859
   239
        then show ?thesis using sets by auto
hoelzl@40859
   240
      qed }
hoelzl@40859
   241
    moreover {
hoelzl@40859
   242
      have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
hoelzl@40859
   243
        using main_part_null_part_Un[OF F] by auto
hoelzl@40859
   244
      also have "\<dots> = main_part (?F (f x)) - ?N"
hoelzl@40859
   245
        using N `x \<in> space M` by auto
hoelzl@40859
   246
      finally have "?F (f x) - ?N \<in> sets M"
hoelzl@40859
   247
        using F sets by auto }
hoelzl@40859
   248
    ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
hoelzl@40859
   249
  next
hoelzl@40859
   250
    show "AE x. f x = ?f' x"
hoelzl@40859
   251
      by (rule AE_I', rule sets) auto
hoelzl@40859
   252
  qed
hoelzl@40859
   253
qed
hoelzl@40859
   254
hoelzl@41981
   255
lemma (in completeable_measure_space) completion_ex_borel_measurable_pos:
hoelzl@41981
   256
  fixes g :: "'a \<Rightarrow> extreal"
hoelzl@41981
   257
  assumes g: "g \<in> borel_measurable completion" and "\<And>x. 0 \<le> g x"
hoelzl@40859
   258
  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
hoelzl@40859
   259
proof -
hoelzl@41981
   260
  from g[THEN completion.borel_measurable_implies_simple_function_sequence'] guess f . note f = this
hoelzl@41981
   261
  from this(1)[THEN completion_ex_simple_function]
hoelzl@41981
   262
  have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x. f i x = f' x)" ..
hoelzl@40859
   263
  from this[THEN choice] obtain f' where
hoelzl@41689
   264
    sf: "\<And>i. simple_function M (f' i)" and
hoelzl@40859
   265
    AE: "\<forall>i. AE x. f i x = f' i x" by auto
hoelzl@40859
   266
  show ?thesis
hoelzl@40859
   267
  proof (intro bexI)
hoelzl@41981
   268
    from AE[unfolded AE_all_countable[symmetric]]
hoelzl@41097
   269
    show "AE x. g x = (SUP i. f' i x)" (is "AE x. g x = ?f x")
hoelzl@41705
   270
    proof (elim AE_mp, safe intro!: AE_I2)
hoelzl@40859
   271
      fix x assume eq: "\<forall>i. f i x = f' i x"
hoelzl@41981
   272
      moreover have "g x = (SUP i. f i x)"
hoelzl@41981
   273
        unfolding f using `0 \<le> g x` by (auto split: split_max)
hoelzl@41981
   274
      ultimately show "g x = ?f x" by auto
hoelzl@40859
   275
    qed
hoelzl@40859
   276
    show "?f \<in> borel_measurable M"
hoelzl@41097
   277
      using sf by (auto intro: borel_measurable_simple_function)
hoelzl@40859
   278
  qed
hoelzl@40859
   279
qed
hoelzl@40859
   280
hoelzl@41981
   281
lemma (in completeable_measure_space) completion_ex_borel_measurable:
hoelzl@41981
   282
  fixes g :: "'a \<Rightarrow> extreal"
hoelzl@41981
   283
  assumes g: "g \<in> borel_measurable completion"
hoelzl@41981
   284
  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
hoelzl@41981
   285
proof -
hoelzl@41981
   286
  have "(\<lambda>x. max 0 (g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (g x)" using g by auto
hoelzl@41981
   287
  from completion_ex_borel_measurable_pos[OF this] guess g_pos ..
hoelzl@41981
   288
  moreover
hoelzl@41981
   289
  have "(\<lambda>x. max 0 (- g x)) \<in> borel_measurable completion" "\<And>x. 0 \<le> max 0 (- g x)" using g by auto
hoelzl@41981
   290
  from completion_ex_borel_measurable_pos[OF this] guess g_neg ..
hoelzl@41981
   291
  ultimately
hoelzl@41981
   292
  show ?thesis
hoelzl@41981
   293
  proof (safe intro!: bexI[of _ "\<lambda>x. g_pos x - g_neg x"])
hoelzl@41981
   294
    show "AE x. max 0 (- g x) = g_neg x \<longrightarrow> max 0 (g x) = g_pos x \<longrightarrow> g x = g_pos x - g_neg x"
hoelzl@41981
   295
    proof (intro AE_I2 impI)
hoelzl@41981
   296
      fix x assume g: "max 0 (- g x) = g_neg x" "max 0 (g x) = g_pos x"
hoelzl@41981
   297
      show "g x = g_pos x - g_neg x" unfolding g[symmetric]
hoelzl@41981
   298
        by (cases "g x") (auto split: split_max)
hoelzl@41981
   299
    qed
hoelzl@41981
   300
  qed auto
hoelzl@41981
   301
qed
hoelzl@41981
   302
hoelzl@40859
   303
end