Theory Weak_Star_Topology
section ‹‹Weak_Star_Topology› -- Weak* topology on complex bounded operators›
theory Weak_Star_Topology
imports Trace_Class Weak_Operator_Topology Misc_Tensor_Product_TTS
begin
unbundle cblinfun_syntax
definition weak_star_topology :: ‹('a::chilbert_space ⇒⇩C⇩L'b::chilbert_space) topology›
where ‹weak_star_topology = pullback_topology UNIV (λx. λt∈Collect trace_class. trace (t o⇩C⇩L x))
(product_topology (λ_. euclidean) (Collect trace_class))›
lemma open_map_product_topology_reindex:
fixes π :: ‹'b ⇒ 'a›
assumes bij_π: ‹bij_betw π B A› and ST: ‹⋀x. x∈B ⟹ S x = T (π x)›
assumes g_def: ‹⋀f. g f = restrict (f o π) B›
shows ‹open_map (product_topology T A) (product_topology S B) g›
proof -
define π' g' where ‹π' = inv_into B π› and ‹g' f = restrict (f ∘ π') A› for f :: ‹'b ⇒ 'c›
have bij_g: ‹bij_betw g (Pi⇩E A V) (Pi⇩E B (V ∘ π))› for V
apply (rule bij_betw_byWitness[where f'=g'])
subgoal
unfolding g'_def g_def π'_def
by (smt (verit, best) PiE_restrict bij_π bij_betw_imp_surj_on bij_betw_inv_into_right comp_eq_dest_lhs inv_into_into restrict_def restrict_ext)
subgoal
unfolding g'_def g_def π'_def
by (smt (verit, ccfv_SIG) PiE_restrict bij_π bij_betwE bij_betw_inv_into_left comp_apply restrict_apply restrict_ext)
subgoal
unfolding g'_def g_def π'_def
using PiE_mem bij_π bij_betw_imp_surj_on by fastforce
subgoal
unfolding g'_def g_def π'_def
by (smt (verit, best) PiE_mem bij_π bij_betw_iff_bijections bij_betw_inv_into_left comp_def image_subset_iff restrict_PiE_iff)
done
have open_gU: ‹openin (product_topology S B) (g ` U)› if ‹openin (product_topology T A) U› for U
proof -
from product_topology_open_contains_basis[OF that]
obtain V where xAV: ‹x ∈ PiE A (V x)› and openV: ‹openin (T a) (V x a)› and finiteV: ‹finite {a. V x a ≠ topspace (T a)}›
and AVU: ‹Pi⇩E A (V x) ⊆ U› if ‹x ∈ U› for x a
apply atomize_elim
apply (rule choice4)
by meson
define V' where ‹V' x b = (if b ∈ B then V x (π b) else topspace (S b))› for b x
have PiEV': ‹Pi⇩E B (V x ∘ π) = Pi⇩E B (V' x)› for x
by (metis (mono_tags, opaque_lifting) PiE_cong V'_def comp_def)
from xAV AVU have AVU': ‹(⋃x∈U. Pi⇩E A (V x)) = U›
by blast
have openVb: ‹openin (S b) (V' x b)› if [simp]: ‹x ∈ U› for x b
by (auto simp: ST V'_def intro!: openV)
have ‹bij_betw π' {a∈A. V x a ≠ topspace (T a)} {b∈B. (V x ∘ π) b ≠ topspace (S b)}› for x
apply (rule bij_betw_byWitness[where f'=π])
apply simp
apply (metis π'_def bij_π bij_betw_inv_into_right)
using π'_def bij_π bij_betw_imp_inj_on apply fastforce
apply (smt (verit, best) ST π'_def bij_π bij_betw_imp_surj_on comp_apply f_inv_into_f image_Collect_subsetI inv_into_into mem_Collect_eq)
using ST bij_π bij_betwE by fastforce
then have ‹finite {b∈B. (V x ∘ π) b ≠ topspace (S b)}› if ‹x ∈ U› for x
apply (rule bij_betw_finite[THEN iffD1])
using that finiteV
by simp
also have ‹{b∈B. (V x ∘ π) b ≠ topspace (S b)} = {b. V' x b ≠ topspace (S b)}› if ‹x ∈ U› for x
by (auto simp: V'_def)
finally have finiteVπ: ‹finite {b. V' x b ≠ topspace (S b)}› if ‹x ∈ U› for x
using that by -
from openVb finiteVπ
have ‹openin (product_topology S B) (Pi⇩E B (V' x))› if [simp]: ‹x ∈ U› for x
by (auto intro!: product_topology_basis)
with bij_g PiEV' have ‹openin (product_topology S B) (g ` (Pi⇩E A (V x)))› if ‹x ∈ U› for x
by (metis bij_betw_imp_surj_on that)
then have ‹openin (product_topology S B) (⋃x∈U. (g ` (Pi⇩E A (V x))))›
by blast
with AVU' show ‹openin (product_topology S B) (g ` U)›
by (metis image_UN)
qed
show ‹open_map (product_topology T A) (product_topology S B) g›
by (simp add: open_gU open_map_def)
qed
lemma homeomorphic_map_product_topology_reindex:
fixes π :: ‹'b ⇒ 'a›
assumes big_π: ‹bij_betw π B A› and ST: ‹⋀x. x∈B ⟹ S x = T (π x)›
assumes g_def: ‹⋀f. g f = restrict (f o π) B›
shows ‹homeomorphic_map (product_topology T A) (product_topology S B) g›
proof (rule bijective_open_imp_homeomorphic_map)
show open_map: ‹open_map (product_topology T A) (product_topology S B) g›
using assms by (rule open_map_product_topology_reindex)
define π' g' where ‹π' = inv_into B π› and ‹g' f = restrict (f ∘ π') A› for f :: ‹'b ⇒ 'c›
have ‹bij_betw π' A B›
by (simp add: π'_def big_π bij_betw_inv_into)
have l1: ‹x ∈ (λx. restrict (x ∘ π) B) ` (Π⇩E i∈A. topspace (T i))› if ‹x ∈ (Π⇩E i∈B. topspace (S i))› for x
proof -
have ‹g' x ∈ (Π⇩E i∈A. topspace (T i))›
by (smt (z3) g'_def PiE_mem π'_def assms(1) assms(2) bij_betw_imp_surj_on bij_betw_inv_into_right comp_apply inv_into_into restrict_PiE_iff that)
moreover have ‹x = restrict (g' x ∘ π) B›
by (smt (verit) PiE_restrict π'_def assms(1) bij_betwE bij_betw_inv_into_left comp_apply restrict_apply restrict_ext that g'_def)
ultimately show ?thesis
by (intro rev_image_eqI)
qed
show topspace: ‹g ` topspace (product_topology T A) = topspace (product_topology S B)›
using l1 assms unfolding g_def [abs_def] topspace_product_topology
by (auto simp: bij_betw_def)
show ‹inj_on g (topspace (product_topology T A))›
apply (simp add: g_def[abs_def])
by (smt (verit) PiE_ext assms(1) bij_betw_iff_bijections comp_apply inj_on_def restrict_apply')
have open_map_g': ‹open_map (product_topology S B) (product_topology T A) g'›
using ‹bij_betw π' A B› apply (rule open_map_product_topology_reindex)
apply (metis ST π'_def big_π bij_betw_imp_surj_on bij_betw_inv_into_right inv_into_into)
using g'_def by blast
have g'g: ‹g' (g x) = x› if ‹x ∈ topspace (product_topology T A)› for x
using that unfolding g'_def g_def topspace_product_topology
by (smt (verit) PiE_restrict ‹bij_betw π' A B› π'_def big_π bij_betwE
bij_betw_inv_into_right comp_def restrict_apply' restrict_ext)
have gg': ‹g (g' x) = x› if ‹x ∈ topspace (product_topology S B)› for x
unfolding g'_def g_def
by (metis (no_types, lifting) g'_def f_inv_into_f g'g g_def inv_into_into that topspace)
from open_map_g'
have ‹openin (product_topology T A) (g' ` U)› if ‹openin (product_topology S B) U› for U
using open_map_def that by blast
also have ‹g' ` U = (g -` U) ∩ (topspace (product_topology T A))› if ‹openin (product_topology S B) U› for U
proof -
from that
have U_top: ‹U ⊆ topspace (product_topology S B)›
using openin_subset by blast
from topspace
have topspace': ‹topspace (product_topology T A) = g' ` topspace (product_topology S B)›
by (metis bij_betw_byWitness bij_betw_def calculation g'g gg' openin_subset openin_topspace)
show ?thesis
unfolding topspace'
using U_top gg'
by auto
qed
finally have open_gU2: ‹openin (product_topology T A) ((g -` U) ∩ (topspace (product_topology T A)))›
if ‹openin (product_topology S B) U› for U
using that by blast
then show ‹continuous_map (product_topology T A) (product_topology S B) g›
by (smt (verit, best) g'g image_iff open_eq_continuous_inverse_map open_map_g' topspace)
qed
lemma weak_star_topology_def':
‹weak_star_topology = pullback_topology UNIV (λx t. trace (from_trace_class t o⇩C⇩L x)) euclidean›
proof -
define f g where ‹f x = (λt∈Collect trace_class. trace (t o⇩C⇩L x))› and ‹g f' = f' o from_trace_class› for x :: ‹'a ⇒⇩C⇩L 'b› and f' :: ‹'b ⇒⇩C⇩L 'a ⇒ complex›
have ‹homeomorphic_map (product_topology (λ_. euclidean) (Collect trace_class)) (product_topology (λ_. euclidean) UNIV) g›
unfolding g_def[abs_def]
apply (rule homeomorphic_map_product_topology_reindex[where π=from_trace_class])
subgoal
by (smt (verit, best) UNIV_I bij_betwI' from_trace_class from_trace_class_cases from_trace_class_inject)
by auto
then have homeo_g: ‹homeomorphic_map (product_topology (λ_. euclidean) (Collect trace_class)) euclidean g›
by (simp add: euclidean_product_topology)
have ‹weak_star_topology = pullback_topology UNIV f (product_topology (λ_. euclidean) (Collect trace_class))›
by (simp add: weak_star_topology_def pullback_topology_homeo_cong homeo_g f_def[abs_def])
also have ‹… = pullback_topology UNIV (g o f) euclidean›
by (subst pullback_topology_homeo_cong)
(auto simp add: homeo_g f_def[abs_def] split: if_splits)
also have ‹… = pullback_topology UNIV (λx t. trace (from_trace_class t o⇩C⇩L x)) euclidean›
by (auto simp: f_def[abs_def] g_def[abs_def] o_def)
finally show ?thesis
by -
qed
lemma weak_star_topology_topspace[simp]:
"topspace weak_star_topology = UNIV"
unfolding weak_star_topology_def topspace_pullback_topology topspace_euclidean by auto
lemma weak_star_topology_basis':
fixes f::"('a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space)" and U::"'i ⇒ complex set" and t::"'i ⇒ ('b,'a) trace_class"
assumes "finite I" "⋀i. i ∈ I ⟹ open (U i)"
shows "openin weak_star_topology {f. ∀i∈I. trace (from_trace_class (t i) o⇩C⇩L f) ∈ U i}"
proof -
have 1: "open {g. ∀i∈I. g (t i) ∈ U i}"
using assms by (rule product_topology_basis')
show ?thesis
unfolding weak_star_topology_def'
apply (subst openin_pullback_topology)
apply (intro exI conjI)
using 1 by auto
qed
lemma weak_star_topology_basis:
fixes f::"('a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space)" and U::"'i ⇒ complex set" and t::"'i ⇒ ('b ⇒⇩C⇩L 'a)"
assumes "finite I" "⋀i. i ∈ I ⟹ open (U i)"
assumes tc: ‹⋀i. i ∈ I ⟹ trace_class (t i)›
shows "openin weak_star_topology {f. ∀i∈I. trace (t i o⇩C⇩L f) ∈ U i}"
proof -
obtain t' where tt': ‹t i = from_trace_class (t' i)› if ‹i ∈ I› for i
by (atomize_elim, rule choice) (use tc from_trace_class_cases in blast)
show ?thesis
using assms by (auto simp: tt' o_def intro!: weak_star_topology_basis')
qed
lemma wot_weaker_than_weak_star:
"continuous_map weak_star_topology cweak_operator_topology (λf. f)"
unfolding weak_star_topology_def cweak_operator_topology_def
proof (rule continuous_map_pullback_both)
define g' :: ‹('b ⇒⇩C⇩L 'a ⇒ complex) ⇒ 'b × 'a ⇒ complex› where
‹g' f = (λ(x,y). f (butterfly y x))› for f
show ‹(λx. λt∈Collect trace_class. trace (t o⇩C⇩L x)) -` topspace (product_topology (λ_. euclidean) (Collect trace_class)) ∩ UNIV
⊆ (λf. f) -` UNIV›
by simp
show ‹g' (λt∈Collect trace_class. trace (t o⇩C⇩L x)) = (λ(xa, y). xa ∙⇩C (x *⇩V y))›
if ‹(λt∈Collect trace_class. trace (t o⇩C⇩L x)) ∈ topspace (product_topology (λ_. euclidean) (Collect trace_class))›
for x
by (auto intro!: ext simp: g'_def trace_butterfly_comp)
show ‹continuous_map (product_topology (λ_. euclidean) (Collect trace_class)) euclidean g'›
apply (subst euclidean_product_topology[symmetric])
apply (rule continuous_map_coordinatewise_then_product)
subgoal for i
unfolding g'_def case_prod_unfold
by (metis continuous_map_product_projection mem_Collect_eq trace_class_butterfly)
subgoal
by (auto simp: g'_def[abs_def])
done
qed
lemma wot_weaker_than_weak_star':
‹openin cweak_operator_topology U ⟹ openin weak_star_topology U›
using wot_weaker_than_weak_star[where 'a='a and 'b='b]
by (auto simp: continuous_map_def weak_star_topology_topspace)
lemma weak_star_topology_continuous_duality':
shows "continuous_map weak_star_topology euclidean (λx. trace (from_trace_class t o⇩C⇩L x))"
proof -
have "continuous_map weak_star_topology euclidean ((λf. f t) o (λx t. trace (from_trace_class t o⇩C⇩L x)))"
unfolding weak_star_topology_def' apply (rule continuous_map_pullback)
using continuous_on_product_coordinates by fastforce
then show ?thesis unfolding comp_def by simp
qed
lemma weak_star_topology_continuous_duality:
assumes ‹trace_class t›
shows "continuous_map weak_star_topology euclidean (λx. trace (t o⇩C⇩L x))"
by (metis assms from_trace_class_cases mem_Collect_eq weak_star_topology_continuous_duality')
lemma continuous_on_weak_star_topo_iff_coordinatewise:
fixes f :: ‹'a ⇒ 'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space›
shows "continuous_map T weak_star_topology f
⟷ (∀t. trace_class t ⟶ continuous_map T euclidean (λx. trace (t o⇩C⇩L f x)))"
proof (intro iffI allI impI)
fix t :: ‹'c ⇒⇩C⇩L 'b›
assume ‹trace_class t›
assume "continuous_map T weak_star_topology f"
with continuous_map_compose[OF this weak_star_topology_continuous_duality, OF ‹trace_class t›]
have "continuous_map T euclidean ((λx. trace (t o⇩C⇩L x)) o f)"
by simp
then show "continuous_map T euclidean (λx. trace (t o⇩C⇩L f x))"
unfolding comp_def by auto
next
assume ‹∀t. trace_class t ⟶ continuous_map T euclidean (λx. trace (t o⇩C⇩L f x))›
then have ‹continuous_map T euclidean (λx. trace (from_trace_class t o⇩C⇩L f x))› for t
by auto
then have *: "continuous_map T euclidean ((λx t. trace (from_trace_class t o⇩C⇩L x)) o f)"
by (auto simp flip: euclidean_product_topology simp: o_def)
show "continuous_map T weak_star_topology f"
unfolding weak_star_topology_def'
apply (rule continuous_map_pullback')
by (auto simp add: *)
qed
lemma weak_star_topology_weaker_than_euclidean:
"continuous_map euclidean weak_star_topology (λf. f)"
apply (subst continuous_on_weak_star_topo_iff_coordinatewise)
by (auto intro!: linear_continuous_on bounded_clinear.bounded_linear bounded_clinear_trace_duality)
typedef (overloaded) ('a,'b) cblinfun_weak_star = ‹UNIV :: ('a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector) set›
morphisms from_weak_star to_weak_star ..
setup_lifting type_definition_cblinfun_weak_star
lift_definition id_weak_star :: ‹('a::complex_normed_vector, 'a) cblinfun_weak_star› is id_cblinfun .
instantiation cblinfun_weak_star :: (complex_normed_vector, complex_normed_vector) complex_vector begin
lift_definition scaleC_cblinfun_weak_star :: ‹complex ⇒ ('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star›
is ‹scaleC› .
lift_definition uminus_cblinfun_weak_star :: ‹('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star› is uminus .
lift_definition zero_cblinfun_weak_star :: ‹('a, 'b) cblinfun_weak_star› is 0 .
lift_definition minus_cblinfun_weak_star :: ‹('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star› is minus .
lift_definition plus_cblinfun_weak_star :: ‹('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star› is plus .
lift_definition scaleR_cblinfun_weak_star :: ‹real ⇒ ('a, 'b) cblinfun_weak_star ⇒ ('a, 'b) cblinfun_weak_star› is scaleR .
instance
by (intro_classes; transfer) (auto simp add: scaleR_scaleC scaleC_add_right scaleC_add_left)
end
instantiation cblinfun_weak_star :: (chilbert_space, chilbert_space) topological_space begin
lift_definition open_cblinfun_weak_star :: ‹('a, 'b) cblinfun_weak_star set ⇒ bool› is ‹openin weak_star_topology› .
instance
proof intro_classes
show ‹open (UNIV :: ('a,'b) cblinfun_weak_star set)›
by transfer (metis weak_star_topology_topspace openin_topspace)
show ‹open S ⟹ open T ⟹ open (S ∩ T)› for S T :: ‹('a,'b) cblinfun_weak_star set›
by transfer auto
show ‹∀S∈K. open S ⟹ open (⋃ K)› for K :: ‹('a,'b) cblinfun_weak_star set set›
by transfer auto
qed
end
lemma transfer_nhds_weak_star_topology[transfer_rule]:
includes lifting_syntax
shows ‹(cr_cblinfun_weak_star ===> rel_filter cr_cblinfun_weak_star) (nhdsin weak_star_topology) nhds›
proof -
have "(cr_cblinfun_weak_star ===> rel_filter cr_cblinfun_weak_star)
(λa. ⨅ (principal ` {S. openin weak_star_topology S ∧ a ∈ S}))
(λa. ⨅ (principal ` {S. open S ∧ a ∈ S}))"
by transfer_prover
thus ?thesis
unfolding nhds_def nhdsin_def weak_star_topology_topspace by simp
qed
lemma limitin_weak_star_topology':
‹limitin weak_star_topology f l F ⟷ (∀t. ((λj. trace (from_trace_class t o⇩C⇩L f j)) ⤏ trace (from_trace_class t o⇩C⇩L l)) F)›
by (simp add: weak_star_topology_def' limitin_pullback_topology tendsto_coordinatewise)
lemma limitin_weak_star_topology:
‹limitin weak_star_topology f l F ⟷ (∀t. trace_class t ⟶ ((λj. trace (t o⇩C⇩L f j)) ⤏ trace (t o⇩C⇩L l)) F)›
by (smt (z3) eventually_mono from_trace_class from_trace_class_cases limitin_weak_star_topology' mem_Collect_eq tendsto_def)
lemma filterlim_weak_star_topology:
‹filterlim f (nhdsin weak_star_topology l) = limitin weak_star_topology f l›
by (auto simp: weak_star_topology_topspace simp flip: filterlim_nhdsin_iff_limitin)
lemma openin_weak_star_topology': ‹openin weak_star_topology U ⟷ (∃V. open V ∧ U = (λx t. trace (from_trace_class t o⇩C⇩L x)) -` V)›
by (simp add: weak_star_topology_def' openin_pullback_topology)
lemma hausdorff_weak_star[simp]: ‹Hausdorff_space weak_star_topology›
by (metis cweak_operator_topology_topspace hausdorff_cweak_operator_topology
Hausdorff_space_def weak_star_topology_topspace wot_weaker_than_weak_star')
lemma Domainp_cr_cblinfun_weak_star[simp]: ‹Domainp cr_cblinfun_weak_star = (λ_. True)›
by (metis (no_types, opaque_lifting) DomainPI cblinfun_weak_star.left_total left_totalE)
lemma Rangep_cr_cblinfun_weak_star[simp]: ‹Rangep cr_cblinfun_weak_star = (λ_. True)›
by (meson RangePI cr_cblinfun_weak_star_def)
lemma transfer_euclidean_weak_star_topology[transfer_rule]:
includes lifting_syntax
shows ‹(rel_topology cr_cblinfun_weak_star) weak_star_topology euclidean›
proof (unfold rel_topology_def, intro conjI allI impI)
show ‹(rel_set cr_cblinfun_weak_star ===> (=)) (openin weak_star_topology) (openin euclidean)›
unfolding rel_fun_def rel_set_def open_openin [symmetric] cr_cblinfun_weak_star_def
by (transfer, intro allI impI arg_cong[of _ _ "openin x" for x]) blast
next
fix U :: ‹('a ⇒⇩C⇩L 'b) set›
assume ‹openin weak_star_topology U›
show ‹Domainp (rel_set cr_cblinfun_weak_star) U›
by (simp add: Domainp_set)
next
fix U :: ‹('a, 'b) cblinfun_weak_star set›
assume ‹openin euclidean U›
show ‹Rangep (rel_set cr_cblinfun_weak_star) U›
by (simp add: Rangep_set)
qed
instance cblinfun_weak_star :: (chilbert_space, chilbert_space) t2_space
apply (rule hausdorff_OFCLASS_t2_space)
apply transfer
by (rule hausdorff_weak_star)
lemma weak_star_topology_plus_cont: ‹LIM (x,y) nhdsin weak_star_topology a ×⇩F nhdsin weak_star_topology b.
x + y :> nhdsin weak_star_topology (a + b)›
proof -
have trace_plus: ‹trace (t o⇩C⇩L (a + b)) = trace (t o⇩C⇩L a) + trace (t o⇩C⇩L b)› if ‹trace_class t› for t :: ‹'b ⇒⇩C⇩L 'a› and a b
by (auto simp: cblinfun_compose_add_right trace_plus that trace_class_comp_left)
show ?thesis
unfolding weak_star_topology_def'
by (rule pullback_topology_bi_cont[where f'=plus])
(auto simp: trace_plus case_prod_unfold tendsto_add_Pair)
qed
instance cblinfun_weak_star :: (chilbert_space, chilbert_space) topological_group_add
proof intro_classes
show ‹((λx. fst x + snd x) ⤏ a + b) (nhds a ×⇩F nhds b)› for a b :: ‹('a,'b) cblinfun_weak_star›
apply transfer
using weak_star_topology_plus_cont
by (auto simp: case_prod_unfold)
have ‹continuous_map weak_star_topology euclidean (λx. trace (t o⇩C⇩L - x))› if ‹trace_class t› for t :: ‹'b ⇒⇩C⇩L 'a›
using weak_star_topology_continuous_duality[of ‹-t›]
by (auto simp: cblinfun_compose_uminus_left cblinfun_compose_uminus_right intro!: that trace_class_uminus)
then have *: ‹continuous_map weak_star_topology weak_star_topology (uminus :: ('a ⇒⇩C⇩L 'b) ⇒ _)›
by (auto simp: continuous_on_weak_star_topo_iff_coordinatewise)
show ‹(uminus ⤏ - a) (nhds a)› for a :: ‹('a,'b) cblinfun_weak_star›
apply (subst tendsto_at_iff_tendsto_nhds[symmetric])
apply (subst isCont_def[symmetric])
apply (rule continuous_on_interior[where S=UNIV])
apply (subst continuous_map_iff_continuous2[symmetric])
apply transfer
using * by auto
qed
lemma continuous_map_left_comp_weak_star:
‹continuous_map weak_star_topology weak_star_topology (λa::'a::chilbert_space ⇒⇩C⇩L _. b o⇩C⇩L a)›
for b :: ‹'b::chilbert_space ⇒⇩C⇩L 'c::chilbert_space›
proof (unfold weak_star_topology_def, rule continuous_map_pullback_both)
define g' :: ‹('b ⇒⇩C⇩L 'a ⇒ complex) ⇒ ('c ⇒⇩C⇩L 'a ⇒ complex)› where
‹g' f = (λt∈Collect trace_class. f (t o⇩C⇩L b))› for f
show ‹(λx. λt∈Collect trace_class. trace (t o⇩C⇩L x)) -` topspace (product_topology (λ_. euclidean) (Collect trace_class)) ∩ UNIV
⊆ (o⇩C⇩L) b -` UNIV›
by simp
show ‹g' (λt∈Collect trace_class. trace (t o⇩C⇩L x)) = (λt∈Collect trace_class. trace (t o⇩C⇩L (b o⇩C⇩L x)))› for x
by (auto intro!: ext simp: g'_def[abs_def] cblinfun_compose_assoc trace_class_comp_left)
show ‹continuous_map (product_topology (λ_. euclidean) (Collect trace_class))
(product_topology (λ_. euclidean) (Collect trace_class)) g'›
apply (rule continuous_map_coordinatewise_then_product)
subgoal for i
unfolding g'_def
apply (subst restrict_apply')
subgoal by simp
subgoal by (metis continuous_map_product_projection mem_Collect_eq trace_class_comp_left)
done
subgoal by (auto simp: g'_def[abs_def])
done
qed
lemma continuous_map_right_comp_weak_star:
‹continuous_map weak_star_topology weak_star_topology (λb::'b::chilbert_space ⇒⇩C⇩L _. b o⇩C⇩L a)›
for a :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
proof (subst weak_star_topology_def, subst weak_star_topology_def, rule continuous_map_pullback_both)
define g' :: ‹('c ⇒⇩C⇩L 'b ⇒ complex) ⇒ ('c ⇒⇩C⇩L 'a ⇒ complex)› where
‹g' f = (λt∈Collect trace_class. f (a o⇩C⇩L t))› for f
show ‹(λx. λt∈Collect trace_class. trace (t o⇩C⇩L x)) -` topspace (product_topology (λ_. euclidean) (Collect trace_class)) ∩ UNIV
⊆ (λb. b o⇩C⇩L a) -` UNIV›
by simp
have *: "trace (a o⇩C⇩L y o⇩C⇩L x) = trace (y o⇩C⇩L (x o⇩C⇩L a))" if "trace_class y" for x :: "'b ⇒⇩C⇩L 'c" and y :: "'c ⇒⇩C⇩L 'a"
by (simp add: circularity_of_trace simp_a_oCL_b that trace_class_comp_left)
show ‹g' (λt∈Collect trace_class. trace (t o⇩C⇩L x)) = (λt∈Collect trace_class. trace (t o⇩C⇩L (x o⇩C⇩L a)))› for x
by (auto intro!: ext simp: g'_def[abs_def] trace_class_comp_right *)
show ‹continuous_map (product_topology (λ_. euclidean) (Collect trace_class))
(product_topology (λ_. euclidean) (Collect trace_class)) g'›
apply (rule continuous_map_coordinatewise_then_product)
subgoal for i
unfolding g'_def mem_Collect_eq
apply (subst restrict_apply')
subgoal by simp
subgoal
by (metis continuous_map_product_projection mem_Collect_eq trace_class_comp_right)
done
subgoal by (auto simp: g'_def[abs_def])
done
qed
lemma continuous_map_scaleC_weak_star: ‹continuous_map weak_star_topology weak_star_topology (scaleC c)›
apply (subst asm_rl[of ‹scaleC c = (o⇩C⇩L) (c *⇩C id_cblinfun)›])
subgoal by auto
subgoal by (rule continuous_map_left_comp_weak_star)
done
lemma continuous_scaleC_weak_star: ‹continuous_on X (scaleC c :: (_,_) cblinfun_weak_star ⇒ _)›
apply (rule continuous_on_subset[rotated, where s=UNIV])
subgoal by simp
subgoal
apply (subst continuous_map_iff_continuous2[symmetric])
apply transfer
by (rule continuous_map_scaleC_weak_star)
done
lemma weak_star_closure_is_csubspace[simp]:
fixes A::"('a::chilbert_space, 'b::chilbert_space) cblinfun_weak_star set"
assumes ‹csubspace A›
shows ‹csubspace (closure A)›
proof (rule complex_vector.subspaceI)
include lattice_syntax
show 0: ‹0 ∈ closure A›
by (simp add: assms closure_def complex_vector.subspace_0)
show ‹x + y ∈ closure A› if ‹x ∈ closure A› ‹y ∈ closure A› for x y
proof -
define FF where ‹FF = ((nhds x ⊓ principal A) ×⇩F (nhds y ⊓ principal A))›
have nt: ‹FF ≠ bot›
by (simp add: prod_filter_eq_bot that(1) that(2) FF_def flip: closure_nhds_principal)
have ‹∀⇩F x in FF. fst x ∈ A›
unfolding FF_def
by (smt (verit, ccfv_SIG) eventually_prod_filter fst_conv inf_sup_ord(2) le_principal)
moreover have ‹∀⇩F x in FF. snd x ∈ A›
unfolding FF_def
by (smt (verit, ccfv_SIG) eventually_prod_filter snd_conv inf_sup_ord(2) le_principal)
ultimately have FF_plus: ‹∀⇩F x in FF. fst x + snd x ∈ A›
by (smt (verit, best) assms complex_vector.subspace_add eventually_elim2)
have ‹(fst ⤏ x) ((nhds x ⊓ principal A) ×⇩F (nhds y ⊓ principal A))›
apply (simp add: filterlim_def)
using filtermap_fst_prod_filter
using le_inf_iff by blast
moreover have ‹(snd ⤏ y) ((nhds x ⊓ principal A) ×⇩F (nhds y ⊓ principal A))›
apply (simp add: filterlim_def)
using filtermap_snd_prod_filter
using le_inf_iff by blast
ultimately have ‹(id ⤏ (x,y)) FF›
by (simp add: filterlim_def nhds_prod prod_filter_mono FF_def)
moreover note tendsto_add_Pair[of x y]
ultimately have ‹(((λx. fst x + snd x) o id) ⤏ (λx. fst x + snd x) (x,y)) FF›
unfolding filterlim_def nhds_prod
by (smt (verit, best) filterlim_compose filterlim_def filterlim_filtermap fst_conv snd_conv tendsto_compose_filtermap)
then have ‹((λx. fst x + snd x) ⤏ (x+y)) FF›
by simp
then show ‹x + y ∈ closure A›
using nt FF_plus by (rule limit_in_closure)
qed
show ‹c *⇩C x ∈ closure A› if ‹x ∈ closure A› for x c
proof (cases "c = 0")
case False
have "(*⇩C) c ` closure A ⊆ closure A"
using csubspace_scaleC_invariant[of c A] ‹csubspace A› False closure_subset[of A]
by (intro image_closure_subset continuous_scaleC_weak_star closed_closure) auto
thus ?thesis
using that by blast
qed (use 0 in auto)
qed
lemma transfer_csubspace_cblinfun_weak_star[transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_weak_star ===> (=)) csubspace csubspace›
unfolding complex_vector.subspace_def
by transfer_prover
lemma transfer_closed_cblinfun_weak_star[transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_weak_star ===> (=)) (closedin weak_star_topology) closed›
proof -
have "(rel_set cr_cblinfun_weak_star ===> (=))
(λS. openin weak_star_topology (UNIV - S))
(λS. open (UNIV - S)) "
by transfer_prover
thus ?thesis
by (simp add: closed_def[abs_def] closedin_def[abs_def] Compl_eq_Diff_UNIV)
qed
lemma transfer_closure_cblinfun_weak_star[transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_weak_star ===> rel_set cr_cblinfun_weak_star) (Abstract_Topology.closure_of weak_star_topology) closure›
apply (subst closure_of_hull[where X=weak_star_topology, unfolded weak_star_topology_topspace, simplified, abs_def])
apply (subst closure_hull[abs_def])
unfolding hull_def
by transfer_prover
lemma weak_star_closure_is_csubspace'[simp]:
fixes A::"('a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space) set"
assumes ‹csubspace A›
shows ‹csubspace (weak_star_topology closure_of A)›
using weak_star_closure_is_csubspace[of ‹to_weak_star ` A›] assms
apply (transfer fixing: A)
by simp
lemma has_sum_closed_weak_star_topology:
assumes aA: ‹⋀i. a i ∈ A›
assumes closed: ‹closedin weak_star_topology A›
assumes subspace: ‹csubspace A›
assumes has_sum: ‹⋀t. trace_class t ⟹ ((λi. trace (t o⇩C⇩L a i)) has_sum trace (t o⇩C⇩L b)) I›
shows ‹b ∈ A›
proof -
have 1: ‹range (sum a) ⊆ A›
proof -
have ‹sum a X ∈ A› for X
apply (induction X rule:infinite_finite_induct)
by (auto simp add: subspace complex_vector.subspace_0 aA complex_vector.subspace_add)
then show ?thesis
by auto
qed
from has_sum
have ‹((λF. ∑i∈F. trace (t o⇩C⇩L a i)) ⤏ trace (t o⇩C⇩L b)) (finite_subsets_at_top I)› if ‹trace_class t› for t
by (auto intro: that simp: has_sum_def)
then have ‹limitin weak_star_topology (λF. ∑i∈F. a i) b (finite_subsets_at_top I)›
by (auto simp add: limitin_weak_star_topology cblinfun_compose_sum_right trace_sum trace_class_comp_left)
then show ‹b ∈ A›
using 1 closed apply (rule limitin_closedin)
by simp
qed
lemma has_sum_in_weak_star:
‹has_sum_in weak_star_topology f A l ⟷
(∀t. trace_class t ⟶ ((λi. trace (t o⇩C⇩L f i)) has_sum trace (t o⇩C⇩L l)) A)›
proof -
have *: ‹trace (t o⇩C⇩L sum f F) = sum (λi. trace (t o⇩C⇩L f i)) F› if ‹trace_class t›
for t F
by (simp_all add: cblinfun_compose_sum_right that trace_class_comp_left trace_sum)
show ?thesis
by (simp add: * has_sum_def has_sum_in_def limitin_weak_star_topology)
qed
lemma has_sum_butterfly_ket: ‹has_sum_in weak_star_topology (λi. butterfly (ket i) (ket i)) UNIV id_cblinfun›
proof (rule has_sum_in_weak_star[THEN iffD2, rule_format])
fix t :: ‹'a ell2 ⇒⇩C⇩L 'a ell2›
assume [simp]: ‹trace_class t›
from trace_has_sum[OF is_onb_ket ‹trace_class t›]
have ‹((λi. ket i ∙⇩C (t *⇩V ket i)) has_sum trace t) UNIV›
apply (subst (asm) has_sum_reindex)
by (auto simp: o_def)
then show ‹((λi. trace (t o⇩C⇩L butterfly (ket i) (ket i))) has_sum trace (t o⇩C⇩L id_cblinfun)) UNIV›
by (simp add: trace_butterfly_comp')
qed
lemma sandwich_weak_star_cont[simp]:
‹continuous_map weak_star_topology weak_star_topology (sandwich A)›
using continuous_map_compose[OF continuous_map_left_comp_weak_star continuous_map_right_comp_weak_star]
by (auto simp: o_def sandwich_apply[abs_def])
lemma has_sum_butterfly_ket_a: ‹has_sum_in weak_star_topology (λi. butterfly (a *⇩V ket i) (ket i)) UNIV a›
proof -
have ‹has_sum_in weak_star_topology ((λb. a o⇩C⇩L b) ∘ (λi. butterfly (ket i) (ket i))) UNIV (a o⇩C⇩L id_cblinfun)›
apply (rule has_sum_in_comm_additive)
by (auto intro!: has_sum_butterfly_ket continuous_map_is_continuous_at_point limitin_continuous_map
continuous_map_left_comp_weak_star cblinfun_compose_add_right
simp: Modules.additive_def)
then show ?thesis
by (auto simp: o_def cblinfun_comp_butterfly)
qed
lemma finite_rank_weak_star_dense[simp]: ‹weak_star_topology closure_of (Collect finite_rank) = (UNIV :: ('a ell2 ⇒⇩C⇩L 'b::chilbert_space) set)›
proof -
have ‹x ∈ weak_star_topology closure_of (Collect finite_rank)› for x :: ‹'a ell2 ⇒⇩C⇩L 'b›
proof (rule limitin_closure_of)
define f :: ‹'a ⇒ 'a ell2 ⇒⇩C⇩L 'b› where ‹f = (λi. butterfly (x *⇩V ket i) (ket i))›
have ‹has_sum_in weak_star_topology f UNIV x›
using f_def has_sum_butterfly_ket_a by blast
then show ‹limitin weak_star_topology (sum f) x (finite_subsets_at_top UNIV)›
using has_sum_in_def by blast
show ‹∀⇩F F in finite_subsets_at_top UNIV.
(∑i∈F. butterfly (x *⇩V ket i) (ket i)) ∈ Collect finite_rank›
by (auto intro!: finite_rank_sum simp: f_def)
show ‹finite_subsets_at_top UNIV ≠ ⊥›
by simp
qed
then show ?thesis
by auto
qed
lemma butterkets_weak_star_dense[simp]:
‹weak_star_topology closure_of cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV) = UNIV›
proof -
from continuous_map_image_closure_subset[OF weak_star_topology_weaker_than_euclidean]
have ‹weak_star_topology closure_of (cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV))
⊇ closure (cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV))› (is ‹_ ⊇ …›)
by auto
moreover
have ‹… = Collect compact_op›
unfolding finite_rank_dense_compact[OF is_onb_ket is_onb_ket, symmetric]
by (simp add: image_image case_prod_beta flip: map_prod_image)
moreover have ‹… ⊇ Collect finite_rank›
by (metis closure_subset compact_op_finite_rank mem_Collect_eq subsetI subset_antisym)
ultimately have *: ‹weak_star_topology closure_of (cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV)) ⊇ Collect finite_rank›
by blast
have ‹weak_star_topology closure_of cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV)
= weak_star_topology closure_of (weak_star_topology closure_of cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV))›
by simp
also have ‹… ⊇ weak_star_topology closure_of Collect finite_rank› (is ‹_ ⊇ …›)
using * closure_of_mono by blast
also have ‹… = UNIV›
by simp
finally show ?thesis
by auto
qed
lemma weak_star_clinear_eq_butterfly_ketI:
fixes F G :: ‹('a ell2 ⇒⇩C⇩L 'b ell2) ⇒ 'c::complex_vector›
assumes "clinear F" and "clinear G"
and ‹continuous_map weak_star_topology T F› and ‹continuous_map weak_star_topology T G›
and ‹Hausdorff_space T›
assumes "⋀i j. F (butterfly (ket i) (ket j)) = G (butterfly (ket i) (ket j))"
shows "F = G"
proof -
have FG: ‹F x = G x› if ‹x ∈ cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV)› for x
by (smt (verit) assms(1) assms(2) assms(6) complex_vector.linear_eq_on imageE split_def that)
show ?thesis
apply (rule ext)
using ‹Hausdorff_space T› FG
apply (rule closure_of_eqI[where f=F and g=G and S=‹cspan ((λ(ξ,η). butterfly (ket ξ) (ket η)) ` UNIV)›])
using assms butterkets_weak_star_dense by auto
qed
lemma continuous_map_scaleC_weak_star'[continuous_intros]:
assumes ‹continuous_map T weak_star_topology f›
shows ‹continuous_map T weak_star_topology (λx. scaleC c (f x))›
using continuous_map_compose[OF assms continuous_map_scaleC_weak_star]
by (simp add: o_def)
lemma continuous_map_uminus_weak_star[continuous_intros]:
assumes ‹continuous_map T weak_star_topology f›
shows ‹continuous_map T weak_star_topology (λx. - f x)›
apply (subst scaleC_minus1_left[abs_def,symmetric])
by (intro continuous_map_scaleC_weak_star' assms)
lemma continuous_map_add_weak_star[continuous_intros]:
assumes ‹continuous_map T weak_star_topology f›
assumes ‹continuous_map T weak_star_topology g›
shows ‹continuous_map T weak_star_topology (λx. f x + g x)›
proof -
have ‹continuous_map T euclidean (λx. trace (t o⇩C⇩L f x))› if ‹trace_class t› for t
using assms(1) continuous_on_weak_star_topo_iff_coordinatewise that by auto
moreover have ‹continuous_map T euclidean (λx. trace (t o⇩C⇩L g x))› if ‹trace_class t› for t
using assms(2) continuous_on_weak_star_topo_iff_coordinatewise that by auto
ultimately show ?thesis
by (auto intro!: continuous_map_add simp add: continuous_on_weak_star_topo_iff_coordinatewise
cblinfun_compose_add_right trace_class_comp_left trace_plus)
qed
lemma continuous_map_minus_weak_star[continuous_intros]:
assumes ‹continuous_map T weak_star_topology f›
assumes ‹continuous_map T weak_star_topology g›
shows ‹continuous_map T weak_star_topology (λx. f x - g x)›
by (subst diff_conv_add_uminus) (intro assms continuous_intros)
lemma weak_star_topology_is_norm_topology_fin_dim[simp]:
‹(weak_star_topology :: ('a::{cfinite_dim,chilbert_space} ⇒⇩C⇩L 'b::{cfinite_dim,chilbert_space}) topology) = euclidean›
proof -
have 1: ‹continuous_map euclidean weak_star_topology (id :: 'a⇒⇩C⇩L'b ⇒ _)›
by (simp add: id_def weak_star_topology_weaker_than_euclidean)
have ‹continuous_map weak_star_topology cweak_operator_topology (id :: 'a⇒⇩C⇩L'b ⇒ _)›
by (simp only: id_def wot_weaker_than_weak_star)
then have 2: ‹continuous_map weak_star_topology euclidean (id :: 'a⇒⇩C⇩L'b ⇒ _)›
by (simp only: wot_is_norm_topology_findim)
from 1 2
show ?thesis
by (auto simp: topology_finer_continuous_id[symmetric] simp flip: openin_inject)
qed
lemma infsum_mono_wot:
fixes f :: "'a ⇒ ('b::chilbert_space ⇒⇩C⇩L 'b)"
assumes "summable_on_in cweak_operator_topology f A" and "summable_on_in cweak_operator_topology g A"
assumes ‹⋀x. x ∈ A ⟹ f x ≤ g x›
shows "infsum_in cweak_operator_topology f A ≤ infsum_in cweak_operator_topology g A"
by (meson assms has_sum_in_infsum_in has_sum_mono_wot hausdorff_cweak_operator_topology)
unbundle no cblinfun_syntax
end