src/HOL/Analysis/Complete_Measure.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (3 weeks ago)
changeset 69981 3dced198b9ec
parent 69566 c41954ee87cf
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
hoelzl@63627
     1
(*  Title:      HOL/Analysis/Complete_Measure.thy
hoelzl@40859
     2
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
hoelzl@40859
     3
*)
eberlm@69447
     4
section \<open>Complete Measures\<close>
hoelzl@40859
     5
theory Complete_Measure
hoelzl@63626
     6
  imports Bochner_Integration
hoelzl@40859
     7
begin
hoelzl@40859
     8
eberlm@69447
     9
locale%important complete_measure =
hoelzl@63940
    10
  fixes M :: "'a measure"
hoelzl@63940
    11
  assumes complete: "\<And>A B. B \<subseteq> A \<Longrightarrow> A \<in> null_sets M \<Longrightarrow> B \<in> sets M"
hoelzl@63940
    12
eberlm@69447
    13
definition%important
hoelzl@47694
    14
  "split_completion M A p = (if A \<in> sets M then p = (A, {}) else
hoelzl@47694
    15
   \<exists>N'. A = fst p \<union> snd p \<and> fst p \<inter> snd p = {} \<and> fst p \<in> sets M \<and> snd p \<subseteq> N' \<and> N' \<in> null_sets M)"
hoelzl@41689
    16
eberlm@69447
    17
definition%important
hoelzl@47694
    18
  "main_part M A = fst (Eps (split_completion M A))"
hoelzl@41689
    19
eberlm@69447
    20
definition%important
hoelzl@47694
    21
  "null_part M A = snd (Eps (split_completion M A))"
hoelzl@40859
    22
eberlm@69447
    23
definition%important completion :: "'a measure \<Rightarrow> 'a measure" where
hoelzl@47694
    24
  "completion M = measure_of (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }
hoelzl@47694
    25
    (emeasure M \<circ> main_part M)"
hoelzl@40859
    26
hoelzl@47694
    27
lemma completion_into_space:
hoelzl@47694
    28
  "{ S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' } \<subseteq> Pow (space M)"
immler@50244
    29
  using sets.sets_into_space by auto
hoelzl@40859
    30
hoelzl@47694
    31
lemma space_completion[simp]: "space (completion M) = space M"
hoelzl@47694
    32
  unfolding completion_def using space_measure_of[OF completion_into_space] by simp
hoelzl@40859
    33
hoelzl@47694
    34
lemma completionI:
hoelzl@47694
    35
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
hoelzl@47694
    36
  shows "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
hoelzl@40859
    37
  using assms by auto
hoelzl@40859
    38
hoelzl@47694
    39
lemma completionE:
hoelzl@47694
    40
  assumes "A \<in> { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
hoelzl@47694
    41
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
hoelzl@47694
    42
  using assms by auto
hoelzl@47694
    43
hoelzl@47694
    44
lemma sigma_algebra_completion:
hoelzl@47694
    45
  "sigma_algebra (space M) { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
hoelzl@47694
    46
    (is "sigma_algebra _ ?A")
hoelzl@47694
    47
  unfolding sigma_algebra_iff2
hoelzl@47694
    48
proof (intro conjI ballI allI impI)
hoelzl@47694
    49
  show "?A \<subseteq> Pow (space M)"
immler@50244
    50
    using sets.sets_into_space by auto
hoelzl@40859
    51
next
hoelzl@47694
    52
  show "{} \<in> ?A" by auto
hoelzl@40859
    53
next
hoelzl@47694
    54
  let ?C = "space M"
hoelzl@47694
    55
  fix A assume "A \<in> ?A" from completionE[OF this] guess S N N' .
hoelzl@47694
    56
  then show "space M - A \<in> ?A"
hoelzl@47694
    57
    by (intro completionI[of _ "(?C - S) \<inter> (?C - N')" "(?C - S) \<inter> N' \<inter> (?C - N)"]) auto
hoelzl@47694
    58
next
hoelzl@47694
    59
  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> ?A"
hoelzl@47694
    60
  then have "\<forall>n. \<exists>S N N'. A n = S \<union> N \<and> S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N'"
hoelzl@47694
    61
    by (auto simp: image_subset_iff)
hoelzl@40859
    62
  from choice[OF this] guess S ..
hoelzl@40859
    63
  from choice[OF this] guess N ..
hoelzl@40859
    64
  from choice[OF this] guess N' ..
haftmann@69313
    65
  then show "\<Union>(A ` UNIV) \<in> ?A"
hoelzl@40859
    66
    using null_sets_UN[of N']
haftmann@69313
    67
    by (intro completionI[of _ "\<Union>(S ` UNIV)" "\<Union>(N ` UNIV)" "\<Union>(N' ` UNIV)"]) auto
hoelzl@47694
    68
qed
hoelzl@47694
    69
eberlm@69447
    70
lemma%important sets_completion:
hoelzl@47694
    71
  "sets (completion M) = { S \<union> N |S N N'. S \<in> sets M \<and> N' \<in> null_sets M \<and> N \<subseteq> N' }"
eberlm@69447
    72
  using%unimportant sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion] 
eberlm@69447
    73
  by (simp add: completion_def)
hoelzl@47694
    74
hoelzl@47694
    75
lemma sets_completionE:
hoelzl@47694
    76
  assumes "A \<in> sets (completion M)"
hoelzl@47694
    77
  obtains S N N' where "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
hoelzl@47694
    78
  using assms unfolding sets_completion by auto
hoelzl@47694
    79
hoelzl@47694
    80
lemma sets_completionI:
hoelzl@47694
    81
  assumes "A = S \<union> N" "N \<subseteq> N'" "N' \<in> null_sets M" "S \<in> sets M"
hoelzl@47694
    82
  shows "A \<in> sets (completion M)"
hoelzl@47694
    83
  using assms unfolding sets_completion by auto
hoelzl@47694
    84
hoelzl@47694
    85
lemma sets_completionI_sets[intro, simp]:
hoelzl@47694
    86
  "A \<in> sets M \<Longrightarrow> A \<in> sets (completion M)"
hoelzl@47694
    87
  unfolding sets_completion by force
hoelzl@40859
    88
eberlm@69447
    89
lemma%important measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
eberlm@69447
    90
  by%unimportant (auto simp: measurable_def)
hoelzl@63958
    91
hoelzl@47694
    92
lemma null_sets_completion:
hoelzl@47694
    93
  assumes "N' \<in> null_sets M" "N \<subseteq> N'" shows "N \<in> sets (completion M)"
hoelzl@47694
    94
  using assms by (intro sets_completionI[of N "{}" N N']) auto
hoelzl@47694
    95
eberlm@69447
    96
lemma%important split_completion:
hoelzl@47694
    97
  assumes "A \<in> sets (completion M)"
hoelzl@47694
    98
  shows "split_completion M A (main_part M A, null_part M A)"
eberlm@69447
    99
proof%unimportant cases
hoelzl@47694
   100
  assume "A \<in> sets M" then show ?thesis
hoelzl@47694
   101
    by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
hoelzl@47694
   102
next
hoelzl@47694
   103
  assume nA: "A \<notin> sets M"
hoelzl@47694
   104
  show ?thesis
hoelzl@47694
   105
    unfolding main_part_def null_part_def if_not_P[OF nA]
hoelzl@47694
   106
  proof (rule someI2_ex)
hoelzl@47694
   107
    from assms[THEN sets_completionE] guess S N N' . note A = this
hoelzl@47694
   108
    let ?P = "(S, N - S)"
hoelzl@47694
   109
    show "\<exists>p. split_completion M A p"
hoelzl@47694
   110
      unfolding split_completion_def if_not_P[OF nA] using A
hoelzl@47694
   111
    proof (intro exI conjI)
hoelzl@47694
   112
      show "A = fst ?P \<union> snd ?P" using A by auto
hoelzl@47694
   113
      show "snd ?P \<subseteq> N'" using A by auto
hoelzl@47694
   114
   qed auto
hoelzl@40859
   115
  qed auto
hoelzl@47694
   116
qed
hoelzl@40859
   117
lp15@67982
   118
lemma sets_restrict_space_subset:
lp15@67982
   119
  assumes S: "S \<in> sets (completion M)"
lp15@67982
   120
  shows "sets (restrict_space (completion M) S) \<subseteq> sets (completion M)"
lp15@67982
   121
  by (metis assms sets.Int_space_eq2 sets_restrict_space_iff subsetI)
lp15@67982
   122
hoelzl@47694
   123
lemma
hoelzl@47694
   124
  assumes "S \<in> sets (completion M)"
hoelzl@47694
   125
  shows main_part_sets[intro, simp]: "main_part M S \<in> sets M"
hoelzl@47694
   126
    and main_part_null_part_Un[simp]: "main_part M S \<union> null_part M S = S"
hoelzl@47694
   127
    and main_part_null_part_Int[simp]: "main_part M S \<inter> null_part M S = {}"
hoelzl@47694
   128
  using split_completion[OF assms]
nipkow@62390
   129
  by (auto simp: split_completion_def split: if_split_asm)
hoelzl@40859
   130
hoelzl@47694
   131
lemma main_part[simp]: "S \<in> sets M \<Longrightarrow> main_part M S = S"
hoelzl@47694
   132
  using split_completion[of S M]
nipkow@62390
   133
  by (auto simp: split_completion_def split: if_split_asm)
hoelzl@40859
   134
hoelzl@47694
   135
lemma null_part:
hoelzl@47694
   136
  assumes "S \<in> sets (completion M)" shows "\<exists>N. N\<in>null_sets M \<and> null_part M S \<subseteq> N"
nipkow@62390
   137
  using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm)
hoelzl@47694
   138
hoelzl@47694
   139
lemma null_part_sets[intro, simp]:
hoelzl@47694
   140
  assumes "S \<in> sets M" shows "null_part M S \<in> sets M" "emeasure M (null_part M S) = 0"
hoelzl@40859
   141
proof -
hoelzl@47694
   142
  have S: "S \<in> sets (completion M)" using assms by auto
hoelzl@47694
   143
  have "S - main_part M S \<in> sets M" using assms by auto
hoelzl@40859
   144
  moreover
hoelzl@40859
   145
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
hoelzl@47694
   146
  have "S - main_part M S = null_part M S" by auto
hoelzl@47694
   147
  ultimately show sets: "null_part M S \<in> sets M" by auto
hoelzl@40859
   148
  from null_part[OF S] guess N ..
hoelzl@47694
   149
  with emeasure_eq_0[of N _ "null_part M S"] sets
hoelzl@47694
   150
  show "emeasure M (null_part M S) = 0" by auto
hoelzl@40859
   151
qed
hoelzl@40859
   152
hoelzl@47694
   153
lemma emeasure_main_part_UN:
hoelzl@40859
   154
  fixes S :: "nat \<Rightarrow> 'a set"
hoelzl@47694
   155
  assumes "range S \<subseteq> sets (completion M)"
hoelzl@47694
   156
  shows "emeasure M (main_part M (\<Union>i. (S i))) = emeasure M (\<Union>i. main_part M (S i))"
hoelzl@40859
   157
proof -
hoelzl@47694
   158
  have S: "\<And>i. S i \<in> sets (completion M)" using assms by auto
hoelzl@47694
   159
  then have UN: "(\<Union>i. S i) \<in> sets (completion M)" by auto
hoelzl@47694
   160
  have "\<forall>i. \<exists>N. N \<in> null_sets M \<and> null_part M (S i) \<subseteq> N"
hoelzl@40859
   161
    using null_part[OF S] by auto
hoelzl@40859
   162
  from choice[OF this] guess N .. note N = this
hoelzl@47694
   163
  then have UN_N: "(\<Union>i. N i) \<in> null_sets M" by (intro null_sets_UN) auto
hoelzl@47694
   164
  have "(\<Union>i. S i) \<in> sets (completion M)" using S by auto
hoelzl@40859
   165
  from null_part[OF this] guess N' .. note N' = this
hoelzl@40859
   166
  let ?N = "(\<Union>i. N i) \<union> N'"
hoelzl@47694
   167
  have null_set: "?N \<in> null_sets M" using N' UN_N by (intro null_sets.Un) auto
hoelzl@47694
   168
  have "main_part M (\<Union>i. S i) \<union> ?N = (main_part M (\<Union>i. S i) \<union> null_part M (\<Union>i. S i)) \<union> ?N"
hoelzl@40859
   169
    using N' by auto
hoelzl@47694
   170
  also have "\<dots> = (\<Union>i. main_part M (S i) \<union> null_part M (S i)) \<union> ?N"
hoelzl@40859
   171
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
hoelzl@47694
   172
  also have "\<dots> = (\<Union>i. main_part M (S i)) \<union> ?N"
hoelzl@40859
   173
    using N by auto
hoelzl@47694
   174
  finally have *: "main_part M (\<Union>i. S i) \<union> ?N = (\<Union>i. main_part M (S i)) \<union> ?N" .
hoelzl@47694
   175
  have "emeasure M (main_part M (\<Union>i. S i)) = emeasure M (main_part M (\<Union>i. S i) \<union> ?N)"
hoelzl@47694
   176
    using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto
hoelzl@47694
   177
  also have "\<dots> = emeasure M ((\<Union>i. main_part M (S i)) \<union> ?N)"
hoelzl@40859
   178
    unfolding * ..
hoelzl@47694
   179
  also have "\<dots> = emeasure M (\<Union>i. main_part M (S i))"
hoelzl@47694
   180
    using null_set S by (intro emeasure_Un_null_set) auto
hoelzl@41689
   181
  finally show ?thesis .
hoelzl@40859
   182
qed
hoelzl@40859
   183
eberlm@69447
   184
lemma%important emeasure_completion[simp]:
eberlm@69447
   185
  assumes S: "S \<in> sets (completion M)"
eberlm@69447
   186
  shows "emeasure (completion M) S = emeasure M (main_part M S)"
eberlm@69447
   187
proof%unimportant (subst emeasure_measure_of[OF completion_def completion_into_space])
hoelzl@47694
   188
  let ?\<mu> = "emeasure M \<circ> main_part M"
hoelzl@47694
   189
  show "S \<in> sets (completion M)" "?\<mu> S = emeasure M (main_part M S) " using S by simp_all
hoelzl@47694
   190
  show "positive (sets (completion M)) ?\<mu>"
hoelzl@62975
   191
    by (simp add: positive_def)
hoelzl@47694
   192
  show "countably_additive (sets (completion M)) ?\<mu>"
hoelzl@47694
   193
  proof (intro countably_additiveI)
hoelzl@47694
   194
    fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets (completion M)" "disjoint_family A"
hoelzl@47694
   195
    have "disjoint_family (\<lambda>i. main_part M (A i))"
hoelzl@47694
   196
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
hoelzl@47694
   197
      fix n m assume "A n \<inter> A m = {}"
hoelzl@47694
   198
      then have "(main_part M (A n) \<union> null_part M (A n)) \<inter> (main_part M (A m) \<union> null_part M (A m)) = {}"
hoelzl@47694
   199
        using A by (subst (1 2) main_part_null_part_Un) auto
hoelzl@47694
   200
      then show "main_part M (A n) \<inter> main_part M (A m) = {}" by auto
hoelzl@47694
   201
    qed
hoelzl@47694
   202
    then have "(\<Sum>n. emeasure M (main_part M (A n))) = emeasure M (\<Union>i. main_part M (A i))"
hoelzl@47694
   203
      using A by (auto intro!: suminf_emeasure)
haftmann@69313
   204
    then show "(\<Sum>n. ?\<mu> (A n)) = ?\<mu> (\<Union>(A ` UNIV))"
hoelzl@47694
   205
      by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
hoelzl@47694
   206
  qed
hoelzl@40859
   207
qed
hoelzl@40859
   208
hoelzl@63968
   209
lemma measure_completion[simp]: "S \<in> sets M \<Longrightarrow> measure (completion M) S = measure M S"
hoelzl@63968
   210
  unfolding measure_def by auto
hoelzl@63968
   211
hoelzl@47694
   212
lemma emeasure_completion_UN:
hoelzl@47694
   213
  "range S \<subseteq> sets (completion M) \<Longrightarrow>
hoelzl@47694
   214
    emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
hoelzl@47694
   215
  by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN)
