Theory Prokhorov_Theorem
section ‹Prokhorov's Theorem›
theory Prokhorov_Theorem
imports Levy_Prokhorov_Distance
Alaoglu_Theorem
begin
subsection ‹Prokhorov's Theorem›
context Levy_Prokhorov
begin
lemma relatively_compact_imp_tight_LP:
assumes "Γ ⊆ 𝒫" "separable_space mtopology" mcomplete
and "compactin LPm.mtopology (LPm.mtopology closure_of Γ)"
shows "tight_on_set mtopology Γ"
proof(cases "M = {}")
case True
then have "Γ = {} ∨ Γ = {null_measure (borel_of mtopology)}"
using assms(1) M_empty_P' by auto
thus ?thesis
by(auto simp: tight_on_set_def intro!: finite_measureI)
next
case M_ne:False
have 1: "∃k. ∀N∈Γ. measure N (⋃m≤k. Ui m) > measure N M - e"
if Ui: "⋀i::nat. openin mtopology (Ui i)" "(⋃i. Ui i) = M" and e:"e > 0" for Ui e
proof(rule ccontr)
assume "∄k. ∀N∈Γ. measure N (⋃m≤k. Ui m) > measure N M - e"
then have h: "∀k. ∃N∈Γ. measure N (⋃m≤k. Ui m) ≤ measure N M - e"
by(auto simp: linorder_class.not_less)
then obtain Nk where Nk: "⋀k. Nk k ∈ Γ" "⋀k. measure (Nk k) (⋃m≤k. Ui m) ≤ measure (Nk k) M - e"
by metis
obtain N r where Nr: "N ∈ LPm.mtopology closure_of Γ" "strict_mono r"
"limitin LPm.mtopology (Nk ∘ r) N sequentially"
using assms(1,4) Nk(1) closure_of_subset[of Γ LPm.mtopology]
by(simp add: LPm.compactin_sequentially) (metis image_subset_iff subsetD)
then interpret mweak_conv_fin M d "λi. Nk (r i)" N sequentially
using assms(1) Nk(1) closure_of_subset_topspace[of LPm.mtopology]
by(auto intro!: inP_mweak_conv_fin_all)
have sets_Nk[measurable_cong,simp]:"⋀i. sets (Nk (r i)) = sets (borel_of mtopology)"
using Nk(1) assms(1) inP_D(2) by blast
have wc: "mweak_conv_seq (λi. Nk (r i)) N"
using converge_imp_mweak_conv[OF Nr(3)] Nk(1) assms(1) by(auto simp: comp_def)
interpret Nk: finite_measure "Nk k" for k
using Nk(1) assms(1) inP_D by blast
interpret N: finite_measure N
using finite_measure_N by blast
have 1:"measure N (⋃i≤n. Ui i) ≤ measure N M - e" for n
proof -
have "measure N (⋃i≤n. Ui i) ≤ liminf (λj. measure (Nk (r j)) (⋃i≤n. Ui i))"
using Ui by(auto intro!: conjunct2[OF mweak_conv_eq3[THEN iffD1,OF wc],rule_format])
also have "... ≤ liminf (λj. measure (Nk (r j)) (⋃i≤r j. Ui i))"
by(rule Liminf_mono)
(auto intro!: Ui(1) exI[where x=n] Nk.finite_measure_mono[OF UN_mono]
le_trans[OF _ strict_mono_imp_increasing[OF Nr(2)]] borel_of_open
simp: eventually_sequentially sets_N)
also have "... ≤ liminf (λj. measure (Nk (r j)) M + ereal (- e))"
using Nk by(auto intro!: Liminf_mono eventuallyI)
also have "... ≤ liminf (λj. measure (Nk (r j)) M) + limsup (λi. - e)"
by(rule ereal_liminf_limsup_add)
also have "... = liminf (λj. measure (Nk (r j)) M) + ereal (- e)"
using Limsup_const[of sequentially "- e"] by simp
also have "... = measure N M + ereal (- e)"
proof -
have "(λk. measure (Nk (r k)) M) ⇢ measure N M"
using wc mweak_conv_eq2 by fastforce
from limI[OF tendsto_ereal[OF this]] convergent_liminf_cl[OF convergentI[OF tendsto_ereal[OF this]]]
show ?thesis by simp
qed
finally show ?thesis
by simp
qed
have 2:"(λn. measure N (⋃i≤n. Ui i)) ⇢ measure N M"
proof -
have "(λn. measure N (⋃i≤n. Ui i)) ⇢ measure N (⋃ (range (λn. ⋃i≤n. Ui i)))"
by(fastforce intro!: Ui(1) N.finite_Lim_measure_incseq borel_of_open incseq_SucI simp: sets_N)
moreover have "⋃ (range (λn. ⋃i≤n. Ui i)) = M"
using Ui(2) by blast
ultimately show ?thesis
by simp
qed
show False
using e Lim_bounded[OF 2,of 0 "measure N M - e"] 1 by auto
qed
show ?thesis
unfolding tight_on_set_def
proof safe
fix e :: real
assume e: "0 < e"
obtain U where U: "countable U" "mdense U"
using assms(2) separable_space_def2 by blast
let ?an = "from_nat_into U"
have an: "⋀n. ?an n ∈ M" "mdense (range ?an)"
by (metis M_ne U(2) from_nat_into mdense_def2 mdense_empty_iff subsetD)
(metis M_ne U(1) U(2) mdense_empty_iff range_from_nat_into)
have "∃k. ∀N∈Γ. measure N (⋃n≤k. mball (?an n) (1 / Suc m)) > measure N M - (e / 2) * (1 / 2) ^ Suc m" for m
by(rule 1) (use mdense_balls_cover[OF an(2)] e in auto)
then obtain k where k:
"⋀m N. N ∈ Γ ⟹ measure N (⋃n≤k m. mball (?an n) (1 / Suc m)) > measure N M - (e / 2) * (1 / 2) ^ Suc m"
by metis
let ?K = "⋂m. (⋃i≤k m. mcball (?an i) (1 / Suc m))"
show "∃K. compactin mtopology K ∧ (∀M∈Γ. measure M (space M - K) < e)"
proof(safe intro!: exI[where x="?K"])
have "closedin mtopology ?K"
by(auto intro!: closedin_Union)
moreover have "?K ⊆ M"
by auto
moreover have "mtotally_bounded ?K"
unfolding mtotally_bounded_def2
proof safe
fix e :: real
assume e: "0 < e"
then obtain m where m: "e > 1 / Suc m"
using nat_approx_posE by blast
have "?K ⊆ (⋃i≤k m. mcball (?an i) (1 / real (Suc m)))"
by auto
also have "... ⊆ (⋃x∈?an ` {..k m}. mball x e)"
using mcball_subset_mball_concentric[OF m] by blast
finally show "∃K. finite K ∧ K ⊆ M ∧ ?K ⊆ (⋃x∈K. mball x e)"
using an(1) by(fastforce intro!: exI[where x="?an ` {..k m}"])
qed
ultimately show "compactin mtopology ?K"
using mtotally_bounded_eq_compact_closedin[OF assms(3)] by auto
next
fix N
assume N: "N ∈ Γ"
then interpret N: finite_measure N
using assms(1) inP_D by blast
have sets_N: "sets N = sets (borel_of mtopology)"
using N assms(1) by(auto simp: 𝒫_def)
hence space_N: "space N = M"
by(auto cong: sets_eq_imp_space_eq simp: space_borel_of)
have [measurable]:"⋀a b. mcball a b ∈ sets N" "M ∈ sets N"
by(auto simp: sets_N intro!: borel_of_closed)
have Ne:"measure N (M - (⋃i≤k m. mcball (?an i) (1 / real (Suc m)))) < (e / 2) * (1 / 2) ^ Suc m" for m
proof -
have "measure N (M - (⋃i≤k m. mcball (?an i) (1 / real (Suc m))))
= measure N M - measure N (⋃i≤k m. mcball (?an i) (1 / real (Suc m)))"
by(auto simp: N.finite_measure_compl[simplified space_N])
also have "... ≤ measure N M - measure N (⋃i≤k m. mball (?an i) (1 / real (Suc m)))"
by(fastforce intro!: N.finite_measure_mono)
also have "... < (e / 2) * (1 / 2) ^ Suc m"
using k[OF N,of m] by simp
finally show ?thesis .
qed
have Ne_sum: "summable (λm. (e / 2) * (1 / 2) ^ Suc m)"
by auto
have sum2: "summable (λm. measure N (M - (⋃i≤k m. mcball (from_nat_into U i) (1 / real (Suc m)))))"
using Ne by(auto intro!: summable_comparison_test_ev[OF _ Ne_sum] eventuallyI) (use less_eq_real_def in blast)
show "measure N (space N - ?K) < e"
proof -
have "measure N (space N - ?K) = measure N (⋃m. (M - (⋃i≤k m. mcball (?an i) (1 / Suc m))))"
by(auto simp: space_N)
also have "... ≤ (∑m. measure N (M - (⋃i≤k m. mcball (?an i) (1 / Suc m))))"
by(rule N.finite_measure_subadditive_countably) (use sum2 in auto)
also have "... ≤ (∑m. (e / 2) * (1 / 2) ^ Suc m)"
by(rule suminf_le) (use Ne less_eq_real_def sum2 in auto)
also have "... = (e / 2) * (∑m. (1 / 2) ^ Suc m)"
by(rule suminf_mult) auto
also have "... = e / 2"
using power_half_series sums_unique by fastforce
also have "... < e"
using e by simp
finally show ?thesis .
qed
qed
qed(use assms inP_D in auto)
qed
lemma mcompact_imp_LPmcompact:
assumes "compact_space mtopology"
shows "compactin LPm.mtopology {N. sets N = sets (borel_of mtopology) ∧ N (space N) ≤ ennreal r}"
(is "compactin _ ?N")
proof -
consider "M = {}" | "r < 0" | "r ≥ 0" "M ≠ {}"
by linarith
then show ?thesis
proof cases
assume "M = {}"
then have "finite (topspace LPm.mtopology)"
unfolding LPm.topspace_mtopology using M_empty_P by fastforce
thus ?thesis
using closedin_bounded_measures closedin_compact_space compact_space_def finite_imp_compactin_eq by blast
next
assume "r < 0"
then have "?N = {null_measure (borel_of mtopology)}"
using emeasure_eq_0[OF _ _ sets.sets_into_space]
by(safe,intro measure_eqI) (auto simp: ennreal_lt_0)
thus ?thesis
by(auto intro!: inP_I finite_measureI)
next
assume M_ne:"M ≠ {}" and r:"r ≥ 0"
hence [simp]: "mtopology ≠ trivial_topology"
using topspace_mtopology by force
define Cb where "Cb ≡ cfunspace mtopology (euclidean_metric :: real metric)"
define Cb' where "Cb' ≡ powertop_real (mspace (cfunspace mtopology (euclidean_metric :: real metric)))"
define B where
"B ≡ {φ∈topspace Cb'. φ (λx∈topspace mtopology. 1) ≤ r ∧ positive_linear_functional_on_CX mtopology φ}"
define T :: "'a measure ⇒ ('a ⇒ real) ⇒ real"
where "T ≡ λN. λf∈mspace (cfunspace mtopology euclidean_metric). ∫x. f x ∂N"
have compact: "compactin Cb' B"
unfolding B_def Cb'_def by(rule Alaoglu_theorem_real_functional[OF assms(1)]) (use M_ne in simp)
have metrizable: "metrizable_space (subtopology Cb' B)"
unfolding B_def Cb'_def by(rule metrizable_functional[OF assms metrizable_space_mtopology])
have homeo: "homeomorphic_map (subtopology LPm.mtopology ?N) (subtopology Cb' B) T"
proof -
have T_cont': "continuous_map (subtopology LPm.mtopology ?N) Cb' T"
unfolding continuous_map_atin
proof safe
fix N
assume N:"N ∈ topspace (subtopology LPm.mtopology ?N)"
show "limitin Cb' T (T N) (atin (subtopology LPm.mtopology ?N) N)"
unfolding Cb'_def limitin_componentwise
proof safe
fix g :: "'a ⇒ real"
assume g:"g ∈ mspace (cfunspace mtopology euclidean_metric)"
then have g_bounded:"∃B. ∀x∈M. ¦g x¦ ≤ B"
by(auto simp: bounded_pos_less order_less_le)
show "limitin euclideanreal (λc. T c g) (T N g) (atin (subtopology LPm.mtopology ?N) N)"
unfolding limitin_canonical_iff
proof
fix e :: real
assume e:"0 < e"
have N_in: "N ∈ ?N"
using N by simp
show "∀⇩F c in atin (subtopology LPm.mtopology ?N) N. dist (T c g) (T N g) < e "
unfolding atin_subtopology_within[OF N_in]
proof (safe intro!: eventually_within_imp[THEN iffD2,OF LPm.eventually_atin_sequentially[THEN iffD2]])
fix Ni
assume Ni:"range Ni ⊆ 𝒫 - {N}" "limitin LPm.mtopology Ni N sequentially"
with N interpret mweak_conv_fin M d Ni N sequentially
by(auto intro!: inP_mweak_conv_fin_all)
have wc:"mweak_conv_seq Ni N"
using Ni by(auto intro!: converge_imp_mweak_conv)
hence 1:"(λn. T (Ni n) g) ⇢ T N g"
unfolding T_def by(auto simp: g mweak_conv_def g_bounded)
show "∀⇩F n in sequentially. Ni n ∈ ?N ⟶ dist (T (Ni n) g) (T N g) < e"
by(rule eventually_mp[OF _ 1[simplified tendsto_iff,rule_format,OF e]]) simp
qed
qed
qed(auto simp: T_def)
qed
have T_cont: "continuous_map (subtopology LPm.mtopology ?N) (subtopology Cb' B) T"
unfolding continuous_map_in_subtopology
proof
show "T ` topspace (subtopology LPm.mtopology ?N) ⊆ B"
unfolding B_def Cb'_def
proof safe
fix N
assume N:"N ∈ topspace (subtopology LPm.mtopology ?N)"
then have "finite_measure N" and sets_N:"sets N = sets (borel_of mtopology)"
and space_N:"space N = M" and N_r:"emeasure N (space N) ≤ ennreal r"
by(auto intro!: inP_D)
hence N_r':"measure N (space N) ≤ r"
by (simp add: finite_measure.emeasure_eq_measure r)
interpret N: finite_measure N
by fact
have TN_def: "T N (λx∈topspace mtopology. f x) = (∫x. f x ∂N)" "T N (λx∈M. f x) = (∫x. f x ∂N)"
if f:"continuous_map mtopology euclideanreal f" for f
using f Bochner_Integration.integral_cong[OF refl,of N "λx∈M. f x" f,simplified space_N]
compact_imp_bounded[OF compactin_euclidean_iff[THEN iffD1,
OF image_compactin[OF assms[simplified compact_space_def] f]]]
by(auto simp: T_def)
have N_integrable[simp]: "integrable N f" if f:"continuous_map mtopology euclideanreal f" for f
using compact_imp_bounded[OF compactin_euclidean_iff[THEN iffD1,OF image_compactin[OF
assms[simplified compact_space_def] f]]] continuous_map_measurable[OF f]
by(auto intro!: N.integrable_const_bound AE_I2[of N]
simp: bounded_iff measurable_cong_sets[OF sets_N] borel_of_euclidean space_N)
show "T N (λx∈topspace mtopology. 1) ≤ r"
unfolding TN_def[OF continuous_map_canonical_const]
using N_r' by simp
show "positive_linear_functional_on_CX mtopology (T N)"
unfolding positive_linear_functional_on_CX_compact[OF assms]
proof safe
fix f c
assume f: "continuous_map mtopology euclideanreal f"
show "T N (λx∈topspace mtopology. c * f x) = c * T N (λx∈topspace mtopology. f x)"
using f continuous_map_real_mult_left[OF f,of c] by(auto simp: TN_def)
next
fix f g
assume fg: "continuous_map mtopology euclideanreal f"
"continuous_map mtopology euclideanreal g"
show "T N (λx∈topspace mtopology. f x + g x)
= T N (λx∈topspace mtopology. f x) + T N (λx∈topspace mtopology. g x)"
using fg continuous_map_add[OF fg]
by(auto simp: TN_def intro!: Bochner_Integration.integral_add)
next
fix f
assume "continuous_map mtopology euclideanreal f" "∀x∈topspace mtopology. 0 ≤ f x"
then show "0 ≤ T N (λx∈topspace mtopology. f x)"
by(auto simp: TN_def space_N intro!: Bochner_Integration.integral_nonneg)
qed
show "T N ∈ topspace (powertop_real (mspace (cfunspace mtopology euclidean_metric)))"
by(auto simp: T_def)
qed
qed fact
define T_inv :: "(('a ⇒ real) ⇒ real) ⇒ 'a measure" where
"T_inv ≡ (λφ. THE N. sets N = sets (borel_of mtopology) ∧ finite_measure N ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ φ (restrict f (topspace mtopology)) = integral⇧L N f))"
have T_T_inv: "∀N∈topspace (subtopology LPm.mtopology ?N). T_inv (T N) = N"
proof safe
fix N
assume N:"N ∈ topspace (subtopology LPm.mtopology ?N)"
from Pi_mem[OF continuous_map_funspace[OF T_cont] this]
have TN:"T N ∈ topspace (subtopology Cb' B)"
by blast
hence "∃!N'. sets N' = sets (borel_of mtopology) ∧ finite_measure N' ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ T N (restrict f (topspace mtopology)) = integral⇧L N' f)"
by(intro Riesz_representation_real_compact_metrizable[OF assms metrizable_space_mtopology])
(auto simp del: topspace_mtopology restrict_apply simp: B_def)
moreover have "sets N = sets (borel_of mtopology) ∧ finite_measure N ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ T N (restrict f (topspace mtopology)) = integral⇧L N f)"
using compact_imp_bounded[OF compactin_euclidean_iff[THEN iffD1,OF image_compactin[OF
assms[simplified compact_space_def] _]]] N
by(auto simp: T_def dest:inP_D cong: Bochner_Integration.integral_cong)
ultimately show "T_inv (T N) = N"
unfolding T_inv_def by(rule the1_equality)
qed
have T_inv_T: "∀φ∈topspace (subtopology Cb' B). T (T_inv φ) = φ"
proof safe
fix φ
assume φ:"φ∈topspace (subtopology Cb' B)"
hence 1:"∃!N'. sets N' = sets (borel_of mtopology) ∧ finite_measure N' ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ φ (restrict f (topspace mtopology)) = integral⇧L N' f)"
by(intro Riesz_representation_real_compact_metrizable[OF assms metrizable_space_mtopology])
(auto simp del: topspace_mtopology restrict_apply simp add: B_def)
have T_inv_φ:"sets (T_inv φ) = sets (borel_of mtopology)" "finite_measure (T_inv φ)"
"⋀f. continuous_map mtopology euclideanreal f
⟹ φ (λx∈topspace mtopology. f x) = integral⇧L (T_inv φ) f"
unfolding T_inv_def by(use theI'[OF 1] in blast)+
show "T (T_inv φ) = φ"
proof
fix f
consider "f ∈ mspace Cb" | "f ∉ mspace Cb"
by fastforce
then show "T (T_inv φ) f = φ f"
proof cases
case 1
then have "T (T_inv φ) f = integral⇧L (T_inv φ) f"
by(auto simp: T_def Cb_def)
also have "... = φ (λx∈topspace mtopology. f x)"
by(rule T_inv_φ(3)[symmetric]) (use 1 Cb_def in auto)
also have "... = φ f"
proof -
have 2: "(λx∈topspace mtopology. f x) = f"
using 1 by(auto simp: extensional_def Cb_def)
show ?thesis
unfolding 2 by blast
qed
finally show ?thesis .
next
case 2
then have "T (T_inv φ) f = undefined"
by (auto simp: Cb_def T_def)
also have "... = φ f"
using 2 φ Cb'_def Cb_def PiE_arb by auto
finally show ?thesis .
qed
qed
qed
have T_inv_cont: "continuous_map (subtopology Cb' B) (subtopology LPm.mtopology ?N) T_inv"
unfolding seq_continuous_iff_continuous_first_countable[OF metrizable_imp_first_countable[OF
metrizable],symmetric] seq_continuous_map
proof safe
fix φn φ
assume "limitin (subtopology Cb' B) φn φ sequentially"
then have φB: "φ ∈ B" and h:"limitin Cb' φn φ sequentially" "∀⇩F n in sequentially. φn n ∈ B"
by(auto simp: limitin_subtopology)
then obtain n0 where n0: "⋀n. n ≥ n0 ⟹ φn n ∈ B"
by(auto simp: eventually_sequentially)
have limit: "⋀f. f ∈ mspace (cfunspace mtopology euclidean_metric) ⟹ (λn. φn n f) ⇢ φ f"
using h(1) by(auto simp: limitin_componentwise Cb'_def)
show "limitin (subtopology LPm.mtopology ?N) (λn. T_inv (φn n)) (T_inv φ) sequentially"
proof(rule limitin_sequentially_offset_rev[where k=n0])
from φB have "∃!N. sets N = sets (borel_of mtopology) ∧ finite_measure N ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ φ (restrict f (topspace mtopology)) = integral⇧L N f)"
by(intro Riesz_representation_real_compact_metrizable[OF assms metrizable_space_mtopology])
(auto simp del: topspace_mtopology restrict_apply simp: B_def)
hence "sets (T_inv φ) = sets (borel_of mtopology) ∧ finite_measure (T_inv φ) ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ φ (restrict f (topspace mtopology)) = integral⇧L (T_inv φ) f)"
unfolding T_inv_def by(rule theI')
hence T_inv_φ: "sets (T_inv φ) = sets (borel_of mtopology)" "finite_measure (T_inv φ)"
"⋀f. continuous_map mtopology euclideanreal f
⟹ φ (restrict f (topspace mtopology)) = integral⇧L (T_inv φ) f"
by auto
from this(2) this(3)[of "λx. 1"] φB have T_inv_φ_r: "T_inv φ (space (T_inv φ)) ≤ ennreal r"
unfolding B_def by simp (metis ennreal_le_iff finite_measure.emeasure_eq_measure r)
{
fix n
from n0[of "n + n0",simplified] have "∃!N. sets N = sets (borel_of mtopology) ∧
finite_measure N ∧ (∀f. continuous_map mtopology euclideanreal f
⟶ φn (n + n0) (restrict f (topspace mtopology)) = integral⇧L N f)"
by(intro Riesz_representation_real_compact_metrizable[OF assms metrizable_space_mtopology])
(auto simp del: topspace_mtopology restrict_apply simp: B_def)
hence "sets (T_inv (φn (n + n0))) = sets (borel_of mtopology) ∧ finite_measure (T_inv (φn (n + n0))) ∧
(∀f. continuous_map mtopology euclideanreal f
⟶ φn (n + n0) (restrict f (topspace mtopology)) = integral⇧L (T_inv (φn (n + n0))) f)"
unfolding T_inv_def by(rule theI')
hence "sets (T_inv (φn (n + n0))) = sets (borel_of mtopology)"
"finite_measure (T_inv (φn (n + n0)))"
"⋀f. continuous_map mtopology euclideanreal f
⟹ φn (n + n0) (restrict f (topspace mtopology)) = integral⇧L (T_inv (φn (n + n0))) f"
by auto
}
note T_inv_φn = this
have T_inv_φn_r: "T_inv (φn (n + n0)) (space (T_inv (φn (n + n0)))) ≤ ennreal r" for n
using T_inv_φn(2)[of n] T_inv_φn(3)[of "λx. 1" n] n0[of "n + n0",simplified]
unfolding B_def by simp (metis ennreal_le_iff finite_measure.emeasure_eq_measure r)
show "limitin (subtopology LPm.mtopology ?N) (λn. T_inv (φn (n + n0))) (T_inv φ) sequentially"
proof(intro limitin_subtopology[THEN iffD2] mweak_conv_imp_converge conjI)
show "mweak_conv_seq (λn. T_inv (φn (n + n0))) (T_inv φ)"
unfolding mweak_conv_seq_def
proof safe
fix f :: "'a ⇒ real" and B
assume f:"continuous_map mtopology euclideanreal f" and B:"∀x∈M. ¦f x¦ ≤ B"
hence f': "restrict f (topspace mtopology) ∈ mspace (cfunspace mtopology euclidean_metric)"
by (auto simp: bounded_pos_less intro!: exI[where x="¦B¦ + 1"])
have 1:"(λn. ∫x. f x ∂ T_inv (φn (n + n0))) = (λn. φn (n + n0) (restrict f (topspace mtopology)))"
by(subst T_inv_φn(3)) (use f in auto)
have 2:"(∫x. f x ∂ T_inv φ) = φ (restrict f (topspace mtopology))"
by(subst T_inv_φ(3)) (use f in auto)
show "(λn. ∫x. f x ∂ T_inv (φn (n + n0))) ⇢ (∫x. f x ∂T_inv φ)"
unfolding 1 2 using limit[OF f'] LIMSEQ_ignore_initial_segment by blast
qed(use T_inv_φ(1,2) T_inv_φn(1,2) eventuallyI in auto)
next
show " ∀⇩F a in sequentially. T_inv (φn (a + n0)) ∈ ?N"
by (simp add: T_inv_φn(1) T_inv_φn_r)
next
show "T_inv φ ∈ {N. sets N = sets (borel_of mtopology) ∧ emeasure N (space N) ≤ ennreal r}"
using T_inv_φ(1) T_inv_φ_r by auto
qed(use T_inv_φn(1) T_inv_φn_r T_inv_φ(1) T_inv_φ_r compact_space_imp_separable[OF assms] in auto)
qed
qed
show ?thesis
using T_inv_cont T_cont T_T_inv T_inv_T
by(auto intro!: homeomorphic_maps_imp_map[where g=T_inv] simp: homeomorphic_maps_def)
qed
show ?thesis
using homeomorphic_compact_space[OF homeomorphic_map_imp_homeomorphic_space[OF homeo]]
compact_space_subtopology[OF compact] LPm.closedin_metric closedin_bounded_measures compactin_subspace
by fastforce
qed
qed
lemma tight_imp_relatively_compact_LP:
assumes "Γ ⊆ {N. sets N = sets (borel_of mtopology) ∧ N (space N) ≤ ennreal r}" "separable_space mtopology"
and "tight_on_set mtopology Γ"
shows "compactin LPm.mtopology (LPm.mtopology closure_of Γ)"
proof(cases "r < 0")
assume "r < 0"
then have *:"{N. sets N = sets (borel_of mtopology) ∧ N (space N) ≤ ennreal r} = {null_measure (borel_of mtopology)}"
using emeasure_eq_0[OF _ _ sets.sets_into_space]
by(safe,intro measure_eqI) (auto simp: ennreal_lt_0)
with assms(1) have "Γ = {} ∨ Γ = {null_measure (borel_of mtopology)}"
by auto
hence "LPm.mtopology closure_of Γ = {} ∨ LPm.mtopology closure_of Γ = {null_measure (borel_of mtopology)}"
by (metis (no_types) * closedin_bounded_measures closure_of_empty closure_of_eq)
thus ?thesis
by(auto intro!: inP_I finite_measureI)
next
assume "¬ r < 0"
then have r_nonneg:"r ≥ 0"
by simp
have subst1: "Γ ⊆ 𝒫"
using assms(1) linorder_not_le by(force intro!: finite_measureI inP_I)
have subst2: "LPm.mtopology closure_of Γ ⊆ {N. sets N = sets (borel_of mtopology) ∧ N (space N) ≤ ennreal r}"
by (simp add: assms(1) closedin_bounded_measures closure_of_minimal)
have tight: "tight_on_set mtopology (LPm.mtopology closure_of Γ)"
unfolding tight_on_set_def
proof safe
fix e :: real
assume e: "0 < e"
then obtain K where K: "compactin mtopology K" "⋀N. N ∈ Γ ⟹ measure N (space N - K) < e / 2"
by (metis assms(3) tight_on_set_def zero_less_divide_iff zero_less_numeral)
show "∃K. compactin mtopology K ∧ (∀M∈LPm.mtopology closure_of Γ. measure M (space M - K) < e)"
proof(safe intro!: exI[where x=K])
fix N
assume N:"N ∈ LPm.mtopology closure_of Γ"
then obtain Nn where Nn: "⋀n. Nn n ∈ Γ" "limitin LPm.mtopology Nn N sequentially"
unfolding LPm.closure_of_sequentially by auto
with N subst1 interpret mweak_conv_fin M d Nn N sequentially
using closure_of_subset_topspace by(fastforce intro!: inP_mweak_conv_fin_all simp: closure_of_subset_topspace)
have space_Ni:"⋀i. space (Nn i) = M"
by (meson Nn(1) inP_D(3) subsetD subst1)
have "openin mtopology (M - K)"
using compactin_imp_closedin[OF Hausdorff_space_mtopology K(1)] by blast
hence "ereal (measure N (M - K)) ≤ liminf (λn. ereal (measure (Nn n) (M -K)))"
using mweak_conv_eq3 converge_imp_mweak_conv[OF Nn(2)] Nn(1) subst1 by blast
also have "... ≤ ereal (e / 2)"
using K(2) Nn(1) space_Ni
by(intro Liminf_le eventuallyI ereal_less_eq(3)[THEN iffD2] order.strict_implies_order) fastforce+
also have "... < ereal e"
using e by auto
finally show "measure N (space N - K) < e"
by(auto simp: space_N)
qed fact
qed(use closure_of_subset_topspace[of LPm.mtopology Γ] inP_D in auto)
show ?thesis
unfolding LPm.compactin_sequentially
proof safe
fix Ni :: "nat ⇒ 'a measure"
assume Ni: "range Ni ⊆ LPm.mtopology closure_of Γ"
then have Ni2: "⋀i. finite_measure (Ni i)" and Ni_le_r: "⋀i. Ni i (space (Ni i)) ≤ ennreal r"
and sets_Ni[measurable_cong]:"⋀i. sets (Ni i) = sets (borel_of mtopology)"
and space_Ni:"⋀i. space (Ni i) = M"
using closure_of_subset_topspace[of LPm.mtopology Γ] inP_D subst2 by fastforce+
interpret Ni: finite_measure "Ni i" for i
by fact
have "metrizable_space Hilbert_cube_topology"
by(auto simp: metrizable_space_product_topology metrizable_space_euclidean intro!: metrizable_space_subtopology)
then obtain dH where dH: "Metric_space (UNIV →⇩E {0..1}) dH"
"Metric_space.mtopology (UNIV →⇩E {0..1}) dH = Hilbert_cube_topology"
by (metis Metric_space.topspace_mtopology metrizable_space_def topspace_Hilbert_cube)
then interpret dH: Metric_space "UNIV →⇩E {0..1}" dH
by auto
have compact_dH:"compact_space dH.mtopology"
unfolding dH(2) by(auto simp: compact_space_def compactin_PiE)
from embedding_into_Hilbert_cube[OF metrizable_space_mtopology assms(2)]
obtain A where A: "A ⊆topspace Hilbert_cube_topology"
"mtopology homeomorphic_space subtopology Hilbert_cube_topology A"
by auto
then obtain T T_inv where T: "continuous_map mtopology (subtopology Hilbert_cube_topology A) T"
"continuous_map (subtopology Hilbert_cube_topology A) mtopology T_inv"
"⋀x. x ∈ topspace (subtopology Hilbert_cube_topology A)
⟹ T (T_inv x) = x" "⋀x. x ∈ M ⟹ T_inv (T x) = x"
unfolding homeomorphic_space_def homeomorphic_maps_def by fastforce
hence injT: "inj_on T M"
by(intro inj_on_inverseI)
have T_cont: "continuous_map mtopology dH.mtopology T"
by (metis T(1) continuous_map_in_subtopology dH(2))
from continuous_map_measurable[OF this]
have T_meas[measurable]: "T ∈ measurable (Ni n) (borel_of dH.mtopology)" for n
by(auto simp: sets_Ni cong: measurable_cong_sets)
define νn where "νn ≡ (λi. distr (Ni i) (borel_of dH.mtopology) T)"
have sets_νn: "⋀n. sets (νn n) = sets (borel_of dH.mtopology)"
unfolding νn_def by simp
hence space_νn: "⋀n. space (νn n) = UNIV →⇩E {0..1}"
by(auto cong: sets_eq_imp_space_eq simp: space_borel_of)
interpret νn: finite_measure "νn n" for n
by(auto simp: νn_def space_borel_of PiE_eq_empty_iff intro!: Ni.finite_measure_distr)
have νn_le_r: "νn n (space (νn n)) ≤ ennreal r" for n
by(auto simp: νn_def emeasure_distr order.trans[OF emeasure_space Ni_le_r[of n]])
have measure_νn_compact:"measure (νn n) (space (νn n) - T ` K) = measure (Ni n) (space (Ni n) - K)"
if K: "compactin mtopology K" for K n
proof -
have "compactin dH.mtopology (T ` K)"
using T_cont image_compactin K by blast
hence "T ` K ∈ sets (borel_of dH.mtopology)"
by(auto intro!: borel_of_closed compactin_imp_closedin dH.Hausdorff_space_mtopology)
hence "measure (νn n) (space (νn n) - T ` K)
= measure (Ni n) (T -` (space (νn n) - T ` K) ∩ space (Ni n))"
by(simp add: νn_def measure_distr)
also have "... = measure (Ni n) (space (Ni n) - K)"
using compactin_subset_topspace[OF K] T(4) Pi_mem[OF continuous_map_funspace[OF T(1)]]
by(auto intro!: arg_cong[where f="measure (Ni n)"] simp: space_Ni subset_iff space_νn) metis
finally show ?thesis .
qed
define HP where "HP ≡ {N. sets N = sets (borel_of dH.mtopology) ∧ N (space N) ≤ ennreal r}"
interpret dHs: Levy_Prokhorov "UNIV →⇩E {0..1}" dH
using dH(1) by(auto simp: HP_def Levy_Prokhorov_def)
have HP:"HP ⊆ {N. sets N = sets (borel_of dH.mtopology) ∧ finite_measure N}"
by(auto simp: HP_def top.extremum_unique intro!: finite_measureI)
have νn_HP:"range νn ⊆ HP"
by(fastforce simp: HP_def sets_νn νn_le_r)
then obtain ν' a where ν': "ν' ∈ HP" "strict_mono a" "limitin dHs.LPm.mtopology (νn ∘ a) ν' sequentially"
using dHs.mcompact_imp_LPmcompact[OF compact_dH,of r]
unfolding dHs.LPm.compactin_sequentially HP_def by meson
hence sets_ν'[measurable_cong]: "sets ν' = sets (borel_of dH.mtopology)"
and ν'_le_r: "ν' (space ν') ≤ ennreal r"
by(auto simp: HP_def space_borel_of)
have space_ν': "space ν' = UNIV →⇩E {0..1}"
using sets_eq_imp_space_eq[OF sets_ν'] by(simp add: space_borel_of)
interpret ν': finite_measure ν'
using ν'_le_r by(auto intro!: finite_measureI simp: top_unique)
interpret wc:mweak_conv_fin "UNIV →⇩E {0..1}" dH "νn ∘ a" ν' sequentially
using νn_HP HP by(fastforce intro!: dHs.inP_mweak_conv_fin_all ν' dHs.inP_I)
have claim: "∃E⊆A. E ∈ sets (borel_of dH.mtopology) ∧ measure ν' (space ν' - E) = 0"
proof -
{
fix n
have "∃Kn. compactin mtopology Kn ∧ (∀N∈LPm.mtopology closure_of Γ. measure N (space N - Kn) < 1 / Suc n)"
using tight by(auto simp: tight_on_set_def)
}
then obtain Kn where Kn: "⋀n. compactin mtopology (Kn n)"
"⋀N n. N ∈ LPm.mtopology closure_of Γ ⟹ measure N (space N - Kn n) < 1 / Suc n"
by metis
have TKn_compact:"⋀n. compactin dH.mtopology (T ` (Kn n))"
by (metis Kn(1) T_cont image_compactin)
hence [measurable]:"⋀n. T ` Kn n ∈ sets (borel_of dH.mtopology)"
by(auto intro!: borel_of_closed compactin_imp_closedin dH.Hausdorff_space_mtopology)
have T_img: "⋀n. T ` (Kn n) ⊆ A"
using continuous_map_image_subset_topspace[OF T(1)] compactin_subset_topspace[OF Kn(1)]
by fastforce
define E where "E ≡ (⋃n. T ` (Kn n))"
have [measurable]: "E ∈ sets (borel_of dH.mtopology)"
by(simp add: E_def)
show ?thesis
proof(safe intro!: exI[where x=E])
show "measure ν' (space ν' - E) = 0"
proof(rule antisym[OF field_le_epsilon])
fix e :: real
assume e: "0 < e"
then obtain n0 where n0: "1 / (Suc n0) < e"
using nat_approx_posE by blast
show "measure ν' (space ν' - E) ≤ 0 + e"
proof -
have "ereal (measure ν' (space ν' - E)) ≤ ereal (measure ν' (space ν' - T ` (Kn n0)))"
by(auto intro!: ν'.finite_measure_mono simp: E_def)
also have "... ≤ liminf (λn. ereal (measure ((νn ∘ a) n) (space ν' - T ` (Kn n0))))"
proof -
have "openin dH.mtopology (space ν' - T ` (Kn n0))"
by (metis TKn_compact compactin_imp_closedin dH.Hausdorff_space_mtopology dH.open_in_mspace openin_diff wc.space_N)
with wc.mweak_conv_eq3[THEN iffD1,OF dHs.converge_imp_mweak_conv[OF ν'(3)]]
show ?thesis
using νn_HP HP by(auto simp: dHs.inP_iff)
qed
also have "... = liminf (λn. ereal (measure ((νn ∘ a) n) (space ((νn ∘ a) n) - T ` (Kn n0))))"
by(auto simp: space_νn space_ν')
also have "... = liminf (λn. ereal (measure ((Ni ∘ a) n) (space ((Ni ∘ a) n) - Kn n0)))"
by(simp add: measure_νn_compact[OF Kn(1)])
also have "... ≤ 1 / (Suc n0)"
using Ni
by(intro Liminf_le eventuallyI ereal_less_eq(3)[THEN iffD2] order.strict_implies_order Kn(2))
auto
also have "... < ereal e"
using n0 by auto
finally show ?thesis
by simp
qed
qed simp
qed(use E_def T_img in auto)
qed
then obtain E where E[measurable]: "E ⊆ A"
"E ∈ sets (borel_of dH.mtopology)" "measure ν' (space ν' - E) = 0"
by blast
have measure_ν': "measure ν' (B ∩ E) = measure ν' B"
if B[measurable]: "B ∈ sets (borel_of dH.mtopology)" for B
proof(rule antisym)
have "measure ν' B = measure ν' (B ∩ E ∪ B ∩ (space ν' - E))"
using sets.sets_into_space[OF B]
by(auto intro!: arg_cong[where f="measure ν'"] simp: space_ν' space_borel_of)
also have "... ≤ measure ν' (B ∩ E) + measure ν' (B ∩ (space ν' - E))"
by(auto intro!: measure_Un_le)
also have "... ≤ measure ν' (B ∩ E) + measure ν' ((space ν' - E))"
by(auto intro!: ν'.finite_measure_mono)
also have "... = measure ν' (B ∩ E)"
by(simp add: E)
finally show "measure ν' B ≤ measure ν' (B ∩ E)" .
qed(auto intro!: ν'.finite_measure_mono)
from this[of "space ν'"] sets.sets_into_space[OF E(2)]
have measure_ν'E:"measure ν' E = measure ν' (space ν')"
by(auto simp: space_ν' borel_of_open space_borel_of inf.absorb_iff2)
show "∃N r. N ∈ LPm.mtopology closure_of Γ ∧ strict_mono r ∧ limitin LPm.mtopology (Ni ∘ r) N sequentially"
proof -
define ν where "ν ≡ restrict_space ν' E"
interpret ν: finite_measure ν
by(auto intro!: finite_measure_restrict_space ν'.finite_measure_axioms simp: ν_def)
have space_ν:"space ν = E"
using E(2) ν_def sets_ν' space_restrict_space2 by blast
have ν_le_r: "ν (space ν) ≤ ennreal r"
by(simp add: ν_def emeasure_restrict_space order.trans[OF emeasure_space ν'_le_r])
have measure_ν'2: "measure ν' B = measure ν (B ∩ E)"
if B[measurable]: "B ∈ sets (borel_of dH.mtopology)" for B
by(auto simp: ν_def measure_restrict_space measure_ν')
have T_inv_measurable[measurable]: "T_inv ∈ ν →⇩M borel_of mtopology"
using continuous_map_measurable[OF continuous_map_from_subtopology_mono[OF T(2) E(1)]]
by(auto simp: ν_def borel_of_subtopology dH
cong: sets_restrict_space_cong[OF sets_ν'] measurable_cong_sets)
define N where "N ≡ distr ν (borel_of mtopology) T_inv"
have N_inP:"N ∈ 𝒫"
using Ni2[of 0,simplified subprob_space_def subprob_space_axioms_def]
by(auto simp: 𝒫_def N_def space_Ni emeasure_distr order.trans[OF emeasure_space ν_le_r] ν.finite_measure_distr)
then interpret wcN:mweak_conv_fin M d "Ni ∘ a" N sequentially
using subset_trans[OF Ni closure_of_subset_topspace] by(auto intro!: inP_mweak_conv_fin_all)
show "∃N r. N ∈ LPm.mtopology closure_of Γ ∧ strict_mono r ∧ limitin LPm.mtopology (Ni ∘ r) N sequentially"
proof(safe intro!: exI[where x=N] exI[where x=a])
show limit: "limitin LPm.mtopology (Ni ∘ a) N sequentially"
proof(rule mweak_conv_imp_converge)
show "mweak_conv_seq (Ni ∘ a) N"
unfolding wcN.mweak_conv_eq2
proof safe
have [measurable]:"UNIV →⇩E {0..1} ∈ sets (borel_of dH.mtopology)"
by(auto simp: borel_of_open)
have 1:"measure ((Ni ∘ a) n) M = measure ((νn ∘ a) n) (UNIV →⇩E {0..1})" for n
using continuous_map_funspace[OF T(1)]
by(auto simp: νn_def measure_distr space_Ni intro!: arg_cong[where f="measure (Ni (a n))"])
have 2: "measure N M = measure ν' (space ν')"
proof -
have [measurable]: "M ∈ sets (borel_of mtopology)"
by(auto intro!: borel_of_open)
have "measure N M = measure ν (T_inv -` M ∩ space ν)"
by(auto simp: N_def intro!: measure_distr)
also have "... = measure ν (space ν ∩ E)"
using measurable_space[OF T_inv_measurable]
by(auto intro!: arg_cong[where f="measure ν"] simp: space_borel_of space_ν)
also have "... = measure ν' (space ν)"
by(rule measure_ν'2[symmetric]) (simp add: space_ν)
also have "... = measure ν' (space ν')"
by(simp add: measure_ν'E space_ν)
finally show ?thesis .
qed
show "(λn. measure ((Ni ∘ a) n) M) ⇢ measure N M"
unfolding 1 2 using HP νn_HP wc.mweak_conv_eq2[THEN iffD1,OF dHs.converge_imp_mweak_conv[OF ν'(3)]]
by(auto simp: space_ν' dHs.inP_iff)
next
fix C
assume C: "closedin mtopology C"
hence [measurable]: "C ∈ sets (borel_of mtopology)"
by(auto intro!: borel_of_closed)
have "closedin (subtopology dH.mtopology A) (T ` C)"
proof -
have "T ` C = {x ∈ topspace (subtopology Hilbert_cube_topology A). T_inv x ∈ C}"
using closedin_subset[OF C] T(3,4) continuous_map_funspace[OF T(1)] continuous_map_funspace[OF T(2)]
by (auto simp: rev_image_eqI)
also note closedin_continuous_map_preimage[OF T(2) C]
finally show ?thesis
by(simp add: dH)
qed
then obtain K where K: "closedin dH.mtopology K" "T ` C = K ∩ A"
by (meson closedin_subtopology)
hence [measurable]: "K ∈ sets (borel_of dH.mtopology)"
by(simp add: borel_of_closed)
have C_eq:"C = T -` K ∩ M"
proof -
have "C = (T -` T ` C) ∩ M"
using closedin_subset[OF C] injT by(auto dest: inj_onD)
also have "... = (T -` (K ∩ A)) ∩ M"
by(simp only: K(2))
also have "... = T -` K ∩ M"
using A(1) continuous_map_funspace[OF T(1)] by auto
finally show ?thesis .
qed
hence 1:"measure ((Ni ∘ a) n) C = measure ((νn ∘ a) n) K" for n
by(auto simp: νn_def measure_distr space_Ni)
have "limsup (λn. ereal (measure ((Ni ∘ a) n) C)) = limsup (λn. ereal (measure ((νn ∘ a) n) K))"
unfolding 1 by simp
also have "... ≤ ereal (measure ν' K)"
using νn_HP HP wc.mweak_conv_eq2[THEN iffD1,OF dHs.converge_imp_mweak_conv[OF ν'(3)]] K(1) dHs.inP_iff by auto
also have "... = ereal (measure ν (K ∩ E))"
by(simp add: measure_ν'2)
also have "... = ereal (measure ν (T_inv -` C ∩ space ν))"
using measurable_space[OF T_inv_measurable] K(2) E(1) closedin_subset[OF K(1)] A(1) T(3,4)
by(fastforce intro!: arg_cong[where f="measure ν"] simp: space_ν C_eq space_borel_of subsetD)
also have "... = ereal (measure N C)"
by(auto simp: N_def measure_distr)
finally show "limsup (λn. ereal (measure ((Ni ∘ a) n) C)) ≤ ereal (measure N C)" .
qed
qed(use N_inP Ni assms closure_of_subset_topspace[of LPm.mtopology Γ] in auto)
have "range (Ni ∘ a) ⊆ LPm.mtopology closure_of Γ"
using Ni by auto
thus "N ∈ LPm.mtopology closure_of Γ"
using limit LPm.metric_closedin_iff_sequentially_closed[THEN iffD1,OF closedin_closure_of[of _ Γ]]
by blast
qed fact
qed
qed(use assms(1) closedin_subset[OF closedin_closure_of[of LPm.mtopology]] in auto)
qed
corollary Prokhorov_theorem_LP:
assumes "Γ ⊆ {N. sets N = sets (borel_of mtopology) ∧ emeasure N (space N) ≤ ennreal r}"
and "separable_space mtopology" mcomplete
shows "compactin LPm.mtopology (LPm.mtopology closure_of Γ) ⟷ tight_on_set mtopology Γ"
proof -
have "Γ ⊆ 𝒫"
using assms(1) by(auto intro!: finite_measureI inP_I simp: top.extremum_unique)
thus ?thesis
using assms by(auto simp: relatively_compact_imp_tight_LP tight_imp_relatively_compact_LP)
qed
subsection ‹ Completeness of the L\'evy-Prokhorov Metric ›
lemma mcomplete_tight_on_set:
assumes "Γ ⊆ 𝒫" mcomplete
and "⋀e f. e > 0 ⟹ f > 0
⟹ ∃an n. an ` {..n::nat} ⊆ M ∧ (∀N∈Γ. measure N (M - (⋃i≤n. mball (an i) f)) ≤ e)"
shows "tight_on_set mtopology Γ"
unfolding tight_on_set_def
proof safe
fix e :: real
assume e: "0 < e"
then have "∃an n. an ` {..n::nat} ⊆ M ∧
(∀N∈Γ. measure N (M - (⋃i≤n. mball (an i) (1 / (1 + real m)))) ≤ e / 2 * (1 / 2) ^ Suc m)" for m
using assms(3)[of "e / 2 * (1 / 2) ^ Suc m" "1 / (1 + real m)"] by fastforce
then obtain anm nm where anm: "⋀m. anm m ` {..nm m::nat} ⊆ M"
"⋀m N. N ∈ Γ ⟹ measure N (M - (⋃i≤nm m. mball (anm m i) (1 / (1 + real m)))) ≤ e/ 2 * (1 / 2)^Suc m"
by metis
define K where "K ≡ (⋂m. (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))"
have K_closed: "closedin mtopology K"
by(auto simp: K_def intro!: closedin_Union)
show "∃K. compactin mtopology K ∧ (∀M∈Γ. measure M (space M - K) < e)"
proof(safe intro!: exI[where x=K])
have "mtotally_bounded K"
unfolding mtotally_bounded_def2
proof safe
fix ε :: real
assume ε: "0 < ε"
then obtain m where m: "1 / (1 + real m) < ε"
using nat_approx_posE by auto
show "∃Ka. finite Ka ∧ Ka ⊆ M ∧ K ⊆ (⋃x∈Ka. mball x ε)"
proof(safe intro!: exI[where x="anm m ` {..nm m}"])
fix x
assume "x ∈ K"
then have "x ∈ (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m)))"
by(auto simp: K_def)
also have "... ⊆ (⋃i≤nm m. mball (anm m i) ε)"
by(rule UN_mono) (use m in auto)
finally show "x ∈ (⋃x∈anm m ` {..nm m}. mball x ε)"
by auto
qed(use anm in auto)
qed
thus "compactin mtopology K"
by(simp add: mtotally_bounded_eq_compact_closedin[OF assms(2) K_closed])
next
fix N
assume N:"N ∈ Γ"
then interpret N: finite_measure N
using assms(1) inP_D(1) by auto
have [measurable]: "M ∈ sets N" "⋀a b. mcball a b ∈ sets N"
using N inP_D(2) assms(1) by(auto intro!: borel_of_closed)
have [measurable]: "⋀a b. mball a b ∈ sets N"
using N inP_D(2) assms(1) by(auto intro!: borel_of_open)
have [simp]: "summable (λm. measure N (M - (⋃i≤nm m. mball (anm m i) (1 / (1 + real m)))))"
using anm(2)[OF N]
by(auto intro!: summable_comparison_test_ev[where g="λn. e / 2 * (1 / 2) ^ Suc n"
and f="λm. measure N (M - (⋃i≤nm m. mball (anm m i) (1 / (1 + real m))))"] eventuallyI)
show "measure N (space N - K) < e"
proof -
have "measure N (space N - K) = measure N (M - K)"
using N assms(1) inP_D(3) by auto
also have "... = measure N (⋃m. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))"
by(auto simp: K_def)
also have "... ≤ (∑m. e / 2 * (1 / 2) ^ Suc m)"
proof -
have "(λk. measure N (⋃m≤k. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m)))))
⇢ measure N (⋃i. ⋃m≤i. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))"
by(rule N.finite_Lim_measure_incseq) (auto intro!: incseq_SucI)
moreover have "(⋃i. ⋃m≤i. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))
= (⋃m. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))"
by blast
ultimately have 1:"(λk. measure N (⋃m≤k. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m)))))
⇢ measure N (⋃m. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))"
by simp
show ?thesis
proof(safe intro!: Lim_bounded[OF 1])
fix n
show "measure N (⋃m≤n. M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m))))
≤ (∑m. e / 2 * (1 / 2) ^ Suc m)" (is "?lhs ≤ ?rhs")
proof -
have "?lhs ≤ (∑m≤n. measure N (M - (⋃i≤nm m. mcball (anm m i) (1 / (1 + real m)))))"
by(rule N.finite_measure_subadditive_finite) auto
also have "... ≤ (∑m≤n. measure N (M - (⋃i≤nm m. mball (anm m i) (1 / (1 + real m)))))"
by(rule sum_mono) (auto intro!: N.finite_measure_mono)
also have "... ≤ (∑m. measure N (M - (⋃i≤nm m. mball (anm m i) (1 / (1 + real m)))))"
by(rule sum_le_suminf) auto
also have "... ≤ ?rhs"
by(rule suminf_le) (use anm(2)[OF N] in auto)
finally show ?thesis .
qed
qed
qed
also have "... = e / 2 * (∑m. (1 / 2) ^ Suc m)"
by(rule suminf_mult) auto
also have "... = e / 2"
using power_half_series sums_unique by fastforce
also have "... < e"
using e by simp
finally show ?thesis .
qed
qed
qed(use assms(1) inP_D in auto)
lemma mcomplete_LPmcomplete:
assumes mcomplete "separable_space mtopology"
shows LPm.mcomplete
proof -
consider "M = {}" | "M ≠ {}"
by blast
then show ?thesis
proof cases
case 1
from M_empty_P[OF this]
have "𝒫 = {} ∨ 𝒫 = {count_space {}}" .
then show ?thesis
using LPm.compact_space_eq_Bolzano_Weierstrass LPm.compact_space_imp_mcomplete finite_subset
by fastforce
next
case M_ne:2
show ?thesis
unfolding LPm.mcomplete_def
proof safe
fix Ni
assume cauchy: "LPm.MCauchy Ni"
hence range_Ni: "range Ni ⊆ 𝒫"
by(auto simp: LPm.MCauchy_def)
hence range_Ni2: "range Ni ⊆ LPm.mtopology closure_of (range Ni)"
by (simp add: closure_of_subset)
have Ni_inP: "⋀i. Ni i ∈ 𝒫"
using cauchy by(auto simp: LPm.MCauchy_def)
hence "⋀n. finite_measure (Ni n)"
and sets_Ni[measurable_cong]:"⋀n. sets (Ni n) = sets (borel_of mtopology)"
and space_Ni: "⋀n. space (Ni n) = M"
by(auto dest: inP_D)
then interpret Ni: finite_measure "Ni n" for n
by simp
have "∃r≥0. ∀i. Ni i (space (Ni i)) ≤ ennreal r"
proof -
obtain N where N: "⋀n m. n ≥ N ⟹ m ≥ N ⟹ LPm (Ni n) (Ni m) < 1"
using LPm.MCauchy_def cauchy zero_less_one by blast
define r where "r = max (Max ((λi. measure (Ni i) (space (Ni i))) ` {..N})) (measure (Ni N) (space (Ni N)) + 1)"
show ?thesis
proof(safe intro!: exI[where x=r])
fix i
consider "i ≤ N" | "N ≤ i"
by fastforce
then show "Ni i (space (Ni i)) ≤ ennreal r"
proof cases
assume "i ≤ N"
then have "measure (Ni i) (space (Ni i)) ≤ r"
by(auto simp: r_def intro!: max.coboundedI1)
thus ?thesis
by (simp add: measure_def enn2real_le)
next
assume i:"i ≥ N"
have "measure (Ni i) (space (Ni i)) ≤ r"
proof -
have "measure (Ni i) M ≤ measure (Ni N) (⋃a∈M. mball a 1) + 1"
using range_Ni by(auto intro!: LPm_less_then[of "Ni N"] N i borel_of_open)
also have "... ≤ measure (Ni N) (space (Ni N)) + 1"
using Ni.bounded_measure by auto
also have "... ≤ r"
by(auto simp: r_def)
finally show ?thesis
by(simp add: space_Ni)
qed
thus ?thesis
by (simp add: Ni.emeasure_eq_measure ennreal_leI)
qed
qed(auto simp: r_def intro!: max.coboundedI2)
qed
then obtain r where r_nonneg: "r ≥ 0" and r_bounded:"⋀i. Ni i (space (Ni i)) ≤ ennreal r"
by blast
with sets_Ni have range_Ni':
"range Ni ⊆ {N. sets N = sets (borel_of mtopology) ∧ emeasure N (space N) ≤ ennreal r}"
by blast
have M_meas[measurable]: "M ∈ sets (borel_of mtopology)"
by(simp add: borel_of_open)
have mball_meas[measurable]: "mball a e ∈ sets (borel_of mtopology)" for a e
by(auto intro!: borel_of_open)
have Ni_Cauchy: "⋀e. e > 0 ⟹ ∃n0. ∀n n'. n0 ≤ n ⟶ n0 ≤ n' ⟶ LPm (Ni n) (Ni n') < e"
using cauchy by(auto simp: LPm.MCauchy_def)
have "tight_on_set mtopology (range Ni)"
proof(rule mcomplete_tight_on_set[OF range_Ni assms(1)])
fix e f :: real
assume e: "e > 0" and f: "f > 0"
with Ni_Cauchy[of "min e f / 2"] obtain n0 where n0:
"⋀n m. n0 ≤ n ⟹ n0 ≤ m ⟹ LPm (Ni n) (Ni m) < min e f / 2"
by fastforce
obtain D where D: "mdense D" "countable D"
using assms(2) separable_space_def2 by blast
then obtain an where an: "⋀n::nat. an n ∈ D" "range an = D"
by (metis M_ne mdense_empty_iff rangeI uncountable_def)
have "∃n1. ∀i≤n0. measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))) ≤ min e f / 2"
proof -
have "∃n1. measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))) ≤ min e f / 2" for i
proof -
have "(λn1. measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2)))) ⇢ 0"
proof -
have 1: "(λn1. measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))))
= (λn1. measure (Ni i) M - measure (Ni i) ((⋃i≤n1. mball (an i) (f / 2))))"
using Ni.finite_measure_compl by(auto simp: space_Ni)
have "(λn1. measure (Ni i) ((⋃i≤n1. mball (an i) (f / 2)))) ⇢ measure (Ni i) M"
proof -
have "(λn1. measure (Ni i) ((⋃i≤n1. mball (an i) (f / 2))))
⇢ measure (Ni i) (⋃n1. (⋃i≤n1. mball (an i) (f / 2)))"
by(intro Ni.finite_Lim_measure_incseq incseq_SucI UN_mono) auto
moreover have "(⋃n1. (⋃i≤n1. mball (an i) (f / 2))) = M"
using mdense_balls_cover[OF D(1)[simplified an(2)[symmetric]],of "f / 2"] f by auto
ultimately show ?thesis by argo
qed
from tendsto_diff[OF tendsto_const[where k="measure (Ni i) M"] this] show ?thesis
unfolding 1 by simp
qed
thus ?thesis
by (meson e f LIMSEQ_le_const half_gt_zero less_eq_real_def linorder_not_less min_less_iff_conj)
qed
then obtain ni where ni: "⋀i. measure (Ni i) (M - (⋃i≤ni i. mball (an i) (f / 2))) ≤ min e f / 2"
by metis
define n1 where "n1 ≡ Max (ni ` {..n0})"
show ?thesis
proof(safe intro!: exI[where x=n1])
fix i
assume i: "i ≤ n0"
then have nii:"ni i ≤ n1"
by (simp add: n1_def)
show "measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))) ≤ min e f / 2"
proof -
have "measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2)))
≤ measure (Ni i) (M - (⋃i≤ni i. mball (an i) (f / 2)))"
using nii by(fastforce intro!: Ni.finite_measure_mono)
also have "... ≤ min e f / 2"
by fact
finally show ?thesis .
qed
qed
qed
then obtain n1 where n1:
"⋀i. i ≤ n0 ⟹ measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))) ≤ e / 2"
"⋀i. i ≤ n0 ⟹ measure (Ni i) (M - (⋃i≤n1. mball (an i) (f / 2))) ≤ f / 2"
by auto
show "∃an n. an ` {..n::nat} ⊆ M ∧ (∀N∈range Ni. measure N (M - (⋃i≤n. mball (an i) f)) ≤ e)"
proof(safe intro!: exI[where x=an] exI[where x=n1])
fix n
consider "n ≤ n0" | "n0 ≤ n"
by linarith
then show "measure (Ni n) (M - (⋃i≤n1. mball (an i) f)) ≤ e"
proof cases
case 1
have "measure (Ni n) (M - (⋃i≤n1. mball (an i) f))
≤ measure (Ni n) (M - (⋃i≤n1. mball (an i) (f / 2)))"
using f by(fastforce intro!: Ni.finite_measure_mono)
also have "... ≤ e"
using n1[OF 1] e by linarith
finally show ?thesis .
next
case 2
have "measure (Ni n) (M - (⋃i≤n1. mball (an i) f))
≤ measure (Ni n0) (⋃a∈M - (⋃i≤n1. mball (an i) f). mball a (min e f / 2)) + min e f / 2"
by(intro LPm_less_then(2) n0 2 Ni_inP) auto
also have "... ≤ measure (Ni n0) (M - (⋃i≤n1. mball (an i) (f / 2))) + min e f / 2"
proof -
have "(⋃a∈M - (⋃i≤n1. mball (an i) f). mball a (min e f / 2))
⊆ M - (⋃i≤n1. mball (an i) (f / 2))"
proof safe
fix x a i
assume x: "x ∈ mball a (min e f / 2)" "x ∈ mball (an i) (f / 2)"
and a:"a ∈ M" "a ∉ (⋃i≤n1. mball (an i) f)" and i:"i ≤ n1"
hence "d (an i) x < f / 2" "d x a < f / 2"
by(auto simp: commute)
hence "d (an i) a < f"
using triangle[of "an i" x a] a(1) x(2) by auto
with a(2) i
show False
using a(1) atMost_iff image_eqI x(2) by auto
qed simp
thus ?thesis
by(auto intro!: Ni.finite_measure_mono)
qed
also have "... ≤ e"
using n1(1)[OF order.refl] by linarith
finally show ?thesis .
qed
qed(use an dense_in_subset[OF D(1)] in auto)
qed
from tight_imp_relatively_compact_LP[OF range_Ni' assms(2) this] range_Ni2
obtain l N where "strict_mono l" "limitin LPm.mtopology (Ni ∘ l) N sequentially"
unfolding LPm.compactin_sequentially by blast
from LPm.MCauchy_convergent_subsequence[OF cauchy this]
show "∃N. limitin LPm.mtopology Ni N sequentially"
by blast
qed
qed
qed
subsection ‹ Equivalence of Separability, Completeness, and Compactness ›
lemma return_inP[simp]:"return (borel_of mtopology) x ∈ 𝒫"
by (metis emeasure_empty ennreal_top_neq_zero finite_measureI inP_I infinity_ennreal_def sets_return space_return subprob_space.axioms(1) subprob_space_return_ne)
lemma LPm_return_eq:
assumes "x ∈ M" "y ∈ M"
shows "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) = min 1 (d x y)"
proof(rule antisym[OF min.boundedI])
show "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) ≤ d x y"
proof(rule field_le_epsilon)
fix e :: real
assume e: "e > 0"
show "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) ≤ d x y + e"
proof(rule LPm_imp_le)
fix B
assume B[measurable]: "B ∈ sets (borel_of mtopology)"
have "x ∈ B ⟹ y ∈ (⋃a∈B. mball a (d x y + e))"
using e assms by auto
thus "measure (return (borel_of mtopology) x) B
≤ measure (return (borel_of mtopology) y) (⋃a∈B. mball a (d x y + e)) + (d x y + e)"
using e by(simp add: measure_return indicator_def)
next
fix B
assume B[measurable]: "B ∈ sets (borel_of mtopology)"
have "y ∈ B ⟹ x ∈ (⋃a∈B. mball a (d x y + e))"
using e assms by (auto simp: commute)
thus "measure (return (borel_of mtopology) y) B
≤ measure (return (borel_of mtopology) x) (⋃a∈B. mball a (d x y + e)) + (d x y + e)"
using e by(simp add: measure_return indicator_def)
qed (simp add: add.commute add_pos_nonneg e)
qed
next
consider "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) < 1"
| "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) ≥ 1"
by linarith
then show "min 1 (d x y)≤ LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y)"
proof cases
case 1
have 2:"d x y < a" if a: "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) < a"
"a < 1" for a
proof -
have [measurable]: "{x} ∈ sets (borel_of mtopology)"
using assms by(auto simp add: closedin_t1_singleton t1_space_mtopology intro!: borel_of_closed)
have "measure (return (borel_of mtopology) x) {x}
≤ measure (return (borel_of mtopology) y) (⋃b∈{x}. mball b a) + a"
using assms subprob_space.subprob_emeasure_le_1[OF subprob_space_return_ne[of "borel_of mtopology"]]
by(intro LPm_less_then(1)[where A="{x}",OF _ _ a(1)])
(auto simp: space_borel_of space_scale_measure)
thus ?thesis
using assms a(2) linorder_not_less by(fastforce simp: measure_return indicator_def)
qed
have "d x y < a" if a: "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) < a" for a
proof(cases "a < 1")
assume r1:"~ a < 1"
obtain k where k:"LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) < k" "k < 1"
using dense 1 by blast
show ?thesis
using 2[OF k] k(2) r1 by linarith
qed(use 2 a in auto)
thus ?thesis
by force
qed simp
next
show "LPm (return (borel_of mtopology) x) (return (borel_of mtopology) y) ≤ 1"
by(rule order.trans[OF LPm_le_max_measure])
(metis assms(1) assms(2) indicator_simps(1) max.idem measure_return nle_le sets.top space_borel_of space_return topspace_mtopology)
qed
corollary LPm_return_eq_capped_dist:
assumes "x ∈ M" "y ∈ M"
shows "LPm (return (borel_of mtopology) x)(return (borel_of mtopology) y) = capped_dist 1 x y"
by(simp add: capped_dist_def assms LPm_return_eq)
corollary MCauchy_iff_MCauchy_return:
assumes "range xn ⊆ M"
shows "MCauchy xn ⟷ LPm.MCauchy (λn. return (borel_of mtopology) (xn n))"
proof -
interpret c: Metric_space M "capped_dist 1"
using capped_dist by blast
show ?thesis
using range_subsetD[OF assms(1)]
by(auto simp: MCauchy_capped_metric[of 1,symmetric] c.MCauchy_def LPm.MCauchy_def LPm_return_eq_capped_dist)
qed
lemma conv_conv_return:
assumes "limitin mtopology xn x sequentially"
shows "limitin LPm.mtopology (λn. return (borel_of mtopology) (xn n)) (return (borel_of mtopology) x) sequentially"
proof -
interpret c: Metric_space M "capped_dist 1"
using capped_dist by blast
have clim:"limitin c.mtopology xn x sequentially"
using assms by (simp add: mtopology_capped_metric)
show ?thesis
using LPm_return_eq_capped_dist clim
by(fastforce simp: c.limit_metric_sequentially LPm.limit_metric_sequentially)
qed
lemma conv_iff_conv_return:
assumes "range xn ⊆ M" "x ∈ M"
shows "limitin mtopology xn x sequentially
⟷ limitin LPm.mtopology (λn. return (borel_of mtopology) (xn n))
(return (borel_of mtopology) x) sequentially"
proof -
have xn: "⋀n. xn n ∈ M"
using assms by auto
interpret c: Metric_space M "capped_dist 1"
using capped_dist by blast
have "limitin mtopology xn x sequentially ⟷ limitin c.mtopology xn x sequentially"
by (simp add: mtopology_capped_metric)
also have "...
⟷ limitin LPm.mtopology (λn. return (borel_of mtopology) (xn n)) (return (borel_of mtopology) x) sequentially"
using xn assms by(auto simp: c.limit_metric_sequentially LPm.limit_metric_sequentially LPm_return_eq_capped_dist)
finally show ?thesis .
qed
lemma continuous_map_return: "continuous_map mtopology LPm.mtopology (λx. return (borel_of mtopology) x)"
by(auto simp: continuous_map_iff_limit_seq[OF first_countable_mtopology] conv_conv_return)
lemma homeomorphic_map_return:
"homeomorphic_map mtopology
(subtopology LPm.mtopology ((λx. return (borel_of mtopology) x) ` M))
(λx. return (borel_of mtopology) x)"
proof(rule homeomorphic_maps_imp_map)
define inv where "inv ≡ (λN. THE x. x ∈ M ∧ N = return (borel_of mtopology) x)"
have inv_eq: "inv (return (borel_of mtopology) x) = x" if x: "x ∈ M" for x
proof -
have "inv (return (borel_of mtopology) x) ∈ M ∧ return (borel_of mtopology) x
= return (borel_of mtopology) (inv (return (borel_of mtopology) x))"
unfolding inv_def
proof(rule theI)
fix y
assume "y ∈ M ∧ return (borel_of mtopology) x = return (borel_of mtopology) y"
then show "y = x"
using LPm_return_eq[OF x,of y] x
by (auto intro!: zero[THEN iffD1] simp: commute simp del: zero)
qed(use x in auto)
thus ?thesis
by (metis LPm_return_eq_capped_dist Metric_space.zero capped_dist x)
qed
interpret s: Submetric 𝒫 LPm "(λx. return (borel_of mtopology) x) ` M"
by standard auto
have "continuous_map mtopology s.sub.mtopology (λx. return (borel_of mtopology) x)"
using continuous_map_return
by (simp add: LPm.Metric_space_axioms metric_continuous_map s.sub.Metric_space_axioms)
moreover have "continuous_map s.sub.mtopology mtopology inv"
unfolding continuous_map_iff_limit_seq[OF s.sub.first_countable_mtopology]
proof safe
fix Ni N
assume h:"limitin s.sub.mtopology Ni N sequentially"
then obtain x where x: "x ∈ M" "N = return (borel_of mtopology) x"
using s.sub.limit_metric_sequentially by auto
interpret c: Metric_space M "capped_dist 1"
using capped_dist by blast
show "limitin mtopology (λn. inv (Ni n)) (inv N) sequentially"
unfolding c.limit_metric_sequentially mtopology_capped_metric[of 1,symmetric]
proof safe
fix e :: real
assume "e > 0"
then obtain n0 where n0:
"⋀n. n ≥ n0 ⟹ Ni n ∈ (λx. return (borel_of mtopology) x) ` M"
"⋀n. n ≥ n0 ⟹ LPm (Ni n) N < e"
by (metis h s.sub.limit_metric_sequentially)
then obtain xn where xn: "⋀n. n ≥ n0 ⟹ xn n ∈ M"
"⋀n. n ≥ n0 ⟹ Ni n = return (borel_of mtopology) (xn n)"
unfolding image_def by simp metis
thus "∃Na. ∀n≥Na. inv (Ni n) ∈ M ∧ capped_dist 1 (inv (Ni n)) (inv N) < e"
using n0 by(auto intro!: exI[where x=n0] simp: inv_eq x LPm_return_eq_capped_dist)
qed(simp add: inv_eq x)
qed
moreover have "∀x∈topspace mtopology. inv (return (borel_of mtopology) x) = x"
"∀y∈topspace s.sub.mtopology. return (borel_of mtopology) (inv y) = y"
by(auto simp: inv_eq)
ultimately show "homeomorphic_maps mtopology (subtopology LPm.mtopology ((λx. return (borel_of mtopology) x) ` M))
(λx. return (borel_of mtopology) x) inv"
by(simp add: s.mtopology_submetric homeomorphic_maps_def)
qed
corollary homeomorphic_space_mtopology_return:
"mtopology homeomorphic_space (subtopology LPm.mtopology ((λx. return (borel_of mtopology) x) ` M))"
using homeomorphic_map_return homeomorphic_space by fast
lemma closedin_returnM: "closedin LPm.mtopology ((λx. return (borel_of mtopology) x) ` M)"
unfolding LPm.metric_closedin_iff_sequentially_closed
proof safe
fix Ni N
assume h:"range Ni ⊆ (λx. return (borel_of mtopology) x) ` M" "limitin LPm.mtopology Ni N sequentially"
from range_subsetD[OF this(1)]
obtain xi where xi: "⋀i. xi i ∈ M" "Ni = (λi. return (borel_of mtopology) (xi i))"
unfolding image_def by simp metis
have sets_N[measurable_cong]: "sets N = sets (borel_of mtopology)"
by (meson LPm.limitin_mspace h(2) inP_D)
have [measurable]:"⋀n. {xi n} ∈ sets N"
by (simp add: Hausdorff_space_mtopology borel_of_closed closedin_Hausdorff_sing_eq sets_N xi(1))
interpret N: finite_measure N
by (meson LPm.limitin_metric_dist_null h(2) inP_D(1))
interpret Ni: prob_space "Ni i" for i
by(auto intro!: prob_space_return simp: xi space_borel_of)
have N_r: "ereal (measure N A) ≤ ereal 1" for A
unfolding ereal_less_eq(3)
proof(rule order.trans[OF N.bounded_measure])
interpret mweak_conv_fin M d Ni N sequentially
using limitin_topspace[OF h(2)] by(auto intro!: inP_mweak_conv_fin inP_I return_inP simp: xi(2))
have "mweak_conv_seq Ni N"
using converge_imp_mweak_conv h(2) xi(2) by force
from mweak_conv_imp_limit_space[OF this]
show "measure N (space N) ≤ 1"
by(auto intro!: tendsto_upperbound[where F=sequentially and f="λn. Ni.prob n (space N)"] simp: space_N space_Ni)
qed
have "∃x. limitin mtopology xi x sequentially"
proof(rule ccontr)
assume contr:"∄x. limitin mtopology xi x sequentially"
have MCauchy_xi: "MCauchy xi"
using MCauchy_iff_MCauchy_return[THEN iffD2,of xi,
OF _ LPm.convergent_imp_MCauchy[OF _ h(2)[simplified xi(2)]]] xi
by fastforce
have 0:"∄x. limitin mtopology (xi ∘ a) x sequentially" if a: "strict_mono a" for a :: "nat ⇒ nat"
using MCauchy_convergent_subsequence[OF MCauchy_xi a] contr by blast
have inf: "infinite (range xi)"
by (metis 0 Bolzano_Weierstrass_property MCauchy_xi MCauchy_def finite_subset preorder_class.order.refl)
have cl: "closedin mtopology (range (xi ∘ a))" if a: "strict_mono a" for a :: "nat ⇒ nat"
unfolding closedin_metric
proof safe
fix x
assume x:"x ∈ M" "x ∉ range (xi ∘ a)"
from 0 a have "¬ limitin mtopology (xi ∘ a) x sequentially"
by blast
then obtain e where e: "e > 0" "⋀n0. ∃n≥n0. d ((xi ∘ a) n) x ≥ e"
using xi(1) x by(fastforce simp: limit_metric_sequentially)
then obtain n0 where n0: "⋀n m. n ≥ n0 ⟹ m ≥ n0 ⟹ d ((xi ∘ a) n) ((xi ∘ a) m) < e / 2"
using MCauchy_subsequence[OF a MCauchy_xi]
by (meson MCauchy_def zero_less_divide_iff zero_less_numeral)
obtain n1 where n1: "n1 ≥ n0" "d ((xi ∘ a) n1) x ≥ e"
using e(2) by blast
define e' where "e' ≡ Min ((λn. d x ((xi ∘ a) n))` {..n0})"
have e'_pos: "e' > 0"
unfolding e'_def using x xi(1) by(subst linorder_class.Min_gr_iff) auto
have "d x ((xi ∘ a) n) ≥ min (e / 2) e'" for n
proof(cases "n ≤ n0")
assume "¬ n ≤ n0"
then have "d ((xi ∘ a) n) ((xi ∘ a) n1) < e / 2"
using n1(1) n0 by simp
hence "e / 2 ≤ d x ((xi ∘ a) n1) - d ((xi ∘ a) n) ((xi ∘ a) n1)"
using n1(2) by(simp add: commute)
also have "... ≤ d x ((xi ∘ a) n)"
using triangle[OF x(1) xi(1)[of "a n"] xi(1)[of "a n1"]] by simp
finally show ?thesis
by simp
qed(auto intro!: linorder_class.Min_le min.coboundedI2 simp: e'_def)
thus "∃r>0. disjnt (range (xi ∘ a)) (mball x r)"
using e'_pos e(1) x(1) xi(1) linorder_not_less
by(fastforce intro!: exI[where x="min (e / 2) e'"] simp: disjnt_def simp del: min_less_iff_conj)
qed(use xi in auto)
hence meas: "strict_mono a ⟹ (range (xi ∘ a)) ∈ sets (borel_of mtopology)" for a :: "nat ⇒ nat"
by(auto simp: borel_of_closed)
have 1:"measure N (range (xi ∘ a)) = 1" if a: "strict_mono a" for a :: "nat ⇒ nat"
proof -
interpret mweak_conv_fin M d Ni N sequentially
using limitin_topspace[OF h(2)] xi(1) by(auto intro!: inP_mweak_conv_fin simp: xi(2))
have "mweak_conv_seq Ni N"
using converge_imp_mweak_conv[OF h(2)] xi(2) by simp
hence *: "closedin mtopology A ⟹ limsup (λn. ereal (measure (Ni n) A)) ≤ ereal (measure N A)" for A
using mweak_conv_eq2 by blast
have "ereal 1 ≤ limsup (λn. ereal (measure (Ni n) (range (xi ∘ a))))"
using meas[OF a] seq_suble[OF a]
by(auto simp: limsup_INF_SUP le_Inf_iff le_Sup_iff xi(2) measure_return indicator_def one_ereal_def)
also have "... ≤ ereal (measure N (range (xi ∘ a)))"
by(intro * a cl)
finally show ?thesis
using N_r by(auto intro!: antisym)
qed
have 2:"measure N {xi n} = 0" for n
proof -
have "infinite {i. xi i ≠ xi n}"
proof
assume "finite {i. xi i ≠ xi n}"
then have "finite (xi ` {i. xi i ≠ xi n})"
by blast
moreover have "(xi ` {i. xi i ≠ xi n}) = range xi - {xi n}"
by auto
ultimately show False
using inf by auto
qed
from infinite_enumerate[OF this]
obtain a :: "nat ⇒ nat" where r: "strict_mono a" "⋀i. a i ∈ {i. xi i ≠ xi n}"
by blast
hence disj: "range (xi ∘ a) ∩ {xi n} = {}"
by fastforce
from N.finite_measure_Union[OF _ _ this]
have "measure N (range (xi ∘ a) ∪ {xi n}) = 1 + measure N {xi n}"
using meas[OF r(1)] 1[OF r(1)] by simp
thus ?thesis
using N_r[of "range (xi ∘ a) ∪ {xi n}"] measure_nonneg[of N "{xi n}"] by simp
qed
have "measure N (range xi) = 0"
proof -
have count: "countable (range xi)"
by blast
define Xn where "Xn ≡ (λn. {from_nat_into (range xi) n})"
have Un_Xn: "range xi = (⋃n. Xn n)"
using bij_betw_from_nat_into[OF count inf] by (simp add: UNION_singleton_eq_range Xn_def)
have disjXn: "disjoint_family Xn"
using bij_betw_from_nat_into[OF count inf] by (simp add: inf disjoint_family_on_def Xn_def)
have [measurable]: "⋀n. Xn n ∈ sets N"
using bij_betw_from_nat_into[OF count inf]
by (metis UNIV_I Xn_def ‹⋀n. {xi n} ∈ sets N› bij_betw_iff_bijections image_iff)
have eq0: "⋀n. measure N (Xn n) = 0"
by (metis bij_betw_from_nat_into[OF count inf] 2 UNIV_I Xn_def bij_betw_imp_surj_on image_iff)
have "measure N (range xi) = measure N (⋃n. Xn n)"
by(simp add: Un_Xn)
also have "... = (∑n. measure N (Xn n))"
using N.suminf_measure[OF _ disjXn] by fastforce
also have "... = 0"
by(simp add: eq0)
finally show ?thesis .
qed
with 1[OF strict_mono_id] show False by simp
qed
then obtain x where x: "limitin mtopology xi x sequentially"
by blast
show "N ∈ (λx. return (borel_of mtopology) x) ` M"
using limitin_topspace[OF x] by(simp add: LPm.limitin_metric_unique[OF h(2)[simplified xi(2)] conv_conv_return[OF x]])
qed simp
corollary separable_iff_LPm_separable: "separable_space mtopology ⟷ separable_space LPm.mtopology"
using homeomorphic_space_second_countability[OF homeomorphic_space_mtopology_return] separable_LPm
by(auto simp: separable_space_iff_second_countable LPm.separable_space_iff_second_countable second_countable_subtopology)
corollary LPmcomplete_mcomplete:
assumes LPm.mcomplete
shows mcomplete
unfolding mcomplete_def
proof safe
fix xn
assume h: "MCauchy xn"
hence 1: "range xn ⊆ M"
using MCauchy_def by blast
interpret Submetric 𝒫 LPm "(λx. return (borel_of mtopology) x) ` M"
by (metis LPm.Metric_space_axioms LPm.topspace_mtopology Submetric.intro Submetric_axioms.intro closedin_returnM closedin_subset)
have "sub.mcomplete"
using assms(1) closedin_eq_mcomplete closedin_returnM by blast
moreover have "sub.MCauchy (λn. return (borel_of mtopology) (xn n))"
using MCauchy_iff_MCauchy_return[OF 1] 1 by (simp add: MCauchy_submetric h image_subset_iff)
ultimately obtain x where
x: "x ∈ M" "limitin LPm.mtopology (λn. return (borel_of mtopology) (xn n))
(return (borel_of mtopology) x) sequentially"
unfolding sub.mcomplete_def limitin_submetric_iff by blast
thus "∃x. limitin mtopology xn x sequentially"
by(auto simp: conv_iff_conv_return[OF 1 x(1),symmetric])
qed
corollary mcomplete_iff_LPmcomplete: "separable_space mtopology ⟹ mcomplete ⟷ LPm.mcomplete"
by(auto simp add: mcomplete_LPmcomplete LPmcomplete_mcomplete)
lemma LPmcompact_imp_mcompact: "compact_space LPm.mtopology ⟹ compact_space mtopology"
by (meson closedin_compact_space closedin_returnM compact_space_subtopology homeomorphic_compact_space homeomorphic_space_mtopology_return)
end
corollary Polish_space_weak_conv_topology:
assumes "Polish_space X"
shows "Polish_space (weak_conv_topology X)"
proof -
obtain d where d:"Metric_space (topspace X) d" "Metric_space.mcomplete (topspace X) d"
"Metric_space.mtopology (topspace X) d = X"
by (metis Metric_space.topspace_mtopology assms completely_metrizable_space_def Polish_space_imp_completely_metrizable_space)
then interpret Levy_Prokhorov "topspace X" d
by(auto simp: Levy_Prokhorov_def)
have "separable_space mtopology"
by (simp add: assms d(3) Polish_space_imp_separable_space)
thus ?thesis
using LPm.Polish_space_mtopology LPmtopology_eq_weak_conv_topology d(2) d(3) mcomplete_LPmcomplete separable_LPm by force
qed
subsection ‹ Prokhorov Theorem for Topology of Weak Convergence ›
lemma relatively_compact_imp_tight:
assumes "Polish_space X" "Γ ⊆ {N. sets N = sets (borel_of X) ∧ finite_measure N}"
and "compactin (weak_conv_topology X) (weak_conv_topology X closure_of Γ)"
shows "tight_on_set X Γ"
proof -
obtain d where d:"Metric_space (topspace X) d" "Metric_space.mcomplete (topspace X) d"
"Metric_space.mtopology (topspace X) d = X"
by (metis Metric_space.topspace_mtopology assms(1) completely_metrizable_space_def Polish_space_imp_completely_metrizable_space)
note sep = Polish_space_imp_separable_space[OF assms(1)]
hence sep':"separable_space (Metric_space.mtopology (topspace X) d)"
by(simp add: d)
interpret Levy_Prokhorov "topspace X" d
by(auto simp: d Levy_Prokhorov_def)
show ?thesis
using relatively_compact_imp_tight_LP[of Γ] assms sep inP_iff
by(fastforce simp add: d LPmtopology_eq_weak_conv_topology[OF sep'])
qed
lemma tight_imp_relatively_compact:
assumes "metrizable_space X" "separable_space X"
"Γ ⊆ {N. N (space N) ≤ ennreal r ∧ sets N = sets (borel_of X)}"
and "tight_on_set X Γ"
shows "compactin (weak_conv_topology X) (weak_conv_topology X closure_of Γ)"
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)
hence sep':"separable_space (Metric_space.mtopology (topspace X) d)"
by(simp add: d assms)
show ?thesis
proof(cases "r ≤ 0")
assume "r ≤ 0"
then have "{N. N (space N) ≤ ennreal r ∧ sets N = sets (borel_of X)} = {null_measure (borel_of X)}"
by(fastforce simp: ennreal_neg le_zero_eq[THEN iffD1,OF order.trans[OF emeasure_space]] intro!: measure_eqI)
then have "Γ = {} ∨ Γ = {null_measure (borel_of X)}"
using assms(3) by auto
moreover have "weak_conv_topology X closure_of {null_measure (borel_of X)} = {null_measure (borel_of X)}"
by(intro closure_of_eq[THEN iffD2] closedin_Hausdorff_singleton metrizable_imp_Hausdorff_space
metrizable_space_subtopology metrizable_weak_conv_topology assms)
(auto intro!: finite_measureI)
ultimately show ?thesis
by (auto intro!: finite_measureI)
next
assume "¬ r ≤ 0"
then interpret Levy_Prokhorov "topspace X" d
by(auto simp: d Levy_Prokhorov_def)
show ?thesis
using tight_imp_relatively_compact_LP[of Γ] assms
by(auto simp add: d LPmtopology_eq_weak_conv_topology[OF sep'])
qed
qed
lemma Prokhorov:
assumes "Polish_space X" "Γ ⊆ {N. N (space N) ≤ ennreal r ∧ sets N = sets (borel_of X)}"
shows "tight_on_set X Γ ⟷ compactin (weak_conv_topology X) (weak_conv_topology X closure_of Γ)"
proof -
have "Γ ⊆ {N. sets N = sets (borel_of X) ∧ finite_measure N}"
using assms(2) by(auto intro!: finite_measureI simp: top.extremum_unique)
thus ?thesis
using relatively_compact_imp_tight tight_imp_relatively_compact assms
Polish_space_imp_metrizable_space Polish_space_imp_separable_space
by (metis (mono_tags, lifting))
qed
corollary tight_on_set_imp_convergent_subsequence:
fixes Ni :: "nat ⇒ _ measure"
assumes "metrizable_space X" "separable_space X"
and "tight_on_set X (range Ni)" "⋀i. (Ni i) (space (Ni i)) ≤ ennreal r"
shows "∃a N. strict_mono a ∧ finite_measure N ∧ sets N = sets (borel_of X)
∧ N (space N) ≤ ennreal r ∧ weak_conv_on (Ni ∘ a) N sequentially X"
proof(cases "r ≤ 0")
case True
then have "Ni = (λi. null_measure (borel_of X))"
using assms(3) order.trans[OF emeasure_space assms(4)]
by(auto simp: tight_on_set_def ennreal_neg intro!: measure_eqI)
thus?thesis
using weak_conv_on_const[of Ni]
by(auto intro!: exI[where x=id] exI[where x="null_measure (borel_of X)"] strict_mono_id finite_measureI)
next
case False
then have r[arith]:"r > 0" by linarith
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 d: Metric_space "topspace X" d
by blast
interpret Levy_Prokhorov "topspace X" d
by(auto simp: Levy_Prokhorov_def d )
have range_Ni: "range Ni ⊆ {N. N (space N) ≤ ennreal r ∧ sets N = sets (borel_of X)}"
using assms(3,4) by(auto simp: tight_on_set_def)
hence Ni_fin: "⋀i. finite_measure (Ni i)"
by (meson assms(3) range_eqI tight_on_set_def)
have range_Ni':"LPm.mtopology closure_of range Ni
⊆ {N. N (space N) ≤ ennreal r ∧ sets N = sets (borel_of X)}"
by (metis (no_types, lifting) Collect_cong closedin_bounded_measures closure_of_minimal d(2) range_Ni)
have "compactin LPm.mtopology (LPm.mtopology closure_of (range Ni))"
using assms(2,3) range_Ni by(auto intro!: tight_imp_relatively_compact_LP simp: d(2))
from LPm.compactin_sequentially[THEN iffD1,OF this] range_Ni
obtain a N where "N ∈ LPm.mtopology closure_of range Ni" "strict_mono a"
"limitin LPm.mtopology (Ni ∘ a) N sequentially"
by (metis (no_types, lifting) LPm.topspace_mtopology assms(3) closure_of_subset d(2) inP_I subsetI tight_on_set_def)
moreover hence "finite_measure N" "sets N = sets (borel_of X)" "N (space N) ≤ ennreal r"
using range_Ni' by (auto simp add: LPm.limitin_metric inP_iff)
ultimately show ?thesis
using range_Ni Ni_fin assms(4)
by(fastforce intro!: converge_imp_mweak_conv[simplified d] exI[where x=a] exI[where x=N] inP_I
simp: image_subset_iff d(2))
qed
end