Theory General_Weak_Convergence
section ‹ General Weak Convergence ›
theory General_Weak_Convergence
imports Lemmas_Levy_Prokhorov
"Riesz_Representation.Regular_Measure"
begin
text ‹ We formalize the notion of weak convergence and equivalent conditions.
The formalization of weak convergence in HOL-Probability is restricted to
probability measures on real numbers.
Our formalization is generalized to finite measures on any metric spaces. ›
subsection ‹ Topology of Weak Convegence›
definition weak_conv_topology :: "'a topology ⇒ 'a measure topology" where
"weak_conv_topology X ≡
topology_generated_by
(⋃f∈{f. continuous_map X euclideanreal f ∧ (∃B. ∀x∈topspace X. ¦f x¦ ≤ B)}.
Collect (openin (pullback_topology {N. sets N = sets (borel_of X) ∧ finite_measure N}
(λN. ∫x. f x ∂N) euclideanreal)))"
lemma topspace_weak_conv_topology[simp]:
"topspace (weak_conv_topology X) = {N. sets N = sets (borel_of X) ∧ finite_measure N}"
unfolding weak_conv_topology_def openin_pullback_topology
by(auto intro!: exI[where x="λx. 1"] exI[where x=1]) blast
lemma openin_weak_conv_topology_base:
assumes f:"continuous_map X euclideanreal f" and B:"⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ B"
and U:"open U"
shows "openin (weak_conv_topology X) ((λN. ∫x. f x ∂N) -` U
∩ {N. sets N = sets (borel_of X) ∧ finite_measure N})"
using assms
by(fastforce simp: weak_conv_topology_def openin_topology_generated_by_iff openin_pullback_topology
intro!: Basis)
lemma continuous_map_weak_conv_topology:
assumes f:"continuous_map X euclideanreal f" and B:"⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ B"
shows "continuous_map (weak_conv_topology X) euclideanreal (λN. ∫x. f x ∂N)"
using openin_weak_conv_topology_base[OF assms]
by(auto simp: continuous_map_def Collect_conj_eq Int_commute Int_left_commute vimage_def)
lemma weak_conv_topology_minimal:
assumes "topspace Y = {N. sets N = sets (borel_of X) ∧ finite_measure N}"
and "⋀f B. continuous_map X euclideanreal f
⟹ (⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ B) ⟹ continuous_map Y euclideanreal (λN. ∫x. f x ∂N)"
shows "openin (weak_conv_topology X) U ⟹ openin Y U"
unfolding weak_conv_topology_def openin_topology_generated_by_iff
proof (induct rule: generate_topology_on.induct)
case h:(Basis s)
then obtain f B where f: "continuous_map X euclidean f" "⋀x. x∈topspace X ⟹ ¦f x¦ ≤ B"
"openin (pullback_topology {N. sets N = sets (borel_of X) ∧ finite_measure N} (λN. ∫x. f x ∂N) euclideanreal) s"
by blast
then obtain u where u:
"open u" "s = (λN. ∫x. f x ∂N) -`u ∩ {N. sets N = sets (borel_of X) ∧ finite_measure N}"
unfolding openin_pullback_topology by auto
with assms(2)[OF f(1,2)]
show ?case
using assms(1) continuous_map_open by fastforce
qed auto
lemma weak_conv_topology_continuous_map_integral:
assumes "continuous_map X euclideanreal f" "⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ B"
shows "continuous_map (weak_conv_topology X) euclideanreal (λN. ∫x. f x ∂N)"
unfolding continuous_map
proof safe
fix U
assume "openin euclideanreal U"
then show "openin (weak_conv_topology X) {N ∈ topspace (weak_conv_topology X). (∫x. f x ∂N) ∈ U}"
unfolding weak_conv_topology_def openin_topology_generated_by_iff using assms
by(auto intro!: Basis exI[where x=U] exI[where x=f] exI[where x=B] simp: openin_pullback_topology) blast
qed simp
subsection ‹Weak Convergence›
abbreviation weak_conv_on :: "('a ⇒ 'b measure) ⇒ 'b measure ⇒ 'a filter ⇒ 'b topology ⇒ bool"
( ‹'((_)/ ⇒⇩W⇩C (_)') (_)/ on (_)› [56, 55] 55) where
"weak_conv_on Ni N F X ≡ limitin (weak_conv_topology X) Ni N F"
abbreviation weak_conv_on_seq :: "(nat ⇒ 'b measure) ⇒ 'b measure ⇒ 'b topology ⇒ bool"
( ‹'((_)/ ⇒⇩W⇩C (_)') on (_)› [56, 55] 55) where
"weak_conv_on_seq Ni N X ≡ weak_conv_on Ni N sequentially X"
subsection ‹ Limit in Topology of Weak Convegence ›
lemma weak_conv_on_def:
"weak_conv_on Ni N F X ⟷
(∀⇩F i in F. sets (Ni i) = sets (borel_of X) ∧ finite_measure (Ni i)) ∧ sets N = sets (borel_of X)
∧ finite_measure N
∧ (∀f. continuous_map X euclideanreal f ⟶ (∃B. ∀x∈topspace X. ¦f x¦ ≤ B)
⟶ ((λi. ∫x. f x ∂Ni i) ⤏ (∫x. f x ∂N)) F)"
proof safe
assume h:"weak_conv_on Ni N F X"
then have 1:"sets N = sets (borel_of X)" "finite_measure N"
using limitin_topspace by fastforce+
then show "⋀x. x ∈ sets N ⟹ x ∈ sets (borel_of X)" "⋀x. x ∈ sets (borel_of X) ⟹ x ∈ sets N"
"finite_measure N"
by auto
show 2:"∀⇩F i in F. sets (Ni i) = sets (borel_of X) ∧ finite_measure (Ni i)"
using h by(cases "F = ⊥") (auto simp: limitin_def)
fix f B
assume f:"continuous_map X euclideanreal f" and B:"∀x∈topspace X. ¦f x¦ ≤ B"
show "((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F"
unfolding tendsto_iff
proof safe
fix r :: real
assume [arith]:"r > 0"
then have "openin
(weak_conv_topology X)
((λN. ∫x. f x ∂N) -` (ball (∫x. f x ∂N) r)
∩ {N. sets N = sets (borel_of X) ∧ finite_measure N})" (is "openin _ ?U")
using f B by(auto intro!: openin_weak_conv_topology_base)
moreover have "N ∈ ?U"
using h by (simp add: 1)
ultimately have NnU:"∀⇩F n in F. Ni n ∈ ?U"
using h limitinD by fastforce
show "∀⇩F n in F. dist (∫x. f x ∂Ni n) (∫x. f x ∂N) < r"
by(auto intro!: eventuallyI[THEN eventually_mp[OF _ NnU]] simp: dist_real_def)
qed
next
assume h: "∀⇩F i in F. sets (Ni i) = sets (borel_of X) ∧ finite_measure (Ni i)"
"sets N = sets (borel_of X)"
"finite_measure N"
"∀f. continuous_map X euclideanreal f ⟶ (∃B. ∀x∈topspace X. ¦f x¦ ≤ B)
⟶ ((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F"
show "(Ni ⇒⇩W⇩C N) F on X "
unfolding limitin_def
proof safe
show "N ∈ topspace (weak_conv_topology X)"
using h by auto
fix U
assume h':"openin (weak_conv_topology X) U" "N ∈ U"
show "∀⇩F x in F. Ni x ∈ U"
using h'[simplified weak_conv_topology_def openin_topology_generated_by_iff]
proof induction
case Empty
then show ?case
by simp
next
case (Int a b)
then show ?case
by (simp add: eventually_conj_iff)
next
case (UN K)
then show ?case
using UnionI eventually_mono by fastforce
next
case s:(Basis s)
then obtain f where f: "continuous_map X euclidean f" "∃B. ∀x∈topspace X. ¦f x¦ ≤ B"
"openin (pullback_topology {N. sets N = sets (borel_of X) ∧
finite_measure N} (λN. ∫x. f x ∂N) euclideanreal) s"
by blast
then obtain u where u:
"open u" "s = (λN. ∫x. f x ∂N) -`u ∩ {N. sets N = sets (borel_of X) ∧ finite_measure N}"
unfolding openin_pullback_topology by auto
have "(∫x. f x ∂N) ∈ u"
using u s by blast
moreover have "((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F"
using f h by blast
ultimately have 1:"∀⇩F n in F. (∫x. f x ∂(Ni n)) ∈ u"
by (simp add: tendsto_def u(1))
show ?case
by(auto intro!: eventuallyI[THEN eventually_mp[OF _ eventually_conj[OF 1 h(1)]]] simp: u(2))
qed
qed
qed
lemma weak_conv_on_def':
assumes "⋀i. sets (Ni i) = sets (borel_of X)" and "⋀i. finite_measure (Ni i)"
and "sets N = sets (borel_of X)" and "finite_measure N"
shows "weak_conv_on Ni N F X
⟷ (∀f. continuous_map X euclideanreal f ⟶ (∃B. ∀x∈topspace X. ¦f x¦ ≤ B)
⟶ ((λi. ∫x. f x ∂Ni i) ⤏ (∫x. f x ∂N)) F)"
using assms by(auto simp: weak_conv_on_def)
lemmas weak_conv_seq_def = weak_conv_on_def[where F=sequentially]
lemma weak_conv_on_const:
"(⋀i. Ni i = N) ⟹ sets N = sets (borel_of X)
⟹ finite_measure N ⟹ weak_conv_on Ni N F X"
by(auto simp: weak_conv_on_def)
lemmas weak_conv_on_seq_const = weak_conv_on_const[where F=sequentially]
context Metric_space
begin
abbreviation "mweak_conv ≡ (λNi N F. weak_conv_on Ni N F mtopology)"
abbreviation "mweak_conv_seq ≡ λNi N. mweak_conv Ni N sequentially"
lemmas mweak_conv_def = weak_conv_on_def[where X=mtopology,simplified]
lemmas mweak_conv_seq_def = weak_conv_seq_def[where X=mtopology,simplified]
end
subsection ‹The Portmanteau Theorem›
locale mweak_conv_fin = Metric_space +
fixes Ni :: "'b ⇒ 'a measure" and N :: "'a measure" and F
assumes sets_Ni:"∀⇩F i in F. sets (Ni i) = sets (borel_of mtopology)"
and sets_N[measurable_cong]: "sets N = sets (borel_of mtopology)"
and finite_measure_Ni: "∀⇩F i in F. finite_measure (Ni i)"
and finite_measure_N: "finite_measure N"
begin
interpretation N: finite_measure N
by(simp add: finite_measure_N)
lemma space_N: "space N = M"
using sets_eq_imp_space_eq[OF sets_N] by(auto simp: space_borel_of)
lemma space_Ni: "∀⇩F i in F. space (Ni i) = M"
by(rule eventually_mp[OF _ sets_Ni]) (auto simp: space_borel_of cong: sets_eq_imp_space_eq)
lemma eventually_Ni: "∀⇩F i in F. space (Ni i) = M ∧ sets (Ni i) = sets (borel_of mtopology) ∧ finite_measure (Ni i)"
by(intro eventually_conj space_Ni sets_Ni finite_measure_Ni)
lemma measure_converge_bounded':
assumes "((λn. measure (Ni n) M) ⤏ measure N M) F"
obtains K where "⋀A. ∀⇩F x in F. measure (Ni x) A ≤ K" "⋀A. measure N A ≤ K"
proof -
have "measure N A ≤ measure N M + 1" for A
using N.bounded_measure[of A] by(simp add: space_N)
moreover have "∀⇩F x in F. measure (Ni x) A ≤ measure N M + 1" for A
proof(rule eventuallyI[THEN eventually_mp[OF _ eventually_conj[OF eventually_Ni tendstoD[OF assms,of 1]]]])
fix x
show "(space (Ni x) = M ∧ sets (Ni x) = sets (borel_of mtopology) ∧ finite_measure (Ni x)) ∧
dist (measure (Ni x) M) (measure N M) < 1 ⟶ measure (Ni x) A ≤ measure N M + 1"
using finite_measure.bounded_measure[of "Ni x" A]
by(auto intro!: eventuallyI[THEN eventually_mp[OF _ tendstoD[OF assms,of 1]]] simp: dist_real_def)
qed simp
ultimately show ?thesis
using that by blast
qed
lemma
assumes "F ≠ ⊥" "∀⇩F x in F. measure (Ni x) A ≤ K" "measure N A ≤ K"
shows Liminf_measure_bounded: "Liminf F (λi. measure (Ni i) A) < ∞" "0 ≤ Liminf F (λi. measure (Ni i) A)"
and Limsup_measure_bounded: "Limsup F (λi. measure (Ni i) A) < ∞" "0 ≤ Limsup F (λi. measure (Ni i) A)"
proof -
have "Liminf F (λi. measure (Ni i) A) ≤ K" "Limsup F (λi. measure (Ni i) A) ≤ K"
using assms by(auto intro!: Liminf_le Limsup_bounded)
thus "Liminf F (λi. measure (Ni i) A) < ∞" "Limsup F (λi. measure (Ni i) A) < ∞"
by auto
show "0 ≤ Liminf F (λi. measure (Ni i) A)" "0 ≤ Limsup F (λi. measure (Ni i) A)"
by(auto intro!: le_Limsup Liminf_bounded assms)
qed
lemma mweak_conv1:
fixes f:: "'a ⇒ real"
assumes "mweak_conv Ni N F"
and "uniformly_continuous_map Self euclidean_metric f"
shows "(∃B. ∀x∈M. ¦f x¦ ≤ B) ⟹ ((λn. integral⇧L (Ni n) f) ⤏ integral⇧L N f) F"
using uniformly_continuous_imp_continuous_map[OF assms(2)] assms(1) by(auto simp: mweak_conv_def mtopology_of_def)
lemma mweak_conv2:
assumes "⋀f:: 'a ⇒ real. uniformly_continuous_map Self euclidean_metric f ⟹ (∃B. ∀x∈M. ¦f x¦ ≤ B)
⟹ ((λn. integral⇧L (Ni n) f) ⤏ integral⇧L N f) F"
and "closedin mtopology A"
shows "Limsup F (λx. ereal (measure (Ni x) A)) ≤ ereal (measure N A)"
proof -
consider "A = {}" | "F = ⊥" | "A ≠ {}" "F ≠ ⊥"
by blast
then show ?thesis
proof cases
assume "A = {}"
then show ?thesis
using Limsup_obtain linorder_not_less by fastforce
next
assume A_ne: "A ≠ {}" and F: "F ≠ ⊥"
have A[measurable]: "A ∈ sets N" "∀⇩F i in F. A ∈ sets (Ni i)"
using borel_of_closed[OF assms(2)] by(auto simp: sets_N eventually_mp[OF _ sets_Ni])
have "((λn. measure (Ni n) M) ⤏ measure N M) F"
proof -
have 1:"((λn. measure (Ni n) (space (Ni n))) ⤏ measure N M) F"
using assms(1)[of "λx. 1"] by(auto simp: space_N)
show ?thesis
by(rule tendsto_cong[THEN iffD1,OF eventually_mp[OF _ space_Ni] 1]) simp
qed
then obtain K where K: "⋀A. ∀⇩F x in F. measure (Ni x) A ≤ K" "⋀A. measure N A ≤ K"
using measure_converge_bounded' by auto
define Um where "Um ≡ (λm. ⋃a∈A. mball a (1 / Suc m))"
have Um_open: "openin mtopology (Um m)" for m
by(auto simp: Um_def)
hence Um_m[measurable]: "⋀m. Um m ∈ sets N" "⋀m. ∀⇩F i in F. Um m ∈ sets (Ni i)"
by(auto simp: sets_N intro!: borel_of_open eventually_mono[OF sets_Ni])
have A_Um: "A ⊆ Um m" for m
using closedin_subset[OF assms(2)] by(fastforce simp: Um_def)
have "∃fm:: _ ⇒ real. (∀x. fm x ≥ 0) ∧ (∀x. fm x ≤ 1) ∧ (∀x∈M - Um m. fm x = 0) ∧ (∀x∈A. fm x = 1) ∧
uniformly_continuous_map Self euclidean_metric fm" for m
proof -
have 1: "closedin mtopology (M - Um m)"
using Um_open[of m] by(auto simp: closedin_def Diff_Diff_Int Int_absorb1)
have 2: "A ∩ (M - Um m) = {}"
using A_Um[of m] by blast
have 3: "1 / Suc m ≤ d x y" if "x ∈ A" "y ∈ M - Um m" for x y
proof(rule ccontr)
assume "¬ 1 / real (Suc m) ≤ d x y"
then have "d x y < 1 / (1 + real m)" by simp
thus False
using that closedin_subset[OF assms(2)] by(auto simp: Um_def)
qed
show ?thesis
by (metis Urysohn_lemma_uniform[of Self,simplified mtopology_of_def,simplified,OF assms(2) 1 2 3,simplified] Diff_iff)
qed
then obtain fm :: "nat ⇒ _ ⇒ real" where fm: "⋀m x. fm m x ≥ 0" "⋀m x. fm m x ≤ 1"
"⋀m x. x ∈ A ⟹ fm m x = 1" "⋀m x. x ∈ M ⟹ x ∉ Um m ⟹ fm m x = 0"
"⋀m. uniformly_continuous_map Self euclidean_metric (fm m)"
by (metis Diff_iff)
have fm_m[measurable]: "⋀m. ∀⇩F i in F. fm m ∈ borel_measurable (Ni i)" "⋀m. fm m ∈ borel_measurable N"
using continuous_map_measurable[OF uniformly_continuous_imp_continuous_map[OF fm(5)]]
by(auto simp: borel_of_euclidean mtopology_of_def eventually_mono[OF sets_Ni])
have int_bounded:"∀⇩F n in F. (∫x. fm m x ∂Ni n) ≤ K" for m
proof(rule eventually_mono)
show "∀⇩F n in F. space (Ni n) = M ∧ finite_measure (Ni n) ∧ fm m ∈ borel_measurable (Ni n) ∧
(∫x. fm m x ∂Ni n) ≤ (∫x. 1 ∂Ni n) ∧ (∫x. 1 ∂Ni n) ≤ K"
proof(intro eventually_conj)
show "∀⇩F n in F. (∫x. fm m x ∂Ni n) ≤ (∫x. 1 ∂Ni n)"
proof(rule eventually_mono)
show "∀⇩F n in F. space (Ni n) = M ∧ finite_measure (Ni n) ∧ fm m ∈ borel_measurable (Ni n)"
by(intro eventually_conj space_Ni finite_measure_Ni fm_m)
show "space (Ni n) = M ∧ finite_measure (Ni n) ∧ fm m ∈ borel_measurable (Ni n)
⟹ (∫x. fm m x ∂Ni n) ≤ (∫x. 1 ∂Ni n)" for n
by(rule integral_mono, insert fm) (auto intro!: finite_measure.integrable_const_bound[where B=1])
qed
show "∀⇩F n in F. (∫x. 1 ∂Ni n) ≤ K"
by(rule eventually_mono[OF eventually_conj[OF K(1)[of M] space_Ni]]) simp
qed(auto simp: space_Ni finite_measure_Ni fm_m)
qed simp
have 1: "Limsup F (λn. measure (Ni n) A) ≤ measure N (Um m)" for m
proof -
have "Limsup F (λn. measure (Ni n) A) = Limsup F (λn. ∫x. indicat_real A x ∂Ni n)"
by(intro Limsup_eq[OF eventually_mono[OF A(2)]]) simp
also have "... ≤ Limsup F (λn. ∫x. fm m x ∂Ni n)"
proof(safe intro!: eventuallyI[THEN Limsup_mono[OF eventually_mp[OF _ eventually_conj[OF fm_m(1)[of m]
eventually_conj[OF finite_measure_Ni eventually_conj[OF A(2) int_bounded[of m]]]]]]])
fix n
assume h:"(∫x. fm m x ∂Ni n) ≤ K" "A ∈ sets (Ni n)" "finite_measure (Ni n)" "fm m ∈ borel_measurable (Ni n)"
with fm show "ereal (∫x. indicat_real A x ∂Ni n) ≤ ereal (∫x. fm m x ∂Ni n)"
by(auto intro!: Limsup_mono integral_mono finite_measure.integrable_const_bound[where B=1]
simp del: Bochner_Integration.integral_indicator) (auto simp: indicator_def)
qed
also have "... = (∫x. fm m x ∂N)"
using fm by(auto intro!: lim_imp_Limsup[OF F tendsto_ereal[OF assms(1)[OF fm(5)[of m]]]] exI[where x=1])
also have "... ≤ (∫x. indicat_real (Um m) x ∂N)"
unfolding ereal_less_eq(3) by(rule integral_mono, insert fm(4)[of _ m] fm(1,2))
(auto intro!: N.integrable_const_bound[where B=1],auto simp: indicator_def space_N)
also have "... = measure N (Um m)"
by simp
finally show ?thesis .
qed
have 2: "(λn. measure N (Um n)) ⇢ measure N A"
proof -
have [simp]: "(⋂ (range Um)) = A"
unfolding Um_def
by(rule nbh_Inter_closure_of[OF A_ne _ _ _ LIMSEQ_Suc,simplified closure_of_closedin[OF assms(2)]],
insert sets.sets_into_space[OF A(1)])
(auto intro!: decseq_SucI simp: frac_le space_N lim_1_over_n)
have [simp]: "monotone (≤) (λx y. y ⊆ x) Um"
unfolding Um_def by(rule nbh_decseq) (auto intro!: decseq_SucI simp: frac_le)
have "(λn. measure N (Um n)) ⇢ measure N (⋂ (range Um))"
by(rule N.finite_Lim_measure_decseq) auto
thus ?thesis by simp
qed
show ?thesis
using 1 by(auto intro!: Lim_bounded2[OF tendsto_ereal[OF 2]])
qed simp
qed
lemma mweak_conv3:
assumes "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "((λn. measure (Ni n) M) ⤏ measure N M) F"
and "openin mtopology U"
shows "measure N U ≤ Liminf F (λn. measure (Ni n) U)"
proof(cases "F = ⊥")
assume F: "F ≠ ⊥"
obtain K where K: "⋀A. ∀⇩F x in F. measure (Ni x) A ≤ K" "⋀A. measure N M ≤ K"
using measure_converge_bounded'[OF assms(2)] by metis
have U[measurable]: "U ∈ sets N" "∀⇩F i in F. U ∈ sets (Ni i)"
by(auto simp: sets_N borel_of_open assms eventually_mono[OF sets_Ni])
have "ereal (measure N U) = measure N M - measure N (M - U)"
by(simp add: N.finite_measure_compl[simplified space_N])
also have "... ≤ measure N M - Limsup F (λn. measure (Ni n) (M - U))"
using assms(1)[OF openin_closedin[THEN iffD1,OF _ assms(3)]] openin_subset[OF assms(3)]
by (metis ereal_le_real ereal_minus(1) ereal_minus_mono topspace_mtopology)
also have "... = measure N M + Liminf F (λn. - ereal (measure (Ni n) (M - U)))"
by (metis ereal_Liminf_uminus minus_ereal_def)
also have "... = Liminf F (λn. measure (Ni n) M) + Liminf F (λn. - measure (Ni n) (M - U))"
using tendsto_iff_Liminf_eq_Limsup[OF F,THEN iffD1,OF tendsto_ereal[OF assms(2)]] by simp
also have "... ≤ Liminf F (λn. ereal (measure (Ni n) M) + ereal (- measure (Ni n) (M - U)))"
by(rule ereal_Liminf_add_mono) (use Liminf_measure_bounded[OF F K] in auto)
also have "... = Liminf F (λn. measure (Ni n) U)"
by(auto intro!: Liminf_eq eventually_mono[OF eventually_conj[OF U(2) eventually_conj[OF space_Ni finite_measure_Ni]]]
simp: finite_measure.finite_measure_compl)
finally show ?thesis .
qed simp
lemma mweak_conv3':
assumes "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
and "((λn. measure (Ni n) M) ⤏ measure N M) F"
and "closedin mtopology A"
shows "Limsup F (λn. measure (Ni n) A) ≤ measure N A"
proof(cases "F = ⊥")
assume F: "F ≠ ⊥"
have A[measurable]: "A ∈ sets N""∀⇩F i in F. A ∈ sets (Ni i)"
by(auto simp: sets_N borel_of_closed assms eventually_mono[OF sets_Ni])
have "Limsup F (λn. measure (Ni n) A) = Limsup F (λn. ereal (measure (Ni n) M) + ereal (- measure (Ni n) (M - A)))"
by(auto intro!: Limsup_eq eventually_mono[OF eventually_conj[OF A(2) eventually_conj[OF space_Ni finite_measure_Ni]]]
simp: finite_measure.finite_measure_compl)
also have "... ≤ Limsup F (λn. measure (Ni n) M) + Limsup F (λn. - measure (Ni n) (M - A))"
by(rule ereal_Limsup_add_mono)
also have "... = Limsup F (λn. measure (Ni n) M) + Limsup F (λn. - ereal ( measure (Ni n) (M - A)))"
by simp
also have "... = Limsup F (λn. measure (Ni n) M) - Liminf F (λn. measure (Ni n) (M - A))"
unfolding ereal_Limsup_uminus using minus_ereal_def by presburger
also have "... = measure N M - Liminf F (λn. measure (Ni n) (M - A))"
by(simp add: lim_imp_Limsup[OF F tendsto_ereal[OF assms(2)]])
also have "... ≤ measure N M - measure N (M - A)"
using assms(1)[OF openin_diff[OF openin_topspace assms(3)]] closedin_subset[OF assms(3)]
by (metis assms(1,3) ereal_le_real ereal_minus(1) ereal_minus_mono open_in_mspace openin_diff)
also have "... = measure N A"
by(simp add: N.finite_measure_compl[simplified space_N])
finally show ?thesis .
qed simp
lemma mweak_conv4:
assumes "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
and [measurable]: "A ∈ sets (borel_of mtopology)"
and "measure N (mtopology frontier_of A) = 0"
shows "((λn. measure (Ni n) A) ⤏ measure N A) F"
proof(cases "F = ⊥")
assume F: "F ≠ ⊥"
have [measurable]: "A ∈ sets N" "mtopology closure_of A ∈ sets N" "mtopology interior_of A ∈ sets N"
"mtopology frontier_of A ∈ sets N"
and A: "∀⇩F i in F. A ∈ sets (Ni i)" "∀⇩F i in F. mtopology closure_of A ∈ sets (Ni i)"
"∀⇩F i in F. mtopology interior_of A ∈ sets (Ni i)" "∀⇩F i in F. mtopology frontier_of A ∈ sets (Ni i)"
by(auto simp: sets_N borel_of_open borel_of_closed closedin_frontier_of eventually_mono[OF sets_Ni])
have "Limsup F (λn. measure (Ni n) A) ≤ Limsup F (λn. measure (Ni n) (mtopology closure_of A))"
using sets.sets_into_space[OF assms(3)]
by(fastforce intro!: Limsup_mono finite_measure.finite_measure_mono[OF _ closure_of_subset]
eventually_mono[OF eventually_conj[OF finite_measure_Ni A(2)]] simp: space_borel_of)
also have "... ≤ measure N (mtopology closure_of A)"
by(auto intro!: assms(1))
also have "... ≤ measure N (A ∪ (mtopology frontier_of A))"
using closure_of_subset[of A mtopology] sets.sets_into_space[OF assms(3)] interior_of_subset[of mtopology A]
by(auto simp: space_borel_of interior_of_union_frontier_of[symmetric]
simp del: interior_of_union_frontier_of intro!: N.finite_measure_mono)
also have "... ≤ measure N A + measure N (mtopology frontier_of A)"
by(simp add: N.finite_measure_subadditive)
also have "... = measure N A" by(simp add: assms)
finally have 1: "Limsup F (λn. measure (Ni n) A) ≤ measure N A" .
have "ereal (measure N A) = measure N A - measure N (mtopology frontier_of A)"
by(simp add: assms)
also have "... ≤ measure N (A - mtopology frontier_of A)"
by(auto simp: N.finite_measure_Diff' intro!: N.finite_measure_mono)
also have "... ≤ measure N (mtopology interior_of A)"
using closure_of_subset[OF sets.sets_into_space[OF assms(3),simplified space_borel_of]]
by(auto intro!: N.finite_measure_mono simp: frontier_of_def)
also have "... ≤ Liminf F (λn. measure (Ni n) (mtopology interior_of A))"
by(auto intro!: assms)
also have "... ≤ Liminf F (λn. measure (Ni n) A)"
by(fastforce intro!: Liminf_mono finite_measure.finite_measure_mono interior_of_subset
eventually_mono[OF eventually_conj[OF finite_measure_Ni A(1)]])
finally have 2: "measure N A ≤ Liminf F (λn. measure (Ni n) A)" .
have "Liminf F (λn. measure (Ni n) A) = measure N A ∧ Limsup F (λn. measure (Ni n) A) = measure N A"
using 1 2 order.trans[OF 2 Liminf_le_Limsup[OF F]] order.trans[OF Liminf_le_Limsup[OF F] 1] antisym
by blast
thus ?thesis
by (metis F lim_ereal tendsto_Limsup)
qed simp
lemma mweak_conv5:
assumes "⋀A. A ∈ sets (borel_of mtopology) ⟹ measure N (mtopology frontier_of A) = 0
⟹ ((λn. measure (Ni n) A) ⤏ measure N A) F"
shows "mweak_conv Ni N F"
proof(cases "F = ⊥")
assume F: "F ≠ ⊥"
show ?thesis
unfolding mweak_conv_def
proof safe
fix f B
assume h:"continuous_map mtopology euclideanreal f" "∀x∈M. ¦f x¦ ≤ B"
have "((λn. measure (Ni n) M) ⤏ measure N M) F"
using frontier_of_topspace[of mtopology] by(auto intro!: assms borel_of_open)
then obtain K where K: "⋀A. ∀⇩F x in F. measure (Ni x) A ≤ K" "⋀A. measure N A ≤ K"
using measure_converge_bounded' by metis
from continuous_map_measurable[OF h(1)]
have f[measurable]:"f ∈ borel_measurable N" "∀⇩F i in F. f ∈ borel_measurable (Ni i)"
by(auto cong: measurable_cong_sets simp: sets_N borel_of_euclidean intro!: eventually_mono[OF sets_Ni])
have f_int[simp]: "integrable N f" "∀⇩F i in F. integrable (Ni i) f"
using h by(auto intro!: N.integrable_const_bound[where B=B] finite_measure.integrable_const_bound[where B=B]
eventually_mono[OF eventually_conj[OF eventually_conj[OF space_Ni f(2)] finite_measure_Ni]] simp: space_N)
show "((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F"
proof(cases "B > 0")
case False
with h(2) have 1:"⋀x. x ∈ space N ⟹ f x = 0" "∀⇩F i in F. ∀x. x ∈ space (Ni i) ⟶ f x = 0"
by (fastforce simp: space_N intro!: eventually_mono[OF space_Ni])+
thus ?thesis
by(auto cong: Bochner_Integration.integral_cong
intro!: tendsto_cong[where g="λx. 0" and f="(λn. ∫x. f x ∂Ni n)",THEN iffD2] eventually_mono[OF 1(2)])
next
case B[arith]:True
show ?thesis
proof(cases "K > 0")
case False
then have 1:"measure N A = 0" "∀⇩F x in F. measure (Ni x) M = 0" for A
using K(2)[of A] measure_nonneg[of _ A] measure_le_0_iff
by(fastforce intro!: eventuallyI[THEN eventually_mp[OF _ K(1)[of M]]])+
hence "N = null_measure (borel_of mtopology)"
by(auto intro!: measure_eqI simp: sets_N N.emeasure_eq_measure)
moreover have "∀⇩F x in F. Ni x = null_measure (borel_of mtopology)"
using order.trans[where c=0,OF finite_measure.bounded_measure]
by(intro eventually_mono[OF eventually_conj[OF eventually_conj[OF space_Ni eventually_conj[OF finite_measure_Ni sets_Ni]] 1(2)]] measure_eqI)
(auto simp: finite_measure.emeasure_eq_measure measure_le_0_iff)
ultimately show ?thesis
by (simp add: eventually_mono tendsto_eventually)
next
case [arith]:True
show ?thesis
unfolding tendsto_iff LIMSEQ_def dist_real_def
proof safe
fix r :: real
assume r[arith]: "r > 0"
define ν where "ν ≡ distr N borel f"
have sets_nu[measurable_cong, simp]: "sets ν = sets borel"
by(simp add: ν_def)
interpret ν: finite_measure ν
by(auto simp: ν_def N.finite_measure_distr)
have "(1 / 6) * (r / K) * (1 / B) > 0"
by auto
from nat_approx_posE[OF this]
obtain N' where N': "1 / (Suc N') < (1 / 6) * (r / K) * (1 / B)"
by auto
from mult_strict_right_mono[OF this B] have N'':"B / (Suc N') < (1 / 6) * (r / K)"
by auto
have "∃tn ∈ {B / Suc N' * (real n - 1) - B<..<B / Suc N' * real n - B}. measure ν {tn} = 0" for n
proof(rule ccontr)
assume "¬ (∃tn ∈ {B / Suc N' * (real n - 1) - B<..<B / Suc N' * real n - B}. measure ν {tn} = 0)"
then have "{B / Suc N' * (real n - 1) - B<..<B / Suc N' * real n - B} ⊆ {x. measure ν {x} ≠ 0}"
by auto
moreover have "uncountable {B / Suc N' * (real n - 1) - B<..<B / Suc N' * real n - B}"
unfolding uncountable_open_interval right_diff_distrib by auto
ultimately show False
using ν.countable_support by(meson countable_subset)
qed
then obtain tn where tn: "⋀n. B / Suc N' * (real n - 1) - B < tn n" "⋀n. tn n < B / Suc N' * real n - B"
"⋀n. measure ν {tn n} = 0"
by (metis greaterThanLessThan_iff)
have t0: "tn 0 < - B"
using tn(2)[of 0] by simp
have tN: "B < tn (Suc (2 * (Suc N')))"
proof -
have "B * (2 + 2 * real N') / (1 + real N') = 2 * B"
by(auto simp: divide_eq_eq)
with tn(1)[of "Suc (2 * (Suc N'))"] show ?thesis
by simp
qed
define Aj where "Aj ≡ (λj. f -` {tn j..<tn (Suc j)} ∩ M)"
have sets_Aj[measurable]: "⋀j. Aj j ∈ sets N" "∀⇩F i in F. ∀j. Aj j ∈ sets (Ni i)"
using measurable_sets[OF f(1)]
by(auto simp: Aj_def space_N intro!: eventually_mono[OF eventually_conj[OF space_Ni f(2)]])
have m_f: "measure N (mtopology frontier_of (Aj j)) = 0" for j
proof -
have "measure N (mtopology frontier_of (Aj j)) = measure N (mtopology closure_of (Aj j) - mtopology interior_of (Aj j))"
by(simp add: frontier_of_def)
also have "... ≤ measure ν {tn j, tn (Suc j)}"
proof -
have [simp]: "{x ∈ M. tn j ≤ f x ∧ f x ≤ tn (Suc j)} = f -` {tn j..tn (Suc j)} ∩ M"
"{x ∈ M. tn j < f x ∧ f x < tn (Suc j)} = f -` {tn j<..<tn (Suc j)} ∩ M"
by auto
have "mtopology closure_of (Aj j) ⊆ f -` {tn j..tn (Suc j)} ∩ M"
by(rule closure_of_minimal,insert closedin_continuous_map_preimage[OF h(1),of "{tn j..tn (Suc j)}"])
(auto simp: Aj_def)
moreover have "f -` {tn j<..<tn (Suc j)} ∩ M ⊆ mtopology interior_of (Aj j)"
by(rule interior_of_maximal,insert openin_continuous_map_preimage[OF h(1),of "{tn j<..<tn (Suc j)}"])
(auto simp: Aj_def)
ultimately have "mtopology closure_of (Aj j) - mtopology interior_of (Aj j) ⊆ f -` {tn j,tn (Suc j)} ∩ M"
by(fastforce dest: contra_subsetD)
with closedin_subset[OF closedin_closure_of,of mtopology "Aj j"] show ?thesis
by(auto simp: ν_def measure_distr intro!: N.finite_measure_mono) (auto simp: space_N)
qed
also have "... ≤ measure ν {tn j} + measure ν {tn (Suc j)}"
using ν.finite_measure_subadditive[of "{tn (Suc j)}" "{tn j}"] by auto
also have "... = 0"
by(simp add: tn)
finally show ?thesis
by (simp add: measure_le_0_iff)
qed
hence conv:"((λn. measure (Ni n) (Aj j)) ⤏ measure N (Aj j)) F" for j
by(auto intro!: assms simp: sets_N[symmetric] sets_Ni)
have fil1:"∀⇩F n in F. ¦tn j¦ * ¦measure (Ni n) (Aj j) - measure N (Aj j)¦ < r / (3 * (Suc (Suc (2 * Suc N'))))" for j
proof(cases "¦tn j¦ = 0")
case pos:False
then have "r / (3 * (Suc (Suc (2 * Suc N')))) * (1 / ¦tn j¦) > 0"
by auto
with conv[of j]
have 1:"∀⇩F n in F. ¦measure (Ni n) (Aj j) - measure N (Aj j)¦
< r / (3 * (Suc (Suc (2 * Suc N')))) * (1 / ¦tn j¦)"
unfolding tendsto_iff dist_real_def by metis
have "∀⇩F n in F. ¦tn j¦ * ¦measure (Ni n) (Aj j) - measure N (Aj j)¦ < r / (3 * (Suc (Suc (2 * Suc N'))))"
proof(rule eventuallyI[THEN eventually_mp[OF _ 1]])
show "¦measure (Ni n) (Aj j) - measure N (Aj j)¦ < r / real (3 * Suc (Suc (2 * Suc N'))) * (1 / ¦tn j¦)
⟶ ¦tn j¦ * ¦measure (Ni n) (Aj j) - measure N (Aj j)¦ < r / real (3 * Suc (Suc (2 * Suc N')))" for n
using mult_less_cancel_right_pos[of "¦tn j¦" "¦measure (Ni n) (Aj j) - measure N (Aj j)¦"
"r / real (3 * Suc (Suc (2 * Suc N'))) * (1 / ¦tn j¦)"] pos by(simp add: mult.commute)
qed
thus ?thesis by auto
qed auto
hence fil1:"∀⇩F n in F. ∀j∈{..Suc (2 * Suc N')}. ¦tn j¦ * ¦measure (Ni n) (Aj j) - measure N (Aj j)¦
< r / (3 * (Suc (Suc (2 * Suc N'))))"
by(auto intro!: eventually_ball_finite)
have tn_strictmono: "strict_mono tn"
unfolding strict_mono_Suc_iff
proof safe
fix n
show "tn n < tn (Suc n)"
using tn(1)[of "Suc n"] tn(2)[of n] by auto
qed
from strict_mono_less[OF this] have Aj_disj: "disjoint_family Aj"
by(auto simp: disjoint_family_on_def Aj_def) (metis linorder_not_le not_less_eq order_less_le order_less_trans)
have Aj_un: "M = (⋃i∈{..Suc (2 * Suc N')}. Aj i)"
proof
show "M ⊆ ⋃ (Aj ` {..Suc (2 * Suc N')})"
proof
fix x
assume x:"x ∈ M"
with h(2) tN t0 have h':"tn 0 < f x" "f x < tn (Suc (2 * Suc N'))"
by fastforce+
define n where "n ≡ LEAST n. f x < tn (Suc n)"
have "f x < tn (Suc n)"
unfolding n_def by(rule LeastI_ex) (use h' in auto)
moreover have "tn n ≤ f x"
by (metis Least_le Suc_n_not_le_n h'(1) less_eq_real_def linorder_not_less n_def not0_implies_Suc)
moreover have "n ≤ 2 * Suc N'"
unfolding n_def by(rule Least_le) (use h' in auto)
ultimately show "x ∈ ⋃ (Aj ` {..Suc (2 * Suc N')})"
by(auto simp: Aj_def x)
qed
qed(auto simp: Aj_def)
define h where "h ≡ (λx. ∑i≤Suc (2 * (Suc N')). tn i * indicat_real (Aj i) x)"
have h[measurable]: "h ∈ borel_measurable N" "∀⇩F i in F. h ∈ borel_measurable (Ni i)"
by(auto simp: h_def simp del: sum.atMost_Suc sum_mult_indicator intro!: borel_measurable_sum eventually_mono[OF sets_Aj(2)])
have h_f: "h x ≤ f x" if "x ∈ M" for x
proof -
from that disjoint_family_onD[OF Aj_disj]
obtain n where n: "x ∈ Aj n" "n ≤ Suc (2 * Suc N')" "⋀m. m ≠ n ⟹ x ∉ Aj m"
by(auto simp: Aj_un)
have "h x = (∑i≤Suc (2 * (Suc N')). if i = n then tn i else 0)"
unfolding h_def by(rule Finite_Cartesian_Product.sum_cong_aux) (use n in auto)
also have "... = tn n"
using n by auto
also have "... ≤ f x"
using n(1) by(auto simp: Aj_def)
finally show ?thesis .
qed
have f_h: "f x < h x + (1 / 3) * (r / enn2real K)" if "x ∈ M" for x
proof -
from that disjoint_family_onD[OF Aj_disj]
obtain n where n: "x ∈ Aj n" "n ≤ Suc (2 * Suc N')" "⋀m. m ≠ n ⟹ x ∉ Aj m"
by(auto simp: Aj_un)
have "h x = (∑i≤Suc (2 * (Suc N')). if i = n then tn i else 0)"
unfolding h_def by(rule Finite_Cartesian_Product.sum_cong_aux) (use n in auto)
also have "... = tn n"
using n by auto
finally have hx: "h x = tn n" .
have "f x < tn (Suc n)"
using n by(auto simp: Aj_def)
hence "f x - tn n < tn (Suc n) - tn n" by auto
also have "... < B / real (Suc N') * real (Suc n) - (B / real (Suc N') * (real n - 1))"
using tn(1)[of n] tn(2)[of "Suc n"] by auto
also have "... = 2 * B / real (Suc N')"
by(auto simp: diff_divide_distrib[symmetric]) (simp add: ring_distribs(1) right_diff_distrib)
also have "... < (1 / 3) * (r / enn2real K)"
using N'' by auto
finally show ?thesis
using hx by simp
qed
with h_f have fh:"⋀x. x ∈ M ⟹ ¦f x - h x¦ < (1 / 3) * (r / enn2real K)"
by fastforce
have h_bounded: "¦h x¦ ≤ (∑i≤Suc (2 * (Suc N')). ¦tn i¦)" for x
unfolding h_def by(rule order.trans[OF sum_abs[of "λi. tn i * indicat_real (Aj i) x"
"{..Suc (2 * (Suc N'))}"] sum_mono]) (auto simp: indicator_def)
hence h_int[simp]: "integrable N h" "∀⇩F i in F. integrable (Ni i) h"
by(auto intro!: N.integrable_const_bound[where B="∑i≤Suc (2 * (Suc N')). ¦tn i¦"]
finite_measure.integrable_const_bound[where B="∑i≤Suc (2 * (Suc N')). ¦tn i¦"]
eventually_mono[OF eventually_conj[OF finite_measure_Ni h(2)]])
show "∀⇩F n in F. ¦(∫x. f x ∂Ni n) - (∫x. f x ∂N)¦ < r"
proof(safe intro!: eventually_mono[OF eventually_conj[OF K(1)[of M]
eventually_conj[OF eventually_conj[OF fil1 h_int(2)]
eventually_conj[OF f_int(2)
eventually_conj[OF eventually_conj[OF finite_measure_Ni space_Ni]
sets_Aj(2)]]]]])
fix n
assume n:"∀j∈{..Suc (2 * Suc N')}.
¦tn j¦ * ¦measure (Ni n) (Aj j) - measure N (Aj j)¦ < r / real (3 * Suc (Suc (2 * Suc N')))"
"measure (Ni n) (space (Ni n)) ≤ K"
and h_intn[simp]:"integrable (Ni n) h" and f_intn[simp]:"integrable (Ni n) f"
and sets_Aj2[measurable]:"∀j. Aj j ∈ sets (Ni n)"
and space_Ni:"M = space (Ni n)"
and "finite_measure (Ni n)"
interpret Ni: finite_measure "(Ni n)" by fact
have "¦(∫x. f x ∂Ni n) - (∫x. f x ∂N)¦
= ¦(∫x. f x - h x ∂Ni n) + ((∫x. h x ∂Ni n) - (∫x. h x ∂N)) - (∫x. f x - h x ∂N)¦"
by(simp add: Bochner_Integration.integral_diff[OF f_int(1) h_int(1)] Bochner_Integration.integral_diff[OF f_intn h_intn])
also have "... ≤ ¦∫x. f x - h x ∂Ni n¦ + ¦(∫x. h x ∂Ni n) - (∫x. h x ∂N)¦ + ¦∫x. f x - h x ∂N¦"
by linarith
also have "... ≤ (∫x. ¦f x - h x¦ ∂Ni n) + ¦(∫x. h x ∂Ni n) - (∫x. h x ∂N)¦ + (∫x. ¦f x - h x¦ ∂N)"
using integral_abs_bound by (simp add: add_mono del: f_int f_intn)
also have "... ≤ r / 3 + ¦(∫x. h x ∂Ni n) - (∫x. h x ∂N)¦ + r / 3"
proof -
have "(∫x. ¦f x - h x¦ ∂Ni n) ≤ (∫x. (1 / 3) * (r / enn2real K) ∂Ni n)"
by(rule integral_mono) (insert fh, auto simp: space_Ni order.strict_implies_order)
also have "... = measure (Ni n) (space (Ni n)) / K * (r / 3)"
by auto
also have "... ≤ r / 3"
by(rule mult_left_le_one_le) (use n space_Ni in auto)
finally have 1:"(∫x. ¦f x - h x¦ ∂Ni n) ≤ r / 3" .
have "(∫x. ¦f x - h x¦ ∂N) ≤ (∫x. (1 / 3) * (r / K) ∂N)"
by(rule integral_mono) (insert fh, auto simp: space_N order.strict_implies_order)
also have "... = measure N (space N) / enn2real K * (r / 3)"
by auto
also have "... ≤ r / 3"
by(rule mult_left_le_one_le) (use K space_N in auto)
finally show ?thesis
using 1 by auto
qed
also have "... < r"
proof -
have "¦(∫x. h x ∂Ni n) - (∫x. h x ∂N)¦
= ¦(∫x. (∑i≤Suc (2 * (Suc N')). tn i * indicat_real (Aj i) x) ∂Ni n)
- (∫x. (∑i≤Suc (2 * (Suc N')). tn i * indicat_real (Aj i) x) ∂N)¦"
by(simp add: h_def)
also have "... = ¦(∑i≤Suc (2 * (Suc N')). (∫x. tn i * indicat_real (Aj i) x ∂Ni n))
- (∑i≤Suc (2 * (Suc N')). (∫x. tn i * indicat_real (Aj i) x ∂N))¦"
proof -
have 1: "(∫x. (∑i≤Suc (2 * (Suc N')). tn i * indicat_real (Aj i) x) ∂Ni n)
= (∑i≤Suc (2 * (Suc N')). (∫x. tn i * indicat_real (Aj i) x ∂Ni n))"
by(rule Bochner_Integration.integral_sum) (use integrable_real_mult_indicator sets_Aj2 in blast)
have 2: "(∫x. (∑i≤Suc (2 * (Suc N')). tn i * indicat_real (Aj i) x) ∂N)
= (∑i≤Suc (2 * (Suc N')). (∫x. tn i * indicat_real (Aj i) x ∂N))"
by(rule Bochner_Integration.integral_sum) (use integrable_real_mult_indicator sets_Aj(1) in blast)
show ?thesis
by(simp only: 1 2)
qed
also have "... = ¦(∑i≤Suc (2 * (Suc N')). tn i * measure (Ni n) (Aj i))
- (∑i≤Suc (2 * (Suc N')). tn i * measure N (Aj i))¦"
by simp
also have "... = ¦∑i≤Suc (2 * (Suc N')). tn i * (measure (Ni n) (Aj i) - measure N (Aj i))¦"
by(auto simp: sum_subtractf right_diff_distrib)
also have "... ≤ (∑i≤Suc (2 * (Suc N')). ¦tn i * (measure (Ni n) (Aj i) - measure N (Aj i))¦)"
by(rule sum_abs)
also have "... ≤ (∑i≤Suc (2 * (Suc N')). ¦tn i¦ * ¦(measure (Ni n) (Aj i) - measure N (Aj i))¦)"
by(simp add: abs_mult)
also have "... < (∑i≤Suc (2 * (Suc N')). r / (3 * (Suc (Suc (2 * Suc N')))))"
by(rule sum_strict_mono) (use n in auto)
also have "... = real (Suc (Suc (2 * Suc N'))) * (1 / (Suc (Suc (2 * Suc N'))) * (r / 3))"
by auto
also have "... = r / 3"
unfolding mult.assoc[symmetric] by simp
finally show ?thesis by auto
qed
finally show "¦(∫x. f x ∂Ni n) - (∫x. f x ∂N)¦ < r" .
qed
qed
qed
qed
qed(auto simp: sets_N finite_measure_N intro!: eventually_mono[OF eventually_Ni])
qed (simp add: mweak_conv_def sets_Ni sets_N finite_measure_N)
lemma mweak_conv_eq: "mweak_conv Ni N F
⟷ (∀f::'a ⇒ real. continuous_map mtopology euclidean f ⟶ (∃B. ∀x∈M. ¦f x¦ ≤ B)
⟶ ((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F)"
by(auto simp: sets_N mweak_conv_def finite_measure_N
intro!: eventually_mono[OF eventually_conj[OF finite_measure_Ni sets_Ni]])
lemma mweak_conv_eq1: "mweak_conv Ni N F
⟷ (∀f::'a ⇒ real. uniformly_continuous_map Self euclidean_metric f ⟶ (∃B. ∀x∈M. ¦f x¦ ≤ B)
⟶ ((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F)"
proof
assume h:"∀f::'a ⇒ real. uniformly_continuous_map Self euclidean_metric f ⟶ (∃B. ∀x∈M. ¦f x¦ ≤ B)
⟶ ((λn. ∫x. f x ∂Ni n) ⤏ (∫x. f x ∂N)) F"
have 1:"((λn. measure (Ni n) M) ⤏ measure N M) F"
proof -
have 1:"((λn. measure (Ni n) (space (Ni n))) ⤏ measure N M) F"
using h[rule_format,OF uniformly_continuous_map_const[THEN iffD2,of _ 1]]
by(auto simp: space_N)
show ?thesis
by(auto intro!: tendsto_cong[THEN iffD1,OF _ 1] eventually_mono[OF space_Ni])
qed
have "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
using mweak_conv2[OF h[rule_format]] mweak_conv3[OF _ 1] by auto
hence "⋀A. A ∈ sets (borel_of mtopology) ⟹ measure N (mtopology frontier_of A) = 0
⟹ ((λn. measure (Ni n) A) ⤏ measure N A) F"
using mweak_conv4 by auto
with mweak_conv5 show "mweak_conv Ni N F" by auto
qed(use mweak_conv1 in auto)
lemma mweak_conv_eq2: "mweak_conv Ni N F
⟷ ((λn. measure (Ni n) M) ⤏ measure N M) F ∧ (∀A. closedin mtopology A
⟶ Limsup F (λn. measure (Ni n) A) ≤ measure N A)"
proof safe
assume "mweak_conv Ni N F"
note h = this[simplified mweak_conv_eq1]
show 1:"((λn. measure (Ni n) M) ⤏ measure N M) F"
proof -
have 1:"((λn. measure (Ni n) (space (Ni n))) ⤏ measure N M) F"
using h[rule_format,OF uniformly_continuous_map_const[THEN iffD2,of _ 1]]
by(auto simp: space_N)
show ?thesis
by(auto intro!: tendsto_cong[THEN iffD1,OF _ 1] eventually_mono[OF space_Ni])
qed
show "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
using mweak_conv2[OF h[rule_format]] by auto
next
assume h: "((λn. measure (Ni n) M) ⤏ measure N M) F"
"∀A. closedin mtopology A ⟶ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
then have "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
using mweak_conv3 by auto
hence "⋀A. A ∈ sets (borel_of mtopology) ⟹ measure N (mtopology frontier_of A) = 0
⟹ ((λn. measure (Ni n) A) ⤏ measure N A) F"
using mweak_conv4 by auto
with mweak_conv5 show "mweak_conv Ni N F" by auto
qed
lemma mweak_conv_eq3: "mweak_conv Ni N F
⟷ ((λn. measure (Ni n) M) ⤏ measure N M) F ∧
(∀U. openin mtopology U ⟶ measure N U ≤ Liminf F (λn. measure (Ni n) U))"
proof safe
assume "mweak_conv Ni N F"
note h = this[simplified mweak_conv_eq1]
show 1:"((λn. measure (Ni n) M) ⤏ measure N M) F"
proof -
have 1:"((λn. measure (Ni n) (space (Ni n))) ⤏ measure N M) F"
using h[rule_format,OF uniformly_continuous_map_const[THEN iffD2,of _ 1]]
by(auto simp: space_N)
show ?thesis
by(auto intro!: tendsto_cong[THEN iffD1,OF _ 1] eventually_mono[OF space_Ni])
qed
show "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
using mweak_conv2[OF h[rule_format]] mweak_conv3[OF _ 1] by auto
next
assume h: "((λn. measure (Ni n) M) ⤏ measure N M) F"
"∀U. openin mtopology U ⟶ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
then have "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
using mweak_conv3' by auto
hence "⋀A. A ∈ sets (borel_of mtopology) ⟹ measure N (mtopology frontier_of A) = 0
⟹ ((λn. measure (Ni n) A) ⤏ measure N A) F"
using mweak_conv4 by auto
with mweak_conv5 show "mweak_conv Ni N F" by auto
qed
lemma mweak_conv_eq4: "mweak_conv Ni N F
⟷ (∀A ∈ sets (borel_of mtopology). measure N (mtopology frontier_of A) = 0
⟶ ((λn. measure (Ni n) A) ⤏ measure N A) F)"
proof safe
assume "mweak_conv Ni N F"
note h = this[simplified mweak_conv_eq1]
have 1:"((λn. measure (Ni n) M) ⤏ measure N M) F"
proof -
have 1:"((λn. measure (Ni n) (space (Ni n))) ⤏ measure N M) F"
using h[rule_format,OF uniformly_continuous_map_const[THEN iffD2,of _ 1]]
by(auto simp: space_N)
show ?thesis
by(auto intro!: tendsto_cong[THEN iffD1,OF _ 1] eventually_mono[OF space_Ni])
qed
have "⋀A. closedin mtopology A ⟹ Limsup F (λn. measure (Ni n) A) ≤ measure N A"
and "⋀U. openin mtopology U ⟹ measure N U ≤ Liminf F (λn. measure (Ni n) U)"
using mweak_conv2[OF h[rule_format]] mweak_conv3[OF _ 1] by auto
thus "⋀A. A ∈ sets (borel_of mtopology) ⟹ measure N (mtopology frontier_of A) = 0
⟹ ((λn. measure (Ni n) A) ⤏ measure N A) F"
using mweak_conv4 by auto
qed(use mweak_conv5 in auto)
corollary mweak_conv_imp_limit_space:
assumes "mweak_conv Ni N F"
shows "((λi. measure (Ni i) M) ⤏ measure N M) F"
using assms by(simp add: mweak_conv_eq3)
end
lemma
assumes "metrizable_space X"
and "∀⇩F i in F. sets (Ni i) = sets (borel_of X)" "∀⇩F i in F. finite_measure (Ni i)"
and "sets N = sets (borel_of X)" "finite_measure N"
shows weak_conv_on_eq1:
"weak_conv_on Ni N F X
⟷ ((λn. measure (Ni n) (topspace X)) ⤏ measure N (topspace X)) F
∧ (∀A. closedin X A ⟶ Limsup F (λn. measure (Ni n) A) ≤ measure N A)" (is ?eq1)
and weak_conv_on_eq2:
"weak_conv_on Ni N F X
⟷ ((λn. measure (Ni n) (topspace X)) ⤏ measure N (topspace X)) F
∧ (∀U. openin X U ⟶ measure N U ≤ Liminf F (λn. measure (Ni n) U))" (is ?eq2)
and weak_conv_on_eq3:
"weak_conv_on Ni N F X
⟷ (∀A ∈ sets (borel_of X). measure N (X frontier_of A) = 0
⟶ ((λn. measure (Ni n) A) ⤏ measure N A) F)" (is ?eq3)
proof -
obtain d where d: "Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X"
by (metis Metric_space.topspace_mtopology assms(1) metrizable_space_def)
then interpret mweak_conv_fin "topspace X" d Ni N
by(auto simp: mweak_conv_fin_def mweak_conv_fin_axioms_def assms)
show ?eq1 ?eq2 ?eq3
using mweak_conv_eq2 mweak_conv_eq3 mweak_conv_eq4 unfolding d(2) by blast+
qed
end