src/HOL/Probability/Complete_Measure.thy
author hoelzl
Wed Dec 01 19:20:30 2010 +0100 (2010-12-01)
changeset 40859 de0b30e6c2d2
child 40871 688f6ff859e1
permissions -rw-r--r--
Support product spaces on sigma finite measures.
Introduce the almost everywhere quantifier.
Introduce 'morphism' theorems for most constants.
Prove uniqueness of measures on cut stable generators.
Prove uniqueness of the Radon-Nikodym derivative.
Removed misleading suffix from borel_space and lebesgue_space.
Use product spaces to introduce Fubini on the Lebesgue integral.
Combine Euclidean_Lebesgue and Lebesgue_Measure.
Generalize theorems about mutual information and entropy to arbitrary probability spaces.
Remove simproc mult_log as it does not work with interpretations.
Introduce completion of measure spaces.
Change type of sigma.
Introduce dynkin systems.
hoelzl@40859
     1
(*  Title:      Complete_Measure.thy
hoelzl@40859
     2
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
hoelzl@40859
     3
*)
hoelzl@40859
     4
theory Complete_Measure
hoelzl@40859
     5
imports Product_Measure
hoelzl@40859
     6
begin
hoelzl@40859
     7
hoelzl@40859
     8
locale completeable_measure_space = measure_space
hoelzl@40859
     9
hoelzl@40859
    10
definition (in completeable_measure_space) completion :: "'a algebra" where
hoelzl@40859
    11
  "completion = \<lparr> space = space M,
hoelzl@40859
    12
    sets = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets \<and> N \<subseteq> N' } \<rparr>"
hoelzl@40859
    13
hoelzl@40859
    14
lemma (in completeable_measure_space) space_completion[simp]:
hoelzl@40859
    15
  "space completion = space M" unfolding completion_def by simp
hoelzl@40859
    16
hoelzl@40859
    17
lemma (in completeable_measure_space) sets_completionE:
hoelzl@40859
    18
  assumes "A \<in> sets completion"
hoelzl@40859
    19
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
hoelzl@40859
    20
  using assms unfolding completion_def by auto
hoelzl@40859
    21
hoelzl@40859
    22
lemma (in completeable_measure_space) sets_completionI:
hoelzl@40859
    23
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets" "S \<in> sets M"
hoelzl@40859
    24
  shows "A \<in> sets completion"
hoelzl@40859
    25
  using assms unfolding completion_def by auto
hoelzl@40859
    26
hoelzl@40859
    27
lemma (in completeable_measure_space) sets_completionI_sets[intro]:
hoelzl@40859
    28
  "A \<in> sets M \<Longrightarrow> A \<in> sets completion"
hoelzl@40859
    29
  unfolding completion_def by force
hoelzl@40859
    30
hoelzl@40859
    31
lemma (in completeable_measure_space) null_sets_completion:
hoelzl@40859
    32
  assumes "N' \<in> null_sets" "N \<subseteq> N'" shows "N \<in> sets completion"
