(* Title: HOL/Probability/Regularity.thy
Author: Fabian Immler, TU München
*)
section \Regularity of Measures\
theory Regularity
imports Measure_Space Borel_Space
begin
lemma ereal_approx_SUP:
fixes x::ereal
assumes A_notempty: "A \ {}"
assumes f_bound: "\i. i \ A \ f i \ x"
assumes f_fin: "\i. i \ A \ f i \ \"
assumes f_nonneg: "\i. 0 \ f i"
assumes approx: "\e. (e::real) > 0 \ \i \ A. x \ f i + e"
shows "x = (SUP i : A. f i)"
proof (subst eq_commute, rule SUP_eqI)
show "\i. i \ A \ f i \ x" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\i::'a. i \ A \ f i \ y)"
with A_notempty f_nonneg have "y \ 0" by auto (metis order_trans)
show "x \ y"
proof (rule ccontr)
assume "\ x \ y" hence "x > y" by simp
hence y_fin: "\y\ \ \" using \y \ 0\ by auto
have x_fin: "\x\ \ \" using \x > y\ f_fin approx[where e = 1] by auto
def e \ "real_of_ereal ((x - y) / 2)"
have e: "x > y + e" "e > 0" using \x > y\ y_fin x_fin by (auto simp: e_def field_simps)
note e(1)
also from approx[OF \e > 0\] obtain i where i: "i \ A" "x \ f i + e" by blast
note i(2)
finally have "y < f i" using y_fin f_fin by (metis add_right_mono linorder_not_le)
moreover have "f i \ y" by (rule f_le_y) fact
ultimately show False by simp
qed
qed
lemma ereal_approx_INF:
fixes x::ereal
assumes A_notempty: "A \ {}"
assumes f_bound: "\i. i \ A \ x \ f i"
assumes f_fin: "\i. i \ A \ f i \ \"
assumes f_nonneg: "\i. 0 \ f i"
assumes approx: "\e. (e::real) > 0 \ \i \ A. f i \ x + e"
shows "x = (INF i : A. f i)"
proof (subst eq_commute, rule INF_eqI)
show "\i. i \ A \ x \ f i" using f_bound by simp
next
fix y :: ereal assume f_le_y: "(\i::'a. i \ A \ y \ f i)"
with A_notempty f_fin have "y \ \" by force
show "y \ x"
proof (rule ccontr)
assume "\ y \ x" hence "y > x" by simp hence "y \ - \" by auto
hence y_fin: "\y\ \ \" using \y \ \\ by auto
have x_fin: "\x\ \ \" using \y > x\ f_fin f_nonneg approx[where e = 1] A_notempty
by auto
def e \ "real_of_ereal ((y - x) / 2)"
have e: "y > x + e" "e > 0" using \y > x\ y_fin x_fin by (auto simp: e_def field_simps)
from approx[OF \e > 0\] obtain i where i: "i \ A" "x + e \ f i" by blast
note i(2)
also note e(1)
finally have "y > f i" .
moreover have "y \ f i" by (rule f_le_y) fact
ultimately show False by simp
qed
qed
lemma INF_approx_ereal:
fixes x::ereal and e::real
assumes "e > 0"
assumes INF: "x = (INF i : A. f i)"
assumes "\x\ \ \"
shows "\i \ A. f i < x + e"
proof (rule ccontr, clarsimp)
assume "\i\A. \ f i < x + e"
moreover
from INF have "\y. (\i. i \ A \ y \ f i) \ y \ x" by (auto intro: INF_greatest)
ultimately
have "(INF i : A. f i) = x + e" using \e > 0\
by (intro INF_eqI)
(force, metis add.comm_neutral add_left_mono ereal_less(1)
linorder_not_le not_less_iff_gr_or_eq)
thus False using assms by auto
qed
lemma SUP_approx_ereal:
fixes x::ereal and e::real
assumes "e > 0"
assumes SUP: "x = (SUP i : A. f i)"
assumes "\x\ \ \"
shows "\i \ A. x \ f i + e"
proof (rule ccontr, clarsimp)
assume "\i\A. \ x \ f i + e"
moreover
from SUP have "\y. (\i. i \ A \ f i \ y) \ y \ x" by (auto intro: SUP_least)
ultimately
have "(SUP i : A. f i) = x - e" using \e > 0\ \\x\ \ \\
by (intro SUP_eqI)
(metis PInfty_neq_ereal(2) abs_ereal.simps(1) ereal_minus_le linorder_linear,
metis ereal_between(1) ereal_less(2) less_eq_ereal_def order_trans)
thus False using assms by auto
qed
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 + ereal e) \ ?inner A"
by (rule ereal_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 + ereal e) \ ?outer A"
by (rule ereal_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: closed_cball 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 simp
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:
"\e. e > 0 \
\K \ {K. K \ space M \ compact K}. emeasure M (space M) \ emeasure M K + ereal e"
(is "\e. _ \ ?thesis e")
proof -
fix e :: real assume "e > 0"
def B \ "\n. \i\{0..k e (Suc n)}. cball (from_nat_into X i) (1 / Suc n)"
have "\n. closed (B n)" by (auto simp: B_def closed_cball)
hence [simp]: "\n. B n \ sets M" by (simp add: sb)
from k[OF \e > 0\