hoelzl@40859
   216
hoelzl@47694
   217
lemma emeasure_completion_Un:
hoelzl@47694
   218
  assumes S: "S \<in> sets (completion M)" and T: "T \<in> sets (completion M)"
hoelzl@47694
   219
  shows "emeasure (completion M) (S \<union> T) = emeasure M (main_part M S \<union> main_part M T)"
hoelzl@47694
   220
proof (subst emeasure_completion)
hoelzl@47694
   221
  have UN: "(\<Union>i. binary (main_part M S) (main_part M T) i) = (\<Union>i. main_part M (binary S T i))"
nipkow@62390
   222
    unfolding binary_def by (auto split: if_split_asm)
hoelzl@47694
   223
  show "emeasure M (main_part M (S \<union> T)) = emeasure M (main_part M S \<union> main_part M T)"
hoelzl@47694
   224
    using emeasure_main_part_UN[of "binary S T" M] assms
haftmann@62343
   225
    by (simp add: range_binary_eq, simp add: Un_range_binary UN)
hoelzl@47694
   226
qed (auto intro: S T)
hoelzl@47694
   227
hoelzl@47694
   228
lemma sets_completionI_sub:
hoelzl@47694
   229
  assumes N: "N' \<in> null_sets M" "N \<subseteq> N'"
hoelzl@47694
   230
  shows "N \<in> sets (completion M)"
