(* Title: HOL/Analysis/Complete_Measure.thy Author: Robert Himmelmann, Johannes Hoelzl, TU Muenchen *) section ‹Complete Measures› theory Complete_Measure imports Bochner_Integration begin locale✐‹tag important› complete_measure = fixes M :: "'a measure" assumes complete: "⋀A B. B ⊆ A ⟹ A ∈ null_sets M ⟹ B ∈ sets M" definition✐‹tag important› "split_completion M A p = (if A ∈ sets M then p = (A, {}) else ∃N'. A = fst p ∪ snd p ∧ fst p ∩ snd p = {} ∧ fst p ∈ sets M ∧ snd p ⊆ N' ∧ N' ∈ null_sets M)" definition✐‹tag important› "main_part M A = fst (Eps (split_completion M A))" definition✐‹tag important› "null_part M A = snd (Eps (split_completion M A))" definition✐‹tag important› completion :: "'a measure ⇒ '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 ∘ 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✐‹tag important› 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✐‹tag important› measurable_completion: "f ∈ M →⇩_{M}N ⟹ f ∈ completion M →⇩_{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✐‹tag important› 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✐‹tag important› 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 ?μ = "emeasure M ∘ 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) (⋃i::nat. (S i)) = emeasure M (⋃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 ∈ ?N then ?F undefined ∪ ?N else if f x = undefined then ?F (f x) ∪ ?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 ‹x ∈ space M› 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✐‹tag important› 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 ‹null_part M A ⊆ N› 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 →⇩_{M}borel" "(λx. ennreal (- g x)) ∈ completion M →⇩_{M}borel" using g by auto from this[THEN completion_ex_borel_measurable] obtain pf nf :: "'a ⇒ ennreal" where [measurable]: "nf ∈ M →⇩_{M}borel" "pf ∈ M →⇩_{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 →⇩_{M}borel" using ‹N ∈ null_sets M› by auto show "AE x in M. g x = ?F x" using ‹N ∈ null_sets M›[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⇧^{S}(completion M) s ≤ integral⇧^{S}M j" proof (safe intro!: bexI[of _ s'']) have "integral⇧^{S}(completion M) s = integral⇧^{S}(completion M) s''" by (intro simple_integral_cong_AE s simple_function_completion s'' ae_s_eq_s'') then show "integral⇧^{S}(completion M) s ≤ integral⇧^{S}M s''" using s'' by (simp add: simple_integral_completion) from ‹s ≤ f› show "s'' ≤ 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⇧^{S}M s ≤ integral⇧^{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 →⇩_{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 →⇩_{M}borel" shows "integral⇧^{L}(completion M) f = integral⇧^{L}M f" by (rule integral_subalgebra[symmetric]) (auto intro: f) locale✐‹tag important› semifinite_measure = fixes M :: "'a measure" assumes semifinite: "⋀A. A ∈ sets M ⟹ emeasure M A = ∞ ⟹ ∃B∈sets M. B ⊆ A ∧ emeasure M B < ∞" locale✐‹tag important› 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✐‹tag important› cld_measure = complete_measure M + locally_determined_measure M for M :: "'a measure" definition✐‹tag important› outer_measure_of :: "'a measure ⇒ 'a set ⇒ 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 ‹A ⊆ space M› 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 ‹⋀n. A ⊆ E n› by auto have " (INF i. emeasure M (E i)) ≤ outer_measure_of M A" unfolding ‹outer_measure_of M A = (INF n. f n)› 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 ‹⋀n. A ⊆ E n›) 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 ‹outer_measure_of M A = (INF n. f n)› 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 ‹incseq A›, of n] ‹⋀n. A n ⊆ E n› 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 ‹A n ⊆ F n›) qed have "outer_measure_of M (⋃n. A n) ≤ outer_measure_of M (⋃n. F n)" using ‹⋀n. A n ⊆ F n› 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✐‹tag important› measurable_envelope :: "'a measure ⇒ 'a set ⇒ 'a set ⇒ bool" where "measurable_envelope M A E ⟷ (A ⊆ E ∧ E ∈ sets M ∧ (∀F∈sets M. emeasure M (F ∩ E) = outer_measure_of M (F ∩ 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] ‹F ∈ sets M› by (auto simp: measurable_envelope_def) also have "… = outer_measure_of M {}" using ‹F ⊆ E - A› 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: ‹E ∈ sets M› ‹A ⊆ E›) 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 ‹E ∈ sets M› ‹G ∈ sets M› ‹F ∈ sets M› by (auto intro!: emeasure_mono) from G have "E ∩ F - G ∈ sets M" "E ∩ F - G ⊆ E - A" using ‹F ∈ sets M› ‹E ∈ sets M› 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 ‹E ∈ sets M› ‹F ∈ sets M› 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 ‹measurable_envelope M A E› have "emeasure M (E ∩ E) = outer_measure_of M (E ∩ 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✐‹tag important› 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 ‹A ⊆ E› ‹E ∈ sets M›] proof (intro conjI ballI impI assms) fix F assume F: "F ∈ sets M" "F ⊆ E - A" with ‹E ∈ sets M› have le: "emeasure M F ≤ emeasure M E" by (intro emeasure_mono) auto from F ‹A ⊆ E› have "outer_measure_of M A ≤ outer_measure_of M (E - F)" by (intro outer_measure_of_mono) auto then have "emeasure M E - 0 ≤ emeasure M (E - F)" using * ‹E ∈ sets M› ‹F ∈ sets M› by simp also have "… = emeasure M E - emeasure M F" using ‹E ∈ sets M› ‹emeasure M E < ∞› 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 ‹F ⊆ (⋃n. E n)› 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 ‹C n ∈ sets M› 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 ‹A ⊆ (⋃n. C n)› 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 ‹A ⊆ B› 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 ‹A ∈ fmeasurable M› 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 ‹N ⊆ N'› have "{x∈space M. ¬ P x} ⊆ 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 ‹null_part M A ⊆ N› 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 ‹N ∈ null_sets M› 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 →⇩_{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' ∈ sets M" and ae_N': "AE x∈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' ∈ null_sets M" then show "N' ∈ sets M" "AE x∈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: ‹A ∈ completion (density M f)› 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 ‹A ∈ completion (density M f)›] 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 →⇩_{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' ∈ null_sets N" "null_part N A ⊆ N'" using null_part[OF A] by auto then have N': "N' ∈ 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 ‹null_part N A ⊆ N'› 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 →⇩_{M}N ⟹ null_sets N ⊆ null_sets (distr M N f) ⟹ A ∈ completion N ⟹ f -` null_part N A ∩ space M ∈ sets M" using vimage_null_part_null_sets[of f N A] by auto lemma (in complete_measure) measurable_completion2: assumes f: "f ∈ M →⇩_{M}N" and null_sets: "null_sets N ⊆ null_sets (distr M N f)" shows "f ∈ M →⇩_{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 →⇩_{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 →⇩_{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 ⟷ (∀e>0. ∃T∈fmeasurable M. ∃U∈fmeasurable M. T ⊆ S ∧ S ⊆ U ∧ ¦measure M T - measure M U¦ < e)" (is "_ ⟷ ?approx") proof safe let ?μ = "measure M" let ?D = "λT U . ¦?μ T - ?μ U¦" 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) ∧ (fst (A n) ⊆ fst (A (Suc n)) ∧ snd (A (Suc n)) ⊆ 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 ‹?approx›[THEN spec, of 1] by auto next fix A n assume "?P n A" moreover from ‹?approx›[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 ‹?P n A› * 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) ⟷ (∀e>0. ∃T∈fmeasurable M. T ⊆ S ∧ m - e < measure M T) ∧ (∀e>0. ∃U∈fmeasurable M. S ⊆ U ∧ 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 _ ‹T ∈ fmeasurable M›]) apply (rule_tac bexI[OF _ ‹U ∈ fmeasurable M›]) by auto qed moreover have "m = measure M S" using ‹S ∈ fmeasurable M› 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) ⟷ (∀e>0. ∃T∈fmeasurable M. T ⊆ S ∧ m - e ≤ measure M T) ∧ (∀e>0. ∃U∈fmeasurable M. S ⊆ U ∧ measure M U ≤ 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 ∩ E) = emeasure M B ∧ outer_measure_of M (B - E) = emeasure M B" proof - from locally_determined[OF ‹E ⊆ space M›] ‹E ∉ sets M› 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 ‹E ∩ F ∉ sets M› show False using complete[OF ‹F ∩ E ⊆ F ∩ H›] 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 ‹E ∩ F ∉ sets M› emeasure_mono[of "F ∩ H" F M] ‹emeasure M F < ∞› have "F ∩ E ∈ sets M" by (intro complete_sets_sandwich[OF _ _ subset]) auto with ‹E ∩ F ∉ sets M› 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 ‹emeasure M F < ∞› show "0 < emeasure M G" "emeasure M G < ∞" using ‹emeasure M G ≠ 0› 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 ‹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 ‹K›.› 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∈A. f x ≤ a}) (outer_measure_of M {x∈A. b ≤ f x}) < emeasure M A" shows "f ∈ M →⇩_{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 →⇩_{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 ‹K ∈ sets M›[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' ⊆ K" and me_K': "measurable_envelope M (K ∩ ?F (b n)) K'" by auto then have K'_le_K: "emeasure M K' ≤ 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 ‹K' ∈ sets M›[THEN sets.sets_into_space] ‹K' ⊆ K› by auto also have "{x∈K'. b n ≤ f x} = K' ∩ (K ∩ ?F (b n))" using ‹K' ∈ sets M›[THEN sets.sets_into_space] ‹K' ⊆ K› by auto finally have "min (emeasure M K) (emeasure M K') < emeasure M K'" unfolding measurable_envelopeD(3)[OF me_K ‹K' ∈ sets M›, symmetric] measurable_envelopeD(3)[OF me_K' ‹K' ∈ sets M›, symmetric] using ‹K' ⊆ K› by (simp add: Int_absorb1 Int_absorb2) with K'_le_K show False by (auto simp: min_def split: if_split_asm) qed end