Quelle Complete_Measure.thy Sprache: Isabelle

(*  Title:      HOL/Analysis/Complete_Measure.thy
    Author:     Robert Himmelmann, Johannes Hoelzl, TU Muenchen
*)
section \<open>Complete Measures\<close>
theory Complete_Measure
  imports Bochner_Integration
begin

locale\<^marker>\<open>tag important\<close> complete_measure =
  fixes M :: "'a measure"
  assumes complete: "\A B. B \ A \ A \ null_sets M \ B \ sets M"

definition\<^marker>\<open>tag important\<close>
  "split_completion M A p = (if A \ sets M then p = (A, {}) else
   \<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)"

definition\<^marker>\<open>tag important\<close>
  "main_part M A = fst (Eps (split_completion M A))"

definition\<^marker>\<open>tag important\<close>
  "null_part M A = snd (Eps (split_completion M A))"

definition\<^marker>\<open>tag important\<close> completion :: "'a measure \<Rightarrow> 'a measure" where
  "completion M = measure_of (space M) { S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' }
    (emeasure M \<circ> main_part M)"

lemma completion_into_space:
  "{ S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' } \ Pow (space M)"
  using sets.sets_into_space by auto

lemma space_completion[simp]: "space (completion M) = space M"
  unfolding completion_def using space_measure_of[OF completion_into_space] by simp

lemma completionI:
  assumes "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
  shows "A \ { S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' }"
  using assms by auto

lemma completionE:
  assumes "A \ { S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' }"
  obtains S N N' where "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
  using assms by auto

lemma sigma_algebra_completion:
  "sigma_algebra (space M) { S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' }"
    (is "sigma_algebra _ ?A")
  unfolding sigma_algebra_iff2
proof (intro conjI ballI allI impI)
  show "?A \ Pow (space M)"
    using sets.sets_into_space by auto
next
  show "{} \ ?A" by auto
next
  let ?C = "space M"
  fix A assume "A \ ?A"
  then obtain S N N'
    where "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
    by (rule completionE)
  then show "space M - A \ ?A"
    by (intro completionI[of _ "(?C - S) \ (?C - N')" "(?C - S) \ N' \ (?C - N)"]) auto
