(* Title: HOL/Analysis/Regularity.thy Author: Fabian Immler, TU München *) section ‹Regularity of Measures› theory Regularity imports Measure_Space Borel_Space begin lemma fixes M::"'a::{second_countable_topology, complete_space} measure" assumes sb: "sets M = sets borel" assumes "emeasure M (space M) ≠ ∞" assumes "B ∈ sets borel" shows inner_regular: "emeasure M B = (SUP K : {K. K ⊆ B ∧ compact K}. emeasure M K)" (is "?inner B") and outer_regular: "emeasure M B = (INF U : {U. B ⊆ U ∧ open U}. emeasure M U)" (is "?outer B") proof - have Us: "UNIV = space M" by (metis assms(1) sets_eq_imp_space_eq space_borel) hence sU: "space M = UNIV" by simp interpret finite_measure M by rule fact have approx_inner: "⋀A. A ∈ sets M ⟹ (⋀e. e > 0 ⟹ ∃K. K ⊆ A ∧ compact K ∧ emeasure M A ≤ emeasure M K + ennreal e) ⟹ ?inner A" by (rule ennreal_approx_SUP) (force intro!: emeasure_mono simp: compact_imp_closed emeasure_eq_measure)+ have approx_outer: "⋀A. A ∈ sets M ⟹ (⋀e. e > 0 ⟹ ∃B. A ⊆ B ∧ open B ∧ emeasure M B ≤ emeasure M A + ennreal e) ⟹ ?outer A" by (rule ennreal_approx_INF) (force intro!: emeasure_mono simp: emeasure_eq_measure sb)+ from countable_dense_setE guess X::"'a set" . note X = this { fix r::real assume "r > 0" hence "⋀y. open (ball y r)" "⋀y. ball y r ≠ {}" by auto with X(2)[OF this] have x: "space M = (⋃x∈X. cball x r)" by (auto simp add: sU) (metis dist_commute order_less_imp_le) let ?U = "⋃k. (⋃n∈{0..k}. cball (from_nat_into X n) r)" have "(λk. emeasure M (⋃n∈{0..k}. cball (from_nat_into X n) r)) ⇢ M ?U" by (rule Lim_emeasure_incseq) (auto intro!: borel_closed bexI simp: incseq_def Us sb) also have "?U = space M" proof safe fix x from X(2)[OF open_ball[of x r]] ‹r > 0› obtain d where d: "d∈X" "d ∈ ball x r" by auto show "x ∈ ?U" using X(1) d by simp (auto intro!: exI [where x = "to_nat_on X d"] simp: dist_commute Bex_def) qed (simp add: sU) finally have "(λk. M (⋃n∈{0..k}. cball (from_nat_into X n) r)) ⇢ M (space M)" . } note M_space = this { fix e ::real and n :: nat assume "e > 0" "n > 0" hence "1/n > 0" "e * 2 powr - n > 0" by (auto) from M_space[OF ‹1/n>0›] have "(λk. measure M (⋃i∈{0..k}. cball (from_nat_into X i) (1/real n))) ⇢ measure M (space M)" unfolding emeasure_eq_measure by (auto simp: measure_nonneg) from metric_LIMSEQ_D[OF this ‹0 < e * 2 powr -n›] obtain k where "dist (measure M (⋃i∈{0..k}. cball (from_nat_into X i) (1/real n))) (measure M (space M)) < e * 2 powr -n" by auto hence "measure M (⋃i∈{0..k}. cball (from_nat_into X i) (1/real n)) ≥ measure M (space M) - e * 2 powr -real n" by (auto simp: dist_real_def) hence "∃k. measure M (⋃i∈{0..k}. cball (from_nat_into X i) (1/real n)) ≥ measure M (space M) - e * 2 powr - real n" .. } note k=this hence "∀e∈{0<..}. ∀(n::nat)∈{0<..}. ∃k. measure M (⋃i∈{0..k}. cball (from_nat_into X i) (1/real n)) ≥ measure M (space M) - e * 2 powr - real n" by blast then obtain k where k: "∀e∈{0<..}. ∀n∈{0<..}. measure M (space M) - e * 2 powr - real (n::nat) ≤ measure M (⋃i∈{0..k e n}. cball (from_nat_into X i) (1 / n))" by metis hence k: "⋀e n. e > 0 ⟹ n > 0 ⟹ measure M (space M) - e * 2 powr - n ≤ measure M (⋃i∈{0..k e n}. cball (from_nat_into X i) (1 / n))" unfolding Ball_def by blast have approx_space: "∃K ∈ {K. K ⊆ space M ∧ compact K}. emeasure M (space M) ≤ emeasure M K + ennreal e" (is "?thesis e") if "0 < e" for e :: real proof - define B where [abs_def]: "B n = (⋃i∈{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n))" for n have "⋀n. closed (B n)" by (auto simp: B_def) hence [simp]: "⋀n. B n ∈ sets M" by (simp add: sb) from k[OF ‹e > 0› zero_less_Suc] have "⋀n. measure M (space M) - measure M (B n) ≤ e * 2 powr - real (Suc n)" by (simp add: algebra_simps B_def finite_measure_compl) hence B_compl_le: "⋀n::nat. measure M (space M - B n) ≤ e * 2 powr - real (Suc n)" by (simp add: finite_measure_compl) define K where "K = (⋂n. B n)" from ‹closed (B _)› have "closed K" by (auto simp: K_def) hence [simp]: "K ∈ sets M" by (simp add: sb) have "measure M (space M) - measure M K = measure M (space M - K)" by (simp add: finite_measure_compl) also have "… = emeasure M (⋃n. space M - B n)" by (auto simp: K_def emeasure_eq_measure) also have "… ≤ (∑n. emeasure M (space M - B n))" by (rule emeasure_subadditive_countably) (auto simp: summable_def) also have "… ≤ (∑n. ennreal (e*2 powr - real (Suc n)))" using B_compl_le by (intro suminf_le) (simp_all add: measure_nonneg emeasure_eq_measure ennreal_leI) also have "… ≤ (∑n. ennreal (e * (1 / 2) ^ Suc n))" by (simp add: powr_minus powr_realpow field_simps del: of_nat_Suc) also have "… = ennreal e * (∑n. ennreal ((1 / 2) ^ Suc n))" unfolding ennreal_power[symmetric] using ‹0 < e› by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def ennreal_power[symmetric]) also have "… = e" by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto finally have "measure M (space M) ≤ measure M K + e" using ‹0 < e› by simp hence "emeasure M (space M) ≤ emeasure M K + e" using ‹0 < e› by (simp add: emeasure_eq_measure flip: ennreal_plus) moreover have "compact K" unfolding compact_eq_totally_bounded proof safe show "complete K" using ‹closed K› by (simp add: complete_eq_closed) fix e'::real assume "0 < e'" from nat_approx_posE[OF this] guess n . note n = this let ?k = "from_nat_into X ` {0..k e (Suc n)}" have "finite ?k" by simp moreover have "K ⊆ (⋃x∈?k. ball x e')" unfolding K_def B_def using n by force ultimately show "∃k. finite k ∧ K ⊆ (⋃x∈k. ball x e')" by blast qed ultimately show ?thesis by (auto simp: sU) qed { fix A::"'a set" assume "closed A" hence "A ∈ sets borel" by (simp add: compact_imp_closed) hence [simp]: "A ∈ sets M" by (simp add: sb) have "?inner A" proof (rule approx_inner) fix e::real assume "e > 0" from approx_space[OF this] obtain K where K: "K ⊆ space M" "compact K" "emeasure M (space M) ≤ emeasure M K + e" by (auto simp: emeasure_eq_measure) hence [simp]: "K ∈ sets M" by (simp add: sb compact_imp_closed) have "measure M A - measure M (A ∩ K) = measure M (A - A ∩ K)" by (subst finite_measure_Diff) auto also have "A - A ∩ K = A ∪ K - K" by auto also have "measure M … = measure M (A ∪ K) - measure M K" by (subst finite_measure_Diff) auto also have "… ≤ measure M (space M) - measure M K" by (simp add: emeasure_eq_measure sU sb finite_measure_mono) also have "… ≤ e" using K ‹0 < e› by (simp add: emeasure_eq_measure flip: ennreal_plus) finally have "emeasure M A ≤ emeasure M (A ∩ K) + ennreal e" using ‹0<e› by (simp add: emeasure_eq_measure algebra_simps flip: ennreal_plus) moreover have "A ∩ K ⊆ A" "compact (A ∩ K)" using ‹closed A› ‹compact K› by auto ultimately show "∃K ⊆ A. compact K ∧ emeasure M A ≤ emeasure M K + ennreal e" by blast qed simp have "?outer A" proof cases assume "A ≠ {}" let ?G = "λd. {x. infdist x A < d}" { fix d have "?G d = (λx. infdist x A) -` {..<d}" by auto also have "open …" by (intro continuous_open_vimage) (auto intro!: continuous_infdist continuous_ident) finally have "open (?G d)" . } note open_G = this from in_closed_iff_infdist_zero[OF ‹closed A› ‹A ≠ {}›] have "A = {x. infdist x A = 0}" by auto also have "… = (⋂i. ?G (1/real (Suc i)))" proof (auto simp del: of_nat_Suc, rule ccontr) fix x assume "infdist x A ≠ 0" hence pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp from nat_approx_posE[OF this] guess n . moreover assume "∀i. infdist x A < 1 / real (Suc i)" hence "infdist x A < 1 / real (Suc n)" by auto ultimately show False by simp qed also have "M … = (INF n. emeasure M (?G (1 / real (Suc n))))" proof (rule INF_emeasure_decseq[symmetric], safe) fix i::nat from open_G[of "1 / real (Suc i)"] show "?G (1 / real (Suc i)) ∈ sets M" by (simp add: sb borel_open) next show "decseq (λi. {x. infdist x A < 1 / real (Suc i)})" by (auto intro: less_trans intro!: divide_strict_left_mono simp: decseq_def le_eq_less_or_eq) qed simp finally have "emeasure M A = (INF n. emeasure M {x. infdist x A < 1 / real (Suc n)})" . moreover have "… ≥ (INF U:{U. A ⊆ U ∧ open U}. emeasure M U)" proof (intro INF_mono) fix m have "?G (1 / real (Suc m)) ∈ {U. A ⊆ U ∧ open U}" using open_G by auto moreover have "M (?G (1 / real (Suc m))) ≤ M (?G (1 / real (Suc m)))" by simp ultimately show "∃U∈{U. A ⊆ U ∧ open U}. emeasure M U ≤ emeasure M {x. infdist x A < 1 / real (Suc m)}" by blast qed moreover have "emeasure M A ≤ (INF U:{U. A ⊆ U ∧ open U}. emeasure M U)" by (rule INF_greatest) (auto intro!: emeasure_mono simp: sb) ultimately show ?thesis by simp qed (auto intro!: INF_eqI) note ‹?inner A› ‹?outer A› } note closed_in_D = this from ‹B ∈ sets borel› have "Int_stable (Collect closed)" "Collect closed ⊆ Pow UNIV" "B ∈ sigma_sets UNIV (Collect closed)" by (auto simp: Int_stable_def borel_eq_closed) then show "?inner B" "?outer B" proof (induct B rule: sigma_sets_induct_disjoint) case empty { case 1 show ?case by (intro SUP_eqI[symmetric]) auto } { case 2 show ?case by (intro INF_eqI[symmetric]) (auto elim!: meta_allE[of _ "{}"]) } next case (basic B) { case 1 from basic closed_in_D show ?case by auto } { case 2 from basic closed_in_D show ?case by auto } next case (compl B) note inner = compl(2) and outer = compl(3) from compl have [simp]: "B ∈ sets M" by (auto simp: sb borel_eq_closed) case 2 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) also have "… = (INF K:{K. K ⊆ B ∧ compact K}. M (space M) - M K)" by (subst ennreal_SUP_const_minus) (auto simp: less_top[symmetric] inner) also have "… = (INF U:{U. U ⊆ B ∧ compact U}. M (space M - U))" by (rule INF_cong) (auto simp add: emeasure_compl sb compact_imp_closed) also have "… ≥ (INF U:{U. U ⊆ B ∧ closed U}. M (space M - U))" by (rule INF_superset_mono) (auto simp add: compact_imp_closed) also have "(INF U:{U. U ⊆ B ∧ closed U}. M (space M - U)) = (INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U)" unfolding INF_image [of _ "λu. space M - u" _, symmetric, unfolded comp_def] by (rule INF_cong) (auto simp add: sU Compl_eq_Diff_UNIV [symmetric, simp]) finally have "(INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U) ≤ emeasure M (space M - B)" . moreover have "(INF U:{U. space M - B ⊆ U ∧ open U}. emeasure M U) ≥ emeasure M (space M - B)" by (auto simp: sb sU intro!: INF_greatest emeasure_mono) ultimately show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) case 1 have "M (space M - B) = M (space M) - emeasure M B" by (auto simp: emeasure_compl) also have "… = (SUP U: {U. B ⊆ U ∧ open U}. M (space M) - M U)" unfolding outer by (subst ennreal_INF_const_minus) auto also have "… = (SUP U:{U. B ⊆ U ∧ open U}. M (space M - U))" by (rule SUP_cong) (auto simp add: emeasure_compl sb compact_imp_closed) also have "… = (SUP K:{K. K ⊆ space M - B ∧ closed K}. emeasure M K)" unfolding SUP_image [of _ "λu. space M - u" _, symmetric, unfolded comp_def] by (rule SUP_cong) (auto simp add: sU) also have "… = (SUP K:{K. K ⊆ space M - B ∧ compact K}. emeasure M K)" proof (safe intro!: antisym SUP_least) fix K assume "closed K" "K ⊆ space M - B" from closed_in_D[OF ‹closed K›] have K_inner: "emeasure M K = (SUP K:{Ka. Ka ⊆ K ∧ compact Ka}. emeasure M K)" by simp show "emeasure M K ≤ (SUP K:{K. K ⊆ space M - B ∧ compact K}. emeasure M K)" unfolding K_inner using ‹K ⊆ space M - B› by (auto intro!: SUP_upper SUP_least) qed (fastforce intro!: SUP_least SUP_upper simp: compact_imp_closed) finally show ?case by (auto intro!: antisym simp: sets_eq_imp_space_eq[OF sb]) next case (union D) then have "range D ⊆ sets M" by (auto simp: sb borel_eq_closed) with union have M[symmetric]: "(∑i. M (D i)) = M (⋃i. D i)" by (intro suminf_emeasure) also have "(λn. ∑i<n. M (D i)) ⇢ (∑i. M (D i))" by (intro summable_LIMSEQ) auto finally have measure_LIMSEQ: "(λn. ∑i<n. measure M (D i)) ⇢ measure M (⋃i. D i)" by (simp add: emeasure_eq_measure measure_nonneg sum_nonneg) have "(⋃i. D i) ∈ sets M" using ‹range D ⊆ sets M› by auto case 1 show ?case proof (rule approx_inner) fix e::real assume "e > 0" with measure_LIMSEQ have "∃no. ∀n≥no. ¦(∑i<n. measure M (D i)) -measure M (⋃x. D x)¦ < e/2" by (auto simp: lim_sequentially dist_real_def simp del: less_divide_eq_numeral1) hence "∃n0. ¦(∑i<n0. measure M (D i)) - measure M (⋃x. D x)¦ < e/2" by auto then obtain n0 where n0: "¦(∑i<n0. measure M (D i)) - measure M (⋃i. D i)¦ < e/2" unfolding choice_iff by blast have "ennreal (∑i<n0. measure M (D i)) = (∑i<n0. M (D i))" by (auto simp add: emeasure_eq_measure sum_nonneg measure_nonneg) also have "… ≤ (∑i. M (D i))" by (rule sum_le_suminf) auto also have "… = M (⋃i. D i)" by (simp add: M) also have "… = measure M (⋃i. D i)" by (simp add: emeasure_eq_measure) finally have n0: "measure M (⋃i. D i) - (∑i<n0. measure M (D i)) < e/2" using n0 by (auto simp: measure_nonneg sum_nonneg) have "∀i. ∃K. K ⊆ D i ∧ compact K ∧ emeasure M (D i) ≤ emeasure M K + e/(2*Suc n0)" proof fix i from ‹0 < e› have "0 < e/(2*Suc n0)" by simp have "emeasure M (D i) = (SUP K:{K. K ⊆ (D i) ∧ compact K}. emeasure M K)" using union by blast from SUP_approx_ennreal[OF ‹0 < e/(2*Suc n0)› _ this] show "∃K. K ⊆ D i ∧ compact K ∧ emeasure M (D i) ≤ emeasure M K + e/(2*Suc n0)" by (auto simp: emeasure_eq_measure intro: less_imp_le compact_empty) qed then obtain K where K: "⋀i. K i ⊆ D i" "⋀i. compact (K i)" "⋀i. emeasure M (D i) ≤ emeasure M (K i) + e/(2*Suc n0)" unfolding choice_iff by blast let ?K = "⋃i∈{..<n0}. K i" have "disjoint_family_on K {..<n0}" using K ‹disjoint_family D› unfolding disjoint_family_on_def by blast hence mK: "measure M ?K = (∑i<n0. measure M (K i))" using K by (intro finite_measure_finite_Union) (auto simp: sb compact_imp_closed) have "measure M (⋃i. D i) < (∑i<n0. measure M (D i)) + e/2" using n0 by simp also have "(∑i<n0. measure M (D i)) ≤ (∑i<n0. measure M (K i) + e/(2*Suc n0))" using K ‹0 < e› by (auto intro: sum_mono simp: emeasure_eq_measure simp flip: ennreal_plus) also have "… = (∑i<n0. measure M (K i)) + (∑i<n0. e/(2*Suc n0))" by (simp add: sum.distrib) also have "… ≤ (∑i<n0. measure M (K i)) + e / 2" using ‹0 < e› by (auto simp: field_simps intro!: mult_left_mono) finally have "measure M (⋃i. D i) < (∑i<n0. measure M (K i)) + e / 2 + e / 2" by auto hence "M (⋃i. D i) < M ?K + e" using ‹0<e› by (auto simp: mK emeasure_eq_measure sum_nonneg ennreal_less_iff simp flip: ennreal_plus) moreover have "?K ⊆ (⋃i. D i)" using K by auto moreover have "compact ?K" using K by auto ultimately have "?K⊆(⋃i. D i) ∧ compact ?K ∧ emeasure M (⋃i. D i) ≤ emeasure M ?K + ennreal e" by simp thus "∃K⊆⋃i. D i. compact K ∧ emeasure M (⋃i. D i) ≤ emeasure M K + ennreal e" .. qed fact case 2 show ?case proof (rule approx_outer[OF ‹(⋃i. D i) ∈ sets M›]) fix e::real assume "e > 0" have "∀i::nat. ∃U. D i ⊆ U ∧ open U ∧ e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" proof fix i::nat from ‹0 < e› have "0 < e/(2 powr Suc i)" by simp have "emeasure M (D i) = (INF U:{U. (D i) ⊆ U ∧ open U}. emeasure M U)" using union by blast from INF_approx_ennreal[OF ‹0 < e/(2 powr Suc i)› this] show "∃U. D i ⊆ U ∧ open U ∧ e/(2 powr Suc i) > emeasure M U - emeasure M (D i)" using ‹0<e› by (auto simp: emeasure_eq_measure sum_nonneg ennreal_less_iff ennreal_minus finite_measure_mono sb simp flip: ennreal_plus) qed then obtain U where U: "⋀i. D i ⊆ U i" "⋀i. open (U i)" "⋀i. e/(2 powr Suc i) > emeasure M (U i) - emeasure M (D i)" unfolding choice_iff by blast let ?U = "⋃i. U i" have "ennreal (measure M ?U - measure M (⋃i. D i)) = M ?U - M (⋃i. D i)" using U(1,2) by (subst ennreal_minus[symmetric]) (auto intro!: finite_measure_mono simp: sb measure_nonneg emeasure_eq_measure) also have "… = M (?U - (⋃i. D i))" using U ‹(⋃i. D i) ∈ sets M› by (subst emeasure_Diff) (auto simp: sb) also have "… ≤ M (⋃i. U i - D i)" using U ‹range D ⊆ sets M› by (intro emeasure_mono) (auto simp: sb intro!: sets.countable_nat_UN sets.Diff) also have "… ≤ (∑i. M (U i - D i))" using U ‹range D ⊆ sets M› by (intro emeasure_subadditive_countably) (auto intro!: sets.Diff simp: sb) also have "… ≤ (∑i. ennreal e/(2 powr Suc i))" using U ‹range D ⊆ sets M› using ‹0<e› by (intro suminf_le, subst emeasure_Diff) (auto simp: emeasure_Diff emeasure_eq_measure sb measure_nonneg ennreal_minus finite_measure_mono divide_ennreal ennreal_less_iff intro: less_imp_le) also have "… ≤ (∑n. ennreal (e * (1 / 2) ^ Suc n))" using ‹0<e› by (simp add: powr_minus powr_realpow field_simps divide_ennreal del: of_nat_Suc) also have "… = ennreal e * (∑n. ennreal ((1 / 2) ^ Suc n))" unfolding ennreal_power[symmetric] using ‹0 < e› by (simp add: ac_simps ennreal_mult' divide_ennreal[symmetric] divide_ennreal_def ennreal_power[symmetric]) also have "… = ennreal e" by (subst suminf_ennreal_eq[OF zero_le_power power_half_series]) auto finally have "emeasure M ?U ≤ emeasure M (⋃i. D i) + ennreal e" using ‹0<e› by (simp add: emeasure_eq_measure flip: ennreal_plus) moreover have "(⋃i. D i) ⊆ ?U" using U by auto moreover have "open ?U" using U by auto ultimately have "(⋃i. D i) ⊆ ?U ∧ open ?U ∧ emeasure M ?U ≤ emeasure M (⋃i. D i) + ennreal e" by simp thus "∃B. (⋃i. D i) ⊆ B ∧ open B ∧ emeasure M B ≤ emeasure M (⋃i. D i) + ennreal e" .. qed qed qed end