hoelzl@47694
   231
  using assms by (intro sets_completionI[of _ "{}" N N']) auto
hoelzl@47694
   232
hoelzl@47694
   233
lemma completion_ex_simple_function:
hoelzl@47694
   234
  assumes f: "simple_function (completion M) f"
hoelzl@47694
   235
  shows "\<exists>f'. simple_function M f' \<and> (AE x in M. f x = f' x)"
hoelzl@40859
   236
proof -
wenzelm@46731
   237
  let ?F = "\<lambda>x. f -` {x} \<inter> space M"
hoelzl@47694
   238
  have F: "\<And>x. ?F x \<in> sets (completion M)" and fin: "finite (f`space M)"
hoelzl@47694
   239
    using simple_functionD[OF f] simple_functionD[OF f] by simp_all
hoelzl@47694
   240
  have "\<forall>x. \<exists>N. N \<in> null_sets M \<and> null_part M (?F x) \<subseteq> N"
hoelzl@40859
   241
    using F null_part by auto
hoelzl@40859
   242
  from choice[OF this] obtain N where
hoelzl@47694
   243
    N: "\<And>x. null_part M (?F x) \<subseteq> N x" "\<And>x. N x \<in> null_sets M" by auto
wenzelm@46731
   244
  let ?N = "\<Union>x\<in>f`space M. N x"
wenzelm@46731
   245
  let ?f' = "\<lambda>x. if x \<in> ?N then undefined else f x"
hoelzl@47694
   246
  have sets: "?N \<in> null_sets M" using N fin by (intro null_sets.finite_UN) auto
hoelzl@40859
   247
  show ?thesis unfolding simple_function_def
hoelzl@40859
   248
  proof (safe intro!: exI[of _ ?f'])
hoelzl@40859
   249
    have "?f' ` space M \<subseteq> f`space M \<union> {undefined}" by auto
hoelzl@47694
   250
    from finite_subset[OF this] simple_functionD(1)[OF f]
hoelzl@40859
   251
    show "finite (?f' ` space M)" by auto
hoelzl@40859
   252
  next
hoelzl@40859
   253
    fix x assume "x \<in> space M"
hoelzl@40859
   254
    have "?f' -` {?f' x} \<inter> space M =
hoelzl@40859
   255
      (if x \<in> ?N then ?F undefined \<union> ?N
hoelzl@40859
   256
       else if f x = undefined then ?F (f x) \<union> ?N
hoelzl@40859
   257
       else ?F (f x) - ?N)"
nipkow@62390
   258
      using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def)
hoelzl@40859
   259
    moreover { fix y have "?F y \<union> ?N \<in> sets M"
hoelzl@40859
   260
      proof cases
hoelzl@40859
   261
        assume y: "y \<in> f`space M"
hoelzl@47694
   262
        have "?F y \<union> ?N = (main_part M (?F y) \<union> null_part M (?F y)) \<union> ?N"
hoelzl@40859
   263
          using main_part_null_part_Un[OF F] by auto
hoelzl@47694
   264
        also have "\<dots> = main_part M (?F y) \<union> ?N"
hoelzl@40859
   265
          using y N by auto
hoelzl@40859
   266
        finally show ?thesis
hoelzl@40859
   267
          using F sets by auto
hoelzl@40859
   268
      next
hoelzl@40859
   269
        assume "y \<notin> f`space M" then have "?F y = {}" by auto
hoelzl@40859
   270
        then show ?thesis using sets by auto
hoelzl@40859
   271
      qed }
hoelzl@40859
   272
    moreover {
hoelzl@47694
   273
      have "?F (f x) - ?N = main_part M (?F (f x)) \<union> null_part M (?F (f x)) - ?N"
hoelzl@40859
   274
        using main_part_null_part_Un[OF F] by auto
hoelzl@47694
   275
      also have "\<dots> = main_part M (?F (f x)) - ?N"
wenzelm@61808
   276
        using N \<open>x \<in> space M\<close> by auto
hoelzl@40859
   277
      finally have "?F (f x) - ?N \<in> sets M"
hoelzl@40859
   278
        using F sets by auto }
hoelzl@40859
   279
    ultimately show "?f' -` {?f' x} \<inter> space M \<in> sets M" by auto
hoelzl@40859
   280
  next
hoelzl@47694
   281
    show "AE x in M. f x = ?f' x"
hoelzl@40859
   282
      by (rule AE_I', rule sets) auto
hoelzl@40859
   283
  qed
hoelzl@40859
   284
qed
hoelzl@40859
   285
eberlm@69447
   286
lemma%important completion_ex_borel_measurable:
hoelzl@62975
   287
  fixes g :: "'a \<Rightarrow> ennreal"
hoelzl@62975
   288
  assumes g: "g \<in> borel_measurable (completion M)"
hoelzl@47694
   289
  shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
eberlm@69447
   290
proof%unimportant -
hoelzl@47694
   291
  from g[THEN borel_measurable_implies_simple_function_sequence'] guess f . note f = this
hoelzl@41981
   292
  from this(1)[THEN completion_ex_simple_function]
hoelzl@47694
   293
  have "\<forall>i. \<exists>f'. simple_function M f' \<and> (AE x in M. f i x = f' x)" ..
hoelzl@40859
   294
  from this[THEN choice] obtain f' where
hoelzl@41689
   295
    sf: "\<And>i. simple_function M (f' i)" and
hoelzl@47694
   296
    AE: "\<forall>i. AE x in M. f i x = f' i x" by auto
hoelzl@40859
   297
  show ?thesis
hoelzl@40859
   298
  proof (intro bexI)
hoelzl@41981
   299
    from AE[unfolded AE_all_countable[symmetric]]
hoelzl@47694
   300
    show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
hoelzl@41705
   301
    proof (elim AE_mp, safe intro!: AE_I2)
hoelzl@40859
   302
      fix x assume eq: "\<forall>i. f i x = f' i x"
hoelzl@41981
   303
      moreover have "g x = (SUP i. f i x)"
hoelzl@62975
   304
        unfolding f by (auto split: split_max)
hoelzl@41981
   305
      ultimately show "g x = ?f x" by auto
hoelzl@40859
   306
    qed
hoelzl@40859
   307
    show "?f \<in> borel_measurable M"
hoelzl@56949
   308
      using sf[THEN borel_measurable_simple_function] by auto
hoelzl@40859
   309
  qed
hoelzl@40859
   310
qed
hoelzl@40859
   311
hoelzl@58587
   312
lemma null_sets_completionI: "N \<in> null_sets M \<Longrightarrow> N \<in> null_sets (completion M)"
hoelzl@58587
   313
  by (auto simp: null_sets_def)
hoelzl@58587
   314
hoelzl@58587
   315
lemma AE_completion: "(AE x in M. P x) \<Longrightarrow> (AE x in completion M. P x)"
hoelzl@58587
   316
  unfolding eventually_ae_filter by (auto intro: null_sets_completionI)
hoelzl@58587
   317
hoelzl@58587
   318
lemma null_sets_completion_iff: "N \<in> sets M \<Longrightarrow> N \<in> null_sets (completion M) \<longleftrightarrow> N \<in> null_sets M"
hoelzl@58587
   319
  by (auto simp: null_sets_def)
hoelzl@58587
   320
hoelzl@63940
   321
lemma sets_completion_AE: "(AE x in M. \<not> P x) \<Longrightarrow> Measurable.pred (completion M) P"
hoelzl@63940
   322
  unfolding pred_def sets_completion eventually_ae_filter
hoelzl@63940
   323
  by auto
hoelzl@63940
   324
hoelzl@63940
   325
lemma null_sets_completion_iff2:
hoelzl@63940
   326
  "A \<in> null_sets (completion M) \<longleftrightarrow> (\<exists>N'\<in>null_sets M. A \<subseteq> N')"
hoelzl@63940
   327
proof safe
hoelzl@63940
   328
  assume "A \<in> null_sets (completion M)"
hoelzl@63940
   329
  then have A: "A \<in> sets (completion M)" and "main_part M A \<in> null_sets M"
hoelzl@63940
   330
    by (auto simp: null_sets_def)
hoelzl@63940
   331
  moreover obtain N where "N \<in> null_sets M" "null_part M A \<subseteq> N"
hoelzl@63940
   332
    using null_part[OF A] by auto
hoelzl@63940
   333
  ultimately show "\<exists>N'\<in>null_sets M. A \<subseteq> N'"
hoelzl@63940
   334
  proof (intro bexI)
hoelzl@63940
   335
    show "A \<subseteq> N \<union> main_part M A"
hoelzl@63940
   336
      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[OF A, symmetric]) auto
hoelzl@63940
   337
  qed auto
hoelzl@63940
   338
next
hoelzl@63940
   339
  fix N assume "N \<in> null_sets M" "A \<subseteq> N"
hoelzl@63940
   340
  then have "A \<in> sets (completion M)" and N: "N \<in> sets M" "A \<subseteq> N" "emeasure M N = 0"
hoelzl@63940
   341
    by (auto intro: null_sets_completion)
hoelzl@63940
   342
  moreover have "emeasure (completion M) A = 0"
hoelzl@63940
   343
    using N by (intro emeasure_eq_0[of N _ A]) auto
hoelzl@63940
   344
  ultimately show "A \<in> null_sets (completion M)"
hoelzl@63940
   345
    by auto
hoelzl@63940
   346
qed
hoelzl@63940
   347
hoelzl@63940
   348
lemma null_sets_completion_subset:
hoelzl@63940
   349
  "B \<subseteq> A \<Longrightarrow> A \<in> null_sets (completion M) \<Longrightarrow> B \<in> null_sets (completion M)"
hoelzl@63940
   350
  unfolding null_sets_completion_iff2 by auto
hoelzl@63940
   351
hoelzl@63958
   352
interpretation completion: complete_measure "completion M" for M
hoelzl@63958
   353
proof
hoelzl@63958
   354
  show "B \<subseteq> A \<Longrightarrow> A \<in> null_sets (completion M) \<Longrightarrow> B \<in> sets (completion M)" for B A
hoelzl@63958
   355
    using null_sets_completion_subset[of B A M] by (simp add: null_sets_def)
hoelzl@63958
   356
qed
hoelzl@63958
   357
hoelzl@63940
   358
lemma null_sets_restrict_space:
hoelzl@63940
   359
  "\<Omega> \<in> sets M \<Longrightarrow> A \<in> null_sets (restrict_space M \<Omega>) \<longleftrightarrow> A \<subseteq> \<Omega> \<and> A \<in> null_sets M"
hoelzl@63940
   360
  by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)
hoelzl@63941
   361
hoelzl@63940
   362
lemma completion_ex_borel_measurable_real:
hoelzl@63940
   363
  fixes g :: "'a \<Rightarrow> real"
hoelzl@63940
   364
  assumes g: "g \<in> borel_measurable (completion M)"
hoelzl@63940
   365
  shows "\<exists>g'\<in>borel_measurable M. (AE x in M. g x = g' x)"
hoelzl@63940
   366
proof -
hoelzl@63940
   367
  have "(\<lambda>x. ennreal (g x)) \<in> completion M \<rightarrow>\<^sub>M borel" "(\<lambda>x. ennreal (- g x)) \<in> completion M \<rightarrow>\<^sub>M borel"
hoelzl@63940
   368
    using g by auto
hoelzl@63940
   369
  from this[THEN completion_ex_borel_measurable]
hoelzl@63940
   370
  obtain pf nf :: "'a \<Rightarrow> ennreal"
hoelzl@63940
   371
    where [measurable]: "nf \<in> M \<rightarrow>\<^sub>M borel" "pf \<in> M \<rightarrow>\<^sub>M borel"
hoelzl@63940
   372
      and ae: "AE x in M. pf x = ennreal (g x)" "AE x in M. nf x = ennreal (- g x)"
hoelzl@63940
   373
    by (auto simp: eq_commute)
hoelzl@63940
   374
  then have "AE x in M. pf x = ennreal (g x) \<and> nf x = ennreal (- g x)"
hoelzl@63940
   375
    by auto
hoelzl@63940
   376
  then obtain N where "N \<in> null_sets M" "{x\<in>space M. pf x \<noteq> ennreal (g x) \<and> nf x \<noteq> ennreal (- g x)} \<subseteq> N"
hoelzl@63940
   377
    by (auto elim!: AE_E)
hoelzl@63940
   378
  show ?thesis
hoelzl@63940
   379
  proof
hoelzl@63940
   380
    let ?F = "\<lambda>x. indicator (space M - N) x * (enn2real (pf x) - enn2real (nf x))"
hoelzl@63940
   381
    show "?F \<in> M \<rightarrow>\<^sub>M borel"
hoelzl@63940
   382
      using \<open>N \<in> null_sets M\<close> by auto
hoelzl@63940
   383
    show "AE x in M. g x = ?F x"
hoelzl@63940
   384
      using \<open>N \<in> null_sets M\<close>[THEN AE_not_in] ae AE_space
hoelzl@63940
   385
      apply eventually_elim
hoelzl@63940
   386
      subgoal for x
hoelzl@63940
   387
        by (cases "0::real" "g x" rule: linorder_le_cases) (auto simp: ennreal_neg)
hoelzl@63940
   388
      done
hoelzl@63940
   389
  qed
hoelzl@63940
   390
qed
hoelzl@63940
   391
hoelzl@63940
   392
lemma simple_function_completion: "simple_function M f \<Longrightarrow> simple_function (completion M) f"
hoelzl@63940
   393
  by (simp add: simple_function_def)
hoelzl@63940
   394
hoelzl@63940
   395
lemma simple_integral_completion:
hoelzl@63940
   396
  "simple_function M f \<Longrightarrow> simple_integral (completion M) f = simple_integral M f"
hoelzl@63940
   397
  unfolding simple_integral_def by simp
hoelzl@63940
   398
hoelzl@63940
   399
lemma nn_integral_completion: "nn_integral (completion M) f = nn_integral M f"
hoelzl@63940
   400
  unfolding nn_integral_def
hoelzl@63940
   401
proof (safe intro!: SUP_eq)
hoelzl@63940
   402
  fix s assume s: "simple_function (completion M) s" and "s \<le> f"
hoelzl@63940
   403
  then obtain s' where s': "simple_function M s'" "AE x in M. s x = s' x"
hoelzl@63940
   404
    by (auto dest: completion_ex_simple_function)
hoelzl@63940
   405
  then obtain N where N: "N \<in> null_sets M" "{x\<in>space M. s x \<noteq> s' x} \<subseteq> N"
hoelzl@63940
   406
    by (auto elim!: AE_E)
hoelzl@63940
   407
  then have ae_N: "AE x in M. (s x \<noteq> s' x \<longrightarrow> x \<in> N) \<and> x \<notin> N"
hoelzl@63940
   408
    by (auto dest: AE_not_in)
hoelzl@63940
   409
  define s'' where "s'' x = (if x \<in> N then 0 else s x)" for x
hoelzl@63940
   410
  then have ae_s_eq_s'': "AE x in completion M. s x = s'' x"
hoelzl@63940
   411
    using s' ae_N by (intro AE_completion) auto
hoelzl@63940
   412
  have s'': "simple_function M s''"
hoelzl@63940
   413
  proof (subst simple_function_cong)
hoelzl@63940
   414
    show "t \<in> space M \<Longrightarrow> s'' t = (if t \<in> N then 0 else s' t)" for t
hoelzl@63940
   415
      using N by (auto simp: s''_def dest: sets.sets_into_space)
hoelzl@63940
   416
    show "simple_function M (\<lambda>t. if t \<in> N then 0 else s' t)"
hoelzl@63940
   417
      unfolding s''_def[abs_def] using N by (auto intro!: simple_function_If s')
hoelzl@63940
   418
  qed
hoelzl@63940
   419
hoelzl@63940
   420
  show "\<exists>j\<in>{g. simple_function M g \<and> g \<le> f}. integral\<^sup>S (completion M) s \<le> integral\<^sup>S M j"
hoelzl@63940
   421
  proof (safe intro!: bexI[of _ s''])
hoelzl@63940
   422
    have "integral\<^sup>S (completion M) s = integral\<^sup>S (completion M) s''"
hoelzl@63940
   423
      by (intro simple_integral_cong_AE s simple_function_completion s'' ae_s_eq_s'')
hoelzl@63940
   424
    then show "integral\<^sup>S (completion M) s \<le> integral\<^sup>S M s''"
hoelzl@63940
   425
      using s'' by (simp add: simple_integral_completion)
hoelzl@63940
   426
    from \<open>s \<le> f\<close> show "s'' \<le> f"
hoelzl@63940
   427
      unfolding s''_def le_fun_def by auto
hoelzl@63940
   428
  qed fact
hoelzl@63940
   429
next
hoelzl@63940
   430
  fix s assume "simple_function M s" "s \<le> f"
hoelzl@63940
   431
  then show "\<exists>j\<in>{g. simple_function (completion M) g \<and> g \<le> f}. integral\<^sup>S M s \<le> integral\<^sup>S (completion M) j"
hoelzl@63940
   432
    by (intro bexI[of _ s]) (auto simp: simple_integral_completion simple_function_completion)
hoelzl@63940
   433
qed
hoelzl@63940
   434
hoelzl@63958
   435
lemma integrable_completion:
hoelzl@63958
   436
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@63958
   437
  shows "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> integrable (completion M) f \<longleftrightarrow> integrable M f"
hoelzl@63958
   438
  by (rule integrable_subalgebra[symmetric]) auto
hoelzl@63958
   439
hoelzl@63958
   440
lemma integral_completion:
hoelzl@63958
   441
  fixes f :: "'a \<Rightarrow> 'b::{banach, second_countable_topology}"
hoelzl@63958
   442
  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
hoelzl@63958
   443
  by (rule integral_subalgebra[symmetric]) (auto intro: f)
hoelzl@63958
   444
eberlm@69447
   445
locale%important semifinite_measure =
hoelzl@63940
   446
  fixes M :: "'a measure"
hoelzl@63940
   447
  assumes semifinite:
hoelzl@63940
   448
    "\<And>A. A \<in> sets M \<Longrightarrow> emeasure M A = \<infinity> \<Longrightarrow> \<exists>B\<in>sets M. B \<subseteq> A \<and> emeasure M B < \<infinity>"
hoelzl@63940
   449
eberlm@69447
   450
locale%important locally_determined_measure = semifinite_measure +
hoelzl@63940
   451
  assumes locally_determined:
hoelzl@63940
   452
    "\<And>A. A \<subseteq> space M \<Longrightarrow> (\<And>B. B \<in> sets M \<Longrightarrow> emeasure M B < \<infinity> \<Longrightarrow> A \<inter> B \<in> sets M) \<Longrightarrow> A \<in> sets M"
hoelzl@63940
   453
eberlm@69447
   454
locale%important cld_measure =
eberlm@69447
   455
  complete_measure M + locally_determined_measure M for M :: "'a measure"
hoelzl@63940
   456
eberlm@69447
   457
definition%important outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
haftmann@69260
   458
  where "outer_measure_of M A = (INF B \<in> {B\<in>sets M. A \<subseteq> B}. emeasure M B)"
hoelzl@63940
   459
hoelzl@63940
   460
lemma outer_measure_of_eq[simp]: "A \<in> sets M \<Longrightarrow> outer_measure_of M A = emeasure M A"
hoelzl@63940
   461
  by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono)
hoelzl@63940
   462
hoelzl@63940
   463
lemma outer_measure_of_mono: "A \<subseteq> B \<Longrightarrow> outer_measure_of M A \<le> outer_measure_of M B"
hoelzl@63940
   464
  unfolding outer_measure_of_def by (intro INF_superset_mono) auto
hoelzl@63940
   465
hoelzl@63940
   466
lemma outer_measure_of_attain:
hoelzl@63940
   467
  assumes "A \<subseteq> space M"
hoelzl@63940
   468
  shows "\<exists>E\<in>sets M. A \<subseteq> E \<and> outer_measure_of M A = emeasure M E"
hoelzl@63940
   469
proof -
hoelzl@63940
   470
  have "emeasure M ` {B \<in> sets M. A \<subseteq> B} \<noteq> {}"
hoelzl@63940
   471
    using \<open>A \<subseteq> space M\<close> by auto
hoelzl@63940
   472
  from ennreal_Inf_countable_INF[OF this]
hoelzl@63940
   473
  obtain f
hoelzl@63940
   474
    where f: "range f \<subseteq> emeasure M ` {B \<in> sets M. A \<subseteq> B}" "decseq f"
hoelzl@63940
   475
      and "outer_measure_of M A = (INF i. f i)"
hoelzl@63940
   476
    unfolding outer_measure_of_def by auto
hoelzl@63940
   477
  have "\<exists>E. \<forall>n. (E n \<in> sets M \<and> A \<subseteq> E n \<and> emeasure M (E n) \<le> f n) \<and> E (Suc n) \<subseteq> E n"
hoelzl@63940
   478
  proof (rule dependent_nat_choice)
hoelzl@63940
   479
    show "\<exists>x. x \<in> sets M \<and> A \<subseteq> x \<and> emeasure M x \<le> f 0"
hoelzl@63940
   480
      using f(1) by (fastforce simp: image_subset_iff image_iff intro: eq_refl[OF sym])
hoelzl@63940
   481
  next
hoelzl@63940
   482
    fix E n assume "E \<in> sets M \<and> A \<subseteq> E \<and> emeasure M E \<le> f n"
hoelzl@63940
   483
    moreover obtain F where "F \<in> sets M" "A \<subseteq> F" "f (Suc n) = emeasure M F"
hoelzl@63940
   484
      using f(1) by (auto simp: image_subset_iff image_iff)
hoelzl@63940
   485
    ultimately show "\<exists>y. (y \<in> sets M \<and> A \<subseteq> y \<and> emeasure M y \<le> f (Suc n)) \<and> y \<subseteq> E"
hoelzl@63940
   486
      by (auto intro!: exI[of _ "F \<inter> E"] emeasure_mono)
hoelzl@63940
   487
  qed
hoelzl@63940
   488
  then obtain E
hoelzl@63940
   489
    where [simp]: "\<And>n. E n \<in> sets M"
hoelzl@63940
   490
      and "\<And>n. A \<subseteq> E n"
hoelzl@63940
   491
      and le_f: "\<And>n. emeasure M (E n) \<le> f n"
hoelzl@63940
   492
      and "decseq E"
hoelzl@63940
   493
    by (auto simp: decseq_Suc_iff)
hoelzl@63940
   494
  show ?thesis
hoelzl@63940
   495
  proof cases
hoelzl@63940
   496
    assume fin: "\<exists>i. emeasure M (E i) < \<infinity>"
hoelzl@63940
   497
    show ?thesis
hoelzl@63940
   498
    proof (intro bexI[of _ "\<Inter>i. E i"] conjI)
hoelzl@63940
   499
      show "A \<subseteq> (\<Inter>i. E i)" "(\<Inter>i. E i) \<in> sets M"
hoelzl@63940
   500
        using \<open>\<And>n. A \<subseteq> E n\<close> by auto
hoelzl@63940
   501
hoelzl@63940
   502
      have " (INF i. emeasure M (E i)) \<le> outer_measure_of M A"
hoelzl@63940
   503
        unfolding \<open>outer_measure_of M A = (INF n. f n)\<close>
hoelzl@63940
   504
        by (intro INF_superset_mono le_f) auto
hoelzl@63940
   505
      moreover have "outer_measure_of M A \<le> (INF i. outer_measure_of M (E i))"
hoelzl@63940
   506
        by (intro INF_greatest outer_measure_of_mono \<open>\<And>n. A \<subseteq> E n\<close>)
hoelzl@63940
   507
      ultimately have "outer_measure_of M A = (INF i. emeasure M (E i))"
hoelzl@63940
   508
        by auto
hoelzl@63940
   509
      also have "\<dots> = emeasure M (\<Inter>i. E i)"
hoelzl@63940
   510
        using fin by (intro INF_emeasure_decseq' \<open>decseq E\<close>) (auto simp: less_top)
hoelzl@63940
   511
      finally show "outer_measure_of M A = emeasure M (\<Inter>i. E i)" .
hoelzl@63940
   512
    qed
hoelzl@63940
   513
  next
hoelzl@63940
   514
    assume "\<nexists>i. emeasure M (E i) < \<infinity>"
hoelzl@63940
   515
    then have "f n = \<infinity>" for n
hoelzl@63940
   516
      using le_f by (auto simp: not_less top_unique)
hoelzl@63940
   517
    moreover have "\<exists>E\<in>sets M. A \<subseteq> E \<and> f 0 = emeasure M E"
hoelzl@63940
   518
      using f by auto
hoelzl@63940
   519
    ultimately show ?thesis
hoelzl@63940
   520
      unfolding \<open>outer_measure_of M A = (INF n. f n)\<close> by simp
hoelzl@63940
   521
  qed
hoelzl@63940
   522
qed
hoelzl@63940
   523
hoelzl@63940
   524
lemma SUP_outer_measure_of_incseq:
hoelzl@63940
   525
  assumes A: "\<And>n. A n \<subseteq> space M" and "incseq A"
hoelzl@63940
   526
  shows "(SUP n. outer_measure_of M (A n)) = outer_measure_of M (\<Union>i. A i)"
hoelzl@63940
   527
proof (rule antisym)
hoelzl@63940
   528
  obtain E
hoelzl@63940
   529
    where E: "\<And>n. E n \<in> sets M" "\<And>n. A n \<subseteq> E n" "\<And>n. outer_measure_of M (A n) = emeasure M (E n)"
hoelzl@63940
   530
    using outer_measure_of_attain[OF A] by metis
hoelzl@63940
   531
hoelzl@63940
   532
  define F where "F n = (\<Inter>i\<in>{n ..}. E i)" for n
hoelzl@63940
   533
  with E have F: "incseq F" "\<And>n. F n \<in> sets M"
hoelzl@63940
   534
    by (auto simp: incseq_def)
hoelzl@63940
   535
  have "A n \<subseteq> F n" for n
hoelzl@63940
   536
    using incseqD[OF \<open>incseq A\<close>, of n] \<open>\<And>n. A n \<subseteq> E n\<close> by (auto simp: F_def)
hoelzl@63940
   537
hoelzl@63940
   538
  have eq: "outer_measure_of M (A n) = outer_measure_of M (F n)" for n
hoelzl@63940
   539
  proof (intro antisym)
hoelzl@63940
   540
    have "outer_measure_of M (F n) \<le> outer_measure_of M (E n)"
hoelzl@63940
   541
      by (intro outer_measure_of_mono) (auto simp add: F_def)
hoelzl@63940
   542
    with E show "outer_measure_of M (F n) \<le> outer_measure_of M (A n)"
hoelzl@63940
   543
      by auto
hoelzl@63940
   544
    show "outer_measure_of M (A n) \<le> outer_measure_of M (F n)"
hoelzl@63940
   545
      by (intro outer_measure_of_mono \<open>A n \<subseteq> F n\<close>)
hoelzl@63940
   546
  qed
hoelzl@63940
   547
hoelzl@63940
   548
  have "outer_measure_of M (\<Union>n. A n) \<le> outer_measure_of M (\<Union>n. F n)"
hoelzl@63940
   549
    using \<open>\<And>n. A n \<subseteq> F n\<close> by (intro outer_measure_of_mono) auto
hoelzl@63940
   550
  also have "\<dots> = (SUP n. emeasure M (F n))"
hoelzl@63940
   551
    using F by (simp add: SUP_emeasure_incseq subset_eq)
hoelzl@63940
   552
  finally show "outer_measure_of M (\<Union>n. A n) \<le> (SUP n. outer_measure_of M (A n))"
hoelzl@63940
   553
    by (simp add: eq F)
hoelzl@63940
   554
qed (auto intro: SUP_least outer_measure_of_mono)
hoelzl@63940
   555
eberlm@69447
   556
definition%important measurable_envelope :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
hoelzl@63940
   557
  where "measurable_envelope M A E \<longleftrightarrow>
hoelzl@63940
   558
    (A \<subseteq> E \<and> E \<in> sets M \<and> (\<forall>F\<in>sets M. emeasure M (F \<inter> E) = outer_measure_of M (F \<inter> A)))"
hoelzl@63940
   559
hoelzl@63940
   560
lemma measurable_envelopeD:
hoelzl@63940
   561
  assumes "measurable_envelope M A E"
hoelzl@63940
   562
  shows "A \<subseteq> E"
hoelzl@63940
   563
    and "E \<in> sets M"
hoelzl@63940
   564
    and "\<And>F. F \<in> sets M \<Longrightarrow> emeasure M (F \<inter> E) = outer_measure_of M (F \<inter> A)"
hoelzl@63940
   565
    and "A \<subseteq> space M"
hoelzl@63940
   566
  using assms sets.sets_into_space[of E] by (auto simp: measurable_envelope_def)
hoelzl@63940
   567
hoelzl@63940
   568
lemma measurable_envelopeD1:
hoelzl@63940
   569
  assumes E: "measurable_envelope M A E" and F: "F \<in> sets M" "F \<subseteq> E - A"
hoelzl@63940
   570
  shows "emeasure M F = 0"
hoelzl@63940
   571
proof -
hoelzl@63940
   572
  have "emeasure M F = emeasure M (F \<inter> E)"
hoelzl@63940
   573
    using F by (intro arg_cong2[where f=emeasure]) auto
hoelzl@63940
   574
  also have "\<dots> = outer_measure_of M (F \<inter> A)"
hoelzl@63940
   575
    using measurable_envelopeD[OF E] \<open>F \<in> sets M\<close> by (auto simp: measurable_envelope_def)
hoelzl@63940
   576
  also have "\<dots> = outer_measure_of M {}"
hoelzl@63940
   577
    using \<open>F \<subseteq> E - A\<close> by (intro arg_cong2[where f=outer_measure_of]) auto
hoelzl@63940
   578
  finally show "emeasure M F = 0"
hoelzl@63940
   579
    by simp
hoelzl@63940
   580
qed
hoelzl@63940
   581
hoelzl@63940
   582
lemma measurable_envelope_eq1:
hoelzl@63940
   583
  assumes "A \<subseteq> E" "E \<in> sets M"
hoelzl@63940
   584
  shows "measurable_envelope M A E \<longleftrightarrow> (\<forall>F\<in>sets M. F \<subseteq> E - A \<longrightarrow> emeasure M F = 0)"
hoelzl@63940
   585
proof safe
hoelzl@63940
   586
  assume *: "\<forall>F\<in>sets M. F \<subseteq> E - A \<longrightarrow> emeasure M F = 0"
hoelzl@63940
   587
  show "measurable_envelope M A E"
hoelzl@63940
   588
    unfolding measurable_envelope_def
hoelzl@63940
   589
  proof (rule ccontr, auto simp add: \<open>E \<in> sets M\<close> \<open>A \<subseteq> E\<close>)
hoelzl@63940
   590
    fix F assume "F \<in> sets M" "emeasure M (F \<inter> E) \<noteq> outer_measure_of M (F \<inter> A)"
hoelzl@63940
   591
    then have "outer_measure_of M (F \<inter> A) < emeasure M (F \<inter> E)"
hoelzl@63940
   592
      using outer_measure_of_mono[of "F \<inter> A" "F \<inter> E" M] \<open>A \<subseteq> E\<close> \<open>E \<in> sets M\<close> by (auto simp: less_le)
hoelzl@63940
   593
    then obtain G where G: "G \<in> sets M" "F \<inter> A \<subseteq> G" and less: "emeasure M G < emeasure M (E \<inter> F)"
hoelzl@63940
   594
      unfolding outer_measure_of_def INF_less_iff by (auto simp: ac_simps)
hoelzl@63940
   595
    have le: "emeasure M (G \<inter> E \<inter> F) \<le> emeasure M G"
hoelzl@63940
   596
      using \<open>E \<in> sets M\<close> \<open>G \<in> sets M\<close> \<open>F \<in> sets M\<close> by (auto intro!: emeasure_mono)
hoelzl@63940
   597
hoelzl@63940
   598
    from G have "E \<inter> F - G \<in> sets M" "E \<inter> F - G \<subseteq> E - A"
hoelzl@63940
   599
      using \<open>F \<in> sets M\<close> \<open>E \<in> sets M\<close> by auto
hoelzl@63940
   600
    with * have "0 = emeasure M (E \<inter> F - G)"
hoelzl@63940
   601
      by auto
hoelzl@63940
   602
    also have "E \<inter> F - G = E \<inter> F - (G \<inter> E \<inter> F)"
hoelzl@63940
   603
      by auto
hoelzl@63940
   604
    also have "emeasure M (E \<inter> F - (G \<inter> E \<inter> F)) = emeasure M (E \<inter> F) - emeasure M (G \<inter> E \<inter> F)"
hoelzl@63940
   605
      using \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> le less G by (intro emeasure_Diff) (auto simp: top_unique)
hoelzl@63940
   606
    also have "\<dots> > 0"
hoelzl@63940
   607
      using le less by (intro diff_gr0_ennreal) auto
hoelzl@63940
   608
    finally show False by auto
hoelzl@63940
   609
  qed
hoelzl@63940
   610
qed (rule measurable_envelopeD1)
hoelzl@63940
   611
hoelzl@63940
   612
lemma measurable_envelopeD2:
hoelzl@63940
   613
  assumes E: "measurable_envelope M A E" shows "emeasure M E = outer_measure_of M A"
hoelzl@63940
   614
proof -
hoelzl@63940
   615
  from \<open>measurable_envelope M A E\<close> have "emeasure M (E \<inter> E) = outer_measure_of M (E \<inter> A)"
hoelzl@63940
   616
    by (auto simp: measurable_envelope_def)
hoelzl@63940
   617
  with measurable_envelopeD[OF E] show "emeasure M E = outer_measure_of M A"
hoelzl@63940
   618
    by (auto simp: Int_absorb1)
hoelzl@63940
   619
qed
hoelzl@63940
   620
eberlm@69447
   621
lemma%important measurable_envelope_eq2:
hoelzl@63940
   622
  assumes "A \<subseteq> E" "E \<in> sets M" "emeasure M E < \<infinity>"
hoelzl@63940
   623
  shows "measurable_envelope M A E \<longleftrightarrow> (emeasure M E = outer_measure_of M A)"
hoelzl@63940
   624
proof safe
hoelzl@63940
   625
  assume *: "emeasure M E = outer_measure_of M A"
hoelzl@63940
   626
  show "measurable_envelope M A E"
hoelzl@63940
   627
    unfolding measurable_envelope_eq1[OF \<open>A \<subseteq> E\<close> \<open>E \<in> sets M\<close>]
hoelzl@63940
   628
  proof (intro conjI ballI impI assms)
hoelzl@63940
   629
    fix F assume F: "F \<in> sets M" "F \<subseteq> E - A"
hoelzl@63940
   630
    with \<open>E \<in> sets M\<close> have le: "emeasure M F \<le> emeasure M  E"
hoelzl@63940
   631
      by (intro emeasure_mono) auto
hoelzl@63940
   632
    from F \<open>A \<subseteq> E\<close> have "outer_measure_of M A \<le> outer_measure_of M (E - F)"
hoelzl@63940
   633
      by (intro outer_measure_of_mono) auto
hoelzl@63940
   634
    then have "emeasure M E - 0 \<le> emeasure M (E - F)"
hoelzl@63940
   635
      using * \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> by simp
hoelzl@63940
   636
    also have "\<dots> = emeasure M E - emeasure M F"
hoelzl@63940
   637
      using \<open>E \<in> sets M\<close> \<open>emeasure M E < \<infinity>\<close> F le by (intro emeasure_Diff) (auto simp: top_unique)
hoelzl@63940
   638
    finally show "emeasure M F = 0"
hoelzl@63940
   639
      using ennreal_mono_minus_cancel[of "emeasure M E" 0 "emeasure M F"] le assms by auto
hoelzl@63940
   640
  qed
hoelzl@63940
   641
qed (auto intro: measurable_envelopeD2)
hoelzl@63940
   642
hoelzl@63940
   643
lemma measurable_envelopeI_countable:
hoelzl@63940
   644
  fixes A :: "nat \<Rightarrow> 'a set"
hoelzl@63940
   645
  assumes E: "\<And>n. measurable_envelope M (A n) (E n)"
hoelzl@63940
   646
  shows "measurable_envelope M (\<Union>n. A n) (\<Union>n. E n)"
hoelzl@63940
   647
proof (subst measurable_envelope_eq1)
hoelzl@63940
   648
  show "(\<Union>n. A n) \<subseteq> (\<Union>n. E n)" "(\<Union>n. E n) \<in> sets M"
hoelzl@63940
   649
    using measurable_envelopeD(1,2)[OF E] by auto
hoelzl@63940
   650
  show "\<forall>F\<in>sets M. F \<subseteq> (\<Union>n. E n) - (\<Union>n. A n) \<longrightarrow> emeasure M F = 0"
hoelzl@63940
   651
  proof safe
hoelzl@63940
   652
    fix F assume F: "F \<in> sets M" "F \<subseteq> (\<Union>n. E n) - (\<Union>n. A n)"
hoelzl@63940
   653
    then have "F \<inter> E n \<in> sets M" "F \<inter> E n \<subseteq> E n - A n" "F \<subseteq> (\<Union>n. E n)" for n
hoelzl@63940
   654
      using measurable_envelopeD(1,2)[OF E] by auto
hoelzl@63940
   655
    then have "emeasure M (\<Union>n. F \<inter> E n) = 0"
hoelzl@63940
   656
      by (intro emeasure_UN_eq_0 measurable_envelopeD1[OF E]) auto
hoelzl@63940
   657
    then show "emeasure M F = 0"
hoelzl@63940
   658
      using \<open>F \<subseteq> (\<Union>n. E n)\<close> by (auto simp: Int_absorb2)
hoelzl@63940
   659
  qed
hoelzl@63940
   660
qed
hoelzl@63940
   661
hoelzl@63940
   662
lemma measurable_envelopeI_countable_cover:
hoelzl@63940
   663
  fixes A and C :: "nat \<Rightarrow> 'a set"
hoelzl@63940
   664
  assumes C: "A \<subseteq> (\<Union>n. C n)" "\<And>n. C n \<in> sets M" "\<And>n. emeasure M (C n) < \<infinity>"
hoelzl@63940
   665
  shows "\<exists>E\<subseteq>(\<Union>n. C n). measurable_envelope M A E"
hoelzl@63940
   666
proof -
hoelzl@63940
   667
  have "A \<inter> C n \<subseteq> space M" for n
hoelzl@63940
   668
    using \<open>C n \<in> sets M\<close> by (auto dest: sets.sets_into_space)
hoelzl@63940
   669
  then have "\<forall>n. \<exists>E\<in>sets M. A \<inter> C n \<subseteq> E \<and> outer_measure_of M (A \<inter> C n) = emeasure M E"
hoelzl@63940
   670
    using outer_measure_of_attain[of "A \<inter> C n" M for n] by auto
hoelzl@63940
   671
  then obtain E
hoelzl@63940
   672
    where E: "\<And>n. E n \<in> sets M" "\<And>n. A \<inter> C n \<subseteq> E n"
hoelzl@63940
   673
      and eq: "\<And>n. outer_measure_of M (A \<inter> C n) = emeasure M (E n)"
hoelzl@63940
   674
    by metis
hoelzl@63940
   675
hoelzl@63940
   676
  have "outer_measure_of M (A \<inter> C n) \<le> outer_measure_of M (E n \<inter> C n)" for n
hoelzl@63940
   677
    using E by (intro outer_measure_of_mono) auto
hoelzl@63940
   678
  moreover have "outer_measure_of M (E n \<inter> C n) \<le> outer_measure_of M (E n)" for n
hoelzl@63940
   679
    by (intro outer_measure_of_mono) auto
hoelzl@63940
   680
  ultimately have eq: "outer_measure_of M (A \<inter> C n) = emeasure M (E n \<inter> C n)" for n
hoelzl@63940
   681
    using E C by (intro antisym) (auto simp: eq)
hoelzl@63940
   682
hoelzl@63940
   683
  { fix n
hoelzl@63940
   684
    have "outer_measure_of M (A \<inter> C n) \<le> outer_measure_of M (C n)"
hoelzl@63940
   685
      by (intro outer_measure_of_mono) simp
hoelzl@63940
   686
    also have "\<dots> < \<infinity>"
hoelzl@63940
   687
      using assms by auto
hoelzl@63940
   688
    finally have "emeasure M (E n \<inter> C n) < \<infinity>"
hoelzl@63940
   689
      using eq by simp }
hoelzl@63940
   690
  then have "measurable_envelope M (\<Union>n. A \<inter> C n) (\<Union>n. E n \<inter> C n)"
hoelzl@63940
   691
    using E C by (intro measurable_envelopeI_countable measurable_envelope_eq2[THEN iffD2]) (auto simp: eq)
hoelzl@63940
   692
  with \<open>A \<subseteq> (\<Union>n. C n)\<close> show ?thesis
hoelzl@63940
   693
    by (intro exI[of _ "(\<Union>n. E n \<inter> C n)"]) (auto simp add: Int_absorb2)
hoelzl@63940
   694
qed
hoelzl@63940
   695
hoelzl@63940
   696
lemma (in complete_measure) complete_sets_sandwich:
hoelzl@63940
   697
  assumes [measurable]: "A \<in> sets M" "C \<in> sets M" and subset: "A \<subseteq> B" "B \<subseteq> C"
hoelzl@63940
   698
    and measure: "emeasure M A = emeasure M C" "emeasure M A < \<infinity>"
hoelzl@63940
   699
  shows "B \<in> sets M"
hoelzl@63940
   700
proof -
hoelzl@63940
   701
  have "B - A \<in> sets M"
hoelzl@63940
   702
  proof (rule complete)
hoelzl@63940
   703
    show "B - A \<subseteq> C - A"
hoelzl@63940
   704
      using subset by auto
hoelzl@63940
   705
    show "C - A \<in> null_sets M"
hoelzl@63940
   706
      using measure subset by(simp add: emeasure_Diff null_setsI)
hoelzl@63940
   707
  qed
hoelzl@63940
   708
  then have "A \<union> (B - A) \<in> sets M"
hoelzl@63940
   709
    by measurable
hoelzl@63940
   710
  also have "A \<union> (B - A) = B"
hoelzl@63940
   711
    using \<open>A \<subseteq> B\<close> by auto
hoelzl@63940
   712
  finally show ?thesis .
hoelzl@63940
   713
qed
hoelzl@63940
   714
hoelzl@63958
   715
lemma (in complete_measure) complete_sets_sandwich_fmeasurable:
hoelzl@63958
   716
  assumes [measurable]: "A \<in> fmeasurable M" "C \<in> fmeasurable M" and subset: "A \<subseteq> B" "B \<subseteq> C"
hoelzl@63958
   717
    and measure: "measure M A = measure M C"
hoelzl@63958
   718
  shows "B \<in> fmeasurable M"
hoelzl@63958
   719
proof (rule fmeasurableI2)
hoelzl@63958
   720
  show "B \<subseteq> C" "C \<in> fmeasurable M" by fact+
hoelzl@63958
   721
  show "B \<in> sets M"
hoelzl@63958
   722
  proof (rule complete_sets_sandwich)
hoelzl@63958
   723
    show "A \<in> sets M" "C \<in> sets M" "A \<subseteq> B" "B \<subseteq> C"
hoelzl@63958
   724
      using assms by auto
hoelzl@63958
   725
    show "emeasure M A < \<infinity>"
hoelzl@63958
   726
      using \<open>A \<in> fmeasurable M\<close> by (auto simp: fmeasurable_def)
hoelzl@63958
   727
    show "emeasure M A = emeasure M C"
hoelzl@63958
   728
      using assms by (simp add: emeasure_eq_measure2)
hoelzl@63958
   729
  qed
hoelzl@63958
   730
qed
hoelzl@63958
   731
hoelzl@63958
   732
lemma AE_completion_iff: "(AE x in completion M. P x) \<longleftrightarrow> (AE x in M. P x)"
hoelzl@63958
   733
proof
hoelzl@63958
   734
  assume "AE x in completion M. P x"
hoelzl@63958
   735
  then obtain N where "N \<in> null_sets (completion M)" and P: "{x\<in>space M. \<not> P x} \<subseteq> N"
hoelzl@63958
   736
    unfolding eventually_ae_filter by auto
hoelzl@63958
   737
  then obtain N' where N': "N' \<in> null_sets M" and "N \<subseteq> N'"
hoelzl@63958
   738
    unfolding null_sets_completion_iff2 by auto
hoelzl@63958
   739
  from P \<open>N \<subseteq> N'\<close> have "{x\<in>space M. \<not> P x} \<subseteq> N'"
hoelzl@63958
   740
    by auto
hoelzl@63958
   741
  with N' show "AE x in M. P x"
hoelzl@63958
   742
    unfolding eventually_ae_filter by auto
hoelzl@63958
   743
qed (rule AE_completion)
hoelzl@63958
   744
hoelzl@63958
   745
lemma null_part_null_sets: "S \<in> completion M \<Longrightarrow> null_part M S \<in> null_sets (completion M)"
hoelzl@63958
   746
  by (auto dest!: null_part intro: null_sets_completionI null_sets_completion_subset)
hoelzl@63958
   747
hoelzl@63958
   748
lemma AE_notin_null_part: "S \<in> completion M \<Longrightarrow> (AE x in M. x \<notin> null_part M S)"
hoelzl@63958
   749
  by (auto dest!: null_part_null_sets AE_not_in simp: AE_completion_iff)
hoelzl@63958
   750
hoelzl@63958
   751
lemma completion_upper:
hoelzl@63958
   752
  assumes A: "A \<in> sets (completion M)"
hoelzl@63958
   753
  shows "\<exists>A'\<in>sets M. A \<subseteq> A' \<and> emeasure (completion M) A = emeasure M A'"
hoelzl@63958
   754
proof -
hoelzl@63958
   755
  from AE_notin_null_part[OF A] obtain N where N: "N \<in> null_sets M" "null_part M A \<subseteq> N"
hoelzl@63958
   756
    unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto
hoelzl@63958
   757
  show ?thesis
hoelzl@63958
   758
  proof (intro bexI conjI)
hoelzl@63958
   759
    show "A \<subseteq> main_part M A \<union> N"
hoelzl@63958
   760
      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[symmetric, OF A]) auto
hoelzl@63958
   761
    show "emeasure (completion M) A = emeasure M (main_part M A \<union> N)"
hoelzl@63958
   762
      using A \<open>N \<in> null_sets M\<close> by (simp add: emeasure_Un_null_set)
hoelzl@63958
   763
  qed (use A N in auto)
hoelzl@63958
   764
qed
hoelzl@63958
   765
hoelzl@63958
   766
lemma AE_in_main_part:
hoelzl@63958
   767
  assumes A: "A \<in> completion M" shows "AE x in M. x \<in> main_part M A \<longleftrightarrow> x \<in> A"
hoelzl@63958
   768
  using AE_notin_null_part[OF A]
hoelzl@63958
   769
  by (subst (2) main_part_null_part_Un[symmetric, OF A]) auto
hoelzl@63958
   770
hoelzl@63958
   771
lemma completion_density_eq:
hoelzl@63958
   772
  assumes ae: "AE x in M. 0 < f x" and [measurable]: "f \<in> M \<rightarrow>\<^sub>M borel"
hoelzl@63958
   773
  shows "completion (density M f) = density (completion M) f"
hoelzl@63958
   774
proof (intro measure_eqI)
hoelzl@63958
   775
  have "N' \<in> sets M \<and> (AE x\<in>N' in M. f x = 0) \<longleftrightarrow> N' \<in> null_sets M" for N'
hoelzl@63958
   776
  proof safe
hoelzl@63958
   777
    assume N': "N' \<in> sets M" and ae_N': "AE x\<in>N' in M. f x = 0"
hoelzl@63958
   778
    from ae_N' ae have "AE x in M. x \<notin> N'"
hoelzl@63958
   779
      by eventually_elim auto
hoelzl@63958
   780
    then show "N' \<in> null_sets M"
hoelzl@63958
   781
      using N' by (simp add: AE_iff_null_sets)
hoelzl@63958
   782
  next
hoelzl@63958
   783
    assume N': "N' \<in> null_sets M" then show "N' \<in> sets M" "AE x\<in>N' in M. f x = 0"
hoelzl@63958
   784
      using ae AE_not_in[OF N'] by (auto simp: less_le)
hoelzl@63958
   785
  qed
hoelzl@63958
   786
  then show sets_eq: "sets (completion (density M f)) = sets (density (completion M) f)"
hoelzl@63958
   787
    by (simp add: sets_completion null_sets_density_iff)
hoelzl@63958
   788
hoelzl@63958
   789
  fix A assume A: \<open>A \<in> completion (density M f)\<close>
hoelzl@63958
   790
  moreover
hoelzl@63958
   791
  have "A \<in> completion M"
hoelzl@63958
   792
    using A unfolding sets_eq by simp
hoelzl@63958
   793
  moreover
hoelzl@63958
   794
  have "main_part (density M f) A \<in> M"
hoelzl@63958
   795
    using A main_part_sets[of A "density M f"] unfolding sets_density sets_eq by simp
hoelzl@63958
   796
  moreover have "AE x in M. x \<in> main_part (density M f) A \<longleftrightarrow> x \<in> A"
hoelzl@63958
   797
    using AE_in_main_part[OF \<open>A \<in> completion (density M f)\<close>] ae by (auto simp add: AE_density)
hoelzl@63958
   798
  ultimately show "emeasure (completion (density M f)) A = emeasure (density (completion M) f) A"
hoelzl@63958
   799
    by (auto simp add: emeasure_density measurable_completion nn_integral_completion intro!: nn_integral_cong_AE)
hoelzl@63958
   800
qed
hoelzl@63958
   801
hoelzl@64284
   802
lemma null_sets_subset: "B \<in> null_sets M \<Longrightarrow> A \<in> sets M \<Longrightarrow> A \<subseteq> B \<Longrightarrow> A \<in> null_sets M"
hoelzl@63958
   803
  using emeasure_mono[of A B M] by (simp add: null_sets_def)
hoelzl@63958
   804
hoelzl@63958
   805
lemma (in complete_measure) complete2: "A \<subseteq> B \<Longrightarrow> B \<in> null_sets M \<Longrightarrow> A \<in> null_sets M"
hoelzl@64284
   806
  using complete[of A B] null_sets_subset[of B M A] by simp
hoelzl@63958
   807
hoelzl@63959
   808
lemma (in complete_measure) AE_iff_null_sets: "(AE x in M. P x) \<longleftrightarrow> {x\<in>space M. \<not> P x} \<in> null_sets M"
hoelzl@63959
   809
  unfolding eventually_ae_filter by (auto intro: complete2)
hoelzl@63959
   810
hoelzl@63959
   811
lemma (in complete_measure) null_sets_iff_AE: "A \<in> null_sets M \<longleftrightarrow> ((AE x in M. x \<notin> A) \<and> A \<subseteq> space M)"
hoelzl@63959
   812
  unfolding AE_iff_null_sets by (auto cong: rev_conj_cong dest: sets.sets_into_space simp: subset_eq)
hoelzl@63959
   813
hoelzl@63959
   814
lemma (in complete_measure) in_sets_AE:
hoelzl@63959
   815
  assumes ae: "AE x in M. x \<in> A \<longleftrightarrow> x \<in> B" and A: "A \<in> sets M" and B: "B \<subseteq> space M"
hoelzl@63959
   816
  shows "B \<in> sets M"
hoelzl@63959
   817
proof -
hoelzl@63959
   818
  have "(AE x in M. x \<notin> B - A \<and> x \<notin> A - B)"
hoelzl@63959
   819
    using ae by eventually_elim auto
hoelzl@63959
   820
  then have "B - A \<in> null_sets M" "A - B \<in> null_sets M"
hoelzl@63959
   821
    using A B unfolding null_sets_iff_AE by (auto dest: sets.sets_into_space)
hoelzl@63959
   822
  then have "A \<union> (B - A) - (A - B) \<in> sets M"
hoelzl@63959
   823
    using A by blast
hoelzl@63959
   824
  also have "A \<union> (B - A) - (A - B) = B"
hoelzl@63959
   825
    by auto
hoelzl@63959
   826
  finally show "B \<in> sets M" .
hoelzl@63959
   827
qed
hoelzl@63959
   828
hoelzl@63958
   829
lemma (in complete_measure) vimage_null_part_null_sets:
hoelzl@63958
   830
  assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and eq: "null_sets N \<subseteq> null_sets (distr M N f)"
hoelzl@63958
   831
    and A: "A \<in> completion N"
hoelzl@63958
   832
  shows "f -` null_part N A \<inter> space M \<in> null_sets M"
hoelzl@63958
   833
proof -
hoelzl@63958
   834
  obtain N' where "N' \<in> null_sets N" "null_part N A \<subseteq> N'"
hoelzl@63958
   835
    using null_part[OF A] by auto
hoelzl@63958
   836
  then have N': "N' \<in> null_sets (distr M N f)"
hoelzl@63958
   837
    using eq by auto
hoelzl@63958
   838
  show ?thesis
hoelzl@63958
   839
  proof (rule complete2)
hoelzl@63958
   840
    show "f -` null_part N A \<inter> space M \<subseteq> f -` N' \<inter> space M"
hoelzl@63958
   841
      using \<open>null_part N A \<subseteq> N'\<close> by auto
hoelzl@63958
   842
    show "f -` N' \<inter> space M \<in> null_sets M"
hoelzl@63958
   843
      using f N' by (auto simp: null_sets_def emeasure_distr)
hoelzl@63958
   844
  qed
hoelzl@63958
   845
qed
hoelzl@63958
   846
hoelzl@63958
   847
lemma (in complete_measure) vimage_null_part_sets:
hoelzl@63958
   848
  "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> null_sets N \<subseteq> null_sets (distr M N f) \<Longrightarrow> A \<in> completion N \<Longrightarrow>
hoelzl@63958
   849
  f -` null_part N A \<inter> space M \<in> sets M"
hoelzl@63958
   850
  using vimage_null_part_null_sets[of f N A] by auto
hoelzl@63958
   851
hoelzl@63958
   852
lemma (in complete_measure) measurable_completion2:
hoelzl@63958
   853
  assumes f: "f \<in> M \<rightarrow>\<^sub>M N" and null_sets: "null_sets N \<subseteq> null_sets (distr M N f)"
hoelzl@63958
   854
  shows "f \<in> M \<rightarrow>\<^sub>M completion N"
hoelzl@63958
   855
proof (rule measurableI)
hoelzl@63958
   856
  show "x \<in> space M \<Longrightarrow> f x \<in> space (completion N)" for x
hoelzl@63958
   857
    using f[THEN measurable_space] by auto
hoelzl@63958
   858
  fix A assume A: "A \<in> sets (completion N)"
hoelzl@63958
   859
  have "f -` A \<inter> space M = (f -` main_part N A \<inter> space M) \<union> (f -` null_part N A \<inter> space M)"
hoelzl@63958
   860
    using main_part_null_part_Un[OF A] by auto
hoelzl@63958
   861
  then show "f -` A \<inter> space M \<in> sets M"
hoelzl@63958
   862
    using f A null_sets by (auto intro: vimage_null_part_sets measurable_sets)
hoelzl@63958
   863
qed
hoelzl@63958
   864
hoelzl@63958
   865
lemma (in complete_measure) completion_distr_eq:
hoelzl@63958
   866
  assumes X: "X \<in> M \<rightarrow>\<^sub>M N" and null_sets: "null_sets (distr M N X) = null_sets N"
hoelzl@63958
   867
  shows "completion (distr M N X) = distr M (completion N) X"
hoelzl@63958
   868
proof (rule measure_eqI)
hoelzl@63958
   869
  show eq: "sets (completion (distr M N X)) = sets (distr M (completion N) X)"
hoelzl@63958
   870
    by (simp add: sets_completion null_sets)
hoelzl@63958
   871
hoelzl@63958
   872
  fix A assume A: "A \<in> completion (distr M N X)"
hoelzl@63958
   873
  moreover have A': "A \<in> completion N"
hoelzl@63958
   874
    using A by (simp add: eq)
hoelzl@63958
   875
  moreover have "main_part (distr M N X) A \<in> sets N"
hoelzl@63958
   876
    using main_part_sets[OF A] by simp
hoelzl@63958
   877
  moreover have "X -` A \<inter> space M = (X -` main_part (distr M N X) A \<inter> space M) \<union> (X -` null_part (distr M N X) A \<inter> space M)"
hoelzl@63958
   878
    using main_part_null_part_Un[OF A] by auto
hoelzl@63958
   879
  moreover have "X -` null_part (distr M N X) A \<inter> space M \<in> null_sets M"
hoelzl@63958
   880
    using X A by (intro vimage_null_part_null_sets) (auto cong: distr_cong)
hoelzl@63958
   881
  ultimately show "emeasure (completion (distr M N X)) A = emeasure (distr M (completion N) X) A"
hoelzl@63958
   882
    using X by (auto simp: emeasure_distr measurable_completion null_sets measurable_completion2
hoelzl@63958
   883
                     intro!: emeasure_Un_null_set[symmetric])
hoelzl@63958
   884
qed
hoelzl@63958
   885
hoelzl@63958
   886
lemma distr_completion: "X \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> distr (completion M) N X = distr M N X"
hoelzl@63958
   887
  by (intro measure_eqI) (auto simp: emeasure_distr measurable_completion)
hoelzl@63958
   888
hoelzl@63958
   889
proposition (in complete_measure) fmeasurable_inner_outer:
hoelzl@63958
   890
  "S \<in> fmeasurable M \<longleftrightarrow>
hoelzl@63958
   891
    (\<forall>e>0. \<exists>T\<in>fmeasurable M. \<exists>U\<in>fmeasurable M. T \<subseteq> S \<and> S \<subseteq> U \<and> \<bar>measure M T - measure M U\<bar> < e)"
hoelzl@63958
   892
  (is "_ \<longleftrightarrow> ?approx")
hoelzl@63958
   893
proof safe
hoelzl@63958
   894
  let ?\<mu> = "measure M" let ?D = "\<lambda>T U . \<bar>?\<mu> T - ?\<mu> U\<bar>"
hoelzl@63958
   895
  assume ?approx
hoelzl@63958
   896
  have "\<exists>A. \<forall>n. (fst (A n) \<in> fmeasurable M \<and> snd (A n) \<in> fmeasurable M \<and> fst (A n) \<subseteq> S \<and> S \<subseteq> snd (A n) \<and>
hoelzl@63958
   897
    ?D (fst (A n)) (snd (A n)) < 1/Suc n) \<and> (fst (A n) \<subseteq> fst (A (Suc n)) \<and> snd (A (Suc n)) \<subseteq> snd (A n))"
hoelzl@63958
   898
    (is "\<exists>A. \<forall>n. ?P n (A n) \<and> ?Q (A n) (A (Suc n))")
hoelzl@63958
   899
  proof (intro dependent_nat_choice)
hoelzl@63958
   900
    show "\<exists>A. ?P 0 A"
hoelzl@63958
   901
      using \<open>?approx\<close>[THEN spec, of 1] by auto
hoelzl@63958
   902
  next
hoelzl@63958
   903
    fix A n assume "?P n A"
hoelzl@63958
   904
    moreover
hoelzl@63958
   905
    from \<open>?approx\<close>[THEN spec, of "1/Suc (Suc n)"]
hoelzl@63958
   906
    obtain T U where *: "T \<in> fmeasurable M" "U \<in> fmeasurable M" "T \<subseteq> S" "S \<subseteq> U" "?D T U < 1 / Suc (Suc n)"
hoelzl@63958
   907
      by auto
hoelzl@63958
   908
    ultimately have "?\<mu> T \<le> ?\<mu> (T \<union> fst A)" "?\<mu> (U \<inter> snd A) \<le> ?\<mu> U"
hoelzl@63958
   909
      "?\<mu> T \<le> ?\<mu> U" "?\<mu> (T \<union> fst A) \<le> ?\<mu> (U \<inter> snd A)"
hoelzl@63958
   910
      by (auto intro!: measure_mono_fmeasurable)
hoelzl@63958
   911
    then have "?D (T \<union> fst A) (U \<inter> snd A) \<le> ?D T U"
hoelzl@63958
   912
      by auto
hoelzl@63958
   913
    also have "?D T U < 1/Suc (Suc n)" by fact
hoelzl@63958
   914
    finally show "\<exists>B. ?P (Suc n) B \<and> ?Q A B"
hoelzl@63958
   915
      using \<open>?P n A\<close> *
hoelzl@63958
   916
      by (intro exI[of _ "(T \<union> fst A, U \<inter> snd A)"] conjI) auto
hoelzl@63958
   917
  qed
hoelzl@63958
   918
  then obtain A
hoelzl@63958
   919
    where lm: "\<And>n. fst (A n) \<in> fmeasurable M" "\<And>n. snd (A n) \<in> fmeasurable M"
hoelzl@63958
   920
      and set_bound: "\<And>n. fst (A n) \<subseteq> S" "\<And>n. S \<subseteq> snd (A n)"
hoelzl@63958
   921
      and mono: "\<And>n. fst (A n) \<subseteq> fst (A (Suc n))" "\<And>n. snd (A (Suc n)) \<subseteq> snd (A n)"
hoelzl@63958
   922
      and bound: "\<And>n. ?D (fst (A n)) (snd (A n)) < 1/Suc n"
hoelzl@63958
   923
    by metis
hoelzl@63958
   924
hoelzl@63958
   925
  have INT_sA: "(\<Inter>n. snd (A n)) \<in> fmeasurable M"
hoelzl@63958
   926
    using lm by (intro fmeasurable_INT[of _ 0]) auto
hoelzl@63958
   927
  have UN_fA: "(\<Union>n. fst (A n)) \<in> fmeasurable M"
hoelzl@63958
   928
    using lm order_trans[OF set_bound(1) set_bound(2)[of 0]] by (intro fmeasurable_UN[of _ _ "snd (A 0)"]) auto
hoelzl@63958
   929
hoelzl@63958
   930
  have "(\<lambda>n. ?\<mu> (fst (A n)) - ?\<mu> (snd (A n))) \<longlonglongrightarrow> 0"
hoelzl@63958
   931
    using bound
hoelzl@63958
   932
    by (subst tendsto_rabs_zero_iff[symmetric])
hoelzl@63958
   933
       (intro tendsto_sandwich[OF _ _ tendsto_const LIMSEQ_inverse_real_of_nat];
hoelzl@63958
   934
        auto intro!: always_eventually less_imp_le simp: divide_inverse)
hoelzl@63958
   935
  moreover
hoelzl@63958
   936
  have "(\<lambda>n. ?\<mu> (fst (A n)) - ?\<mu> (snd (A n))) \<longlonglongrightarrow> ?\<mu> (\<Union>n. fst (A n)) - ?\<mu> (\<Inter>n. snd (A n))"
hoelzl@63958
   937
  proof (intro tendsto_diff Lim_measure_incseq Lim_measure_decseq)
hoelzl@63958
   938
    show "range (\<lambda>i. fst (A i)) \<subseteq> sets M" "range (\<lambda>i. snd (A i)) \<subseteq> sets M"
hoelzl@63958
   939
      "incseq (\<lambda>i. fst (A i))" "decseq (\<lambda>n. snd (A n))"
hoelzl@63958
   940
      using mono lm by (auto simp: incseq_Suc_iff decseq_Suc_iff intro!: measure_mono_fmeasurable)
hoelzl@63958
   941
    show "emeasure M (\<Union>x. fst (A x)) \<noteq> \<infinity>" "emeasure M (snd (A n)) \<noteq> \<infinity>" for n
hoelzl@63958
   942
      using lm(2)[of n] UN_fA by (auto simp: fmeasurable_def)
hoelzl@63958
   943
  qed
hoelzl@63958
   944
  ultimately have eq: "0 = ?\<mu> (\<Union>n. fst (A n)) - ?\<mu> (\<Inter>n. snd (A n))"
hoelzl@63958
   945
    by (rule LIMSEQ_unique)
hoelzl@63958
   946
hoelzl@63958
   947
  show "S \<in> fmeasurable M"
hoelzl@63958
   948
    using UN_fA INT_sA
hoelzl@63958
   949
  proof (rule complete_sets_sandwich_fmeasurable)
hoelzl@63958
   950
    show "(\<Union>n. fst (A n)) \<subseteq> S" "S \<subseteq> (\<Inter>n. snd (A n))"
hoelzl@63958
   951
      using set_bound by auto
hoelzl@63958
   952
    show "?\<mu> (\<Union>n. fst (A n)) = ?\<mu> (\<Inter>n. snd (A n))"
hoelzl@63958
   953
      using eq by auto
hoelzl@63958
   954
  qed
hoelzl@63958
   955
qed (auto intro!: bexI[of _ S])
hoelzl@63958
   956
hoelzl@63958
   957
lemma (in complete_measure) fmeasurable_measure_inner_outer:
hoelzl@63958
   958
   "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
hoelzl@63958
   959
      (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e < measure M T) \<and>
hoelzl@63958
   960
      (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U < m + e)"
hoelzl@63958
   961
    (is "?lhs = ?rhs")
hoelzl@63958
   962
proof
hoelzl@63958
   963
  assume RHS: ?rhs
hoelzl@63958
   964
  then have T: "\<And>e. 0 < e \<longrightarrow> (\<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e < measure M T)"
hoelzl@63958
   965
        and U: "\<And>e. 0 < e \<longrightarrow> (\<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U < m + e)"
hoelzl@63958
   966
    by auto
hoelzl@63958
   967
  have "S \<in> fmeasurable M"
hoelzl@63958
   968
  proof (subst fmeasurable_inner_outer, safe)
hoelzl@63958
   969
    fix e::real assume "0 < e"
hoelzl@63958
   970
    with RHS obtain T U where T: "T \<in> fmeasurable M" "T \<subseteq> S" "m - e/2 < measure M T"
hoelzl@63958
   971
                          and U: "U \<in> fmeasurable M" "S \<subseteq> U" "measure M U < m + e/2"
hoelzl@63958
   972
      by (meson half_gt_zero)+
hoelzl@63958
   973
    moreover have "measure M U - measure M T < (m + e/2) - (m - e/2)"
hoelzl@63958
   974
      by (intro diff_strict_mono) fact+
hoelzl@63958
   975
    moreover have "measure M T \<le> measure M U"
hoelzl@63958
   976
      using T U by (intro measure_mono_fmeasurable) auto
hoelzl@63958
   977
    ultimately show "\<exists>T\<in>fmeasurable M. \<exists>U\<in>fmeasurable M. T \<subseteq> S \<and> S \<subseteq> U \<and> \<bar>measure M T - measure M U\<bar> < e"
hoelzl@63958
   978
      apply (rule_tac bexI[OF _ \<open>T \<in> fmeasurable M\<close>])
hoelzl@63958
   979
      apply (rule_tac bexI[OF _ \<open>U \<in> fmeasurable M\<close>])
hoelzl@63958
   980
      by auto
hoelzl@63958
   981
  qed
hoelzl@63958
   982
  moreover have "m = measure M S"
hoelzl@63958
   983
    using \<open>S \<in> fmeasurable M\<close> U[of "measure M S - m"] T[of "m - measure M S"]
hoelzl@63958
   984
    by (cases m "measure M S" rule: linorder_cases)
hoelzl@63958
   985
       (auto simp: not_le[symmetric] measure_mono_fmeasurable)
hoelzl@63958
   986
  ultimately show ?lhs
hoelzl@63958
   987
    by simp
hoelzl@63958
   988
qed (auto intro!: bexI[of _ S])
hoelzl@63958
   989
hoelzl@63959
   990
lemma (in complete_measure) null_sets_outer:
hoelzl@63959
   991
  "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
hoelzl@63959
   992
proof -
hoelzl@63959
   993
  have "S \<in> null_sets M \<longleftrightarrow> (S \<in> fmeasurable M \<and> 0 = measure M S)"
hoelzl@63959
   994
    by (auto simp: null_sets_def emeasure_eq_measure2 intro: fmeasurableI) (simp add: measure_def)
hoelzl@63959
   995
  also have "\<dots> = (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T < e)"
hoelzl@63959
   996
    unfolding fmeasurable_measure_inner_outer by auto
hoelzl@63959
   997
  finally show ?thesis .
hoelzl@63959
   998
qed
hoelzl@63959
   999
lp15@67982
  1000
lemma (in complete_measure) fmeasurable_measure_inner_outer_le:
lp15@67982
  1001
     "(S \<in> fmeasurable M \<and> m = measure M S) \<longleftrightarrow>
lp15@67982
  1002
        (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e \<le> measure M T) \<and>
lp15@67982
  1003
        (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U \<le> m + e)" (is ?T1)
lp15@67982
  1004
  and null_sets_outer_le:
lp15@67982
  1005
     "S \<in> null_sets M \<longleftrightarrow> (\<forall>e>0. \<exists>T\<in>fmeasurable M. S \<subseteq> T \<and> measure M T \<le> e)" (is ?T2)
lp15@67982
  1006
proof -
lp15@67982
  1007
  have "e > 0 \<and> m - e/2 \<le> t \<Longrightarrow> m - e < t"
lp15@67982
  1008
       "e > 0 \<and> t \<le> m + e/2 \<Longrightarrow> t < m + e"
lp15@67982
  1009
       "e > 0 \<longleftrightarrow> e/2 > 0"
lp15@67982
  1010
       for e t
lp15@67982
  1011
    by auto
lp15@67982
  1012
  then show ?T1 ?T2
lp15@67982
  1013
    unfolding fmeasurable_measure_inner_outer null_sets_outer
lp15@67982
  1014
    by (meson dense le_less_trans less_imp_le)+
lp15@67982
  1015
qed
lp15@67982
  1016
hoelzl@63940
  1017
lemma (in cld_measure) notin_sets_outer_measure_of_cover:
hoelzl@63940
  1018
  assumes E: "E \<subseteq> space M" "E \<notin> sets M"
hoelzl@63940
  1019
  shows "\<exists>B\<in>sets M. 0 < emeasure M B \<and> emeasure M B < \<infinity> \<and>
hoelzl@63940
  1020
    outer_measure_of M (B \<inter> E) = emeasure M B \<and> outer_measure_of M (B - E) = emeasure M B"
hoelzl@63940
  1021
proof -
hoelzl@63940
  1022
  from locally_determined[OF \<open>E \<subseteq> space M\<close>] \<open>E \<notin> sets M\<close>
hoelzl@63940
  1023
  obtain F
hoelzl@63940
  1024
    where [measurable]: "F \<in> sets M" and "emeasure M F < \<infinity>" "E \<inter> F \<notin> sets M"
hoelzl@63940
  1025
    by blast
hoelzl@63940
  1026
  then obtain H H'
hoelzl@63940
  1027
    where H: "measurable_envelope M (F \<inter> E) H" and H': "measurable_envelope M (F - E) H'"
hoelzl@63940
  1028
    using measurable_envelopeI_countable_cover[of "F \<inter> E" "\<lambda>_. F" M]
hoelzl@63940
  1029
       measurable_envelopeI_countable_cover[of "F - E" "\<lambda>_. F" M]
hoelzl@63940
  1030
    by auto
hoelzl@63940
  1031
  note measurable_envelopeD(2)[OF H', measurable] measurable_envelopeD(2)[OF H, measurable]
hoelzl@63940
  1032
hoelzl@63940
  1033
  from measurable_envelopeD(1)[OF H'] measurable_envelopeD(1)[OF H]
hoelzl@63940
  1034
  have subset: "F - H' \<subseteq> F \<inter> E" "F \<inter> E \<subseteq> F \<inter> H"
hoelzl@63940
  1035
    by auto
hoelzl@63940
  1036
  moreover define G where "G = (F \<inter> H) - (F - H')"
hoelzl@63940
  1037
  ultimately have G: "G = F \<inter> H \<inter> H'"
hoelzl@63940
  1038
    by auto
hoelzl@63940
  1039
  have "emeasure M (F \<inter> H) \<noteq> 0"
hoelzl@63940
  1040
  proof
hoelzl@63940
  1041
    assume "emeasure M (F \<inter> H) = 0"
hoelzl@63940
  1042
    then have "F \<inter> H \<in> null_sets M"
hoelzl@63940
  1043
      by auto
hoelzl@63940
  1044
    with \<open>E \<inter> F \<notin> sets M\<close> show False
hoelzl@63940
  1045
      using complete[OF \<open>F \<inter> E \<subseteq> F \<inter> H\<close>] by (auto simp: Int_commute)
hoelzl@63940
  1046
  qed
hoelzl@63940
  1047
  moreover
hoelzl@63940
  1048
  have "emeasure M (F - H') \<noteq> emeasure M (F \<inter> H)"
hoelzl@63940
  1049
  proof
hoelzl@63940
  1050
    assume "emeasure M (F - H') = emeasure M (F \<inter> H)"
hoelzl@63940
  1051
    with \<open>E \<inter> F \<notin> sets M\<close> emeasure_mono[of "F \<inter> H" F M] \<open>emeasure M F < \<infinity>\<close>
hoelzl@63940
  1052
    have "F \<inter> E \<in> sets M"
hoelzl@63940
  1053
      by (intro complete_sets_sandwich[OF _ _ subset]) auto
hoelzl@63940
  1054
    with \<open>E \<inter> F \<notin> sets M\<close> show False
hoelzl@63940
  1055
      by (simp add: Int_commute)
hoelzl@63940
  1056
  qed
hoelzl@63940
  1057
  moreover have "emeasure M (F - H') \<le> emeasure M (F \<inter> H)"
hoelzl@63940
  1058
    using subset by (intro emeasure_mono) auto
hoelzl@63940
  1059
  ultimately have "emeasure M G \<noteq> 0"
hoelzl@63940
  1060
    unfolding G_def using subset
hoelzl@63940
  1061
    by (subst emeasure_Diff) (auto simp: top_unique diff_eq_0_iff_ennreal)
hoelzl@63940
  1062
  show ?thesis
hoelzl@63940
  1063
  proof (intro bexI conjI)
hoelzl@63940
  1064
    have "emeasure M G \<le> emeasure M F"
hoelzl@63940
  1065
      unfolding G by (auto intro!: emeasure_mono)
hoelzl@63940
  1066
    with \<open>emeasure M F < \<infinity>\<close> show "0 < emeasure M G" "emeasure M G < \<infinity>"
hoelzl@63940
  1067
      using \<open>emeasure M G \<noteq> 0\<close> by (auto simp: zero_less_iff_neq_zero)
hoelzl@63940
  1068
    show [measurable]: "G \<in> sets M"
hoelzl@63940
  1069
      unfolding G by auto
hoelzl@63940
  1070
hoelzl@63940
  1071
    have "emeasure M G = outer_measure_of M (F \<inter> H' \<inter> (F \<inter> E))"
hoelzl@63940
  1072
      using measurable_envelopeD(3)[OF H, of "F \<inter> H'"] unfolding G by (simp add: ac_simps)
hoelzl@63940
  1073
    also have "\<dots> \<le> outer_measure_of M (G \<inter> E)"
hoelzl@63940
  1074
      using measurable_envelopeD(1)[OF H] by (intro outer_measure_of_mono) (auto simp: G)
hoelzl@63940
  1075
    finally show "outer_measure_of M (G \<inter> E) = emeasure M G"
hoelzl@63940
  1076
      using outer_measure_of_mono[of "G \<inter> E" G M] by auto
hoelzl@63940
  1077
hoelzl@63940
  1078
    have "emeasure M G = outer_measure_of M (F \<inter> H \<inter> (F - E))"
hoelzl@63940
  1079
      using measurable_envelopeD(3)[OF H', of "F \<inter> H"] unfolding G by (simp add: ac_simps)
hoelzl@63940
  1080
    also have "\<dots> \<le> outer_measure_of M (G - E)"
hoelzl@63940
  1081
      using measurable_envelopeD(1)[OF H'] by (intro outer_measure_of_mono) (auto simp: G)
hoelzl@63940
  1082
    finally show "outer_measure_of M (G - E) = emeasure M G"
hoelzl@63940
  1083
      using outer_measure_of_mono[of "G - E" G M] by auto
hoelzl@63940
  1084
  qed
hoelzl@63940
  1085
qed
hoelzl@63940
  1086
hoelzl@63940
  1087
text \<open>The following theorem is a specialization of D.H. Fremlin, Measure Theory vol 4I (413G). We
wenzelm@69566
  1088
  only show one direction and do not use a inner regular family \<open>K\<close>.\<close>
hoelzl@63940
  1089
hoelzl@63940
  1090
lemma (in cld_measure) borel_measurable_cld:
hoelzl@63940
  1091
  fixes f :: "'a \<Rightarrow> real"
hoelzl@63940
  1092
  assumes "\<And>A a b. A \<in> sets M \<Longrightarrow> 0 < emeasure M A \<Longrightarrow> emeasure M A < \<infinity> \<Longrightarrow> a < b \<Longrightarrow>
hoelzl@63940
  1093
      min (outer_measure_of M {x\<in>A. f x \<le> a}) (outer_measure_of M {x\<in>A. b \<le> f x}) < emeasure M A"
hoelzl@63940
  1094
  shows "f \<in> M \<rightarrow>\<^sub>M borel"
hoelzl@63940
  1095
proof (rule ccontr)
hoelzl@63940
  1096
  let ?E = "\<lambda>a. {x\<in>space M. f x \<le> a}" and ?F = "\<lambda>a. {x\<in>space M. a \<le> f x}"
hoelzl@63940
  1097
hoelzl@63940
  1098
  assume "f \<notin> M \<rightarrow>\<^sub>M borel"
hoelzl@63940
  1099
  then obtain a where "?E a \<notin> sets M"
hoelzl@63940
  1100
    unfolding borel_measurable_iff_le by blast
hoelzl@63940
  1101
  from notin_sets_outer_measure_of_cover[OF _ this]
hoelzl@63940
  1102
  obtain K
hoelzl@63940
  1103
    where K: "K \<in> sets M" "0 < emeasure M K" "emeasure M K < \<infinity>"
hoelzl@63940
  1104
      and eq1: "outer_measure_of M (K \<inter> ?E a) = emeasure M K"
hoelzl@63940
  1105
      and eq2: "outer_measure_of M (K - ?E a) = emeasure M K"
hoelzl@63940
  1106
    by auto
hoelzl@63940
  1107
  then have me_K: "measurable_envelope M (K \<inter> ?E a) K"
hoelzl@63940
  1108
    by (subst measurable_envelope_eq2) auto
hoelzl@63940
  1109
hoelzl@63940
  1110
  define b where "b n = a + inverse (real (Suc n))" for n
hoelzl@63940
  1111
  have "(SUP n. outer_measure_of M (K \<inter> ?F (b n))) = outer_measure_of M (\<Union>n. K \<inter> ?F (b n))"
hoelzl@63940
  1112
  proof (intro SUP_outer_measure_of_incseq)
hoelzl@63940
  1113
    have "x \<le> y \<Longrightarrow> b y \<le> b x" for x y
hoelzl@63940
  1114
      by (auto simp: b_def field_simps)
hoelzl@63940
  1115
    then show "incseq (\<lambda>n. K \<inter> {x \<in> space M. b n \<le> f x})"
hoelzl@63940
  1116
      by (auto simp: incseq_def intro: order_trans)
hoelzl@63940
  1117
  qed auto
hoelzl@63940
  1118
  also have "(\<Union>n. K \<inter> ?F (b n)) = K - ?E a"
hoelzl@63940
  1119
  proof -
hoelzl@63940
  1120
    have "b \<longlonglongrightarrow> a"
hoelzl@63940
  1121
      unfolding b_def by (rule LIMSEQ_inverse_real_of_nat_add)
hoelzl@63940
  1122
    then have "\<forall>n. \<not> b n \<le> f x \<Longrightarrow> f x \<le> a" for x
hoelzl@63940
  1123
      by (rule LIMSEQ_le_const) (auto intro: less_imp_le simp: not_le)
hoelzl@63940
  1124
    moreover have "\<not> b n \<le> a" for n
hoelzl@63940
  1125
      by (auto simp: b_def)
hoelzl@63940
  1126
    ultimately show ?thesis
hoelzl@63940
  1127
      using \<open>K \<in> sets M\<close>[THEN sets.sets_into_space] by (auto simp: subset_eq intro: order_trans)
hoelzl@63940
  1128
  qed
hoelzl@63940
  1129
  finally have "0 < (SUP n. outer_measure_of M (K \<inter> ?F (b n)))"
hoelzl@63940
  1130
    using K by (simp add: eq2)
hoelzl@63940
  1131
  then obtain n where pos_b: "0 < outer_measure_of M (K \<inter> ?F (b n))" and "a < b n"
hoelzl@63940
  1132
    unfolding less_SUP_iff by (auto simp: b_def)
hoelzl@63940
  1133
  from measurable_envelopeI_countable_cover[of "K \<inter> ?F (b n)" "\<lambda>_. K" M] K
hoelzl@63940
  1134
  obtain K' where "K' \<subseteq> K" and me_K': "measurable_envelope M (K \<inter> ?F (b n)) K'"
hoelzl@63940
  1135
    by auto
hoelzl@63940
  1136
  then have K'_le_K: "emeasure M K' \<le> emeasure M K"
hoelzl@63940
  1137
    by (intro emeasure_mono K)
hoelzl@63940
  1138
  have "K' \<in> sets M"
hoelzl@63940
  1139
    using me_K' by (rule measurable_envelopeD)
hoelzl@63940
  1140
hoelzl@63940
  1141
  have "min (outer_measure_of M {x\<in>K'. f x \<le> a}) (outer_measure_of M {x\<in>K'. b n \<le> f x}) < emeasure M K'"
hoelzl@63940
  1142
  proof (rule assms)
hoelzl@63940
  1143
    show "0 < emeasure M K'" "emeasure M K' < \<infinity>"
hoelzl@63940
  1144
      using measurable_envelopeD2[OF me_K'] pos_b K K'_le_K by auto
hoelzl@63940
  1145
  qed fact+
hoelzl@63940
  1146
  also have "{x\<in>K'. f x \<le> a} = K' \<inter> (K \<inter> ?E a)"
hoelzl@63940
  1147
    using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto
hoelzl@63940
  1148
  also have "{x\<in>K'. b n \<le> f x} = K' \<inter> (K \<inter> ?F (b n))"
hoelzl@63940
  1149
    using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto
hoelzl@63940
  1150
  finally have "min (emeasure M K) (emeasure M K') < emeasure M K'"
hoelzl@63940
  1151
    unfolding
hoelzl@63940
  1152
      measurable_envelopeD(3)[OF me_K \<open>K' \<in> sets M\<close>, symmetric]
hoelzl@63940
  1153
      measurable_envelopeD(3)[OF me_K' \<open>K' \<in> sets M\<close>, symmetric]
hoelzl@63940
  1154
    using \<open>K' \<subseteq> K\<close> by (simp add: Int_absorb1 Int_absorb2)
hoelzl@63940
  1155
  with K'_le_K show False
hoelzl@63940
  1156
    by (auto simp: min_def split: if_split_asm)
hoelzl@63940
  1157
qed
hoelzl@63940
  1158
hoelzl@40859
  1159
end