Theory Lemmas_Levy_Prokhorov
section ‹Preliminaries›
theory Lemmas_Levy_Prokhorov
imports "Standard_Borel_Spaces.StandardBorel"
begin
lemma(in Metric_space) [measurable]:
shows mball_sets: "mball x e ∈ sets (borel_of mtopology)"
and mcball_sets: "mcball x e ∈ sets (borel_of mtopology)"
by(auto simp: borel_of_open borel_of_closed)
lemma Metric_space_eq_MCauchy:
assumes "Metric_space M d" "⋀x y. x ∈ M ⟹ y ∈ M ⟹ d x y = d' x y"
and "⋀x y. d' x y = d' y x" "⋀x y. d' x y ≥ 0"
shows "Metric_space.MCauchy M d xn ⟷ Metric_space.MCauchy M d' xn"
proof -
interpret d: Metric_space M d by fact
interpret d': Metric_space M d'
using Metric_space_eq assms d.Metric_space_axioms by blast
show ?thesis
using assms(2) by(auto simp: d.MCauchy_def d'.MCauchy_def subsetD)
qed
lemma borel_of_compact: "Hausdorff_space X ⟹ compactin X K ⟹ K ∈ sets (borel_of X)"
by(auto intro!: borel_of_closed compactin_imp_closedin)
lemma prob_algebra_cong: "sets M = sets N ⟹ prob_algebra M = prob_algebra N"
by(simp add: prob_algebra_def cong: subprob_algebra_cong)
lemma topology_eq_closedin: "X = Y ⟷ (∀C. closedin X C ⟷ closedin Y C)"
unfolding topology_eq
by (metis closedin_def closedin_topspace openin_closedin_eq openin_topspace subset_antisym)
text ‹ Another version of @{thm finite_measure.countable_support}›
lemma(in finite_measure) countable_support_sets:
assumes "disjoint_family_on Ai D"
shows "countable {i∈D. measure M (Ai i) ≠ 0}"
proof cases
assume "measure M (space M) = 0"
with bounded_measure measure_le_0_iff have [simp]:"{i∈D. measure M (Ai i) ≠ 0} = {}"
by auto
show ?thesis
by simp
next
let ?M = "measure M (space M)" and ?m = "λi. measure M (Ai i)"
assume "?M ≠ 0"
then have *: "{i∈D. ?m i ≠ 0} = (⋃n. {i∈D. ?M / Suc n < ?m i})"
using reals_Archimedean[of "?m x / ?M" for x]
by (auto simp: field_simps not_le[symmetric] divide_le_0_iff measure_le_0_iff)
have **: "⋀n. finite {i∈D. ?M / Suc n < ?m i}"
proof (rule ccontr)
fix n assume "infinite {i∈D. ?M / Suc n < ?m i}" (is "infinite ?X")
then obtain X where "finite X" "card X = Suc (Suc n)" "X ⊆ ?X"
by (meson infinite_arbitrarily_large)
from this(3) have *: "⋀x. x ∈ X ⟹ ?M / Suc n ≤ ?m x"
by auto
{ fix i assume "i ∈ X"
from ‹?M ≠ 0› *[OF this] have "?m i ≠ 0" by (auto simp: field_simps measure_le_0_iff)
then have "Ai i ∈ sets M" by (auto dest: measure_notin_sets) }
note sets_Ai = this
have disj: "disjoint_family_on Ai X"
using ‹X ⊆ ?X› assms by(auto simp: disjoint_family_on_def)
have "?M < (∑x∈X. ?M / Suc n)"
using ‹?M ≠ 0›
by (simp add: ‹card X = Suc (Suc n)› field_simps less_le)
also have "… ≤ (∑x∈X. ?m x)"
by (rule sum_mono) fact
also have "… = measure M (⋃i∈X. Ai i)"
using sets_Ai ‹finite X› by (intro finite_measure_finite_Union[symmetric,OF _ _ disj])
(auto simp: disjoint_family_on_def)
finally have "?M < measure M (⋃i∈X. Ai i)" .
moreover have "measure M (⋃i∈X. Ai i) ≤ ?M"
using sets_Ai[THEN sets.sets_into_space] by (intro finite_measure_mono) auto
ultimately show False by simp
qed
show ?thesis
unfolding * by (intro countable_UN countableI_type countable_finite[OF **])
qed
subsection ‹ Finite Sum of Measures ›
definition sum_measure :: "'b measure ⇒ 'a set ⇒ ('a ⇒ 'b measure) ⇒ 'b measure" where
"sum_measure M I Mi ≡ measure_of (space M) (sets M) (λA. ∑i∈I. emeasure (Mi i) A)"
lemma sum_measure_cong:
assumes "sets M = sets M'" "⋀i. i ∈ I ⟹ N i = N' i"
shows "sum_measure M I N = sum_measure M' I N'"
by(simp add: sum_measure_def assms cong: sets_eq_imp_space_eq)
lemma [simp]:
shows space_sum_measure: "space (sum_measure M I Mi) = space M"
and sets_sum_measure[measurable_cong]: "sets (sum_measure M I Mi) = sets M"
by(auto simp: sum_measure_def)
lemma emeasure_sum_measure:
assumes [measurable]:"A ∈ sets M" and "⋀i. i ∈ I ⟹ sets (Mi i) = sets M"
shows "emeasure (sum_measure M I Mi) A = (∑i∈I. Mi i A)"
proof(rule emeasure_measure_of[of _ "space M" "sets M"])
show "countably_additive (sets (sum_measure M I Mi)) (λA. ∑i∈I. emeasure (Mi i) A)"
unfolding sum_measure_def sets.sets_measure_of_eq countably_additive_def
proof safe
fix Ai :: "nat ⇒ _"
assume h:"range Ai ⊆ sets M" "disjoint_family Ai"
then have [measurable]: "⋀i j. j ∈ I ⟹ Ai i ∈ sets (Mi j)"
by(auto simp: assms)
show "(∑i. ∑j∈I. emeasure (Mi j) (Ai i)) = (∑i∈I. emeasure (Mi i) (⋃ (range Ai)))"
by(auto simp: suminf_sum intro!: Finite_Cartesian_Product.sum_cong_aux suminf_emeasure h)
qed
qed(auto simp: positive_def sum_measure_def intro!: sets.sets_into_space)
lemma sum_measure_infinite: "infinite I ⟹ sum_measure M I Mi = null_measure M"
by(auto simp: sum_measure_def null_measure_def)
lemma nn_integral_sum_measure:
assumes "f ∈ borel_measurable M" and [measurable_cong]: "⋀i. i ∈ I ⟹ sets (Mi i) = sets M"
shows "(∫⇧+x. f x ∂sum_measure M I Mi) = (∑i∈I. (∫⇧+x. f x ∂(Mi i)))"
using assms(1)
proof induction
case h:(cong f g)
then show ?case (is "?lhs = ?rhs")
by(auto cong: nn_integral_cong[of "sum_measure M I Mi",simplified] intro!: Finite_Cartesian_Product.sum_cong_aux)
(auto cong: nn_integral_cong simp: sets_eq_imp_space_eq[OF assms(2)[symmetric]])
next
case (set A)
then show ?case
by(auto simp: emeasure_sum_measure assms)
next
case (mult u c)
then show ?case
by(auto simp add: nn_integral_cmult sum_distrib_left intro!: Finite_Cartesian_Product.sum_cong_aux)
next
case (add u v)
then show ?case
by(auto simp: nn_integral_add sum.distrib)
next
case ih[measurable]:(seq U)
show ?case (is "?lhs = ?rhs")
proof -
have "?lhs = (∫⇧+ x. (⨆i. U i x) ∂sum_measure M I Mi)"
by(auto intro!: nn_integral_cong) (use SUP_apply in auto)
also have "... = (⨆i. (∫⇧+x. U i x ∂sum_measure M I Mi))"
by(rule nn_integral_monotone_convergence_SUP) (use ih in auto)
also have "... = (⨆i. ∑j∈I. (∫⇧+x. U i x ∂(Mi j)))"
by(simp add: ih)
also have "... = (∑j∈I. ⨆i. ∫⇧+x. U i x ∂(Mi j))"
by(auto intro!: incseq_nn_integral ih ennreal_SUP_sum)
also have "... = (∑j∈I. ∫⇧+x. (⨆i. U i x) ∂(Mi j))"
by(auto intro!: Finite_Cartesian_Product.sum_cong_aux nn_integral_monotone_convergence_SUP[symmetric] ih)
also have "... = ?rhs"
by(auto intro!: Finite_Cartesian_Product.sum_cong_aux nn_integral_cong) (metis SUP_apply Sup_apply)
finally show ?thesis .
qed
qed
corollary integrable_sum_measure_iff_ne:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable_cong]: "⋀i. i ∈ I ⟹ sets (Mi i) = sets M" and "finite I" and "I ≠ {}"
shows "integrable (sum_measure M I Mi) f ⟷ (∀i∈I. integrable (Mi i) f)"
proof safe
fix i
assume [measurable]: "integrable (sum_measure M I Mi) f" and i:"i ∈ I"
then have [measurable]:"⋀i. i ∈ I ⟹ f ∈ borel_measurable (Mi i)"
"f ∈ borel_measurable M" "(∫⇧+ x. ennreal (norm (f x)) ∂sum_measure M I Mi) < ∞"
by(auto simp: integrable_iff_bounded)
hence "(∑i∈I. ∫⇧+ x. ennreal (norm (f x)) ∂Mi i) < ∞"
by(simp add: nn_integral_sum_measure assms)
thus "integrable (Mi i) f"
by(auto simp: assms integrable_iff_bounded i)
next
assume h:"∀i∈I. integrable (Mi i) f"
obtain i where i:"i ∈ I"
using assms by auto
have [measurable]: "f ∈ borel_measurable M"
using h[rule_format,OF i] i by auto
show "integrable (sum_measure M I Mi) f"
using h by(auto simp: integrable_iff_bounded nn_integral_sum_measure assms)
qed
corollary integrable_sum_measure_iff:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable_cong]: "⋀i. i ∈ I ⟹ sets (Mi i) = sets M" and "finite I"
and [measurable]: "f ∈ borel_measurable M"
shows "integrable (sum_measure M I Mi) f ⟷ (∀i∈I. integrable (Mi i) f)"
proof safe
fix i
assume "integrable (sum_measure M I Mi) f" "i ∈ I"
thus "integrable (Mi i) f"
using integrable_sum_measure_iff_ne[of I Mi,OF assms(1-2)] by auto
qed(auto simp: integrable_iff_bounded nn_integral_sum_measure assms)
lemma integral_sum_measure:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes [measurable_cong]:"⋀i. i ∈ I ⟹ sets (Mi i) = sets M" "⋀i. i ∈ I ⟹ integrable (Mi i) f"
shows "(∫x. f x ∂sum_measure M I Mi) = (∑i∈I. (∫x. f x ∂(Mi i)))"
proof -
consider "I = {}" | "finite I" "I ≠ {}" | "infinite I" by auto
then show ?thesis
proof cases
case 1
then show ?thesis
by(auto simp: sum_measure_def integral_null_measure[simplified null_measure_def])
next
case 2
have "integrable (sum_measure M I Mi) f"
by(auto simp: assms(2) integrable_sum_measure_iff_ne[of I Mi,OF assms(1) 2,simplified])
thus ?thesis
proof induction
case h:(base A c)
then have h':"⋀i. i ∈ I ⟹ emeasure (Mi i) A < ⊤"
by(auto simp: emeasure_sum_measure assms 2)
show ?case
using h
by(auto simp: measure_def h' emeasure_sum_measure assms enn2real_sum[of I "λi. emeasure (Mi i) A",OF h'] scaleR_left.sum
intro!: Finite_Cartesian_Product.sum_cong_aux)
next
case ih:(add f g)
then have "⋀i. i ∈ I ⟹ integrable (Mi i) g" "⋀i. i ∈ I ⟹ integrable (Mi i) f"
by(auto simp: integrable_sum_measure_iff_ne assms 2)
with ih show ?case
by(auto simp: sum.distrib)
next
case ih:(lim f s)
then have [measurable]:"f ∈ borel_measurable M" "⋀i. s i ∈ borel_measurable M"
by auto
have int[measurable]:"integrable (Mi i) f" "⋀j. integrable (Mi i) (s j)" if "i ∈ I" for i
using that ih 2 by(auto simp add: integrable_sum_measure_iff assms)
show ?case
proof(rule LIMSEQ_unique[where X="λi. ∑j∈I. ∫x. s i x ∂(Mi j)"])
show "(λi. ∑j∈I. ∫x. s i x ∂(Mi j)) ⇢ (∫x. f x ∂sum_measure M I Mi)"
using ih by(auto simp: ih(5)[symmetric] intro!: integral_dominated_convergence[where w="λx. 2*norm (f x)"])
show "(λi. ∑j∈I. ∫x. s i x ∂(Mi j)) ⇢ (∑j∈I. (∫x. f x ∂(Mi j)))"
proof(rule tendsto_sum)
fix j
assume j: "j ∈ I"
show "(λi. ∫x. s i x ∂(Mi j)) ⇢ (∫x. f x ∂(Mi j))"
using integral_dominated_convergence[of f "Mi j" s "λx. 2 * norm (f x)",OF _ _ _ AE_I2 AE_I2] ih int[OF j]
by(auto simp: sets_eq_imp_space_eq[OF assms(1)[OF j]])
qed
qed
qed
next
case 3
then show ?thesis
by(simp add: sum_measure_infinite)
qed
qed
text ‹ Lemmas related to scale measure ›
lemma integrable_scale_measure:
fixes f :: "'a ⇒ 'b::{banach, second_countable_topology}"
assumes "integrable M f"
shows "integrable (scale_measure (ennreal r) M) f"
using assms ennreal_less_top
by(auto simp: integrable_iff_bounded nn_integral_scale_measure ennreal_mult_less_top)
lemma integral_scale_measure:
assumes "r ≥ 0" "integrable M f"
shows "(∫x. f x ∂scale_measure (ennreal r) M) = r * (∫x. f x ∂M)"
using assms(2)
proof induction
case ih:(lim f s)
show ?case
proof(rule LIMSEQ_unique[where X="λi. ∫x. s i x ∂scale_measure (ennreal r) M"])
from ih(1-4) show "(λi. ∫x. s i x ∂scale_measure (ennreal r) M) ⇢ (∫x. f x ∂scale_measure (ennreal r) M)"
by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f x)"] integrable_scale_measure
simp: space_scale_measure)
show "(λi. ∫x. s i x ∂scale_measure (ennreal r) M) ⇢ r * (∫x. f x ∂M)"
unfolding ih(5) using ih(1-4) by(auto intro!: integral_dominated_convergence[where w="λx. 2 * norm (f x)"] tendsto_mult_left)
qed
qed(auto simp: measure_scale_measure[OF assms(1)] ring_class.ring_distribs(1) integrable_scale_measure)
lemma
fixes c :: ereal
assumes c: "c ≠ - ∞" and a: "⋀n. 0 ≤ a n"
shows liminf_cadd: "liminf (λn. c + a n) = c + liminf a"
and limsup_cadd: "limsup (λn. c + a n) = c + limsup a"
by(auto simp add: liminf_SUP_INF limsup_INF_SUP INF_ereal_add_right[OF _ c a] SUP_ereal_add_right[OF _ c]
intro!: INF_ereal_add_right c SUP_upper2 a)
lemma(in Metric_space) frontier_measure_zero_balls:
assumes "sets N = sets (borel_of mtopology)" "finite_measure N" "M ≠ {}"
and "e > 0" and "separable_space mtopology"
obtains ai ri where
"(⋃i::nat. mball (ai i) (ri i)) = M" "(⋃i::nat. mcball (ai i) (ri i)) = M"
"⋀i. ai i ∈ M" "⋀i. ri i > 0" "⋀i. ri i < e"
"⋀i. measure N (mtopology frontier_of (mball (ai i) (ri i))) = 0"
"⋀i. measure N (mtopology frontier_of (mcball (ai i) (ri i))) = 0"
proof -
interpret N: finite_measure N by fact
have [measurable]: "⋀a r. mball a r ∈ sets N" "⋀a r. mcball a r ∈ sets N"
"⋀a r. mtopology frontier_of (mball a r) ∈ sets N" "⋀a r. mtopology frontier_of (mcball a r) ∈ sets N"
by(auto simp: assms(1) borel_of_closed borel_of_open[OF openin_mball] closedin_frontier_of)
have mono:"mtopology frontier_of (mball a r) ⊆ {y∈M. d a y = r}"
"mtopology frontier_of (mcball a r) ⊆ {y∈M. d a y = r}" for a r
proof -
have "mtopology frontier_of (mball a r) ⊆ mcball a r - mball a r"
using closure_of_mball by(auto simp: frontier_of_def interior_of_openin[OF openin_mball])
also have "... ⊆ {y∈M. d a y = r}"
by auto
finally show "mtopology frontier_of (mball a r) ⊆ {y∈M. d a y = r}" .
have "mtopology frontier_of (mcball a r) ⊆ mcball a r - mball a r"
using interior_of_mcball by(auto simp: frontier_of_def closure_of_closedin[OF closedin_mcball])
also have "... ⊆ {y∈M. d a y = r}"
by(auto simp: mcball_def mball_def)
finally show "mtopology frontier_of (mcball a r) ⊆ {y∈M. d a y = r}" .
qed
have sets[measurable]: "{y∈M. d a y = r} ∈ sets N" if "a ∈ M" for a r
proof -
have [simp]: "d a -` {r} ∩ M = {y∈M. d a y = r}" by blast
show ?thesis
using measurable_sets[OF continuous_map_measurable[OF uniformly_continuous_imp_continuous_map[OF mdist_set_uniformly_continuous[of Self "{a}"]]],of "{r}"]
by(simp add: borel_of_euclidean mtopology_of_def space_borel_of assms(1) mdist_set_Self)
(metis (no_types, lifting) ‹d a -` {r} ∩ M = {y ∈ M. d a y = r}› commute d_set_singleton that vimage_inter_cong)
qed
from assms(5) obtain U where U: "countable U" "mdense U" by(auto simp: separable_space_def2)
with assms(3) have U_ne: "U ≠ {}"
by(auto simp: mdense_empty_iff)
{ fix i :: nat
have "countable {r ∈ {e/2<..<e}. measure N {y ∈ M. d (from_nat_into U i) y = r} ≠ 0}"
by(rule N.countable_support_sets) (auto simp: disjoint_family_on_def)
from real_interval_avoid_countable_set[of "e / 2" e,OF _ this] assms(4)
have "∃r. measure N {y∈M. d (from_nat_into U i) y = r} = 0 ∧ r > e / 2 ∧ r < e"
by auto
}
then obtain ri where ri: "⋀i. measure N {y∈M. d (from_nat_into U i) y = ri i} = 0"
"⋀i. ri i > e / 2" "⋀i. ri i < e"
by metis
have 1: "(⋃i. mball (from_nat_into U i) (ri i)) = M" "(⋃i. mcball (from_nat_into U i) (ri i)) = M"
proof -
have "M = (⋃u∈U. mball u (e / 2))"
by(rule mdense_balls_cover[OF U(2),symmetric]) (simp add: assms(4))
also have "... = (⋃i. mball (from_nat_into U i) (e / 2))"
by(rule UN_from_nat_into[OF U(1) U_ne])
also have "... ⊆ (⋃i. mball (from_nat_into U i) (ri i))"
using mball_subset_concentric[OF order.strict_implies_order[OF ri(2)]] by auto
finally have 1:"M ⊆ (⋃i. mball (from_nat_into U i) (ri i))" .
moreover have "M ⊆ (⋃i. mcball (from_nat_into U i) (ri i))"
by(rule order.trans[OF 1]) fastforce
ultimately show "(⋃i. mball (from_nat_into U i) (ri i)) = M" "(⋃i. mcball (from_nat_into U i) (ri i)) = M"
by fastforce+
qed
have 2: "⋀i. from_nat_into U i ∈ M" "⋀i. ri i > 0" "⋀i. ri i < e"
using from_nat_into[OF U_ne] dense_in_subset[OF U(2)] ri(3) assms(4)
by(auto intro!: order.strict_trans[OF _ ri(2),of 0])
have 3: "measure N (mtopology frontier_of (mball (from_nat_into U i) (ri i))) = 0"
"measure N (mtopology frontier_of (mcball (from_nat_into U i) (ri i))) = 0" for i
using N.finite_measure_mono[OF mono(1) sets[of "from_nat_into U i" "ri i"]]
N.finite_measure_mono[OF mono(2) sets[of "from_nat_into U i" "ri i"]]
by (auto simp add: 2 measure_le_0_iff ri(1))
show ?thesis
using 1 2 3 that by blast
qed
lemma finite_measure_integral_eq_dense:
assumes finite: "finite_measure N" "finite_measure M"
and sets_N:"sets N = sets (borel_of X)" and sets_M: "sets M = sets (borel_of X)"
and dense:"dense_in (mtopology_of (cfunspace X euclidean_metric)) F"
and integ_eq:"⋀f::_ ⇒ real. f ∈ F ⟹ (∫x. f x ∂N) = (∫x. f x ∂M)"
and f:"continuous_map X euclideanreal f" "bounded (f ` topspace X)"
shows "(∫x. f x ∂N) = (∫x. f x ∂M)"
proof -
interpret N: finite_measure N
by fact
interpret M: finite_measure M
by fact
have integ_N: "⋀A. A ∈ sets N ⟹ integrable N (indicat_real A)"
and integ_M: "⋀A. A ∈ sets M ⟹ integrable M (indicat_real A)"
by (auto simp add: N.emeasure_eq_measure M.emeasure_eq_measure)
have space_N: "space N = topspace X" and space_M: "space M = topspace X"
using sets_N sets_M sets_eq_imp_space_eq[of _ "borel_of X"]
by(auto simp: space_borel_of)
from f obtain B where B: "⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ B"
by (meson bounded_real imageI)
show "(∫x. f x ∂N) = (∫x. f x ∂M)"
proof -
have in_mspace_measurable: "g ∈ borel_measurable N" "g ∈ borel_measurable M"
if g:"g ∈ mspace (cfunspace X (euclidean_metric :: real metric))" for g
using continuous_map_measurable[of X euclidean,simplified borel_of_euclidean] g
by(auto simp: sets_M cong: measurable_cong_sets sets_N)
have f':"(λx∈topspace X. f x) ∈ mspace (cfunspace X euclidean_metric)"
using f(1) f(2) by simp
with mdense_of_def3[THEN iffD1,OF assms(5)] obtain fn where fn:
"range fn ⊆ F" "limitin (mtopology_of (cfunspace X euclidean_metric)) fn (λx∈topspace X. f x) sequentially"
by blast
hence fn_space: "⋀n. fn n ∈ mspace (cfunspace X euclidean_metric)"
using dense_in_subset[OF assms(5)] by auto
hence [measurable]: "(λx∈topspace X. f x) ∈ borel_measurable N" "(λx∈topspace X. f x) ∈ borel_measurable M"
"⋀n. fn n ∈ borel_measurable N" "⋀n. fn n ∈ borel_measurable M"
using f' by (auto simp del: mspace_cfunspace intro!: in_mspace_measurable)
interpret d: Metric_space "mspace (cfunspace X euclidean_metric)" "mdist (cfunspace X (euclidean_metric :: real metric))"
by blast
from fn have "limitin d.mtopology fn (λx∈topspace X. f x) sequentially"
by (simp add: mtopology_of_def)
hence limit:"⋀ε. ε > 0 ⟹ ∃N. ∀n≥N. fn n ∈ mspace (cfunspace X euclidean_metric) ∧
mdist (cfunspace X euclidean_metric) (fn n) (restrict f (topspace X)) < ε"
unfolding d.limit_metric_sequentially by blast
from this[of 1] obtain N0 where N0:
"⋀n. n ≥ N0 ⟹ mdist (cfunspace X euclidean_metric) (fn n) (λx∈topspace X. f x) < 1"
by auto
have 1: "(λi. fn (i + N0) x) ⇢ (λx∈topspace X. f x) x" if x:"x ∈ topspace X" for x
proof(rule LIMSEQ_I)
fix r :: real
assume r:"0 < r"
from limit[OF half_gt_zero[OF r]] obtain N where N:
"⋀n. n ≥ N ⟹ mdist (cfunspace X euclidean_metric) (fn n) (restrict f (topspace X)) < r / 2"
by blast
show "∃no. ∀n≥no. norm (fn (n + N0) x - restrict f (topspace X) x) < r"
proof(safe intro!: exI[where x=N])
fix n
assume n:"N ≤ n"
with N[OF trans_le_add1[OF this,of N0]]
have "mdist (cfunspace X euclidean_metric) (fn (n + N0)) (restrict f (topspace X)) ≤ r / 2"
by auto
from order.strict_trans1[OF mdist_cfunspace_imp_mdist_le[OF fn_space f' this x],of r] x r
show "norm (fn (n + N0) x - restrict f (topspace X) x) < r"
by (auto simp: dist_real_def)
qed
qed
have 2: "norm (fn (i + N0) x) ≤ 2 * B + 1" if x:"x ∈ topspace X" for i x
proof-
from N0[of "i + N0"]
have "mdist (cfunspace X euclidean_metric) (fn (i + N0)) (restrict f (topspace X)) ≤ 1"
by linarith
from mdist_cfunspace_imp_mdist_le[OF fn_space f' this x]
have "norm (fn (i + N0) x - f x) ≤ 1"
using x by (auto simp: dist_real_def)
thus ?thesis
using B[OF x] by auto
qed
from 1 2 have "(λi. integral⇧L N (fn (i + N0))) ⇢ integral⇧L N (restrict f (topspace X))"
by(auto intro!: integral_dominated_convergence[where s="λi. fn (i + N0)" and w="λx. 2 * B + 1"]
simp: space_N)
moreover have "(λi. integral⇧L N (fn (i + N0))) ⇢ integral⇧L M (restrict f (topspace X))"
proof -
have [simp]:"integral⇧L N (fn (i + N0)) = integral⇧L M (fn (i + N0))" for i
using fn(1) by(auto intro!: assms(6))
from 1 2 show ?thesis
by(auto intro!: integral_dominated_convergence[where s="λi. fn (i + N0)" and w="λx. 2 * B + 1"]
simp: space_M)
qed
ultimately have "integral⇧L N (restrict f (topspace X)) = integral⇧L M (restrict f (topspace X))"
by(rule tendsto_unique[OF sequentially_bot])
moreover have "integral⇧L N (restrict f (topspace X)) = integral⇧L N f"
by(auto cong: Bochner_Integration.integral_cong[OF refl] simp: space_N[symmetric])
moreover have "integral⇧L M (restrict f (topspace X)) = integral⇧L M f"
by(auto cong: Bochner_Integration.integral_cong[OF refl] simp: space_M[symmetric])
ultimately show ?thesis
by simp
qed
qed
subsection ‹ Sequentially Continuous Maps›
definition seq_continuous_map :: "'a topology ⇒ 'b topology ⇒ ('a ⇒ 'b) ⇒ bool" where
"seq_continuous_map X Y f ≡ (∀xn x. limitin X xn x sequentially ⟶ limitin Y (λn. f (xn n)) (f x) sequentially)"
lemma seq_continuous_map:
"seq_continuous_map X Y f ⟷ (∀xn x. limitin X xn x sequentially ⟶ limitin Y (λn. f (xn n)) (f x) sequentially)"
by(auto simp: seq_continuous_map_def)
lemma seq_continuous_map_funspace:
assumes "seq_continuous_map X Y f"
shows "f ∈ topspace X → topspace Y"
proof
fix x
assume "x ∈ topspace X"
then have "limitin X (λn. x) x sequentially"
by auto
hence "limitin Y (λn. f x) (f x) sequentially"
using assms
by (meson limitin_sequentially seq_continuous_map)
thus "f x ∈ topspace Y"
by auto
qed
lemma seq_continuous_iff_continuous_first_countable:
assumes "first_countable X"
shows "seq_continuous_map X Y = continuous_map X Y"
by standard (simp add: continuous_map_iff_limit_seq assms seq_continuous_map_def)
subsection ‹ Sequential Compactness ›
definition seq_compactin :: "'a topology ⇒ 'a set ⇒ bool" where
"seq_compactin X S
⟷ S ⊆ topspace X ∧ (∀xn. (∀n::nat. xn n ∈ S) ⟶ (∃l∈S. ∃a::nat ⇒ nat. strict_mono a ∧ limitin X (xn ∘ a) l sequentially))"
definition "seq_compact_space X ≡ seq_compactin X (topspace X)"
lemma seq_compactin_subset_topspace: "seq_compactin X S ⟹ S ⊆ topspace X"
by(auto simp: seq_compactin_def)
lemma seq_compactin_empty[simp]: "seq_compactin X {}"
by(auto simp: seq_compactin_def)
lemma seq_compactin_seq_compact[simp]: "seq_compactin euclidean S ⟷ seq_compact S"
by(auto simp: seq_compactin_def seq_compact_def)
lemma image_seq_compactin:
assumes "seq_compactin X S" "seq_continuous_map X Y f"
shows "seq_compactin Y (f ` S)"
unfolding seq_compactin_def
proof safe
fix yn
assume "∀n::nat. yn n ∈ f ` S"
then have "∀n. ∃x∈S. yn n = f x"
by blast
then obtain xn where xn: "⋀n::nat. xn n ∈ S" "⋀n. yn n = f (xn n)"
by metis
then obtain lx a where la: "lx ∈ S" "strict_mono a" "limitin X (xn ∘ a) lx sequentially"
by (meson assms(1) seq_compactin_def)
show "∃l∈f ` S. ∃a. strict_mono a ∧ limitin Y (yn ∘ a) l sequentially"
proof(safe intro!: bexI[where x="f lx"] exI[where x=a])
have [simp]:"yn ∘ a = (λn. f ((xn ∘ a) n))"
by(auto simp: xn(2) comp_def)
show "limitin Y (yn ∘ a) (f lx) sequentially"
using la(3) assms(2) xn(1,2) by(fastforce simp: seq_continuous_map)
qed(use la in auto)
qed(use seq_compactin_subset_topspace[OF assms(1)] seq_continuous_map_funspace[OF assms(2)] in auto)
lemma closed_seq_compactin:
assumes "seq_compactin X K" "C ⊆ K" "closedin X C"
shows "seq_compactin X C"
unfolding seq_compactin_def
proof safe
fix xn
assume xn: "∀n::nat. xn n ∈ C"
then have "∀n. xn n ∈ K"
using assms(2) by blast
with assms(1) obtain l a where l: "l ∈ K" "strict_mono a" "limitin X (xn ∘ a) l sequentially"
by (meson seq_compactin_def)
have "l ∈ C"
using xn by(auto intro!: limitin_closedin[OF l(3) assms(3)])
with l(2,3) show "∃l∈C. ∃a. strict_mono a ∧ limitin X (xn ∘ a) l sequentially"
by blast
qed(use closedin_subset[OF assms(3)] in auto)
corollary closedin_seq_compact_space:
"seq_compact_space X ⟹ closedin X C ⟹ seq_compactin X C"
by(auto intro!: closed_seq_compactin[where K="topspace X" and C=C] closedin_subset simp: seq_compact_space_def)
lemma seq_compactin_subtopology: "seq_compactin (subtopology X S) T ⟷ seq_compactin X T ∧ T ⊆ S"
by(fastforce simp: seq_compactin_def limitin_subtopology subsetD)
corollary seq_compact_space_subtopology: "seq_compactin X S ⟹ seq_compact_space (subtopology X S)"
by(auto simp: seq_compact_space_def seq_compactin_subtopology inf_absorb2 seq_compactin_subset_topspace)
lemma seq_compactin_PiED:
assumes "seq_compactin (product_topology X I) (Pi⇩E I S)"
shows "(Pi⇩E I S = {} ∨ (∀i∈I. seq_compactin (X i) (S i)))"
proof -
consider "Pi⇩E I S = {}" | "Pi⇩E I S ≠ {}"
by blast
then show "(Pi⇩E I S = {} ∨ (∀i∈I. seq_compactin (X i) (S i)))"
proof cases
case 1
then show ?thesis
by simp
next
case 2
then have Si_ne:"⋀i. i ∈ I ⟹ S i ≠ {}"
by blast
then obtain ci where ci: "⋀i. i ∈ I ⟹ ci i ∈ S i"
by (meson PiE_E ex_in_conv)
show ?thesis
proof(safe intro!: disjI2)
fix i
assume i: "i ∈ I"
show "seq_compactin (X i) (S i)"
unfolding seq_compactin_def
proof safe
fix xn
assume xn:"∀n::nat. xn n ∈ S i"
define Xn where "Xn ≡ (λn. λj∈I. if j = i then xn n else ci j)"
have "⋀n. Xn n ∈ Pi⇩E I S"
using i xn ci by(auto simp: Xn_def)
then obtain L a where L: "L ∈ Pi⇩E I S" "strict_mono a"
"limitin (product_topology X I) (Xn ∘ a) L sequentially"
by (meson assms seq_compactin_def)
thus "∃l∈S i. ∃a. strict_mono a ∧ limitin (X i) (xn ∘ a) l sequentially"
using i by(auto simp: limitin_componentwise Xn_def comp_def intro!: bexI[where x="L i"] exI[where x=a])
next
show "⋀x. x ∈ S i ⟹ x ∈ topspace (X i)"
using i subset_PiE[THEN iffD1,OF seq_compactin_subset_topspace[OF assms,simplified]] 2 by auto
qed
qed
qed
qed
lemma metrizable_seq_compactin_iff_compactin:
assumes "metrizable_space X"
shows "seq_compactin X S ⟷ compactin X S"
proof -
obtain d where d: "Metric_space (topspace X) d" "Metric_space.mtopology (topspace X) d = X"
by (metis Metric_space.topspace_mtopology assms metrizable_space_def)
interpret Metric_space "topspace X" d
by fact
have "seq_compactin X S ⟷ seq_compactin mtopology S"
by(simp add: d)
also have "... ⟷ compactin mtopology S"
by(fastforce simp: compactin_sequentially seq_compactin_def)
also have "... ⟷ compactin X S"
by(simp add: d)
finally show ?thesis .
qed
corollary metrizable_seq_compact_space_iff_compact_space:
shows "metrizable_space X ⟹ seq_compact_space X ⟷ compact_space X"
unfolding seq_compact_space_def compact_space_def by(rule metrizable_seq_compactin_iff_compactin)
subsection ‹ Lemmas for Limsup and Liminf›
lemma real_less_add_ex_less_pair:
fixes x w v :: real
assumes "x < w + v"
shows "∃y z. x = y + z ∧ y < w ∧ z < v"
apply(rule exI[where x="w - (w + v - x) / 2"])
apply(rule exI[where x="v - (w + v - x) / 2"])
using assms by auto
lemma ereal_less_add_ex_less_pair:
fixes x w v :: ereal
assumes "- ∞ < w" "- ∞ < v" "x < w + v"
shows "∃y z. x = y + z ∧ y < w ∧ z < v"
proof -
consider "x = - ∞" | "- ∞ < x" "x < ∞" "w = ∞" "v = ∞"
| "- ∞ < x" "x < ∞" "w < ∞" "v = ∞" | "- ∞ < x" "x < ∞" "v < ∞" "w = ∞"
| "- ∞ < x" "x < ∞" "w < ∞" "v < ∞"
using assms(3) less_ereal.simps(2) by blast
then show ?thesis
proof cases
assume "x = - ∞"
then show ?thesis
using assms by(auto intro!: exI[where x="- ∞"])
next
assume h:"- ∞ < x" "x < ∞" "w = ∞" "v = ∞"
show ?thesis
apply(rule exI[where x=0])
apply(rule exI[where x=x])
using h assms by simp
next
assume h:"- ∞ < x" "x < ∞" "w < ∞" "v = ∞"
then obtain x' w' where eq: "w = ereal w'" "x = ereal x'"
using assms by (metis less_irrefl sgn_ereal.cases)
show ?thesis
apply(rule exI[where x="w - 1"])
apply(rule exI[where x="x - (w - 1)"])
using h assms by(auto simp: eq one_ereal_def)
next
assume h:"- ∞ < x" "x < ∞" "v < ∞" "w = ∞"
then obtain x' v' where eq: "v = ereal v'" "x = ereal x'"
using assms by (metis less_irrefl sgn_ereal.cases)
show ?thesis
apply(rule exI[where x="x - (v - 1)"])
apply(rule exI[where x="v - 1"])
using h assms by(auto simp: eq one_ereal_def)
next
assume "- ∞ < x" "x < ∞" "w < ∞" "v < ∞"
then obtain x' v' w' where eq: "x = ereal x'" "w = ereal w'" "v = ereal v'"
using assms by (metis less_irrefl sgn_ereal.cases)
have "∃y' z'. x' = y' + z' ∧ y' < w' ∧ z' < v'"
using real_less_add_ex_less_pair assms by(simp add: eq)
then obtain y' z' where yz':"x' = y' + z' ∧ y' < w' ∧ z' < v'"
by blast
show ?thesis
apply(rule exI[where x="ereal y'"])
apply(rule exI[where x="ereal z'"])
using yz' by(simp add: eq)
qed
qed
lemma real_add_less:
fixes x w v :: real
assumes "w + v < x"
shows "∃y z. x = y + z ∧ w < y ∧ v < z"
apply(rule exI[where x="w + (x - (w + v)) / 2"])
apply(rule exI[where x="v + (x - (w + v)) / 2"])
using assms by auto
lemma ereal_add_less:
fixes x w v :: ereal
assumes "w + v < x"
shows "∃y z. x = y + z ∧ w < y ∧ v < z"
proof -
have "- ∞ < x" "v < ∞" "w < ∞"
using assms less_ereal.simps(2,3) by auto
then consider "x = ∞" "w < ∞" "v < ∞" | "- ∞ < x" "x < ∞" "w = - ∞" "v = - ∞"
| "- ∞ < x" "x < ∞" "w = - ∞" "v < ∞" "- ∞ < v"
| "- ∞ < x" "x < ∞" "v = - ∞" "w < ∞" "- ∞ < w"
| "- ∞ < x" "x < ∞" "- ∞ < w" "w < ∞" "v < ∞" "- ∞ < v"
by blast
thus ?thesis
proof cases
assume "x = ∞" "w < ∞" "v < ∞"
then show ?thesis
by(auto intro!: exI[where x=∞])
next
assume h:"- ∞ < x" "x < ∞" "w = - ∞" "v = - ∞"
show ?thesis
apply(rule exI[where x=0])
apply(rule exI[where x=x])
using h assms by simp
next
assume h:"- ∞ < x" "x < ∞" "w = - ∞" "v < ∞" "- ∞ < v"
then obtain x' v' where xv': "x = ereal x'" "v = ereal v'"
by (metis less_irrefl sgn_ereal.cases)
show ?thesis
apply(rule exI[where x="x - (v + 1)"])
apply(rule exI[where x="v + 1"])
using h by(auto simp: xv')
next
assume h:"- ∞ < x" "x < ∞" "v = - ∞" "w < ∞" "- ∞ < w"
then obtain x' w' where xw': "x = ereal x'" "w = ereal w'"
by (metis less_irrefl sgn_ereal.cases)
show ?thesis
apply(rule exI[where x="w + 1"])
apply(rule exI[where x="x - (w + 1)"])
using h by(auto simp: xw')
next
assume h:"- ∞ < x" "x < ∞" "- ∞ < w" "w < ∞" "v < ∞" "- ∞ < v"
then obtain x' v' w' where eq: "x = ereal x'" "w = ereal w'" "v = ereal v'"
using assms by (metis less_irrefl sgn_ereal.cases)
have "∃y' z'. x' = y' + z' ∧ y' > w' ∧ z' > v'"
using assms real_add_less by(auto simp: eq)
then obtain y' z' where yz':"x' = y' + z' ∧ y' > w' ∧ z' > v'"
by blast
show ?thesis
apply(rule exI[where x="ereal y'"])
apply(rule exI[where x="ereal z'"])
using yz' by(simp add: eq)
qed
qed
text ‹ A generalized version of @{thm ereal_liminf_add_mono}.›
lemma ereal_Liminf_add_mono:
fixes u v::"'a ⇒ ereal"
assumes "¬((Liminf F u = ∞ ∧ Liminf F v = -∞) ∨ (Liminf F u = -∞ ∧ Liminf F v = ∞))"
shows "Liminf F (λn. u n + v n) ≥ Liminf F u + Liminf F v"
proof (cases)
assume "(Liminf F u = -∞) ∨ (Liminf F v = -∞)"
then have *: "Liminf F u + Liminf F v = -∞" using assms by auto
show ?thesis by (simp add: *)
next
assume "¬((Liminf F u = -∞) ∨ (Liminf F v = -∞))"
then have h:"Liminf F u > -∞" "Liminf F v > -∞" by auto
show ?thesis
unfolding le_Liminf_iff
proof safe
fix y
assume y: "y < Liminf F u + Liminf F v"
then obtain x z where xz: "y = x + z" "x < Liminf F u" " z < Liminf F v"
using ereal_less_add_ex_less_pair h by blast
show "∀⇩F x in F. y < u x + v x"
by(rule eventually_mp[OF _ eventually_conj[OF less_LiminfD[OF xz(2)] less_LiminfD[OF xz(3)]]])
(auto simp: xz intro!: eventuallyI ereal_add_strict_mono2)
qed
qed
text ‹ A generalized version of @{thm ereal_limsup_add_mono}.›
lemma ereal_Limsup_add_mono:
fixes u v::"'a ⇒ ereal"
shows "Limsup F (λn. u n + v n) ≤ Limsup F u + Limsup F v"
unfolding Limsup_le_iff
proof safe
fix y
assume "Limsup F u + Limsup F v < y"
then obtain x z where xz: "y = x + z" "Limsup F u < x" "Limsup F v < z"
using ereal_add_less by blast
show "∀⇩F x in F. u x + v x < y"
by(rule eventually_mp[OF _ eventually_conj[OF Limsup_lessD[OF xz(2)] Limsup_lessD[OF xz(3)]]])
(auto simp: xz intro!: eventuallyI ereal_add_strict_mono2)
qed
subsection ‹ A Characterization of Closed Sets by Limit ›
text ‹ There is a net which charactrize closed sets in terms of convergence.
Since Isabelle/HOL's convergent is defined through filters, we transform the net to
a filter. We refer to the lecture notes by Shi~\cite{nets} for the conversion.›
definition derived_filter :: "['i set, 'i ⇒ 'i ⇒ bool] ⇒ 'i filter" where
"derived_filter I op ≡ (⨅i∈I. principal {j∈I. op i j})"
lemma eventually_derived_filter:
assumes "A ≠ {}"
and refl:"⋀a. a ∈ A ⟹ rel a a"
and trans:"⋀a b c. a ∈ A ⟹ b ∈ A ⟹ c ∈ A ⟹ rel a b ⟹ rel b c ⟹ rel a c"
and pair_bounded:"⋀a b. a ∈ A ⟹ b ∈ A ⟹ ∃c∈A. rel a c ∧ rel b c"
shows "eventually P (derived_filter A rel) ⟷ (∃i∈A. ∀n∈A. rel i n ⟶ P n)"
proof -
show ?thesis
unfolding derived_filter_def
proof(subst eventually_INF_base)
fix a b
assume h:"a ∈ A" "b ∈ A"
then obtain z where "z ∈ A" "rel a z" "rel b z"
using pair_bounded by metis
thus "∃x∈A. principal {j ∈ A. rel x j} ≤ principal {j ∈ A. rel a j} ⊓ principal {j ∈ A. rel b j}"
using h by(auto intro!: bexI[where x=z] dest: trans)
next
show "(∃b∈A. eventually P (principal {j ∈ A. rel b j})) ⟷ (∃i∈A. ∀n∈A. rel i n ⟶ P n)"
unfolding eventually_principal by blast
qed fact
qed
definition nhdsin_sets :: "'a topology ⇒ 'a ⇒ 'a set filter" where
"nhdsin_sets X x ≡ derived_filter {U. openin X U ∧ x ∈ U} (⊇)"
lemma eventually_nhdsin_sets:
assumes "x ∈ topspace X"
shows "eventually P (nhdsin_sets X x) ⟷ (∃U. openin X U ∧ x ∈ U ∧ (∀V. openin X V ⟶ x ∈ V ⟶ V ⊆ U ⟶ P V))"
proof -
have h:"{U. openin X U ∧ x ∈ U} ≠ {}"
"⋀a. a ∈ {U. openin X U ∧ x ∈ U} ⟹ (⊇) a a"
"⋀a b c. a ∈ {U. openin X U ∧ x ∈ U} ⟹ b ∈ {U. openin X U ∧ x ∈ U} ⟹ c ∈ {U. openin X U ∧ x ∈ U} ⟹ (⊇) a b ⟹ (⊇) b c ⟹ (⊇) a c"
"⋀a b. a ∈ {U. openin X U ∧ x ∈ U} ⟹ b ∈ {U. openin X U ∧ x ∈ U} ⟹ ∃c∈{U. openin X U ∧ x ∈ U}. (⊇) a c ∧ (⊇) b c"
proof safe
fix U V
assume "x ∈ U" "x ∈ V" "openin X U" "openin X V"
then show "∃W∈{U. openin X U ∧ x ∈ U}. W ⊆ U ∧ W ⊆ V"
using openin_Int[of X U V] by auto
qed(use assms in fastforce)+
show ?thesis
unfolding nhdsin_sets_def
apply(subst eventually_derived_filter[of "{U. openin X U ∧ x ∈ U}" "(⊇)"])
using h apply blast
apply simp
using h
apply blast
using h
apply blast
apply fastforce
done
qed
lemma eventually_nhdsin_setsI:
assumes "x ∈ topspace X" "⋀U. x ∈ U ⟹ openin X U ⟹ P U"
shows "eventually P (nhdsin_sets X x)"
using assms by(auto simp: eventually_nhdsin_sets)
lemma nhdsin_sets_bot[simp, intro]:
assumes "x ∈ topspace X"
shows "nhdsin_sets X x ≠ ⊥"
by(auto simp: trivial_limit_def eventually_nhdsin_sets[OF assms])
corollary limitin_nhdsin_sets: "limitin X xn x (nhdsin_sets X x) ⟷ x ∈ topspace X ∧ (∀U. openin X U ⟶ x ∈ U ⟶ (∃V. openin X V ∧ x ∈ V ∧ (∀W. openin X W ⟶ x ∈ W ⟶ W ⊆ V ⟶ xn W ∈ U)))"
using eventually_nhdsin_sets by(fastforce dest: limitin_topspace simp: limitin_def)
lemma closedin_limitin:
assumes "T ⊆ topspace X" "⋀xn x. x ∈ topspace X ⟹ (⋀U. x ∈ U ⟹ openin X U ⟹ xn U ≠ x) ⟹ (⋀U. x ∈ U ⟹ openin X U ⟹ xn U ∈ T) ⟹ (⋀U. xn U ∈ topspace X) ⟹ limitin X xn x (nhdsin_sets X x) ⟹ x ∈ T"
shows "closedin X T"
proof -
have 1: "X derived_set_of T ⊆ T"
proof
fix x
assume x:"x ∈ X derived_set_of T"
hence x':"x ∈ topspace X"
by (simp add: in_derived_set_of)
define xn where "xn ≡ (λU. if x ∈ U ∧ openin X U then (SOME y. y ≠ x ∧ y ∈ T ∧ y ∈ U) else x)"
have xn: "xn U ≠ x" "xn U ∈ T" "xn U ∈ U" if U: "openin X U" "x ∈ U" for U
proof -
have "(SOME y. y ≠ x ∧ y ∈ T ∧ y ∈ U) ≠ x ∧ (SOME y. y ≠ x ∧ y ∈ T ∧ y ∈ U) ∈ T ∧ (SOME y. y ≠ x ∧ y ∈ T ∧ y ∈ U) ∈ U"
by(rule someI_ex,insert x U) (auto simp: derived_set_of_def)
thus "xn U ≠ x" "xn U ∈ T" "xn U ∈ U"
by(auto simp: xn_def U)
qed
hence 1:"⋀U. x ∈ U ⟹ openin X U ⟹ xn U ≠ x" "⋀U. x ∈ U ⟹ openin X U ⟹ xn U ∈ T"
by simp_all
moreover have "xn U ∈ topspace X" for U
proof(cases "x ∈ U ∧ openin X U")
case True
with assms 1 show ?thesis
by fast
next
case False
with x 1 derived_set_of_subset_topspace[of X T] show ?thesis
by(auto simp: xn_def)
qed
moreover have "limitin X xn x (nhdsin_sets X x)"
unfolding limitin_nhdsin_sets
proof safe
fix U
assume U: "openin X U" "x ∈ U"
then show "∃V. openin X V ∧ x ∈ V ∧ (∀W. openin X W ⟶ x ∈ W ⟶ W ⊆ V ⟶ xn W ∈ U)"
using xn by(fastforce intro!: exI[where x=U])
qed(use x derived_set_of_subset_topspace in fastforce)
ultimately show "x ∈ T"
by(rule assms(2)[OF x'])
qed
thus ?thesis
using assms(1) by(auto intro!: closure_of_eq[THEN iffD1] simp: closure_of)
qed
corollary closedin_iff_limitin_eq:
fixes X :: "'a topology"
shows "closedin X C
⟷ C ⊆ topspace X ∧
(∀xi x (F :: 'a set filter). (∀i. xi i ∈ topspace X) ⟶ x ∈ topspace X
⟶ (∀⇩F i in F. xi i ∈ C) ⟶ F ≠ ⊥ ⟶ limitin X xi x F ⟶ x ∈ C)"
proof
assume "C ⊆ topspace X ∧
(∀xi x (F :: 'a set filter). (∀i. xi i ∈ topspace X) ⟶ x ∈ topspace X
⟶ (∀⇩F i in F. xi i ∈ C) ⟶ F ≠ ⊥ ⟶ limitin X xi x F ⟶ x ∈ C)"
then show "closedin X C"
apply(intro closedin_limitin)
apply blast
by (metis (mono_tags, lifting) nhdsin_sets_bot eventually_nhdsin_setsI)
qed(auto dest: limitin_closedin closedin_subset)
lemma closedin_iff_limitin_sequentially:
assumes "first_countable X"
shows "closedin X S ⟷ S ⊆ topspace X ∧ (∀σ l. range σ ⊆ S ∧ limitin X σ l sequentially ⟶ l ∈ S)" (is "?lhs=?rhs")
proof safe
assume h:"S ⊆ topspace X" "∀σ l. range σ ⊆ S ∧ limitin X σ l sequentially ⟶ l ∈ S"
show "closedin X S"
proof(rule closedin_limitin)
fix xu x
assume xu: "⋀U. x ∈ U ⟹ openin X U ⟹ xu U ∈ S" "⋀U. xu U ∈ topspace X" "limitin X xu x (nhdsin_sets X x)"
then have x:"x ∈ topspace X"
by(auto simp: limitin_topspace)
then obtain B where B: "countable B" "⋀V. V ∈ B ⟹ openin X V"
"⋀U. openin X U ⟹ x ∈ U ⟹ (∃V∈B. x ∈ V ∧ V ⊆ U)"
using assms first_countable_def by metis
define B' where "B' ≡ B ∩ {U. x ∈ U}"
have B'_ne:"B' ≠ {}"
using B'_def B(3) x by fastforce
have cB':"countable B'"
using B by(simp add: B'_def)
have B': "⋀V. V ∈ B' ⟹ openin X V" "⋀U. openin X U ⟹ x ∈ U ⟹ (∃V∈B'. x ∈ V ∧ V ⊆ U)"
using B B'_def by fastforce+
define xn where "xn ≡ (λn. xu (⋂i≤n. (from_nat_into B' i)))"
have xn_in_S: "range xn ⊆ S" and limitin_xn: "limitin X xn x sequentially"
proof -
have 1:"⋀n. openin X (⋂i≤n. (from_nat_into B' i))"
by (auto simp: B'(1) B'_ne from_nat_into)
have 2: "⋀n. x ∈ (⋂i≤n. (from_nat_into B' i))"
by (metis B'_def B'_ne INT_I Int_iff from_nat_into mem_Collect_eq)
thus "range xn ⊆ S"
using 1 by(auto simp: xn_def intro!: xu)
show "limitin X xn x sequentially"
unfolding limitin_sequentially
proof safe
fix U
assume U: "openin X U" "x ∈ U"
then obtain V where V: "x ∈ V" "openin X V" "⋀W. openin X W ⟹ x ∈ W ⟹ W ⊆ V ⟹ xu W ∈ U"
by (metis limitin_nhdsin_sets xu(3))
then obtain V' where V': "V' ∈ B'" "x ∈ V'" "V' ⊆ V"
using B' by meson
then obtain N where N: "(⋂i≤N. (from_nat_into B' i)) ⊆ V'"
by (metis Inf_lower atMost_iff cB' from_nat_into_surj image_iff order.refl)
show "∃N. ∀n≥N. xn n ∈ U"
proof(safe intro!: exI[where x=N])
fix n
assume [arith]:"n ≥ N"
show "xn n ∈ U"
unfolding xn_def
proof(rule V(3))
have "(⋂i≤n. (from_nat_into B' i)) ⊆ (⋂i≤N. (from_nat_into B' i))"
by force
also have "... ⊆ V"
using N V' by simp
finally show "⋂ (from_nat_into B' ` {..n}) ⊆ V" .
qed(use 1 2 in auto)
qed
qed fact
qed
thus "x ∈ S"
using h(2) by blast
qed fact
qed(auto simp: limitin_closedin range_subsetD dest: closedin_subset)
subsection ‹ A Characterization of Topology by Limit ›
lemma topology_eq_filter:
fixes X :: "'a topology"
assumes "topspace X = topspace Y"
and "⋀(F :: 'a set filter) xi x. (⋀i. xi i ∈ topspace X) ⟹ x ∈ topspace X ⟹ limitin X xi x F ⟷ limitin Y xi x F"
shows "X = Y"
unfolding topology_eq_closedin closedin_iff_limitin_eq using assms by simp
lemma topology_eq_limit_sequentially:
assumes "topspace X = topspace Y"
and "first_countable X" "first_countable Y"
and "⋀xn x. (⋀n. xn i ∈ topspace X) ⟹ x ∈ topspace X ⟹ limitin X xn x sequentially ⟷ limitin Y xn x sequentially"
shows "X = Y"
unfolding topology_eq_closedin closedin_iff_limitin_sequentially[OF assms(2)] closedin_iff_limitin_sequentially[OF assms(3)]
by (metis dual_order.trans limitin_topspace range_subsetD assms(1,4))
subsection ‹ A Characterization of Open Sets by Limit ›
corollary openin_limitin:
assumes "U ⊆ topspace X" "⋀xi x. x ∈ topspace X ⟹ (⋀i. xi i ∈ topspace X) ⟹ limitin X xi x (nhdsin_sets X x) ⟹ x ∈ U ⟹ ∀⇩F i in (nhdsin_sets X x). xi i ∈ U"
shows "openin X U"
unfolding openin_closedin_eq
proof(safe intro!: assms(1) closedin_limitin)
fix xi x
assume h:"x ∈ topspace X" "∀V. x ∈ V ⟶ openin X V ⟶ xi V ∈ topspace X - U"
"∀V. xi V ∈ topspace X" "limitin X xi x (nhdsin_sets X x)" "x ∈ U"
show False
using assms(2)[OF h(1,3,4,5)[rule_format]] h(2)
by(auto simp: eventually_nhdsin_sets[OF h(1)])
qed
corollary openin_iff_limitin_eq:
fixes X :: "'a topology"
shows "openin X U ⟷ U ⊆ topspace X ∧ (∀xi x (F :: 'a set filter). (∀i. xi i ∈ topspace X) ⟶ x ∈ U ⟶ limitin X xi x F ⟶ (∀⇩F i in F. xi i ∈ U))"
by(auto intro!: openin_limitin openin_subset simp: limitin_def)
corollary limitin_openin_sequentially:
assumes "first_countable X"
shows "openin X U ⟷ U ⊆ topspace X ∧ (∀xn x. x ∈ U ⟶ limitin X xn x sequentially ⟶ (∃N. ∀n≥N. xn n ∈ U))"
unfolding openin_closedin_eq closedin_iff_limitin_sequentially[OF assms]
apply safe
apply (simp add: assms closedin_iff_limitin_sequentially limitin_sequentially openin_closedin)
apply (simp add: limitin_sequentially)
apply blast
done
lemma upper_semicontinuous_map_limsup_iff:
fixes f :: "'a ⇒ ('b :: {complete_linorder,linorder_topology})"
assumes "first_countable X"
shows "upper_semicontinuous_map X f ⟷ (∀xn x. limitin X xn x sequentially ⟶ limsup (λn. f (xn n)) ≤ f x)"
unfolding upper_semicontinuous_map_def
proof safe
fix xn x
assume h:"∀a. openin X {x ∈ topspace X. f x < a}" "limitin X xn x sequentially"
show "limsup (λn. f (xn n)) ≤ f x"
unfolding Limsup_le_iff eventually_sequentially
proof safe
fix y
assume y:"f x < y"
show "∃N. ∀n≥N. f (xn n) < y"
proof(rule ccontr)
assume "∄N. ∀n≥N. f (xn n) < y"
then have hc:"⋀N. ∃n≥N. f (xn n) ≥ y"
using linorder_not_less by blast
define a :: "nat ⇒ nat" where "a ≡ rec_nat (SOME n. f (xn n) ≥ y) (λn an. SOME m. m > an ∧ f (xn m) ≥ y)"
have "strict_mono a"
proof(rule strict_monoI_Suc)
fix n
have [simp]:"a (Suc n) = (SOME m. m > a n ∧ f (xn m) ≥ y)"
by(auto simp: a_def)
show "a n < a (Suc n)"
by simp (metis (mono_tags, lifting) Suc_le_lessD hc someI)
qed
have *:"f (xn (a n)) ≥ y" for n
proof(cases n)
case 0
then show ?thesis
using hc[of 0] by(auto simp: a_def intro!: someI_ex)
next
case (Suc n')
then show ?thesis
by(simp add: a_def) (metis (mono_tags, lifting) Suc_le_lessD hc someI_ex)
qed
have "∃N. ∀n≥N. (xn ∘ a) n ∈ {x ∈ topspace X. f x < y}"
using limitin_subsequence[OF ‹strict_mono a› h(2)] h(1)[rule_format,of y] y
by(fastforce simp: limitin_sequentially)
with * show False
using leD by auto
qed
qed
next
fix a
assume h:" ∀xn x. limitin X xn x sequentially ⟶ limsup (λn. f (xn n)) ≤ f x"
show "openin X {x ∈ topspace X. f x < a}"
unfolding limitin_openin_sequentially[OF assms]
proof safe
fix x xn
assume h':"limitin X xn x sequentially" "x ∈ topspace X" "f x < a"
with h have "limsup (λn. f (xn n)) ≤ f x"
by auto
with h'(3) obtain N where N:"⋀n. n≥N ⟹ f (xn n) < a"
by(auto simp: Limsup_le_iff eventually_sequentially)
obtain N' where N': "⋀n. n≥N' ⟹ xn n ∈ topspace X"
by (meson h'(1) limitin_sequentially openin_topspace)
thus "∃N. ∀n≥N. xn n ∈ {x ∈ topspace X. f x < a}"
using h'(3) N by(auto intro!: exI[where x="max N N'"])
qed
qed
subsection ‹ Lemmas for Upper/Lower-Semi Continuous Maps ›
lemma upper_semicontinuous_map_limsup_real:
fixes f :: "'a ⇒ real"
assumes "first_countable X"
shows "upper_semicontinuous_map X f ⟷ (∀xn x. limitin X xn x sequentially ⟶ limsup (λn. f (xn n)) ≤ f x)"
unfolding upper_semicontinuous_map_real_iff upper_semicontinuous_map_limsup_iff[OF assms] by simp
lemma lower_semicontinuous_map_liminf_iff:
fixes f :: "'a ⇒ ('b :: {complete_linorder,linorder_topology})"
assumes "first_countable X"
shows "lower_semicontinuous_map X f ⟷ (∀xn x. limitin X xn x sequentially ⟶ f x ≤ liminf (λn. f (xn n)))"
unfolding lower_semicontinuous_map_def
proof safe
fix xn x
assume h:"∀a. openin X {x ∈ topspace X. a < f x}" "limitin X xn x sequentially"
show "f x ≤ liminf (λn. f (xn n))"
unfolding le_Liminf_iff eventually_sequentially
proof safe
fix y
assume y:"y < f x"
show "∃N. ∀n≥N. y < f (xn n)"
proof(rule ccontr)
assume "∄N. ∀n≥N. y < f (xn n)"
then have hc:"⋀N. ∃n≥N. y ≥ f (xn n)"
by (meson verit_comp_simplify1(3))
define a :: "nat ⇒ nat" where "a ≡ rec_nat (SOME n. f (xn n) ≤ y) (λn an. SOME m. m > an ∧ f (xn m) ≤ y)"
have "strict_mono a"
proof(rule strict_monoI_Suc)
fix n
have [simp]:"a (Suc n) = (SOME m. m > a n ∧ f (xn m) ≤ y)"
by(auto simp: a_def)
show "a n < a (Suc n)"
by simp (metis (no_types, lifting) Suc_le_lessD ‹∄N. ∀n≥N. y < f (xn n)› not_le someI_ex)
qed
have *:"f (xn (a n)) ≤ y" for n
proof(cases n)
case 0
then show ?thesis
using hc[of 0] by(auto simp: a_def intro!: someI_ex)
next
case (Suc n')
then show ?thesis
by(simp add: a_def) (metis (mono_tags, lifting) Suc_le_lessD hc someI_ex)
qed
have "∃N. ∀n≥N. (xn ∘ a) n ∈ {x ∈ topspace X. f x > y}"
using limitin_subsequence[OF ‹strict_mono a› h(2)] h(1)[rule_format,of y] y
by(fastforce simp: limitin_sequentially)
with * show False
using leD by auto
qed
qed
next
fix a
assume h:" ∀xn x. limitin X xn x sequentially ⟶ f x ≤ liminf (λn. f (xn n))"
show "openin X {x ∈ topspace X. a < f x}"
unfolding limitin_openin_sequentially[OF assms]
proof safe
fix x xn
assume h':"limitin X xn x sequentially" "x ∈ topspace X" "f x > a"
with h have "f x ≤ liminf (λn. f (xn n))"
by auto
with h'(3) obtain N where N:"⋀n. n≥N ⟹ f (xn n) > a"
by(auto simp: le_Liminf_iff eventually_sequentially)
obtain N' where N': "⋀n. n≥N' ⟹ xn n ∈ topspace X"
by (meson h'(1) limitin_sequentially openin_topspace)
thus "∃N. ∀n≥N. xn n ∈ {x ∈ topspace X. f x > a}"
using h'(3) N by(auto intro!: exI[where x="max N N'"])
qed
qed
lemma lower_semicontinuous_map_liminf_real:
fixes f :: "'a ⇒ real"
assumes "first_countable X"
shows "lower_semicontinuous_map X f ⟷ (∀xn x. limitin X xn x sequentially ⟶ f x ≤ liminf (λn. f (xn n)))"
unfolding lower_semicontinuous_map_real_iff lower_semicontinuous_map_liminf_iff[OF assms] by simp
end