next
  fix A :: "nat \ 'a set" assume A: "range A \ ?A"
  then have "\n. \S N N'. A n = S \ N \ S \ sets M \ N' \ null_sets M \ N \ N'"
    by (auto simp: image_subset_iff)
  then obtain S N N' where "\x. A x = S x \ N x \ S x \ sets M \ N' x \ null_sets M \ N x \ N' x"
    by metis
  then show "\(A ` UNIV) \ ?A"
    using null_sets_UN[of N']
    by (intro completionI[of _ "\(S ` UNIV)" "\(N ` UNIV)" "\(N' ` UNIV)"]) auto
qed

lemma\<^marker>\<open>tag important\<close> sets_completion:
  "sets (completion M) = { S \ N |S N N'. S \ sets M \ N' \ null_sets M \ N \ N' }"
  using sigma_algebra.sets_measure_of_eq[OF sigma_algebra_completion]
  by (simp add: completion_def)

lemma sets_completionE:
  assumes "A \ sets (completion M)"
  obtains S N N' where "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
  using assms unfolding sets_completion by auto

lemma sets_completionI:
  assumes "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
  shows "A \ sets (completion M)"
  using assms unfolding sets_completion by auto

lemma sets_completionI_sets[intro, simp]:
  "A \ sets M \ A \ sets (completion M)"
  unfolding sets_completion by force

lemma\<^marker>\<open>tag important\<close> measurable_completion: "f \<in> M \<rightarrow>\<^sub>M N \<Longrightarrow> f \<in> completion M \<rightarrow>\<^sub>M N"
  by (auto simp: measurable_def)

lemma null_sets_completion:
  assumes "N' \ null_sets M" "N \ N'" shows "N \ sets (completion M)"
  using assms by (intro sets_completionI[of N "{}" N N']) auto

lemma\<^marker>\<open>tag important\<close> split_completion:
  assumes "A \ sets (completion M)"
  shows "split_completion M A (main_part M A, null_part M A)"
proof cases
  assume "A \ sets M" then show ?thesis
    by (simp add: split_completion_def[abs_def] main_part_def null_part_def)
next
  assume nA: "A \ sets M"
  show ?thesis
    unfolding main_part_def null_part_def if_not_P[OF nA]
  proof (rule someI2_ex)
    from assms obtain S N N' where A: "A = S \ N" "N \ N'" "N' \ null_sets M" "S \ sets M"
      by (blast intro: sets_completionE)
    let ?P = "(S, N - S)"
    show "\p. split_completion M A p"
      unfolding split_completion_def if_not_P[OF nA] using A
    proof (intro exI conjI)
      show "A = fst ?P \ snd ?P" using A by auto
      show "snd ?P \ N'" using A by auto
   qed auto
  qed auto
qed

lemma sets_restrict_space_subset:
  assumes S: "S \ sets (completion M)"
  shows "sets (restrict_space (completion M) S) \ sets (completion M)"
  by (metis assms sets.Int_space_eq2 sets_restrict_space_iff subsetI)

lemma
  assumes "S \ sets (completion M)"
  shows main_part_sets[intro, simp]: "main_part M S \ sets M"
    and main_part_null_part_Un[simp]: "main_part M S \ null_part M S = S"
    and main_part_null_part_Int[simp]: "main_part M S \ null_part M S = {}"
  using split_completion[OF assms]
  by (auto simp: split_completion_def split: if_split_asm)

lemma main_part[simp]: "S \ sets M \ main_part M S = S"
  using split_completion[of S M]
  by (auto simp: split_completion_def split: if_split_asm)

lemma null_part:
  assumes "S \ sets (completion M)" shows "\N. N\null_sets M \ null_part M S \ N"
  using split_completion[OF assms] by (auto simp: split_completion_def split: if_split_asm)

lemma null_part_sets[intro, simp]:
  assumes "S \ sets M" shows "null_part M S \ sets M" "emeasure M (null_part M S) = 0"
proof -
  have S: "S \ sets (completion M)" using assms by auto
  have *: "S - main_part M S \ sets M" using assms by auto
  from main_part_null_part_Un[OF S] main_part_null_part_Int[OF S]
  have "S - main_part M S = null_part M S" by auto
  with * show sets: "null_part M S \ sets M" by auto
  from null_part[OF S] obtain N where "N \ null_sets M \ null_part M S \ N" ..
  with emeasure_eq_0[of N _ "null_part M S"] sets
  show "emeasure M (null_part M S) = 0" by auto
qed

lemma emeasure_main_part_UN:
  fixes S :: "nat \ 'a set"
  assumes "range S \ sets (completion M)"
  shows "emeasure M (main_part M (\i. (S i))) = emeasure M (\i. main_part M (S i))"
proof -
  have S: "\i. S i \ sets (completion M)" using assms by auto
  then have UN: "(\i. S i) \ sets (completion M)" by auto
  have "\i. \N. N \ null_sets M \ null_part M (S i) \ N"
    using null_part[OF S] by auto
  then obtain N where N: "\x. N x \ null_sets M \ null_part M (S x) \ N x" by metis
  then have UN_N: "(\i. N i) \ null_sets M" by (intro null_sets_UN) auto
  from S have "(\i. S i) \ sets (completion M)" by auto
  from null_part[OF this] obtain N' where N': "N' \ null_sets M \ null_part M (\ (range S)) \ N'" ..
  let ?N = "(\i. N i) \ N'"
  have null_set: "?N \ null_sets M" using N' UN_N by (intro null_sets.Un) auto
  have "main_part M (\i. S i) \ ?N = (main_part M (\i. S i) \ null_part M (\i. S i)) \ ?N"
    using N' by auto
  also have "\ = (\i. main_part M (S i) \ null_part M (S i)) \ ?N"
    unfolding main_part_null_part_Un[OF S] main_part_null_part_Un[OF UN] by auto
  also have "\ = (\i. main_part M (S i)) \ ?N"
    using N by auto
  finally have *: "main_part M (\i. S i) \ ?N = (\i. main_part M (S i)) \ ?N" .
  have "emeasure M (main_part M (\i. S i)) = emeasure M (main_part M (\i. S i) \ ?N)"
    using null_set UN by (intro emeasure_Un_null_set[symmetric]) auto
  also have "\ = emeasure M ((\i. main_part M (S i)) \ ?N)"
    unfolding * ..
  also have "\ = emeasure M (\i. main_part M (S i))"
    using null_set S by (intro emeasure_Un_null_set) auto
  finally show ?thesis .
qed

lemma\<^marker>\<open>tag important\<close> emeasure_completion[simp]:
  assumes S: "S \ sets (completion M)"
  shows "emeasure (completion M) S = emeasure M (main_part M S)"
proof (subst emeasure_measure_of[OF completion_def completion_into_space])
  let ?\<mu> = "emeasure M \<circ> main_part M"
  show "S \ sets (completion M)" "?\ S = emeasure M (main_part M S) " using S by simp_all
  show "positive (sets (completion M)) ?\"
    by (simp add: positive_def)
  show "countably_additive (sets (completion M)) ?\"
  proof (intro countably_additiveI)
    fix A :: "nat \ 'a set" assume A: "range A \ sets (completion M)" "disjoint_family A"
    have "disjoint_family (\i. main_part M (A i))"
    proof (intro disjoint_family_on_bisimulation[OF A(2)])
      fix n m assume "A n \ A m = {}"
      then have "(main_part M (A n) \ null_part M (A n)) \ (main_part M (A m) \ null_part M (A m)) = {}"
        using A by (subst (1 2) main_part_null_part_Un) auto
      then show "main_part M (A n) \ main_part M (A m) = {}" by auto
    qed
    then have "(\n. emeasure M (main_part M (A n))) = emeasure M (\i. main_part M (A i))"
      using A by (auto intro!: suminf_emeasure)
    then show "(\n. ?\ (A n)) = ?\ (\(A ` UNIV))"
      by (simp add: completion_def emeasure_main_part_UN[OF A(1)])
  qed
qed

lemma measure_completion[simp]: "S \ sets M \ measure (completion M) S = measure M S"
  unfolding measure_def by auto

lemma emeasure_completion_UN:
  "range S \ sets (completion M) \
    emeasure (completion M) (\<Union>i::nat. (S i)) = emeasure M (\<Union>i. main_part M (S i))"
  by (subst emeasure_completion) (auto simp add: emeasure_main_part_UN)

lemma emeasure_completion_Un:
  assumes S: "S \ sets (completion M)" and T: "T \ sets (completion M)"
  shows "emeasure (completion M) (S \ T) = emeasure M (main_part M S \ main_part M T)"
proof (subst emeasure_completion)
  have UN: "(\i. binary (main_part M S) (main_part M T) i) = (\i. main_part M (binary S T i))"
    unfolding binary_def by (auto split: if_split_asm)
  show "emeasure M (main_part M (S \ T)) = emeasure M (main_part M S \ main_part M T)"
    using emeasure_main_part_UN[of "binary S T" M] assms
    by (simp add: range_binary_eq, simp add: Un_range_binary UN)
qed (auto intro: S T)

lemma sets_completionI_sub:
  assumes N: "N' \ null_sets M" "N \ N'"
  shows "N \ sets (completion M)"
  using assms by (intro sets_completionI[of _ "{}" N N']) auto

lemma completion_ex_simple_function:
  assumes f: "simple_function (completion M) f"
  shows "\f'. simple_function M f' \ (AE x in M. f x = f' x)"
proof -
  let ?F = "\x. f -` {x} \ space M"
  have F: "\x. ?F x \ sets (completion M)" and fin: "finite (f`space M)"
    using simple_functionD[OF f] simple_functionD[OF f] by simp_all
  have "\x. \N. N \ null_sets M \ null_part M (?F x) \ N"
    using F null_part by auto
  from choice[OF this] obtain N where
    N: "\x. null_part M (?F x) \ N x" "\x. N x \ null_sets M" by auto
  let ?N = "\x\f`space M. N x"
  let ?f' = "\x. if x \ ?N then undefined else f x"
  have sets: "?N \ null_sets M" using N fin by (intro null_sets.finite_UN) auto
  show ?thesis unfolding simple_function_def
  proof (safe intro!: exI[of _ ?f'])
    have "?f' ` space M \ f`space M \ {undefined}" by auto
    from finite_subset[OF this] simple_functionD(1)[OF f]
    show "finite (?f' ` space M)" by auto
  next
    fix x assume "x \ space M"
    have "?f' -` {?f' x} \ space M =
      (if x \<in> ?N then ?F undefined \<union> ?N
       else if f x = undefined then ?F (f x) \<union> ?N
       else ?F (f x) - ?N)"
      using N(2) sets.sets_into_space by (auto split: if_split_asm simp: null_sets_def)
    moreover { fix y have "?F y \ ?N \ sets M"
      proof cases
        assume y: "y \ f`space M"
        have "?F y \ ?N = (main_part M (?F y) \ null_part M (?F y)) \ ?N"
          using main_part_null_part_Un[OF F] by auto
        also have "\ = main_part M (?F y) \ ?N"
          using y N by auto
        finally show ?thesis
          using F sets by auto
      next
        assume "y \ f`space M" then have "?F y = {}" by auto
        then show ?thesis using sets by auto
      qed }
    moreover {
      have "?F (f x) - ?N = main_part M (?F (f x)) \ null_part M (?F (f x)) - ?N"
        using main_part_null_part_Un[OF F] by auto
      also have "\ = main_part M (?F (f x)) - ?N"
        using N \<open>x \<in> space M\<close> by auto
      finally have "?F (f x) - ?N \ sets M"
        using F sets by auto }
    ultimately show "?f' -` {?f' x} \ space M \ sets M" by auto
  next
    show "AE x in M. f x = ?f' x"
      by (rule AE_I', rule sets) auto
  qed
qed

lemma\<^marker>\<open>tag important\<close> completion_ex_borel_measurable:
  fixes g :: "'a \ ennreal"
  assumes g: "g \ borel_measurable (completion M)"
  shows "\g'\borel_measurable M. (AE x in M. g x = g' x)"
proof -
  obtain f :: "nat \ 'a \ ennreal"
    where *: "\i. simple_function (completion M) (f i)"
      and **: "\x. (SUP i. f i x) = g x"
    using g[THEN borel_measurable_implies_simple_function_sequence'] by metis
  from *[THEN completion_ex_simple_function]
  have "\i. \f'. simple_function M f' \ (AE x in M. f i x = f' x)" ..
  then obtain f'
    where sf: "\i. simple_function M (f' i)"
      and AE: "\i. AE x in M. f i x = f' i x"
    by metis
  show ?thesis
  proof (intro bexI)
    from AE[unfolded AE_all_countable[symmetric]]
    show "AE x in M. g x = (SUP i. f' i x)" (is "AE x in M. g x = ?f x")
    proof (elim AE_mp, safe intro!: AE_I2)
      fix x assume eq: "\i. f i x = f' i x"
      have "g x = (SUP i. f i x)" by (auto simp: ** split: split_max)
      with eq show "g x = ?f x" by auto
    qed
    show "?f \ borel_measurable M"
      using sf[THEN borel_measurable_simple_function] by auto
  qed
qed

lemma null_sets_completionI: "N \ null_sets M \ N \ null_sets (completion M)"
  by (auto simp: null_sets_def)

lemma AE_completion: "(AE x in M. P x) \ (AE x in completion M. P x)"
  unfolding eventually_ae_filter by (auto intro: null_sets_completionI)

lemma null_sets_completion_iff: "N \ sets M \ N \ null_sets (completion M) \ N \ null_sets M"
  by (auto simp: null_sets_def)

lemma sets_completion_AE: "(AE x in M. \ P x) \ Measurable.pred (completion M) P"
  unfolding pred_def sets_completion eventually_ae_filter
  by auto

lemma null_sets_completion_iff2:
  "A \ null_sets (completion M) \ (\N'\null_sets M. A \ N')"
proof safe
  assume "A \ null_sets (completion M)"
  then have A: "A \ sets (completion M)" and "main_part M A \ null_sets M"
    by (auto simp: null_sets_def)
  moreover obtain N where "N \ null_sets M" "null_part M A \ N"
    using null_part[OF A] by auto
  ultimately show "\N'\null_sets M. A \ N'"
  proof (intro bexI)
    show "A \ N \ main_part M A"
      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[OF A, symmetric]) auto
  qed auto
next
  fix N assume "N \ null_sets M" "A \ N"
  then have "A \ sets (completion M)" and N: "N \ sets M" "A \ N" "emeasure M N = 0"
    by (auto intro: null_sets_completion)
  moreover have "emeasure (completion M) A = 0"
    using N by (intro emeasure_eq_0[of N _ A]) auto
  ultimately show "A \ null_sets (completion M)"
    by auto
qed

lemma null_sets_completion_subset:
  "B \ A \ A \ null_sets (completion M) \ B \ null_sets (completion M)"
  unfolding null_sets_completion_iff2 by auto

interpretation completion: complete_measure "completion M" for M
proof
  show "B \ A \ A \ null_sets (completion M) \ B \ sets (completion M)" for B A
    using null_sets_completion_subset[of B A M] by (simp add: null_sets_def)
qed

lemma null_sets_restrict_space:
  "\ \ sets M \ A \ null_sets (restrict_space M \) \ A \ \ \ A \ null_sets M"
  by (auto simp: null_sets_def emeasure_restrict_space sets_restrict_space)

lemma completion_ex_borel_measurable_real:
  fixes g :: "'a \ real"
  assumes g: "g \ borel_measurable (completion M)"
  shows "\g'\borel_measurable M. (AE x in M. g x = g' x)"
proof -
  have "(\x. ennreal (g x)) \ completion M \\<^sub>M borel" "(\x. ennreal (- g x)) \ completion M \\<^sub>M borel"
    using g by auto
  from this[THEN completion_ex_borel_measurable]
  obtain pf nf :: "'a \ ennreal"
    where [measurable]: "nf \ M \\<^sub>M borel" "pf \ M \\<^sub>M borel"
      and ae: "AE x in M. pf x = ennreal (g x)" "AE x in M. nf x = ennreal (- g x)"
    by (auto simp: eq_commute)
  then have "AE x in M. pf x = ennreal (g x) \ nf x = ennreal (- g x)"
    by auto
  then obtain N where "N \ null_sets M" "{x\space M. pf x \ ennreal (g x) \ nf x \ ennreal (- g x)} \ N"
    by (auto elim!: AE_E)
  show ?thesis
  proof
    let ?F = "\x. indicator (space M - N) x * (enn2real (pf x) - enn2real (nf x))"
    show "?F \ M \\<^sub>M borel"
      using \<open>N \<in> null_sets M\<close> by auto
    show "AE x in M. g x = ?F x"
      using \<open>N \<in> null_sets M\<close>[THEN AE_not_in] ae AE_space
      apply eventually_elim
      subgoal for x
        by (cases "0::real" "g x" rule: linorder_le_cases) (auto simp: ennreal_neg)
      done
  qed
qed

lemma simple_function_completion: "simple_function M f \ simple_function (completion M) f"
  by (simp add: simple_function_def)

lemma simple_integral_completion:
  "simple_function M f \ simple_integral (completion M) f = simple_integral M f"
  unfolding simple_integral_def by simp

lemma nn_integral_completion: "nn_integral (completion M) f = nn_integral M f"
  unfolding nn_integral_def
proof (safe intro!: SUP_eq)
  fix s assume s: "simple_function (completion M) s" and "s \ f"
  then obtain s' where s': "simple_function M s'" "AE x in M. s x = s' x"
    by (auto dest: completion_ex_simple_function)
  then obtain N where N: "N \ null_sets M" "{x\space M. s x \ s' x} \ N"
    by (auto elim!: AE_E)
  then have ae_N: "AE x in M. (s x \ s' x \ x \ N) \ x \ N"
    by (auto dest: AE_not_in)
  define s'' where "s'' x = (if x \ N then 0 else s x)" for x
  then have ae_s_eq_s'': "AE x in completion M. s x = s'' x"
    using s' ae_N by (intro AE_completion) auto
  have s'': "simple_function M s''"
  proof (subst simple_function_cong)
    show "t \ space M \ s'' t = (if t \ N then 0 else s' t)" for t
      using N by (auto simp: s''_def dest: sets.sets_into_space)
    show "simple_function M (\t. if t \ N then 0 else s' t)"
      unfolding s''_def[abs_def] using N by (auto intro!: simple_function_If s')
  qed

  show "\j\{g. simple_function M g \ g \ f}. integral\<^sup>S (completion M) s \ integral\<^sup>S M j"
  proof (safe intro!: bexI[of _ s''])
    have "integral\<^sup>S (completion M) s = integral\<^sup>S (completion M) s''"
      by (intro simple_integral_cong_AE s simple_function_completion s'' ae_s_eq_s'')
    then show "integral\<^sup>S (completion M) s \ integral\<^sup>S M s''"
      using s'' by (simp add: simple_integral_completion)
    from \<open>s \<le> f\<close> show "s'' \<le> f"
      unfolding s''_def le_fun_def by auto
  qed fact
next
  fix s assume "simple_function M s" "s \ f"
  then show "\j\{g. simple_function (completion M) g \ g \ f}. integral\<^sup>S M s \ integral\<^sup>S (completion M) j"
    by (intro bexI[of _ s]) (auto simp: simple_integral_completion simple_function_completion)
qed

lemma integrable_completion:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  shows "f \ M \\<^sub>M borel \ integrable (completion M) f \ integrable M f"
  by (rule integrable_subalgebra[symmetric]) auto

lemma integral_completion:
  fixes f :: "'a \ 'b::{banach, second_countable_topology}"
  assumes f: "f \ M \\<^sub>M borel" shows "integral\<^sup>L (completion M) f = integral\<^sup>L M f"
  by (rule integral_subalgebra[symmetric]) (auto intro: f)

locale\<^marker>\<open>tag important\<close> semifinite_measure =
  fixes M :: "'a measure"
  assumes semifinite:
    "\A. A \ sets M \ emeasure M A = \ \ \B\sets M. B \ A \ emeasure M B < \"

locale\<^marker>\<open>tag important\<close> locally_determined_measure = semifinite_measure +
  assumes locally_determined:
    "\A. A \ space M \ (\B. B \ sets M \ emeasure M B < \ \ A \ B \ sets M) \ A \ sets M"

locale\<^marker>\<open>tag important\<close> cld_measure =
  complete_measure M + locally_determined_measure M for M :: "'a measure"

definition\<^marker>\<open>tag important\<close> outer_measure_of :: "'a measure \<Rightarrow> 'a set \<Rightarrow> ennreal"
  where "outer_measure_of M A = (INF B \ {B\sets M. A \ B}. emeasure M B)"

lemma outer_measure_of_eq[simp]: "A \ sets M \ outer_measure_of M A = emeasure M A"
  by (auto simp: outer_measure_of_def intro!: INF_eqI emeasure_mono)

lemma outer_measure_of_mono: "A \ B \ outer_measure_of M A \ outer_measure_of M B"
  unfolding outer_measure_of_def by (intro INF_superset_mono) auto

lemma outer_measure_of_attain:
  assumes "A \ space M"
  shows "\E\sets M. A \ E \ outer_measure_of M A = emeasure M E"
proof -
  have "emeasure M ` {B \ sets M. A \ B} \ {}"
    using \<open>A \<subseteq> space M\<close> by auto
  from ennreal_Inf_countable_INF[OF this]
  obtain f
    where f: "range f \ emeasure M ` {B \ sets M. A \ B}" "decseq f"
      and "outer_measure_of M A = (INF i. f i)"
    unfolding outer_measure_of_def by auto
  have "\E. \n. (E n \ sets M \ A \ E n \ emeasure M (E n) \ f n) \ E (Suc n) \ E n"
  proof (rule dependent_nat_choice)
    show "\x. x \ sets M \ A \ x \ emeasure M x \ f 0"
      using f(1) by (fastforce simp: image_subset_iff image_iff intro: eq_refl[OF sym])
  next
    fix E n assume "E \ sets M \ A \ E \ emeasure M E \ f n"
    moreover obtain F where "F \ sets M" "A \ F" "f (Suc n) = emeasure M F"
      using f(1) by (auto simp: image_subset_iff image_iff)
    ultimately show "\y. (y \ sets M \ A \ y \ emeasure M y \ f (Suc n)) \ y \ E"
      by (auto intro!: exI[of _ "F \ E"] emeasure_mono)
  qed
  then obtain E
    where [simp]: "\n. E n \ sets M"
      and "\n. A \ E n"
      and le_f: "\n. emeasure M (E n) \ f n"
      and "decseq E"
    by (auto simp: decseq_Suc_iff)
  show ?thesis
  proof cases
    assume fin: "\i. emeasure M (E i) < \"
    show ?thesis
    proof (intro bexI[of _ "\i. E i"] conjI)
      show "A \ (\i. E i)" "(\i. E i) \ sets M"
        using \<open>\<And>n. A \<subseteq> E n\<close> by auto

      have " (INF i. emeasure M (E i)) \ outer_measure_of M A"
        unfolding \<open>outer_measure_of M A = (INF n. f n)\<close>
        by (intro INF_superset_mono le_f) auto
      moreover have "outer_measure_of M A \ (INF i. outer_measure_of M (E i))"
        by (intro INF_greatest outer_measure_of_mono \<open>\<And>n. A \<subseteq> E n\<close>)
      ultimately have "outer_measure_of M A = (INF i. emeasure M (E i))"
        by auto
      also have "\ = emeasure M (\i. E i)"
        using fin by (intro INF_emeasure_decseq' \decseq E\) (auto simp: less_top)
      finally show "outer_measure_of M A = emeasure M (\i. E i)" .
    qed
  next
    assume "\i. emeasure M (E i) < \"
    then have "f n = \" for n
      using le_f by (auto simp: not_less top_unique)
    moreover have "\E\sets M. A \ E \ f 0 = emeasure M E"
      using f by auto
    ultimately show ?thesis
      unfolding \<open>outer_measure_of M A = (INF n. f n)\<close> by simp
  qed
qed

lemma SUP_outer_measure_of_incseq:
  assumes A: "\n. A n \ space M" and "incseq A"
  shows "(SUP n. outer_measure_of M (A n)) = outer_measure_of M (\i. A i)"
proof (rule antisym)
  obtain E
    where E: "\n. E n \ sets M" "\n. A n \ E n" "\n. outer_measure_of M (A n) = emeasure M (E n)"
    using outer_measure_of_attain[OF A] by metis

  define F where "F n = (\i\{n ..}. E i)" for n
  with E have F: "incseq F" "\n. F n \ sets M"
    by (auto simp: incseq_def)
  have "A n \ F n" for n
    using incseqD[OF \<open>incseq A\<close>, of n] \<open>\<And>n. A n \<subseteq> E n\<close> by (auto simp: F_def)

  have eq: "outer_measure_of M (A n) = outer_measure_of M (F n)" for n
  proof (intro antisym)
    have "outer_measure_of M (F n) \ outer_measure_of M (E n)"
      by (intro outer_measure_of_mono) (auto simp add: F_def)
    with E show "outer_measure_of M (F n) \ outer_measure_of M (A n)"
      by auto
    show "outer_measure_of M (A n) \ outer_measure_of M (F n)"
      by (intro outer_measure_of_mono \<open>A n \<subseteq> F n\<close>)
  qed

  have "outer_measure_of M (\n. A n) \ outer_measure_of M (\n. F n)"
    using \<open>\<And>n. A n \<subseteq> F n\<close> by (intro outer_measure_of_mono) auto
  also have "\ = (SUP n. emeasure M (F n))"
    using F by (simp add: SUP_emeasure_incseq subset_eq)
  finally show "outer_measure_of M (\n. A n) \ (SUP n. outer_measure_of M (A n))"
    by (simp add: eq F)
qed (auto intro: SUP_least outer_measure_of_mono)

definition\<^marker>\<open>tag important\<close> measurable_envelope :: "'a measure \<Rightarrow> 'a set \<Rightarrow> 'a set \<Rightarrow> bool"
  where "measurable_envelope M A E \
    (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)))"

lemma measurable_envelopeD:
  assumes "measurable_envelope M A E"
  shows "A \ E"
    and "E \ sets M"
    and "\F. F \ sets M \ emeasure M (F \ E) = outer_measure_of M (F \ A)"
    and "A \ space M"
  using assms sets.sets_into_space[of E] by (auto simp: measurable_envelope_def)

lemma measurable_envelopeD1:
  assumes E: "measurable_envelope M A E" and F: "F \ sets M" "F \ E - A"
  shows "emeasure M F = 0"
proof -
  have "emeasure M F = emeasure M (F \ E)"
    using F by (intro arg_cong2[where f=emeasure]) auto
  also have "\ = outer_measure_of M (F \ A)"
    using measurable_envelopeD[OF E] \<open>F \<in> sets M\<close> by (auto simp: measurable_envelope_def)
  also have "\ = outer_measure_of M {}"
    using \<open>F \<subseteq> E - A\<close> by (intro arg_cong2[where f=outer_measure_of]) auto
  finally show "emeasure M F = 0"
    by simp
qed

lemma measurable_envelope_eq1:
  assumes "A \ E" "E \ sets M"
  shows "measurable_envelope M A E \ (\F\sets M. F \ E - A \ emeasure M F = 0)"
proof safe
  assume *: "\F\sets M. F \ E - A \ emeasure M F = 0"
  show "measurable_envelope M A E"
    unfolding measurable_envelope_def
  proof (rule ccontr, auto simp add: \<open>E \<in> sets M\<close> \<open>A \<subseteq> E\<close>)
    fix F assume "F \ sets M" "emeasure M (F \ E) \ outer_measure_of M (F \ A)"
    then have "outer_measure_of M (F \ A) < emeasure M (F \ E)"
      using outer_measure_of_mono[of "F \ A" "F \ E" M] \A \ E\ \E \ sets M\ by (auto simp: less_le)
    then obtain G where G: "G \ sets M" "F \ A \ G" and less: "emeasure M G < emeasure M (E \ F)"
      unfolding outer_measure_of_def INF_less_iff by (auto simp: ac_simps)
    have le: "emeasure M (G \ E \ F) \ emeasure M G"
      using \<open>E \<in> sets M\<close> \<open>G \<in> sets M\<close> \<open>F \<in> sets M\<close> by (auto intro!: emeasure_mono)

    from G have "E \ F - G \ sets M" "E \ F - G \ E - A"
      using \<open>F \<in> sets M\<close> \<open>E \<in> sets M\<close> by auto
    with * have "0 = emeasure M (E \ F - G)"
      by auto
    also have "E \ F - G = E \ F - (G \ E \ F)"
      by auto
    also have "emeasure M (E \ F - (G \ E \ F)) = emeasure M (E \ F) - emeasure M (G \ E \ F)"
      using \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> le less G by (intro emeasure_Diff) (auto simp: top_unique)
    also have "\ > 0"
      using le less by (intro diff_gr0_ennreal) auto
    finally show False by auto
  qed
qed (rule measurable_envelopeD1)

lemma measurable_envelopeD2:
  assumes E: "measurable_envelope M A E" shows "emeasure M E = outer_measure_of M A"
proof -
  from \<open>measurable_envelope M A E\<close> have "emeasure M (E \<inter> E) = outer_measure_of M (E \<inter> A)"
    by (auto simp: measurable_envelope_def)
  with measurable_envelopeD[OF E] show "emeasure M E = outer_measure_of M A"
    by (auto simp: Int_absorb1)
qed

lemma\<^marker>\<open>tag important\<close> measurable_envelope_eq2:
  assumes "A \ E" "E \ sets M" "emeasure M E < \"
  shows "measurable_envelope M A E \ (emeasure M E = outer_measure_of M A)"
proof safe
  assume *: "emeasure M E = outer_measure_of M A"
  show "measurable_envelope M A E"
    unfolding measurable_envelope_eq1[OF \<open>A \<subseteq> E\<close> \<open>E \<in> sets M\<close>]
  proof (intro conjI ballI impI assms)
    fix F assume F: "F \ sets M" "F \ E - A"
    with \<open>E \<in> sets M\<close> have le: "emeasure M F \<le> emeasure M  E"
      by (intro emeasure_mono) auto
    from F \<open>A \<subseteq> E\<close> have "outer_measure_of M A \<le> outer_measure_of M (E - F)"
      by (intro outer_measure_of_mono) auto
    then have "emeasure M E - 0 \ emeasure M (E - F)"
      using * \<open>E \<in> sets M\<close> \<open>F \<in> sets M\<close> by simp
    also have "\ = emeasure M E - emeasure M F"
      using \<open>E \<in> sets M\<close> \<open>emeasure M E < \<infinity>\<close> F le by (intro emeasure_Diff) (auto simp: top_unique)
    finally show "emeasure M F = 0"
      using ennreal_mono_minus_cancel[of "emeasure M E" 0 "emeasure M F"] le assms by auto
  qed
qed (auto intro: measurable_envelopeD2)

lemma measurable_envelopeI_countable:
  fixes A :: "nat \ 'a set"
  assumes E: "\n. measurable_envelope M (A n) (E n)"
  shows "measurable_envelope M (\n. A n) (\n. E n)"
proof (subst measurable_envelope_eq1)
  show "(\n. A n) \ (\n. E n)" "(\n. E n) \ sets M"
    using measurable_envelopeD(1,2)[OF E] by auto
  show "\F\sets M. F \ (\n. E n) - (\n. A n) \ emeasure M F = 0"
  proof safe
    fix F assume F: "F \ sets M" "F \ (\n. E n) - (\n. A n)"
    then have "F \ E n \ sets M" "F \ E n \ E n - A n" "F \ (\n. E n)" for n
      using measurable_envelopeD(1,2)[OF E] by auto
    then have "emeasure M (\n. F \ E n) = 0"
      by (intro emeasure_UN_eq_0 measurable_envelopeD1[OF E]) auto
    then show "emeasure M F = 0"
      using \<open>F \<subseteq> (\<Union>n. E n)\<close> by (auto simp: Int_absorb2)
  qed
qed

lemma measurable_envelopeI_countable_cover:
  fixes A and C :: "nat \ 'a set"
  assumes C: "A \ (\n. C n)" "\n. C n \ sets M" "\n. emeasure M (C n) < \"
  shows "\E\(\n. C n). measurable_envelope M A E"
proof -
  have "A \ C n \ space M" for n
    using \<open>C n \<in> sets M\<close> by (auto dest: sets.sets_into_space)
  then have "\n. \E\sets M. A \ C n \ E \ outer_measure_of M (A \ C n) = emeasure M E"
    using outer_measure_of_attain[of "A \ C n" M for n] by auto
  then obtain E
    where E: "\n. E n \ sets M" "\n. A \ C n \ E n"
      and eq: "\n. outer_measure_of M (A \ C n) = emeasure M (E n)"
    by metis

  have "outer_measure_of M (A \ C n) \ outer_measure_of M (E n \ C n)" for n
    using E by (intro outer_measure_of_mono) auto
  moreover have "outer_measure_of M (E n \ C n) \ outer_measure_of M (E n)" for n
    by (intro outer_measure_of_mono) auto
  ultimately have eq: "outer_measure_of M (A \ C n) = emeasure M (E n \ C n)" for n
    using E C by (intro antisym) (auto simp: eq)

  { fix n
    have "outer_measure_of M (A \ C n) \ outer_measure_of M (C n)"
      by (intro outer_measure_of_mono) simp
    also have "\ < \"
      using assms by auto
    finally have "emeasure M (E n \ C n) < \"
      using eq by simp }
  then have "measurable_envelope M (\n. A \ C n) (\n. E n \ C n)"
    using E C by (intro measurable_envelopeI_countable measurable_envelope_eq2[THEN iffD2]) (auto simp: eq)
  with \<open>A \<subseteq> (\<Union>n. C n)\<close> show ?thesis
    by (intro exI[of _ "(\n. E n \ C n)"]) (auto simp add: Int_absorb2)
qed

lemma (in complete_measure) complete_sets_sandwich:
  assumes [measurable]: "A \ sets M" "C \ sets M" and subset: "A \ B" "B \ C"
    and measure: "emeasure M A = emeasure M C" "emeasure M A < \"
  shows "B \ sets M"
proof -
  have "B - A \ sets M"
  proof (rule complete)
    show "B - A \ C - A"
      using subset by auto
    show "C - A \ null_sets M"
      using measure subset by(simp add: emeasure_Diff null_setsI)
  qed
  then have "A \ (B - A) \ sets M"
    by measurable
  also have "A \ (B - A) = B"
    using \<open>A \<subseteq> B\<close> by auto
  finally show ?thesis .
qed

lemma (in complete_measure) complete_sets_sandwich_fmeasurable:
  assumes [measurable]: "A \ fmeasurable M" "C \ fmeasurable M" and subset: "A \ B" "B \ C"
    and measure: "measure M A = measure M C"
  shows "B \ fmeasurable M"
proof (rule fmeasurableI2)
  show "B \ C" "C \ fmeasurable M" by fact+
  show "B \ sets M"
  proof (rule complete_sets_sandwich)
    show "A \ sets M" "C \ sets M" "A \ B" "B \ C"
      using assms by auto
    show "emeasure M A < \"
      using \<open>A \<in> fmeasurable M\<close> by (auto simp: fmeasurable_def)
    show "emeasure M A = emeasure M C"
      using assms by (simp add: emeasure_eq_measure2)
  qed
qed

lemma AE_completion_iff: "(AE x in completion M. P x) \ (AE x in M. P x)"
proof
  assume "AE x in completion M. P x"
  then obtain N where "N \ null_sets (completion M)" and P: "{x\space M. \ P x} \ N"
    unfolding eventually_ae_filter by auto
  then obtain N' where N': "N' \ null_sets M" and "N \ N'"
    unfolding null_sets_completion_iff2 by auto
  from P \<open>N \<subseteq> N'\<close> have "{x\<in>space M. \<not> P x} \<subseteq> N'"
    by auto
  with N' show "AE x in M. P x"
    unfolding eventually_ae_filter by auto
qed (rule AE_completion)

lemma null_part_null_sets: "S \ completion M \ null_part M S \ null_sets (completion M)"
  by (auto dest!: null_part intro: null_sets_completionI null_sets_completion_subset)

lemma AE_notin_null_part: "S \ completion M \ (AE x in M. x \ null_part M S)"
  by (auto dest!: null_part_null_sets AE_not_in simp: AE_completion_iff)

lemma completion_upper:
  assumes A: "A \ sets (completion M)"
  shows "\A'\sets M. A \ A' \ emeasure (completion M) A = emeasure M A'"
proof -
  from AE_notin_null_part[OF A] obtain N where N: "N \ null_sets M" "null_part M A \ N"
    unfolding eventually_ae_filter using null_part_null_sets[OF A, THEN null_setsD2, THEN sets.sets_into_space] by auto
  show ?thesis
  proof (intro bexI conjI)
    show "A \ main_part M A \ N"
      using \<open>null_part M A \<subseteq> N\<close> by (subst main_part_null_part_Un[symmetric, OF A]) auto
    show "emeasure (completion M) A = emeasure M (main_part M A \ N)"
      using A \<open>N \<in> null_sets M\<close> by (simp add: emeasure_Un_null_set)
  qed (use A N in auto)
qed

lemma AE_in_main_part:
  assumes A: "A \ completion M" shows "AE x in M. x \ main_part M A \ x \ A"
  using AE_notin_null_part[OF A]
  by (subst (2) main_part_null_part_Un[symmetric, OF A]) auto

lemma completion_density_eq:
  assumes ae: "AE x in M. 0 < f x" and [measurable]: "f \ M \\<^sub>M borel"
  shows "completion (density M f) = density (completion M) f"
proof (intro measure_eqI)
  have "N' \ sets M \ (AE x\N' in M. f x = 0) \ N' \ null_sets M" for N'
  proof safe
    assume N': "N' \<in> sets M" and ae_N': "AE x\<in>N' in M. f x = 0"
    from ae_N' ae have "AE x in M. x \ N'"
      by eventually_elim auto
    then show "N' \ null_sets M"
      using N' by (simp add: AE_iff_null_sets)
  next
    assume N': "N' \<in> null_sets M" then show "N' \<in> sets M" "AE x\<in>N' in M. f x = 0"
      using ae AE_not_in[OF N'] by (auto simp: less_le)
  qed
  then show sets_eq: "sets (completion (density M f)) = sets (density (completion M) f)"
    by (simp add: sets_completion null_sets_density_iff)

  fix A assume A: \<open>A \<in> completion (density M f)\<close>
  moreover
  have "A \ completion M"
    using A unfolding sets_eq by simp
  moreover
  have "main_part (density M f) A \ M"
    using A main_part_sets[of A "density M f"] unfolding sets_density sets_eq by simp
  moreover have "AE x in M. x \ main_part (density M f) A \ x \ A"
    using AE_in_main_part[OF \<open>A \<in> completion (density M f)\<close>] ae by (auto simp add: AE_density)
  ultimately show "emeasure (completion (density M f)) A = emeasure (density (completion M) f) A"
    by (auto simp add: emeasure_density measurable_completion nn_integral_completion intro!: nn_integral_cong_AE)
qed

lemma null_sets_subset: "B \ null_sets M \ A \ sets M \ A \ B \ A \ null_sets M"
  using emeasure_mono[of A B M] by (simp add: null_sets_def)

lemma (in complete_measure) complete2: "A \ B \ B \ null_sets M \ A \ null_sets M"
  using complete[of A B] null_sets_subset[of B M A] by simp

lemma (in complete_measure) AE_iff_null_sets: "(AE x in M. P x) \ {x\space M. \ P x} \ null_sets M"
  unfolding eventually_ae_filter by (auto intro: complete2)

lemma (in complete_measure) null_sets_iff_AE: "A \ null_sets M \ ((AE x in M. x \ A) \ A \ space M)"
  unfolding AE_iff_null_sets by (auto cong: rev_conj_cong dest: sets.sets_into_space simp: subset_eq)

lemma (in complete_measure) in_sets_AE:
  assumes ae: "AE x in M. x \ A \ x \ B" and A: "A \ sets M" and B: "B \ space M"
  shows "B \ sets M"
proof -
  have "(AE x in M. x \ B - A \ x \ A - B)"
    using ae by eventually_elim auto
  then have "B - A \ null_sets M" "A - B \ null_sets M"
    using A B unfolding null_sets_iff_AE by (auto dest: sets.sets_into_space)
  then have "A \ (B - A) - (A - B) \ sets M"
    using A by blast
  also have "A \ (B - A) - (A - B) = B"
    by auto
  finally show "B \ sets M" .
qed

lemma (in complete_measure) vimage_null_part_null_sets:
  assumes f: "f \ M \\<^sub>M N" and eq: "null_sets N \ null_sets (distr M N f)"
    and A: "A \ completion N"
  shows "f -` null_part N A \ space M \ null_sets M"
proof -
  obtain N' where "N' \<in> null_sets N" "null_part N A \<subseteq> N'"
    using null_part[OF A] by auto
  then have N': "N' \<in> null_sets (distr M N f)"
    using eq by auto
  show ?thesis
  proof (rule complete2)
    show "f -` null_part N A \ space M \ f -` N' \ space M"
      using \<open>null_part N A \<subseteq> N'\<close> by auto
    show "f -` N' \ space M \ null_sets M"
      using f N' by (auto simp: null_sets_def emeasure_distr)
  qed
qed

lemma (in complete_measure) vimage_null_part_sets:
  "f \ M \\<^sub>M N \ null_sets N \ null_sets (distr M N f) \ A \ completion N \
  f -` null_part N A \<inter> space M \<in> sets M"
  using vimage_null_part_null_sets[of f N A] by auto

lemma (in complete_measure) measurable_completion2:
  assumes f: "f \ M \\<^sub>M N" and null_sets: "null_sets N \ null_sets (distr M N f)"
  shows "f \ M \\<^sub>M completion N"
proof (rule measurableI)
  show "x \ space M \ f x \ space (completion N)" for x
    using f[THEN measurable_space] by auto
  fix A assume A: "A \ sets (completion N)"
  have "f -` A \ space M = (f -` main_part N A \ space M) \ (f -` null_part N A \ space M)"
    using main_part_null_part_Un[OF A] by auto
  then show "f -` A \ space M \ sets M"
    using f A null_sets by (auto intro: vimage_null_part_sets measurable_sets)
qed

lemma (in complete_measure) completion_distr_eq:
  assumes X: "X \ M \\<^sub>M N" and null_sets: "null_sets (distr M N X) = null_sets N"
  shows "completion (distr M N X) = distr M (completion N) X"
proof (rule measure_eqI)
  show eq: "sets (completion (distr M N X)) = sets (distr M (completion N) X)"
    by (simp add: sets_completion null_sets)

  fix A assume A: "A \ completion (distr M N X)"
  moreover have A': "A \ completion N"
    using A by (simp add: eq)
  moreover have "main_part (distr M N X) A \ sets N"
    using main_part_sets[OF A] by simp
  moreover have "X -` A \ space M = (X -` main_part (distr M N X) A \ space M) \ (X -` null_part (distr M N X) A \ space M)"
    using main_part_null_part_Un[OF A] by auto
  moreover have "X -` null_part (distr M N X) A \ space M \ null_sets M"
    using X A by (intro vimage_null_part_null_sets) (auto cong: distr_cong)
  ultimately show "emeasure (completion (distr M N X)) A = emeasure (distr M (completion N) X) A"
    using X by (auto simp: emeasure_distr measurable_completion null_sets measurable_completion2
                     intro!: emeasure_Un_null_set[symmetric])
qed

lemma distr_completion: "X \ M \\<^sub>M N \ distr (completion M) N X = distr M N X"
  by (intro measure_eqI) (auto simp: emeasure_distr measurable_completion)

proposition (in complete_measure) fmeasurable_inner_outer:
  "S \ fmeasurable M \
    (\<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)"
  (is "_ \ ?approx")
proof safe
  let ?\<mu> = "measure M" let ?D = "\<lambda>T U . \<bar>?\<mu> T - ?\<mu> U\<bar>"
  assume ?approx
  have "\A. \n. (fst (A n) \ fmeasurable M \ snd (A n) \ fmeasurable M \ fst (A n) \ S \ S \ snd (A n) \
    ?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))"
    (is "\A. \n. ?P n (A n) \ ?Q (A n) (A (Suc n))")
  proof (intro dependent_nat_choice)
    show "\A. ?P 0 A"
      using \<open>?approx\<close>[THEN spec, of 1] by auto
  next
    fix A n assume "?P n A"
    moreover
    from \<open>?approx\<close>[THEN spec, of "1/Suc (Suc n)"]
    obtain T U where *: "T \ fmeasurable M" "U \ fmeasurable M" "T \ S" "S \ U" "?D T U < 1 / Suc (Suc n)"
      by auto
    ultimately have "?\ T \ ?\ (T \ fst A)" "?\ (U \ snd A) \ ?\ U"
      "?\ T \ ?\ U" "?\ (T \ fst A) \ ?\ (U \ snd A)"
      by (auto intro!: measure_mono_fmeasurable)
    then have "?D (T \ fst A) (U \ snd A) \ ?D T U"
      by auto
    also have "?D T U < 1/Suc (Suc n)" by fact
    finally show "\B. ?P (Suc n) B \ ?Q A B"
      using \<open>?P n A\<close> *
      by (intro exI[of _ "(T \ fst A, U \ snd A)"] conjI) auto
  qed
  then obtain A
    where lm: "\n. fst (A n) \ fmeasurable M" "\n. snd (A n) \ fmeasurable M"
      and set_bound: "\n. fst (A n) \ S" "\n. S \ snd (A n)"
      and mono: "\n. fst (A n) \ fst (A (Suc n))" "\n. snd (A (Suc n)) \ snd (A n)"
      and bound: "\n. ?D (fst (A n)) (snd (A n)) < 1/Suc n"
    by metis

  have INT_sA: "(\n. snd (A n)) \ fmeasurable M"
    using lm by (intro fmeasurable_INT[of _ 0]) auto
  have UN_fA: "(\n. fst (A n)) \ fmeasurable M"
    using lm order_trans[OF set_bound(1) set_bound(2)[of 0]] by (intro fmeasurable_UN[of _ _ "snd (A 0)"]) auto

  have "(\n. ?\ (fst (A n)) - ?\ (snd (A n))) \ 0"
    using bound
    by (subst tendsto_rabs_zero_iff[symmetric])
       (intro tendsto_sandwich[OF _ _ tendsto_const LIMSEQ_inverse_real_of_nat];
        auto intro!: always_eventually less_imp_le simp: divide_inverse)
  moreover
  have "(\n. ?\ (fst (A n)) - ?\ (snd (A n))) \ ?\ (\n. fst (A n)) - ?\ (\n. snd (A n))"
  proof (intro tendsto_diff Lim_measure_incseq Lim_measure_decseq)
    show "range (\i. fst (A i)) \ sets M" "range (\i. snd (A i)) \ sets M"
      "incseq (\i. fst (A i))" "decseq (\n. snd (A n))"
      using mono lm by (auto simp: incseq_Suc_iff decseq_Suc_iff intro!: measure_mono_fmeasurable)
    show "emeasure M (\x. fst (A x)) \ \" "emeasure M (snd (A n)) \ \" for n
      using lm(2)[of n] UN_fA by (auto simp: fmeasurable_def)
  qed
  ultimately have eq: "0 = ?\ (\n. fst (A n)) - ?\ (\n. snd (A n))"
    by (rule LIMSEQ_unique)

  show "S \ fmeasurable M"
    using UN_fA INT_sA
  proof (rule complete_sets_sandwich_fmeasurable)
    show "(\n. fst (A n)) \ S" "S \ (\n. snd (A n))"
      using set_bound by auto
    show "?\ (\n. fst (A n)) = ?\ (\n. snd (A n))"
      using eq by auto
  qed
qed (auto intro!: bexI[of _ S])

lemma (in complete_measure) fmeasurable_measure_inner_outer:
   "(S \ fmeasurable M \ m = measure M S) \
      (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e < measure M T) \<and>
      (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U < m + e)"
    (is "?lhs = ?rhs")
proof
  assume RHS: ?rhs
  then have T: "\e. 0 < e \ (\T\fmeasurable M. T \ S \ m - e < measure M T)"
        and U: "\e. 0 < e \ (\U\fmeasurable M. S \ U \ measure M U < m + e)"
    by auto
  have "S \ fmeasurable M"
  proof (subst fmeasurable_inner_outer, safe)
    fix e::real assume "0 < e"
    with RHS obtain T U where T: "T \ fmeasurable M" "T \ S" "m - e/2 < measure M T"
                          and U: "U \ fmeasurable M" "S \ U" "measure M U < m + e/2"
      by (meson half_gt_zero)+
    moreover have "measure M U - measure M T < (m + e/2) - (m - e/2)"
      by (intro diff_strict_mono) fact+
    moreover have "measure M T \ measure M U"
      using T U by (intro measure_mono_fmeasurable) auto
    ultimately show "\T\fmeasurable M. \U\fmeasurable M. T \ S \ S \ U \ \measure M T - measure M U\ < e"
      apply (rule_tac bexI[OF _ \<open>T \<in> fmeasurable M\<close>])
      apply (rule_tac bexI[OF _ \<open>U \<in> fmeasurable M\<close>])
      by auto
  qed
  moreover have "m = measure M S"
    using \<open>S \<in> fmeasurable M\<close> U[of "measure M S - m"] T[of "m - measure M S"]
    by (cases m "measure M S" rule: linorder_cases)
       (auto simp: not_le[symmetric] measure_mono_fmeasurable)
  ultimately show ?lhs
    by simp
qed (auto intro!: bexI[of _ S])

lemma (in complete_measure) null_sets_outer:
  "S \ null_sets M \ (\e>0. \T\fmeasurable M. S \ T \ measure M T < e)"
proof -
  have "S \ null_sets M \ (S \ fmeasurable M \ 0 = measure M S)"
    by (auto simp: null_sets_def emeasure_eq_measure2 intro: fmeasurableI) (simp add: measure_def)
  also have "\ = (\e>0. \T\fmeasurable M. S \ T \ measure M T < e)"
    unfolding fmeasurable_measure_inner_outer by auto
  finally show ?thesis .
qed

lemma (in complete_measure) fmeasurable_measure_inner_outer_le:
     "(S \ fmeasurable M \ m = measure M S) \
        (\<forall>e>0. \<exists>T\<in>fmeasurable M. T \<subseteq> S \<and> m - e \<le> measure M T) \<and>
        (\<forall>e>0. \<exists>U\<in>fmeasurable M. S \<subseteq> U \<and> measure M U \<le> m + e)" (is ?T1)
  and null_sets_outer_le:
     "S \ null_sets M \ (\e>0. \T\fmeasurable M. S \ T \ measure M T \ e)" (is ?T2)
proof -
  have "e > 0 \ m - e/2 \ t \ m - e < t"
       "e > 0 \ t \ m + e/2 \ t < m + e"
       "e > 0 \ e/2 > 0"
       for e t
    by auto
  then show ?T1 ?T2
    unfolding fmeasurable_measure_inner_outer null_sets_outer
    by (meson dense le_less_trans less_imp_le)+
qed

lemma (in cld_measure) notin_sets_outer_measure_of_cover:
  assumes E: "E \ space M" "E \ sets M"
  shows "\B\sets M. 0 < emeasure M B \ emeasure M B < \ \
    outer_measure_of M (B \<inter> E) = emeasure M B \<and> outer_measure_of M (B - E) = emeasure M B"
proof -
  from locally_determined[OF \<open>E \<subseteq> space M\<close>] \<open>E \<notin> sets M\<close>
  obtain F
    where [measurable]: "F \ sets M" and "emeasure M F < \" "E \ F \ sets M"
    by blast
  then obtain H H'
    where H: "measurable_envelope M (F \ E) H" and H': "measurable_envelope M (F - E) H'"
    using measurable_envelopeI_countable_cover[of "F \ E" "\_. F" M]
       measurable_envelopeI_countable_cover[of "F - E" "\_. F" M]
    by auto
  note measurable_envelopeD(2)[OF H', measurable] measurable_envelopeD(2)[OF H, measurable]

  from measurable_envelopeD(1)[OF H'] measurable_envelopeD(1)[OF H]
  have subset: "F - H' \ F \ E" "F \ E \ F \ H"
    by auto
  moreover define G where "G = (F \ H) - (F - H')"
  ultimately have G: "G = F \ H \ H'"
    by auto
  have "emeasure M (F \ H) \ 0"
  proof
    assume "emeasure M (F \ H) = 0"
    then have "F \ H \ null_sets M"
      by auto
    with \<open>E \<inter> F \<notin> sets M\<close> show False
      using complete[OF \<open>F \<inter> E \<subseteq> F \<inter> H\<close>] by (auto simp: Int_commute)
  qed
  moreover
  have "emeasure M (F - H') \ emeasure M (F \ H)"
  proof
    assume "emeasure M (F - H') = emeasure M (F \ H)"
    with \<open>E \<inter> F \<notin> sets M\<close> emeasure_mono[of "F \<inter> H" F M] \<open>emeasure M F < \<infinity>\<close>
    have "F \ E \ sets M"
      by (intro complete_sets_sandwich[OF _ _ subset]) auto
    with \<open>E \<inter> F \<notin> sets M\<close> show False
      by (simp add: Int_commute)
  qed
  moreover have "emeasure M (F - H') \ emeasure M (F \ H)"
    using subset by (intro emeasure_mono) auto
  ultimately have "emeasure M G \ 0"
    unfolding G_def using subset
    by (subst emeasure_Diff) (auto simp: top_unique diff_eq_0_iff_ennreal)
  show ?thesis
  proof (intro bexI conjI)
    have "emeasure M G \ emeasure M F"
      unfolding G by (auto intro!: emeasure_mono)
    with \<open>emeasure M F < \<infinity>\<close> show "0 < emeasure M G" "emeasure M G < \<infinity>"
      using \<open>emeasure M G \<noteq> 0\<close> by (auto simp: zero_less_iff_neq_zero)
    show [measurable]: "G \ sets M"
      unfolding G by auto

    have "emeasure M G = outer_measure_of M (F \ H' \ (F \ E))"
      using measurable_envelopeD(3)[OF H, of "F \ H'"] unfolding G by (simp add: ac_simps)
    also have "\ \ outer_measure_of M (G \ E)"
      using measurable_envelopeD(1)[OF H] by (intro outer_measure_of_mono) (auto simp: G)
    finally show "outer_measure_of M (G \ E) = emeasure M G"
      using outer_measure_of_mono[of "G \ E" G M] by auto

    have "emeasure M G = outer_measure_of M (F \ H \ (F - E))"
      using measurable_envelopeD(3)[OF H', of "F \ H"] unfolding G by (simp add: ac_simps)
    also have "\ \ outer_measure_of M (G - E)"
      using measurable_envelopeD(1)[OF H'] by (intro outer_measure_of_mono) (auto simp: G)
    finally show "outer_measure_of M (G - E) = emeasure M G"
      using outer_measure_of_mono[of "G - E" G M] by auto
  qed
qed

text \<open>The following theorem is a specialization of D.H. Fremlin, Measure Theory vol 4I (413G). We
  only show one direction and do not use a inner regular family \<open>K\<close>.\<close>

lemma (in cld_measure) borel_measurable_cld:
  fixes f :: "'a \ real"
  assumes "\A a b. A \ sets M \ 0 < emeasure M A \ emeasure M A < \ \ a < b \
      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"
  shows "f \ M \\<^sub>M borel"
proof (rule ccontr)
  let ?E = "\a. {x\space M. f x \ a}" and ?F = "\a. {x\space M. a \ f x}"

  assume "f \ M \\<^sub>M borel"
  then obtain a where "?E a \ sets M"
    unfolding borel_measurable_iff_le by blast
  from notin_sets_outer_measure_of_cover[OF _ this]
  obtain K
    where K: "K \ sets M" "0 < emeasure M K" "emeasure M K < \"
      and eq1: "outer_measure_of M (K \ ?E a) = emeasure M K"
      and eq2: "outer_measure_of M (K - ?E a) = emeasure M K"
    by auto
  then have me_K: "measurable_envelope M (K \ ?E a) K"
    by (subst measurable_envelope_eq2) auto

  define b where "b n = a + inverse (real (Suc n))" for n
  have "(SUP n. outer_measure_of M (K \ ?F (b n))) = outer_measure_of M (\n. K \ ?F (b n))"
  proof (intro SUP_outer_measure_of_incseq)
    have "x \ y \ b y \ b x" for x y
      by (auto simp: b_def field_simps)
    then show "incseq (\n. K \ {x \ space M. b n \ f x})"
      by (auto simp: incseq_def intro: order_trans)
  qed auto
  also have "(\n. K \ ?F (b n)) = K - ?E a"
  proof -
    have "b \ a"
      unfolding b_def by (rule LIMSEQ_inverse_real_of_nat_add)
    then have "\n. \ b n \ f x \ f x \ a" for x
      by (rule LIMSEQ_le_const) (auto intro: less_imp_le simp: not_le)
    moreover have "\ b n \ a" for n
      by (auto simp: b_def)
    ultimately show ?thesis
      using \<open>K \<in> sets M\<close>[THEN sets.sets_into_space] by (auto simp: subset_eq intro: order_trans)
  qed
  finally have "0 < (SUP n. outer_measure_of M (K \ ?F (b n)))"
    using K by (simp add: eq2)
  then obtain n where pos_b: "0 < outer_measure_of M (K \ ?F (b n))" and "a < b n"
    unfolding less_SUP_iff by (auto simp: b_def)
  from measurable_envelopeI_countable_cover[of "K \ ?F (b n)" "\_. K" M] K
  obtain K' where "K' \<subseteq> K" and me_K': "measurable_envelope M (K \<inter> ?F (b n)) K'"
    by auto
  then have K'_le_K: "emeasure M K' \<le> emeasure M K"
    by (intro emeasure_mono K)
  have "K' \ sets M"
    using me_K' by (rule measurable_envelopeD)

  have "min (outer_measure_of M {x\K'. f x \ a}) (outer_measure_of M {x\K'. b n \ f x}) < emeasure M K'"
  proof (rule assms)
    show "0 < emeasure M K'" "emeasure M K' < \"
      using measurable_envelopeD2[OF me_K'] pos_b K K'_le_K by auto
  qed fact+
  also have "{x\K'. f x \ a} = K' \ (K \ ?E a)"
    using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto
  also have "{x\K'. b n \ f x} = K' \ (K \ ?F (b n))"
    using \<open>K' \<in> sets M\<close>[THEN sets.sets_into_space] \<open>K' \<subseteq> K\<close> by auto
  finally have "min (emeasure M K) (emeasure M K') < emeasure M K'"
    unfolding
      measurable_envelopeD(3)[OF me_K \<open>K' \<in> sets M\<close>, symmetric]
      measurable_envelopeD(3)[OF me_K' \K' \ sets M\, symmetric]
    using \<open>K' \<subseteq> K\<close> by (simp add: Int_absorb1 Int_absorb2)
  with K'_le_K show False
    by (auto simp: min_def split: if_split_asm)
qed

end

quality99%

¤ Dauer der Verarbeitung: 0.26 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.