Theory Alaoglu_Theorem
section ‹Alaoglu's Theorem›
theory Alaoglu_Theorem
imports "Lemmas_Levy_Prokhorov"
"Riesz_Representation.Riesz_Representation"
begin
text ‹ We prove (a special case of) Alaoglu's theorem for the space of continuous functions.
We refer to Section~9 of the lecture note by Heil~\cite{Heil}.›
subsection ‹ Metrizability of the Space of Uniformly Bounded Positive Linear Functionals ›
lemma metrizable_functional:
fixes X :: "'a topology" and r :: real
defines "prod_space ≡ powertop_real (mspace (cfunspace X euclidean_metric))"
defines "B ≡ {φ∈topspace prod_space. φ (λx∈topspace X. 1) ≤ r ∧ positive_linear_functional_on_CX X φ}"
defines "Φ ≡ subtopology prod_space B"
assumes compact: "compact_space X" and met: "metrizable_space X"
shows "metrizable_space Φ"
proof(cases "X = trivial_topology")
case True
hence "metrizable_space prod_space"
by(auto simp: prod_space_def metrizable_space_product_topology metrizable_space_euclidean intro!: countable_finite)
thus ?thesis
using Φ_def metrizable_space_subtopology by blast
next
case X_ne:False
have Haus: "Hausdorff_space X"
using met metrizable_imp_Hausdorff_space by blast
consider "r ≥ 0" | "r < 0"
by fastforce
then show ?thesis
proof cases
case r:1
have B: "B ⊆ topspace prod_space"
by(auto simp: B_def)
have ext_eq: "⋀f::'a ⇒ real. f ∈ mspace (cfunspace X euclidean_metric) ⟹ (λx∈topspace X. f x) = f"
by (auto simp: extensional_def)
have met1: "metrizable_space (mtopology_of (cfunspace X euclidean_metric))"
by (metis Metric_space.metrizable_space_mtopology Metric_space_mspace_mdist mtopology_of_def)
have "separable_space (mtopology_of (cfunspace X (euclidean_metric :: real metric)))"
proof -
have "separable_space (mtopology_of (cfunspace X (Met_TC.Self :: real metric)))"
using Met_TC.Metric_space_axioms Met_TC.separable_space_iff_second_countable
by(auto intro!: Metric_space.separable_space_cfunspace[OF _ _ _ met compact])
thus ?thesis
by (simp add: Met_TC.Self_def euclidean_metric_def)
qed
then obtain F where dense:"mdense_of (cfunspace X (euclidean_metric :: real metric)) F" and F_count: "countable F"
using separable_space_def2 by blast
have "infinite (topspace (mtopology_of (cfunspace X (euclidean_metric :: real metric))))"
proof(rule infinite_super[where S="(λn::nat. λx∈topspace X. real n) ` UNIV"])
show "infinite (range (λn. λx∈topspace X. real n))"
proof(intro range_inj_infinite inj_onI)
fix n m
assume h:"(λx∈topspace X. real n) = (λx∈topspace X. real m)"
from X_ne obtain x where "x ∈ topspace X" by fastforce
with fun_cong[OF h,of x] show "n = m"
by simp
qed
qed(auto simp: bounded_iff)
from countable_as_injective_image[OF F_count dense_in_infinite[OF metrizable_imp_t1_space[OF met1] this dense]]
obtain gn :: "nat ⇒ _" where gn: "F = range gn" "inj gn"
by blast
then have gn_in: "⋀n. gn n ∈ F" "⋀n. gn n ∈ mspace (cfunspace X euclidean_metric)"
using dense_in_subset[OF dense] by auto
hence gn_ext: "⋀n. (λx∈topspace X. gn n x) = gn n"
by(auto intro!: ext_eq)
define d :: "[('a ⇒ real) ⇒ real, ('a ⇒ real) ⇒ real] ⇒ real"
where "d ≡ (λφ ψ. (∑n. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn n x)) (ψ (λx∈topspace X. gn n x))))"
have smble[simp]: "summable (λn. (1 / 2) ^ n * mdist (capped_metric 1 (euclidean_metric :: real metric)) (a n) (b n))"
for a b
by(rule summable_comparison_test'[where N=0 and g="λn. (1 / 2) ^ n * 1"]) (auto intro!: mdist_capped)
interpret d: Metric_space "topspace Φ" d
proof
show "⋀x y. 0 ≤ d x y"
by(auto intro!: suminf_nonneg simp: d_def)
show "⋀x y. d x y = d y x"
by(auto simp: d_def simp: mdist_commute)
next
fix φ ψ
assume h:"φ ∈ topspace Φ" "ψ ∈ topspace Φ"
show "d φ ψ = 0 ⟷ φ = ψ"
proof
assume "d φ ψ = 0"
then have "∀n. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn n x)) (ψ (λx∈topspace X. gn n x)) = 0"
by(intro suminf_eq_zero_iff[THEN iffD1]) (auto simp: d_def)
hence eq:"⋀n. φ (λx∈topspace X. gn n x) = ψ (λx∈topspace X. gn n x)"
by simp
show "φ = ψ"
proof
fix f
consider "f ∉ mspace (cfunspace X (euclidean_metric :: real metric))"
| "f ∈ mspace (cfunspace X (euclidean_metric :: real metric))"
by blast
thus "φ f = ψ f"
proof cases
case 1
then show ?thesis
using h by(auto simp: Φ_def prod_space_def PiE_def extensional_def simp del: mspace_cfunspace)
next
case f:2
then have "positive_linear_functional_on_CX X φ" "positive_linear_functional_on_CX X ψ"
using h by(auto simp: Φ_def topspace_subtopology_subset[OF B] B_def)
from Riesz_representation_real_compact_metrizable[OF compact met this(1)]
Riesz_representation_real_compact_metrizable[OF compact met this(2)]
obtain N L where
N: "sets N = sets (borel_of X)" "finite_measure N"
"⋀f. continuous_map X euclideanreal f ⟹ φ (restrict f (topspace X)) = integral⇧L N f"
and L: "sets L = sets (borel_of X)" "finite_measure L"
"⋀f. continuous_map X euclideanreal f ⟹ ψ (restrict f (topspace X)) = integral⇧L L f"
by auto
have f_ext:"(λx∈topspace X. f x) = f"
using f by (auto simp: extensional_def)
have "φ f = φ (λx∈topspace X. f x)"
by(simp add: f_ext)
also have "... = integral⇧L N f"
using f by(auto intro!: N)
also have "... = integral⇧L L f"
proof(rule finite_measure_integral_eq_dense[where F=F and X=X])
fix g
assume "g ∈ F"
then obtain n where n:"g = gn n"
using gn by fast
hence "integral⇧L N g = integral⇧L N (gn n)"
by simp
also have "... = φ (λx∈topspace X. gn n x)"
using gn_in by(auto intro!: N(3)[symmetric])
also have "... = integral⇧L L g"
using gn_in by(auto simp: eq n intro!: L(3))
finally show "integral⇧L N g = integral⇧L L g" .
qed(use N L dense f in auto)
also have "... = ψ (λx∈topspace X. f x)"
using f by(auto intro!: L(3)[symmetric])
also have "... = ψ f"
by(simp add: f_ext)
finally show ?thesis .
qed
qed
qed (auto simp add: d_def capped_metric_mdist)
next
fix φ1 φ2 φ3
assume h: "φ1 ∈ topspace Φ" "φ2 ∈ topspace Φ" "φ3 ∈ topspace Φ"
show "d φ1 φ3 ≤ d φ1 φ2 + d φ2 φ3"
proof -
have "d φ1 φ3 ≤ (∑n. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ1 (λx∈topspace X. gn n x)) (φ2 (λx∈topspace X. gn n x))
+ (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ2 (λx∈topspace X. gn n x)) (φ3 (λx∈topspace X. gn n x)))"
by(auto intro!: suminf_le mdist_triangle summable_add[OF smble smble,simplified distrib_left[symmetric]]
simp: d_def distrib_left[symmetric])
also have "... = d φ1 φ2 + d φ2 φ3"
by(simp add: suminf_add d_def)
finally show ?thesis .
qed
qed
have "Φ = d.mtopology"
unfolding topology_eq
proof safe
have "continuous_map d.mtopology (subtopology prod_space B) id"
unfolding continuous_map_in_subtopology prod_space_def id_apply image_id continuous_map_componentwise
proof safe
fix f :: "'a ⇒ real"
assume f: "f ∈ mspace (cfunspace X (euclidean_metric))"
hence f_ext: "(λx∈topspace X. f x) = f"
by(auto intro!: ext_eq)
show "continuous_map d.mtopology euclideanreal (λx. x f)"
unfolding continuous_map_iff_limit_seq[OF d.first_countable_mtopology]
proof safe
fix φn φ
assume φ_limit:"limitin d.mtopology φn φ sequentially"
have "(λn. φn n f) ⇢ φ f"
proof(rule LIMSEQ_I)
fix e :: real
assume e: "e > 0"
from f mdense_of_def3[THEN iffD1,OF dense] obtain fn where fn:
"⋀n. fn n ∈ F" "limitin (mtopology_of (cfunspace X euclidean_metric)) fn f sequentially"
by fast
with f dense_in_subset[OF dense] have fn_ext:"⋀n. (λx∈topspace X. fn n x) = fn n"
by(intro ext_eq) auto
define a0 where "a0 ≡ (SOME n. ∀x∈topspace X. ¦fn n x - f x¦ ≤ (1 / 3) * (1 / (r + 1)) * e)"
have a0:"∀x∈topspace X. ¦fn a0 x - f x¦ ≤ (1 / 3) * (1 / (r + 1)) * e"
unfolding a0_def
proof(rule someI_ex)
have "⋀e. e > 0 ⟹ ∃N. ∀n≥N. mdist (cfunspace X euclidean_metric) (fn n) f < e"
by (metis Metric_space.limit_metric_sequentially Metric_space_mspace_mdist fn(2) mtopology_of_def)
from this[of "((1 / 3) * (1 / (r + 1)) * e)"]
obtain N where N: "⋀n. n ≥ N ⟹ mdist (cfunspace X euclidean_metric) (fn n) f < ((1 / 3) * (1 / (r + 1)) * e)"
using e r by auto
hence "mdist (cfunspace X euclidean_metric) (fn N) f ≤ ((1 / 3) * (1 / (r + 1)) * e)"
by fastforce
from mdist_cfunspace_imp_mdist_le[OF _ _ this]
have le:"⋀x. x ∈ topspace X ⟹ ¦fn N x - f x¦ ≤ ((1 / 3) * (1 / (r + 1)) * e)"
using fn(1)[of N] dense_in_subset[OF dense] f dist_real_def by auto
thus "∃n. ∀x∈topspace X. ¦fn n x - f x¦ ≤ 1 / 3 * (1 / (r + 1)) * e"
by(auto intro!: exI[where x=N])
qed
obtain l where l: "fn a0 = gn l"
using fn gn by blast
have "⋀e. e > 0 ⟹ ∃N. ∀n≥N. φn n ∈ topspace Φ ∧ d (φn n) φ < e"
using φ_limit by(fastforce simp: mtopology_of_def d.limit_metric_sequentially)
from this[of "(1 / 2) ^ l * (1 / 3) * min 3 e"] e
obtain N where N: "⋀n. n ≥ N ⟹ φn n ∈ topspace Φ"
"⋀n. n ≥ N ⟹ d (φn n) φ < (1 / 2) ^ l * (1 / 3) * min 3 e"
by auto
show "∃no. ∀n≥no. norm (φn n f - φ f) < e"
proof(safe intro!: exI[where x=N])
fix n
assume n: "N ≤ n"
have "norm (φn n f - φ f) ≤ ¦φn n (fn a0) - φ (fn a0)¦ + ¦φ (fn a0) - φ f¦ + ¦φn n (fn a0) - φn n f¦"
by fastforce
also have "... < (1 / 3) * e + (1 / 3) * e + (1 / 3) * e"
proof -
have 1: "¦φn n (fn a0) - φ (fn a0)¦ < (1 / 3) * e"
proof(rule ccontr)
assume " ¬ ¦φn n (fn a0) - φ (fn a0)¦ < 1 / 3 * e"
then have 1:"¦φn n (fn a0) - φ (fn a0)¦ ≥ (1 / 3) * e"
by linarith
have le1: "¦φn n (fn a0) - φ (fn a0)¦ < 1"
proof (rule ccontr)
assume "¬ ¦φn n (fn a0) - φ (fn a0)¦ < 1"
then have contr:"¦φn n (fn a0) - φ (fn a0)¦ ≥ 1"
by linarith
consider "e > 3" | "e ≤ 3"
by fastforce
then show False
proof cases
case 1
with N[OF n] have "d (φn n) φ < (1 / 2) ^ l"
by simp
also have "... = (∑m. if m = l then (1 / 2) ^ l else 0)"
using suminf_split_initial_segment[where f="λm. if m = l then (1 / 2) ^ l else (0 :: real)" and k="Suc l"]
by simp
also have "... ≤ d (φn n) φ"
unfolding d_def
proof(rule suminf_le)
fix m
show "(if m = l then (1 / 2) ^ l else 0)
≤ (1 / 2) ^ m * mdist (capped_metric 1 euclidean_metric)
(φn n (restrict (gn m) (topspace X)))
(φ (restrict (gn m) (topspace X)))"
using contr by(auto simp: l gn_ext capped_metric_mdist dist_real_def)
qed auto
finally show False
by blast
next
case 2
then have "(1 / 2) ^ l * (1 / 3) * min 3 e ≤ (1 / 2)^l"
by simp
also have "... = (∑m. if m = l then (1 / 2) ^ l else 0)"
using suminf_split_initial_segment[where f="λm. if m = l then (1 / 2) ^ l else (0 :: real)" and k="Suc l"]
by simp
also have "... ≤ d (φn n) φ"
unfolding d_def
proof(rule suminf_le)
fix m
show "(if m = l then (1 / 2) ^ l else 0)
≤ (1 / 2) ^ m * mdist (capped_metric 1 euclidean_metric)
(φn n (restrict (gn m) (topspace X)))
(φ (restrict (gn m) (topspace X)))"
using contr by(auto simp: l gn_ext capped_metric_mdist dist_real_def)
qed auto
also have "... < (1 / 2) ^ l * (1 / 3) * min 3 e"
by(rule N[OF n])
finally show False by simp
qed
qed
hence mdist1: "mdist (capped_metric 1 euclidean_metric)
(φn n (restrict (gn l) (topspace X)))
(φ (restrict (gn l) (topspace X)))
= ¦φn n (fn a0) - φ (fn a0)¦"
by(auto simp: capped_metric_mdist dist_real_def gn_ext l)
have "(1 / 2) ^ l * (1 / 3) * min 3 e ≤ (1 / 2) ^ l * (1 / 3) * e"
using e by simp
also have "... = (∑m. if m = l then (1 / 2) ^ l * (1 / 3) * e else 0)"
using suminf_split_initial_segment[where f="λm. if m = l then (1 / 2) ^ l * (1 / 3) * e else 0" and k="Suc l"]
by simp
also have "... ≤ d (φn n) φ"
using 1 le1 by (fastforce simp: mdist1 d_def intro!: suminf_le)
finally show False
using N[OF n] by linarith
qed
have 2: " ¦φ (fn a0) - φ f¦ ≤ (1 / 3) * e"
proof -
from limitin_topspace[OF φ_limit,simplified]
have plf:"positive_linear_functional_on_CX X φ"
by(simp add: Φ_def B_def)
from Riesz_representation_real_compact_metrizable[OF compact met this]
obtain N where N: "sets N = sets (borel_of X)" "finite_measure N"
"⋀f. continuous_map X euclideanreal f ⟹ φ (restrict f (topspace X)) = integral⇧L N f"
by blast
hence space_N: "space N = topspace X"
by(auto cong: sets_eq_imp_space_eq simp: space_borel_of)
interpret N: finite_measure N by fact
have [measurable]: "fn a0 ∈ borel_measurable N" "f ∈ borel_measurable N"
using continuous_map_measurable[of X euclideanreal] fn(1) f dense_in_subset[OF dense]
by(auto simp: measurable_cong_sets[OF N(1) refl]
intro!: continuous_map_measurable[of X euclideanreal,simplified borel_of_euclidean])
have "φ (fn a0) - φ f = φ (λx∈topspace X. fn a0 x) - φ (λx∈topspace X. f x)"
by(simp add: fn_ext f_ext)
also have "... = φ (λx∈topspace X. fn a0 x) + φ (λx∈topspace X. - f x)"
using f by(auto intro!: pos_lin_functional_on_CX_compact_lin(1)[OF plf compact,of _ "-1",simplified,symmetric])
also have "... = φ (λx∈topspace X. fn a0 x + - f x)"
by(rule pos_lin_functional_on_CX_compact_lin(2)[symmetric])
(use fn(1) f dense_in_subset[OF dense] plf compact in auto)
also have "... = φ (λx∈topspace X. fn a0 x - f x)"
by simp
also have "... = (∫x. fn a0 x - f x ∂N)"
using fn(1) f dense_in_subset[OF dense] by(auto intro!: N(3) continuous_map_diff)
finally have "¦φ (fn a0) - φ f¦ = ¦(∫x. fn a0 x - f x ∂N)¦"
by simp
also have "... ≤ (∫x. ¦fn a0 x - f x¦ ∂N)"
by(rule integral_abs_bound)
also have "... ≤ (∫x. (1 / 3) * (1 / (r + 1)) * e ∂N)"
by(rule Bochner_Integration.integral_mono,insert a0)
(auto intro!: N.integrable_const_bound[where B="(1 / 3) * (1 / (r + 1)) * e"] simp: space_N)
also have "... = (1 / 3) * e * ((1 / (r + 1) * measure N (space N)))"
by simp
also have "... ≤ (1 / 3) * e"
proof -
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = φ (λx∈topspace X. 1)"
by(intro N(3)[symmetric]) simp
also have "... ≤ r"
using limitin_topspace[OF φ_limit,simplified] by(auto simp: Φ_def B_def)
finally have "(1 / (r + 1) * measure N (space N)) ≤ 1"
using r by simp
thus ?thesis
unfolding mult_le_cancel_left2 using e by auto
qed
finally show ?thesis .
qed
have 3: " ¦φn n (fn a0) - φn n f¦ ≤ (1 / 3) * e"
proof -
have plf:"positive_linear_functional_on_CX X (φn n)"
using N(1)[OF n] by(simp add: Φ_def B_def)
from Riesz_representation_real_compact_metrizable[OF compact met this]
obtain N where N': "sets N = sets (borel_of X)" "finite_measure N"
"⋀f. continuous_map X euclideanreal f ⟹ φn n (restrict f (topspace X)) = integral⇧L N f"
by blast
hence space_N: "space N = topspace X"
by(auto cong: sets_eq_imp_space_eq simp: space_borel_of)
interpret N: finite_measure N by fact
have [measurable]: "fn a0 ∈ borel_measurable N" "f ∈ borel_measurable N"
using continuous_map_measurable[of X euclideanreal] fn(1) f dense_in_subset[OF dense]
by(auto simp: measurable_cong_sets[OF N'(1) refl]
intro!: continuous_map_measurable[of X euclideanreal,simplified borel_of_euclidean])
have "φn n (fn a0) - φn n f = φn n (λx∈topspace X. fn a0 x) - φn n (λx∈topspace X. f x)"
by(simp add: fn_ext f_ext)
also have "... = φn n (λx∈topspace X. fn a0 x) + φn n (λx∈topspace X. - f x)"
using f by(auto intro!: pos_lin_functional_on_CX_compact_lin(1)[OF plf compact,of _ "-1",simplified,symmetric])
also have "... = φn n (λx∈topspace X. fn a0 x + - f x)"
by(rule pos_lin_functional_on_CX_compact_lin(2)[symmetric])
(use fn(1) plf compact f dense_in_subset[OF dense] in auto)
also have "... = φn n (λx∈topspace X. fn a0 x - f x)"
by simp
also have "... = (∫x. fn a0 x - f x ∂N)"
using fn(1) f dense_in_subset[OF dense] by(auto intro!: N'(3) continuous_map_diff)
finally have "¦φn n (fn a0) - φn n f¦ = ¦(∫x. fn a0 x - f x ∂N)¦"
by simp
also have "... ≤ (∫x. ¦fn a0 x - f x¦ ∂N)"
by(rule integral_abs_bound)
also have "... ≤ (∫x. (1 / 3) * (1 / (r + 1)) * e ∂N)"
by(rule Bochner_Integration.integral_mono,insert a0)
(auto intro!: N.integrable_const_bound[where B="(1 / 3) * (1 / (r + 1)) * e"] simp: space_N)
also have "... = (1 / 3) * e * ((1 / (r + 1) * measure N (space N)))"
by simp
also have "... ≤ (1 / 3) * e"
proof -
have "measure N (space N) = (∫x. 1 ∂N)"
by simp
also have "... = φn n (λx∈topspace X. 1)"
by(intro N'(3)[symmetric]) simp
also have "... ≤ r"
using N(1)[OF n] by(auto simp: Φ_def B_def)
finally have "(1 / (r + 1) * measure N (space N)) ≤ 1"
using r by simp
thus ?thesis
unfolding mult_le_cancel_left2 using e by auto
qed
finally show ?thesis .
qed
show ?thesis
using 1 2 3 by simp
qed
also have "... = e"
by simp
finally show "norm (φn n f - φ f) < e" .
qed
qed
thus "limitin euclideanreal (λn. φn n f) (φ f) sequentially"
by simp
qed
next
show "⋀x. x ∈ topspace d.mtopology ⟹ x ∈ extensional (mspace (cfunspace X euclidean_metric))"
unfolding d.topspace_mtopology by (auto simp: Φ_def prod_space_def extensional_def simp del: mspace_cfunspace)
qed (simp, auto simp: Φ_def)
thus "⋀S. openin Φ S ⟹ openin d.mtopology S"
by (metis Φ_def d.topspace_mtopology topology_finer_continuous_id)
next
have "continuous_map Φ d.mtopology id"
unfolding d.continuous_map_to_metric id_apply
proof safe
fix φ and e::real
assume φ: "φ ∈ topspace Φ" and e: "0 < e"
then obtain N where N: "(1 / 2)^N < e / 2"
by (meson half_gt_zero_iff one_less_numeral_iff reals_power_lt_ex semiring_norm(76))
define e' where "e' ≡ e / 2 - (1 / 2)^N"
have e': "0 < e'"
using N by(auto simp: e'_def)
define U' where "U' ≡ Π⇩E f∈mspace (cfunspace X euclidean_metric).
if ∃n<N. f = gn n then {φ (λx∈topspace X. f x) - e'<..<φ (λx∈topspace X. f x) + e'} else UNIV"
define U where "U ≡ U' ∩ B"
show "∃U. openin Φ U ∧ φ ∈ U ∧ (∀y∈U. y ∈ d.mball φ e)"
proof(safe intro!: exI[where x=U])
show "openin Φ U"
unfolding Φ_def openin_subtopology U_def
proof(safe intro!: exI[where x=U'])
show "openin prod_space U'"
unfolding prod_space_def U'_def openin_PiE_gen
by (auto simp: Let_def)
qed
next
show "φ ∈ U"
unfolding U_def U'_def
proof safe
fix f :: "'a ⇒ real"
assume f: "f ∈ mspace (cfunspace X euclidean_metric)"
then show "φ f ∈ (if ∃n<N. f = gn n
then {φ (restrict f (topspace X)) - e'<..<φ (restrict f (topspace X)) + e'}
else UNIV)"
using e' by(auto simp: Let_def gn_ext)
qed(use φ Φ_def prod_space_def in auto)
next
fix ψ
assume ψ:"ψ ∈ U"
then have ψ2: "ψ ∈ topspace Φ"
using topspace_subtopology_subset[OF B] by(auto simp: U_def Φ_def)
have ψ_le: "¦φ (λx∈topspace X. gn n x) - ψ (λx∈topspace X. gn n x)¦ < e'" if n: "n < N" for n
proof -
have "ψ ∈ (Π⇩E f∈mspace (cfunspace X euclidean_metric).
if ∃n<N. f = gn n
then {φ (restrict f (topspace X)) - e'<..<φ (restrict f (topspace X)) + e'}
else UNIV)"
using ψ by(auto simp: U_def U'_def)
from PiE_mem[OF this gn_in(2)[of n]]
have "ψ (λx∈topspace X. gn n x) ∈ (if ∃m<N. gn n = gn m
then {φ (restrict (gn n) (topspace X)) - e'<..<φ (restrict (gn n) (topspace X)) + e'}
else UNIV)"
by(simp add: gn_ext)
thus ?thesis
by (metis abs_diff_less_iff diff_less_eq greaterThanLessThan_iff n)
qed
have "d φ ψ < e"
proof -
have "d φ ψ = (∑n. (1 / 2) ^ (n + N) * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn (n + N) x))
(ψ (λx∈topspace X. gn (n + N) x)))
+ (∑n<N. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn n x))
(ψ (λx∈topspace X. gn n x)))"
unfolding d_def by(rule suminf_split_initial_segment d_def) simp
also have "... ≤ (∑n. (1 / 2) ^ (n + N))
+ (∑n<N. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn n x))
(ψ (λx∈topspace X. gn n x)))"
by(auto intro!: suminf_le mdist_capped summable_ignore_initial_segment[where k=N])
also have "... = (1 / 2)^N * 2
+ (∑n<N. (1 / 2) ^ n * mdist (capped_metric 1 euclidean_metric)
(φ (λx∈topspace X. gn n x))
(ψ (λx∈topspace X. gn n x)))"
using nsum_of_r'[where r="1/2" and K=1 and k=N,simplified] by simp
also have "... ≤ (1 / 2)^N * 2
+ (∑n<N. (1 / 2) ^ n * ¦φ (λx∈topspace X. gn n x) - ψ (λx∈topspace X. gn n x)¦)"
by(auto intro!: sum_mono mdist_capped_le[where m="euclidean_metric :: real metric",simplified,simplified dist_real_def])
also have "... ≤ (1 / 2)^N * 2 + (∑n<N. (1 / 2) ^ n * e')"
using ψ_le by(fastforce intro!: sum_mono)
also have "... < (1 / 2)^N * 2 + (∑n<Suc N. (1 / 2) ^ n * e')"
using e' by(auto intro!: sum_strict_mono2)
also have "... ≤ (1 / 2)^N * 2 + (∑n. (1 / 2) ^ n * e')"
using e' by(auto intro!: sum_le_suminf summable_mult2 simp del: sum.lessThan_Suc)
also have "... = (1 / 2)^N * 2 + (∑n. (1 / 2) ^ n) * e'"
by(auto intro!: suminf_mult2[symmetric])
also have "... = (1 / 2)^N * 2 + 2 * e'"
by(auto simp: suminf_geometric)
also have "... = e"
by(auto simp: e'_def)
finally show ?thesis .
qed
with φ ψ2 show "ψ ∈ d.mball φ e"
by simp
qed
qed
thus "⋀S. openin d.mtopology S ⟹ openin Φ S"
by (metis d.topspace_mtopology topology_finer_continuous_id)
qed
thus ?thesis
using d.metrizable_space_mtopology by presburger
next
case r:2
have False if h:"φ ∈ B" for φ
proof -
have 1: "φ (λx∈topspace X. 1) ≤ r"
using h by(auto simp: B_def)
have 2: "φ (λx∈topspace X. 1) ≥ 0"
using h by(auto simp: B_def pos_lin_functional_on_CX_compact_pos[OF _ compact])
from 1 2 r show False by linarith
qed
hence "B = {}"
by auto
thus ?thesis
by(auto simp: Φ_def)
qed
qed
subsection ‹Alaoglu's Theorem›
text ‹ According to Alaoglu's theorem, $\{\varphi\in C(X)^*\mid \Vert \varphi\Vert\leq r\}$ is compact.
We show that
$\Phi = \{\varphi\in C(X)^*\mid \Vert\varphi\Vert\leq r\land \varphi\text{ is positive}\}$
is compact.
Note that $\Vert \varphi\Vert = \varphi(1)$ when $\varphi\in C(X)^*$ is positive.›
theorem Alaoglu_theorem_real_functional:
fixes X :: "'a topology" and r :: real
defines "prod_space ≡ powertop_real (mspace (cfunspace X euclidean_metric))"
defines "B ≡ {φ∈topspace prod_space. φ (λx∈topspace X. 1) ≤ r ∧ positive_linear_functional_on_CX X φ}"
assumes compact: "compact_space X" and ne: "topspace X ≠ {}"
shows "compactin prod_space B"
proof -
consider "r ≥ 0" | "r < 0"
by linarith
then show ?thesis
proof cases
assume rpos:"r ≥ 0"
have continuous_map_compact_space_bounded: "⋀f. continuous_map X euclideanreal f ⟹ bounded (f ` topspace X)"
by (meson compact compact_imp_bounded compact_space_def compactin_euclidean_iff image_compactin)
have 1: "compactin prod_space
(Π⇩E f∈mspace (cfunspace X euclidean_metric). {- r * (⨆x∈topspace X. ¦f x¦).. r * (⨆x∈topspace X. ¦f x¦)})"
by(auto simp: prod_space_def compactin_PiE)
have 2: "B ⊆ (Π⇩E f∈mspace (cfunspace X euclidean_metric). {- r * (⨆x∈topspace X. ¦f x¦).. r * (⨆x∈topspace X. ¦f x¦)})"
proof safe
fix φ and f :: "'a ⇒ real"
assume h:"φ ∈ B" "f ∈ mspace (cfunspace X euclidean_metric)"
then have f: "continuous_map X euclideanreal f" "f ∈ topspace X →⇩E UNIV"
by (auto simp: extensional_def)
have plf:"positive_linear_functional_on_CX X φ"
using h(1) by(auto simp: B_def)
note φ = pos_lin_functional_on_CX_compact_lin[OF plf compact]
pos_lin_functional_on_CX_compact_pos[OF plf compact]
note φ_mono = pos_lin_functional_on_CX_compact_mono[OF plf compact]
note φ_neg = pos_lin_functional_on_CX_compact_uminus[OF plf compact f(1),symmetric]
obtain K where K: "⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ K"
using h(2) bounded_real by auto
have f_Sup: "⋀x. x ∈ topspace X ⟹ ¦f x¦ ≤ (⨆x∈topspace X. ¦f x¦)"
by(auto intro!: cSup_upper bdd_aboveI[where M=B] K)
hence f_Sup_nonneg: "(⨆x∈topspace X. ¦f x¦) ≥ 0"
using ne by fastforce
have "¦φ f¦ = ¦φ (λx∈topspace X. f x)¦"
using f(2) by fastforce
also have "... ≤ φ (λx∈topspace X. ¦f x¦)"
using φ_mono[OF _ f(1) continuous_map_norm[OF f(1),simplified]]
φ(3)[OF continuous_map_norm[OF f(1),simplified]]
φ_mono[OF _ continuous_map_minus[OF f(1)] continuous_map_norm[OF f(1),simplified]]
by(cases "φ (restrict f (topspace X)) ≥ 0") (auto simp: φ_neg)
also have "... ≤ φ (λx∈topspace X. (⨆x∈topspace X. ¦f x¦) * 1)"
using continuous_map_norm[where 'b=real] f(1) f_Sup
by(intro φ_mono) auto
also have "... = (⨆x∈topspace X. ¦f x¦) * φ (λx∈topspace X. 1)"
by(intro φ) simp
also have "... ≤ r * (⨆x∈topspace X. ¦f x¦)"
using h(1) f_Sup_nonneg by(auto simp: B_def mult.commute mult_right_mono)
finally show "φ f ∈ {- r * (⨆x∈topspace X. ¦f x¦).. r * (⨆x∈topspace X. ¦f x¦)}"
by auto
qed (auto simp: prod_space_def B_def)
have 3: "closedin prod_space B"
proof(rule closedin_limitin)
fix φn φ
assume h:"⋀U. φ ∈ U ⟹ openin prod_space U ⟹ φn U ≠ φ"
"⋀U. φ ∈ U ⟹ openin prod_space U ⟹ φn U ∈ B"
"limitin prod_space φn φ (nhdsin_sets prod_space φ)"
then have xnx:"φ ∈ extensional (mspace (cfunspace X euclidean_metric))"
"(∀⇩F U in nhdsin_sets prod_space φ. φn U ∈ topspace prod_space)"
"⋀f. f∈mspace (cfunspace X euclidean_metric) ⟹ limitin euclideanreal (λc. φn c f) (φ f) (nhdsin_sets prod_space φ)"
by(auto simp: limitin_componentwise prod_space_def)
have φ_top:"φ ∈ topspace prod_space"
by (meson h(3) limitin_topspace)
show "φ ∈ B"
unfolding B_def
proof safe
have limit: "limitin euclideanreal (λc. φn c (λx∈topspace X. 1)) (φ (λx∈topspace X. 1)) (nhdsin_sets prod_space φ)"
by(rule xnx(3)) (auto simp: bounded_iff)
show "φ (λx∈topspace X. 1) ≤ r"
using h(2)
by(auto intro!: tendsto_upperbound[OF limit[simplified] _ nhdsin_sets_bot[OF φ_top]]
eventually_nhdsin_setsI[OF φ_top] simp: B_def)
next
show "positive_linear_functional_on_CX X φ"
unfolding positive_linear_functional_on_CX_compact[OF compact]
proof safe
fix c f
assume f: "continuous_map X euclideanreal f"
then have f':"(λx∈topspace X. c * f x) ∈ mspace (cfunspace X euclidean_metric)"
"(λx∈topspace X. f x) ∈ mspace (cfunspace X euclidean_metric)"
by(auto simp: intro!: continuous_map_compact_space_bounded continuous_map_real_mult_left)
have tends1:"((λU. c * φn U (λx∈topspace X. f x)) ⤏ φ (λx∈topspace X. c * f x)) (nhdsin_sets prod_space φ)"
using B_def f h(2) by(fastforce intro!: tendsto_cong[THEN iffD1,OF _ xnx(3)[OF f'(1),simplified]]
eventually_nhdsin_setsI[OF φ_top] pos_lin_functional_on_CX_compact_lin[OF _ compact f])
show "φ (λx∈topspace X. c * f x) = c * φ (λx∈topspace X. f x)"
by(rule tendsto_unique[OF nhdsin_sets_bot[OF φ_top] tends1 tendsto_mult_left[OF xnx(3)[OF f'(2),simplified]]])
next
fix f g
assume fg:"continuous_map X euclideanreal f" "continuous_map X euclideanreal g"
then have fg': "(λx∈topspace X. f x) ∈ mspace (cfunspace X euclidean_metric)"
"(λx∈topspace X. g x) ∈ mspace (cfunspace X euclidean_metric)"
"(λx∈topspace X. f x + g x) ∈ mspace (cfunspace X euclidean_metric)"
by(auto intro!: continuous_map_compact_space_bounded continuous_map_add)
have "((λc. φn c (λx∈topspace X. f x) + φn c (λx∈topspace X. g x))
⤏ φ (λx∈topspace X. f x + g x)) (nhdsin_sets prod_space φ)"
using B_def fg h(2)
by(fastforce intro!: tendsto_cong[THEN iffD1,OF _ xnx(3)[OF fg'(3),simplified]]
eventually_nhdsin_setsI[OF φ_top] pos_lin_functional_on_CX_compact_lin[OF _ compact])
moreover have "((λc. φn c (λx∈topspace X. f x) + φn c (λx∈topspace X. g x))
⤏ φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x)) (nhdsin_sets prod_space φ)"
using xnx fg' by(auto intro!: tendsto_add)
ultimately show "φ (λx∈topspace X. f x + g x) = φ (λx∈topspace X. f x) + φ (λx∈topspace X. g x)"
by(rule tendsto_unique[OF nhdsin_sets_bot[OF φ_top]])
next
fix f
assume f:"continuous_map X euclideanreal f" "∀x∈topspace X. 0 ≤ f x"
then have 1:"(λx∈topspace X. f x) ∈ mspace (cfunspace X euclidean_metric)"
by(auto intro!: continuous_map_compact_space_bounded)
from f h(2) show "0 ≤ φ (λx∈topspace X. f x)"
by(auto intro!: tendsto_lowerbound[OF xnx(3)[OF 1,simplified] _ nhdsin_sets_bot[OF φ_top]]
eventually_nhdsin_setsI[OF φ_top] simp: B_def pos_lin_functional_on_CX_compact_pos[OF _ compact f(1)])
qed
qed fact
qed(auto simp: B_def)
show ?thesis
using 1 2 3 by(rule closed_compactin)
next
assume r:"r < 0"
have "B = {}"
proof safe
fix φ
assume h:"φ ∈ B"
then have "⋀f. continuous_map X euclideanreal f ⟹ (⋀x. x ∈ topspace X ⟹ f x ≥ 0) ⟹ φ (λx∈topspace X. f x) ≥ 0"
by(auto simp: B_def pos_lin_functional_on_CX_compact_pos[OF _ compact])
from this[of "λx. 1"] h r show "φ ∈ {}"
by(auto simp: B_def)
qed
thus "compactin prod_space B"
by blast
qed
qed
theorem Alaoglu_theorem_real_functional_seq:
fixes X :: "'a topology" and r :: real
defines "prod_space ≡ powertop_real (mspace (cfunspace X euclidean_metric))"
defines "B ≡ {φ∈topspace prod_space. φ (λx∈topspace X. 1) ≤ r ∧ positive_linear_functional_on_CX X φ}"
assumes compact:"compact_space X" and ne: "topspace X ≠ {}" and met: "metrizable_space X"
shows "seq_compactin prod_space B"
proof -
have "compactin prod_space B"
using Alaoglu_theorem_real_functional[OF compact ne] by(auto simp: B_def prod_space_def)
hence "compact_space (subtopology prod_space B)"
using compact_space_subtopology by blast
hence "seq_compact_space (subtopology prod_space B)"
unfolding B_def prod_space_def
using metrizable_seq_compact_space_iff_compact_space[OF metrizable_functional[OF compact met]]
by fast
moreover have "B ⊆ topspace prod_space"
by(auto simp: B_def)
ultimately show ?thesis
by (simp add: inf.absorb_iff2 seq_compact_space_def seq_compactin_subtopology)
qed
end