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