hoelzl@40859
    33
  apply(rule sets_completionI[of N "{}" N N'])
hoelzl@40859
    34
  using assms by auto
hoelzl@40859
    35
hoelzl@40859
    36
sublocale completeable_measure_space \<subseteq> completion!: sigma_algebra completion
hoelzl@40859
    37
proof (unfold sigma_algebra_iff2, safe)
hoelzl@40859
    38
  fix A x assume "A \<in> sets completion" "x \<in> A"
hoelzl@40859
    39
  with sets_into_space show "x \<in> space completion"
hoelzl@40859
    40
    by (auto elim!: sets_completionE)
hoelzl@40859
    41
next
hoelzl@40859
    42
  fix A assume "A \<in> sets completion"
hoelzl@40859
    43
  from this[THEN sets_completionE] guess S N N' . note A = this
hoelzl@40859
    44
  let ?C = "space completion"
hoelzl@40859
    45
  show "?C - A \<in> sets completion" using A
hoelzl@40859
    46
    by (intro sets_completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"])
hoelzl@40859
    47
       auto
hoelzl@40859
    48
next
hoelzl@40859
    49
  fix A ::"nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion"
hoelzl@40859
    50
  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
    51
    unfolding completion_def by (auto simp: image_subset_iff)
hoelzl@40859
    52
  from choice[OF this] guess S ..
hoelzl@40859
    53
  from choice[OF this] guess N ..
hoelzl@40859
    54
  from choice[OF this] guess N' ..
hoelzl@40859
    55
  then show "UNION UNIV A \<in> sets completion"
hoelzl@40859
    56
    using null_sets_UN[of N']
hoelzl@40859
    57
    by (intro sets_completionI[of _ "UNION UNIV S" "UNION UNIV N" "UNION UNIV N'"])
hoelzl@40859
    58
       auto
hoelzl@40859
    59
qed auto
hoelzl@40859
    60
hoelzl@40859
    61
definition (in completeable_measure_space)
hoelzl@40859
    62
  "split_completion A p = (\<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and>
hoelzl@40859
    63
    fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets)"
hoelzl@40859
    64
hoelzl@40859
    65
definition (in completeable_measure_space)
hoelzl@40859
    66
  "main_part A = fst (Eps (split_completion A))"
hoelzl@40859
    67
hoelzl@40859
    68
definition (in completeable_measure_space)
hoelzl@40859
    69
  "null_part A = snd (Eps (split_completion A))"
hoelzl@40859
    70
hoelzl@40859
    71
lemma (in completeable_measure_space) split_completion:
hoelzl@40859
    72
  assumes "A \<in> sets completion"
hoelzl@40859
    73
  shows "split_completion A (main_part A, null_part A)"
hoelzl@40859
    74
  unfolding main_part_def null_part_def
hoelzl@40859
    75
proof (rule someI2_ex)
hoelzl@40859
    76
  from assms[THEN sets_completionE] guess S N N' . note A = this
hoelzl@40859
    77
  let ?P = "(S, N - S)"
hoelzl@40859
    78
  show "\<exists>p. split_completion A p"
hoelzl@40859
    79
    unfolding split_completion_def using A
hoelzl@40859
    80
  proof (intro exI conjI)
hoelzl@40859
    81
    show "A = fst ?P \<union> snd ?P" using A by auto
hoelzl@40859
    82
    show "snd ?P \<subseteq> N'" using A by auto
hoelzl@40859
    83
  qed auto
hoelzl@40859
    84
qed auto
hoelzl@40859
    85
hoelzl@40859
    86
lemma (in completeable_measure_space)
hoelzl@40859
    87
  assumes "S \<in> sets completion"
hoelzl@40859
    88
  shows main_part_sets[intro, simp]: "main_part S \<in> sets M"
hoelzl@40859
    89
    and main_part_null_part_Un[simp]: "main_part S \<union> null_part S = S"
hoelzl@40859
    90
    and main_part_null_part_Int[simp]: "main_part S \<inter> null_part S = {}"
hoelzl@40859
    91
  using split_completion[OF assms] by (auto simp: split_completion_def)
hoelzl@40859
    92
hoelzl@40859
    93
lemma (in completeable_measure_space) null_part:
hoelzl@40859
    94
  assumes "S \<in> sets completion" shows "\<exists>N. N\<in>null_sets \<and> null_part S \<subseteq> N"
hoelzl@40859
    95
  using split_completion[OF assms] by (auto simp: split_completion_def)
hoelzl@40859
    96
hoelzl@40859
    97
lemma (in completeable_measure_space) null_part_sets[intro, simp]:
hoelzl@40859
    98
  assumes "S \<in> sets M" shows "null_part S \<in> sets M" "\<mu> (null_part S) = 0"
hoelzl@40859
    99
proof -
hoelzl@40859
   100
  have S: "S \<in> sets completion" using assms by auto
hoelzl@40859
   101
  have "S - main_part S \<in> sets M" using assms by auto
hoelzl@40859
   102
  moreover
hoelzl@40859
   103
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
hoelzl@40859
   104
  have "S - main_part S = null_part S" by auto
hoelzl@40859
   105
  ultimately show sets: "null_part S \<in> sets M" by auto
hoelzl@40859
   106
  from null_part[OF S] guess N ..
hoelzl@40859
   107
  with measure_eq_0[of N "null_part S"] sets
hoelzl@40859
   108
  show "\<mu> (null_part S) = 0" by auto
hoelzl@40859
   109
qed
hoelzl@40859
   110
hoelzl@40859
   111
definition (in completeable_measure_space) "\<mu>' A = \<mu> (main_part A)"
hoelzl@40859
   112
hoelzl@40859
   113
lemma (in completeable_measure_space) \<mu>'_set[simp]:
hoelzl@40859
   114
  assumes "S \<in> sets M" shows "\<mu>' S = \<mu> S"
hoelzl@40859
   115
proof -
hoelzl@40859
   116
  have S: "S \<in> sets completion" using assms by auto
hoelzl@40859
   117
  then have "\<mu> S = \<mu> (main_part S \<union> null_part S)" by simp
hoelzl@40859
   118
  also have "\<dots> = \<mu> (main_part S)"
hoelzl@40859
   119
    using S assms measure_additive[of "main_part S" "null_part S"]
hoelzl@40859
   120
    by (auto simp: measure_additive)
hoelzl@40859
   121
  finally show ?thesis unfolding \<mu>'_def by simp
hoelzl@40859
   122
qed
hoelzl@40859
   123
hoelzl@40859
   124
lemma (in completeable_measure_space) sets_completionI_sub:
hoelzl@40859
   125
  assumes N: "N' \<in> null_sets" "N \<subseteq> N'"
hoelzl@40859
   126
  shows "N \<in> sets completion"
hoelzl@40859
   127
  using assms by (intro sets_completionI[of _ "{}" N N']) auto
hoelzl@40859
   128
hoelzl@40859
   129
lemma (in completeable_measure_space) \<mu>_main_part_UN:
hoelzl@40859
   130
  fixes S :: "nat \<Rightarrow> 'a set"
hoelzl@40859
   131
  assumes "range S \<subseteq> sets completion"
hoelzl@40859
   132
  shows "\<mu>' (\<Union>i. (S i)) = \<mu> (\<Union>i. main_part (S i))"
hoelzl@40859
   133
proof -
hoelzl@40859
   134
  have S: "\<And>i. S i \<in> sets completion" using assms by auto
hoelzl@40859
   135
  then have UN: "(\<Union>i. S i) \<in> sets completion" by auto
hoelzl@40859
   136
  have "\<forall>i. \<exists>N. N \<in> null_sets \<and> null_part (S i) \<subseteq> N"
hoelzl@40859
   137
    using null_part[OF S] by auto
hoelzl@40859
   138
  from choice[OF this] guess N .. note N = this
hoelzl@40859
   139
  then have UN_N: "(\<Union>i. N i) \<in> null_sets" by (intro null_sets_UN) auto
hoelzl@40859
   140
  have "(\<Union>i. S i) \<in> sets completion" using S by auto
hoelzl@40859
   141
  from null_part[OF this] guess N' .. note N' = this
hoelzl@40859
   142
  let ?N = "(\<Union>i. N i) \<union> N'"
hoelzl@40859
   143
  have null_set: "?N \<in> null_sets" using N' UN_N by (intro null_sets_Un) auto
hoelzl@40859
   144
  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
   145
    using N' by auto
hoelzl@40859
   146
  also have "\<dots> = (\<Union>i. main_part (S i) \<union> null_part (S i)) \<union> ?N"
hoelzl@40859
   147
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
hoelzl@40859
   148
  also have "\<dots> = (\<Union>i. main_part (S i)) \<union> ?N"
hoelzl@40859
   149
    using N by auto
hoelzl@40859
   150
  finally have *: "main_part (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part (S i)) \<union> ?N" .
hoelzl@40859
   151
  have "\<mu> (main_part (\<Union>i. S i)) = \<mu> (main_part (\<Union>i. S i) \<union> ?N)"
hoelzl@40859
   152
    using null_set UN by (intro measure_Un_null_set[symmetric]) auto
hoelzl@40859
   153
  also have "\<dots> = \<mu> ((\<Union>i. main_part (S i)) \<union> ?N)"
hoelzl@40859
   154
    unfolding * ..
hoelzl@40859
   155
  also have "\<dots> = \<mu> (\<Union>i. main_part (S i))"
hoelzl@40859
   156
    using null_set S by (intro measure_Un_null_set) auto
hoelzl@40859
   157
  finally show ?thesis unfolding \<mu>'_def .
hoelzl@40859
   158
qed
hoelzl@40859
   159
hoelzl@40859
   160
lemma (in completeable_measure_space) \<mu>_main_part_Un:
hoelzl@40859
   161
  assumes S: "S \<in> sets completion" and T: "T \<in> sets completion"
hoelzl@40859
   162
  shows "\<mu>' (S \<union> T) = \<mu> (main_part S \<union> main_part T)"
hoelzl@40859
   163
proof -
hoelzl@40859
   164
  have UN: "(\<Union>i. binary (main_part S) (main_part T) i) = (\<Union>i. main_part (binary S T i))"
hoelzl@40859
   165
    unfolding binary_def by (auto split: split_if_asm)
hoelzl@40859
   166
  show ?thesis
hoelzl@40859
   167
    using \<mu>_main_part_UN[of "binary S T"] assms
hoelzl@40859
   168
    unfolding range_binary_eq Un_range_binary UN by auto
hoelzl@40859
   169
qed
hoelzl@40859
   170
hoelzl@40859
   171
sublocale completeable_measure_space \<subseteq> completion!: measure_space completion \<mu>'
hoelzl@40859
   172
proof
hoelzl@40859
   173
  show "\<mu>' {} = 0" by auto
hoelzl@40859
   174
next
hoelzl@40859
   175
  show "countably_additive completion \<mu>'"
hoelzl@40859
   176
  proof (unfold countably_additive_def, intro allI conjI impI)
hoelzl@40859
   177
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets completion" "disjoint_family A"
hoelzl@40859
   178
    have "disjoint_family (\<lambda>i. main_part (A i))"
hoelzl@40859
   179
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
hoelzl@40859
   180
      fix n m assume "A n \<inter> A m = {}"
hoelzl@40859
   181
      then have "(main_part (A n) \<union> null_part (A n)) \<inter> (main_part (A m) \<union> null_part (A m)) = {}"
hoelzl@40859
   182
        using A by (subst (1 2) main_part_null_part_Un) auto
hoelzl@40859
   183
      then show "main_part (A n) \<inter> main_part (A m) = {}" by auto
hoelzl@40859
   184
    qed
hoelzl@40859
   185
    then have "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu> (\<Union>i. main_part (A i))"
hoelzl@40859
   186
      unfolding \<mu>'_def using A by (intro measure_countably_additive) auto
hoelzl@40859
   187
    then show "(\<Sum>\<^isub>\<infinity>n. \<mu>' (A n)) = \<mu>' (UNION UNIV A)"
hoelzl@40859
   188
      unfolding \<mu>_main_part_UN[OF A(1)] .
hoelzl@40859
   189
  qed
hoelzl@40859
   190
qed
hoelzl@40859
   191
hoelzl@40859
   192
lemma (in sigma_algebra) simple_functionD':
hoelzl@40859
   193
  assumes "simple_function f"
hoelzl@40859
   194
  shows "f -` {x} \<inter> space M \<in> sets M"
hoelzl@40859
   195
proof cases
hoelzl@40859
   196
  assume "x \<in> f`space M" from simple_functionD(2)[OF assms this] show ?thesis .
hoelzl@40859
   197
next
hoelzl@40859
   198
  assume "x \<notin> f`space M" then have "f -` {x} \<inter> space M = {}" by auto
hoelzl@40859
   199
  then show ?thesis by auto
hoelzl@40859
   200
qed
hoelzl@40859
   201
hoelzl@40859
   202
lemma (in sigma_algebra) simple_function_If:
hoelzl@40859
   203
  assumes sf: "simple_function f" "simple_function g" and A: "A \<in> sets M"
hoelzl@40859
   204
  shows "simple_function (\<lambda>x. if x \<in> A then f x else g x)" (is "simple_function ?IF")
hoelzl@40859
   205
proof -
hoelzl@40859
   206
  def F \<equiv> "\<lambda>x. f -` {x} \<inter> space M" and G \<equiv> "\<lambda>x. g -` {x} \<inter> space M"
hoelzl@40859
   207
  show ?thesis unfolding simple_function_def
hoelzl@40859
   208
  proof safe
hoelzl@40859
   209
    have "?IF ` space M \<subseteq> f ` space M \<union> g ` space M" by auto
hoelzl@40859
   210
    from finite_subset[OF this] assms
hoelzl@40859
   211
    show "finite (?IF ` space M)" unfolding simple_function_def by auto
hoelzl@40859
   212
  next
hoelzl@40859
   213
    fix x assume "x \<in> space M"
hoelzl@40859
   214
    then have *: "?IF -` {?IF x} \<inter> space M = (if x \<in> A
hoelzl@40859
   215
      then ((F (f x) \<inter> A) \<union> (G (f x) - (G (f x) \<inter> A)))
hoelzl@40859
   216
      else ((F (g x) \<inter> A) \<union> (G (g x) - (G (g x) \<inter> A))))"
hoelzl@40859
   217
      using sets_into_space[OF A] by (auto split: split_if_asm simp: G_def F_def)
hoelzl@40859
   218
    have [intro]: "\<And>x. F x \<in> sets M" "\<And>x. G x \<in> sets M"
hoelzl@40859
   219
      unfolding F_def G_def using sf[THEN simple_functionD'] by auto
hoelzl@40859
   220
    show "?IF -` {?IF x} \<inter> space M \<in> sets M" unfolding * using A by auto
hoelzl@40859
   221
  qed
hoelzl@40859
   222
qed
hoelzl@40859
   223
hoelzl@40859
   224
lemma (in measure_space) null_sets_finite_UN:
hoelzl@40859
   225
  assumes "finite S" "\<And>i. i \<in> S \<Longrightarrow> A i \<in> null_sets"
hoelzl@40859
   226
  shows "(\<Union>i\<in>S. A i) \<in> null_sets"
hoelzl@40859
   227
proof (intro CollectI conjI)
hoelzl@40859
   228
  show "(\<Union>i\<in>S. A i) \<in> sets M" using assms by (intro finite_UN) auto
hoelzl@40859
   229
  have "\<mu> (\<Union>i\<in>S. A i) \<le> (\<Sum>i\<in>S. \<mu> (A i))"
hoelzl@40859
   230
    using assms by (intro measure_finitely_subadditive) auto
hoelzl@40859
   231
  then show "\<mu> (\<Union>i\<in>S. A i) = 0"
hoelzl@40859
   232
    using assms by auto
hoelzl@40859
   233
qed
hoelzl@40859
   234
hoelzl@40859
   235
lemma (in completeable_measure_space) completion_ex_simple_function:
hoelzl@40859
   236
  assumes f: "completion.simple_function f"
hoelzl@40859
   237
  shows "\<exists>f'. simple_function f' \<and> (AE x. f x = f' x)"
hoelzl@40859
   238
proof -
hoelzl@40859
   239
  let "?F x" = "f -` {x} \<inter> space M"
hoelzl@40859
   240
  have F: "\<And>x. ?F x \<in> sets completion" and fin: "finite (f`space M)"
hoelzl@40859
   241
    using completion.simple_functionD'[OF f]
hoelzl@40859
   242
      completion.simple_functionD[OF f] by simp_all
hoelzl@40859
   243
  have "\<forall>x. \<exists>N. N \<in> null_sets \<and> null_part (?F x) \<subseteq> N"
hoelzl@40859
   244
    using F null_part by auto
hoelzl@40859
   245
  from choice[OF this] obtain N where
hoelzl@40859
   246
    N: "\<And>x. null_part (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets" by auto
hoelzl@40859
   247
  let ?N = "\<Union>x\<in>f`space M. N x" let "?f' x" = "if x \<in> ?N then undefined else f x"
hoelzl@40859
   248
  have sets: "?N \<in> null_sets" using N fin by (intro null_sets_finite_UN) auto
hoelzl@40859
   249
  show ?thesis unfolding simple_function_def
hoelzl@40859
   250
  proof (safe intro!: exI[of _ ?f'])
hoelzl@40859
   251
    have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
hoelzl@40859
   252
    from finite_subset[OF this] completion.simple_functionD(1)[OF f]
hoelzl@40859
   253
    show "finite (?f' ` space M)" by auto
hoelzl@40859
   254
  next
hoelzl@40859
   255
    fix x assume "x \<in> space M"
hoelzl@40859
   256
    have "?f' -` {?f' x} \<inter> space M =
hoelzl@40859
   257
      (if x \<in> ?N then ?F undefined \<union> ?N
hoelzl@40859
   258
       else if f x = undefined then ?F (f x) \<union> ?N
hoelzl@40859
   259
       else ?F (f x) - ?N)"
hoelzl@40859
   260
      using N(2) sets_into_space by (auto split: split_if_asm)
hoelzl@40859
   261
    moreover { fix y have "?F y \<union> ?N \<in> sets M"
hoelzl@40859
   262
      proof cases
hoelzl@40859
   263
        assume y: "y \<in> f`space M"
hoelzl@40859
   264
        have "?F y \<union> ?N = (main_part (?F y) \<union> null_part (?F y)) \<union> ?N"
hoelzl@40859
   265
          using main_part_null_part_Un[OF F] by auto
hoelzl@40859
   266
        also have "\<dots> = main_part (?F y) \<union> ?N"
hoelzl@40859
   267
          using y N by auto
hoelzl@40859
   268
        finally show ?thesis
hoelzl@40859
   269
          using F sets by auto
hoelzl@40859
   270
      next
hoelzl@40859
   271
        assume "y \<notin> f`space M" then have "?F y = {}" by auto
hoelzl@40859
   272
        then show ?thesis using sets by auto
hoelzl@40859
   273
      qed }
hoelzl@40859
   274
    moreover {
hoelzl@40859
   275
      have "?F (f x) - ?N = main_part (?F (f x)) \<union> null_part (?F (f x)) - ?N"
hoelzl@40859
   276
        using main_part_null_part_Un[OF F] by auto
hoelzl@40859
   277
      also have "\<dots> = main_part (?F (f x)) - ?N"
hoelzl@40859
   278
        using N `x \<in> space M` by auto
hoelzl@40859
   279
      finally have "?F (f x) - ?N \<in> sets M"
hoelzl@40859
   280
        using F sets by auto }
hoelzl@40859
   281
    ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
hoelzl@40859
   282
  next
hoelzl@40859
   283
    show "AE x. f x = ?f' x"
hoelzl@40859
   284
      by (rule AE_I', rule sets) auto
hoelzl@40859
   285
  qed
hoelzl@40859
   286
qed
hoelzl@40859
   287
hoelzl@40859
   288
lemma (in completeable_measure_space) completion_ex_borel_measurable:
hoelzl@40859
   289
  fixes g :: "'a \<Rightarrow> pinfreal"
hoelzl@40859
   290
  assumes g: "g \<in> borel_measurable completion"
hoelzl@40859
   291
  shows "\<exists>g'\<in>borel_measurable M. (AE x. g x = g' x)"
hoelzl@40859
   292
proof -
hoelzl@40859
   293
  from g[THEN completion.borel_measurable_implies_simple_function_sequence]
hoelzl@40859
   294
  obtain f where "\<And>i. completion.simple_function (f i)" "f \<up> g" by auto
hoelzl@40859
   295
  then have "\<forall>i. \<exists>f'. simple_function f' \<and> (AE x. f i x = f' x)"
hoelzl@40859
   296
    using completion_ex_simple_function by auto
hoelzl@40859
   297
  from this[THEN choice] obtain f' where
hoelzl@40859
   298
    sf: "\<And>i. simple_function (f' i)" and
hoelzl@40859
   299
    AE: "\<forall>i. AE x. f i x = f' i x" by auto
hoelzl@40859
   300
  show ?thesis
hoelzl@40859
   301
  proof (intro bexI)
hoelzl@40859
   302
    from AE[unfolded all_AE_countable]
hoelzl@40859
   303
    show "AE x. g x = (SUP i. f' i) x" (is "AE x. g x = ?f x")
hoelzl@40859
   304
    proof (rule AE_mp, safe intro!: AE_cong)
hoelzl@40859
   305
      fix x assume eq: "\<forall>i. f i x = f' i x"
hoelzl@40859
   306
      have "g x = (SUP i. f i x)"
hoelzl@40859
   307
        using `f \<up> g` unfolding isoton_def SUPR_fun_expand by auto
hoelzl@40859
   308
      then show "g x = ?f x"
hoelzl@40859
   309
        using eq unfolding SUPR_fun_expand by auto
hoelzl@40859
   310
    qed
hoelzl@40859
   311
    show "?f \<in> borel_measurable M"
hoelzl@40859
   312
      using sf by (auto intro!: borel_measurable_SUP
hoelzl@40859
   313
        intro: borel_measurable_simple_function)
hoelzl@40859
   314
  qed
hoelzl@40859
   315
qed
hoelzl@40859
   316
hoelzl@40859
   317
end