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