Theory Regularity
section ‹Regularity of Measures›
theory Regularity
imports Measure_Space Borel_Space
begin
theorem
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 obtain X :: "'a set"
where X: "countable X" "⋀Y :: 'a set. open Y ⟹ Y ≠ {} ⟹ ∃d∈X. d ∈ Y"
by auto
{
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)
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: 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'"
then obtain n where n: "1 / real (Suc n) < e'" by (rule nat_approx_posE)
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"
then have pos: "infdist x A > 0" using infdist_nonneg[of x A] by simp
then obtain n where n: "1 / real (Suc n) < infdist x A" by (rule nat_approx_posE)
assume "∀i. infdist x A < 1 / real (Suc i)"
then have "infdist x A < 1 / real (Suc n)" by auto
with n 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 (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)"
apply (rule arg_cong [of _ _ Inf])
using sU
apply (auto simp add: image_iff)
apply (rule exI [of _ "UNIV - y" for y])
apply safe
apply (auto simp add: double_diff)
done
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 (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]
apply (rule arg_cong [of _ _ Sup])
using sU apply (auto intro!: imageI)
done
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 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)
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: 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 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 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