Theory Strong_Operator_Topology
section ‹‹Strong_Operator_Topology› -- Strong operator topology on complex bounded operators›
theory Strong_Operator_Topology
imports
Complex_Bounded_Operators.Complex_Bounded_Linear_Function
Misc_Tensor_Product
begin
unbundle cblinfun_syntax
typedef (overloaded) ('a,'b) cblinfun_sot = ‹UNIV :: ('a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector) set› ..
setup_lifting type_definition_cblinfun_sot
instantiation cblinfun_sot :: (complex_normed_vector, complex_normed_vector) complex_vector begin
lift_definition scaleC_cblinfun_sot :: ‹complex ⇒ ('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot›
is ‹scaleC› .
lift_definition uminus_cblinfun_sot :: ‹('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot› is uminus .
lift_definition zero_cblinfun_sot :: ‹('a, 'b) cblinfun_sot› is 0 .
lift_definition minus_cblinfun_sot :: ‹('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot› is minus .
lift_definition plus_cblinfun_sot :: ‹('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot› is plus .
lift_definition scaleR_cblinfun_sot :: ‹real ⇒ ('a, 'b) cblinfun_sot ⇒ ('a, 'b) cblinfun_sot› is scaleR .
instance
apply (intro_classes; transfer)
by (auto simp add: scaleR_scaleC scaleC_add_right scaleC_add_left)
end
instantiation cblinfun_sot :: (complex_normed_vector, complex_normed_vector) topological_space begin
lift_definition open_cblinfun_sot :: ‹('a, 'b) cblinfun_sot set ⇒ bool› is ‹openin cstrong_operator_topology› .
instance
proof intro_classes
show ‹open (UNIV :: ('a,'b) cblinfun_sot set)›
apply transfer
by (metis cstrong_operator_topology_topspace openin_topspace)
show ‹open S ⟹ open T ⟹ open (S ∩ T)› for S T :: ‹('a,'b) cblinfun_sot set›
apply transfer by auto
show ‹∀S∈K. open S ⟹ open (⋃ K)› for K :: ‹('a,'b) cblinfun_sot set set›
apply transfer by auto
qed
end
lemma transfer_nhds_cstrong_operator_topology[transfer_rule]:
includes lifting_syntax
shows ‹(cr_cblinfun_sot ===> rel_filter cr_cblinfun_sot) (nhdsin cstrong_operator_topology) nhds›
unfolding nhds_def nhdsin_def
apply (simp add: cstrong_operator_topology_topspace)
by transfer_prover
lemma filterlim_cstrong_operator_topology: ‹filterlim f (nhdsin cstrong_operator_topology l) = limitin cstrong_operator_topology f l›
by (auto simp: cstrong_operator_topology_topspace simp flip: filterlim_nhdsin_iff_limitin)
lemma hausdorff_sot[simp]: ‹Hausdorff_space cstrong_operator_topology›
proof (rule hausdorffI)
fix a b :: ‹'a ⇒⇩C⇩L 'b›
assume ‹a ≠ b›
then obtain ψ where ‹a *⇩V ψ ≠ b *⇩V ψ›
by (meson cblinfun_eqI)
then obtain U' V' where ‹open U'› ‹open V'› ‹a *⇩V ψ ∈ U'› ‹b *⇩V ψ ∈ V'› ‹U' ∩ V' = {}›
by (meson hausdorff)
define U V where ‹U = {f. ∀i∈{()}. f *⇩V ψ ∈ U'}› and ‹V = {f. ∀i∈{()}. f *⇩V ψ ∈ V'}›
have 1: ‹openin cstrong_operator_topology U›
unfolding U_def apply (rule cstrong_operator_topology_basis)
using ‹open U'› by auto
have 2: ‹openin cstrong_operator_topology V›
unfolding V_def apply (rule cstrong_operator_topology_basis)
using ‹open V'› by auto
show ‹∃U V. openin cstrong_operator_topology U ∧ openin cstrong_operator_topology V ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = {}›
by (rule exI[of _ U], rule exI[of _ V])
(use 1 2 ‹a *⇩V ψ ∈ U'› ‹b *⇩V ψ ∈ V'› ‹U' ∩ V' = {}› in ‹auto simp: U_def V_def›)
qed
instance cblinfun_sot :: (complex_normed_vector, complex_normed_vector) t2_space
proof intro_classes
fix a b :: ‹('a,'b) cblinfun_sot›
show ‹a ≠ b ⟹ ∃U V. open U ∧ open V ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = {}›
apply transfer using hausdorff_sot
by (metis UNIV_I cstrong_operator_topology_topspace Hausdorff_space_def disjnt_def)
qed
lemma Domainp_cr_cblinfun_sot[simp]: ‹Domainp cr_cblinfun_sot = (λ_. True)›
by (metis (no_types, opaque_lifting) DomainPI cblinfun_sot.left_total left_totalE)
lemma Rangep_cr_cblinfun_sot[simp]: ‹Rangep cr_cblinfun_sot = (λ_. True)›
by (meson RangePI cr_cblinfun_sot_def)
lemma Rangep_set[relator_domain]: "Rangep (rel_set T) = (λA. Ball A (Rangep T))"
by (metis (no_types, opaque_lifting) Domainp_conversep Domainp_set rel_set_conversep)
lemma transfer_euclidean_cstrong_operator_topology[transfer_rule]:
includes lifting_syntax
shows ‹(rel_topology cr_cblinfun_sot) cstrong_operator_topology euclidean›
proof (unfold rel_topology_def, intro conjI allI impI)
show ‹(rel_set cr_cblinfun_sot ===> (=)) (openin cstrong_operator_topology) (openin euclidean)›
unfolding rel_fun_def rel_set_def open_openin [symmetric] cr_cblinfun_sot_def
by (transfer, intro allI impI arg_cong[of _ _ "openin x" for x]) blast
next
fix U :: ‹('a ⇒⇩C⇩L 'b) set›
assume ‹openin cstrong_operator_topology U›
show ‹Domainp (rel_set cr_cblinfun_sot) U›
by (simp add: Domainp_set)
next
fix U :: ‹('a, 'b) cblinfun_sot set›
assume ‹openin euclidean U›
show ‹Rangep (rel_set cr_cblinfun_sot) U›
by (simp add: Rangep_set)
qed
lemma openin_cstrong_operator_topology: ‹openin cstrong_operator_topology U ⟷ (∃V. open V ∧ U = (*⇩V) -` V)›
by (simp add: cstrong_operator_topology_def openin_pullback_topology)
lemma cstrong_operator_topology_plus_cont: ‹LIM (x,y) nhdsin cstrong_operator_topology a ×⇩F nhdsin cstrong_operator_topology b.
x + y :> nhdsin cstrong_operator_topology (a + b)›
unfolding cstrong_operator_topology_def
by (rule pullback_topology_bi_cont[where f'=plus])
(auto simp: case_prod_unfold tendsto_add_Pair cblinfun.add_left)
instance cblinfun_sot :: (complex_normed_vector, complex_normed_vector) 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_sot›
apply transfer
using cstrong_operator_topology_plus_cont
by (auto simp: case_prod_unfold)
have *: ‹continuous_map cstrong_operator_topology cstrong_operator_topology uminus›
apply (subst continuous_on_cstrong_operator_topo_iff_coordinatewise)
apply (rewrite at ‹(λy. - y *⇩V x)› in ‹∀x. ⌑› to ‹(λy. y *⇩V - x)› DEADID.rel_mono_strong)
by (auto simp: cstrong_operator_topology_continuous_evaluation cblinfun.minus_left cblinfun.minus_right)
show ‹(uminus ⤏ - a) (nhds a)› for a :: ‹('a,'b) cblinfun_sot›
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_sot[continuous_intros]:
fixes b :: ‹'b::complex_normed_vector ⇒⇩C⇩L 'c::complex_normed_vector›
and f :: ‹'a ⇒ 'd::complex_normed_vector ⇒⇩C⇩L 'b›
assumes ‹continuous_map T cstrong_operator_topology f›
shows ‹continuous_map T cstrong_operator_topology (λx. b o⇩C⇩L f x)›
proof -
have *: ‹open B ⟹ open ((*⇩V) b -` B)› for B
by (simp add: continuous_open_vimage)
have **: ‹((λa. b *⇩V a ψ) -` B ∩ UNIV) = (Pi⇩E UNIV (λi. if i=ψ then (λa. b *⇩V a) -` B else UNIV))›
for ψ :: 'd and B
by (auto simp: PiE_def Pi_def)
have *: ‹continuous_on UNIV (λ(a::'d ⇒ 'b). b *⇩V (a ψ))› for ψ
unfolding continuous_on_open_vimage[OF open_UNIV]
apply (intro allI impI)
apply (subst **)
apply (rule open_PiE)
using * by auto
have *: ‹continuous_on UNIV (λ(a::'d ⇒ 'b) ψ. b *⇩V a ψ)›
apply (rule continuous_on_coordinatewise_then_product)
by (rule *)
have ‹continuous_map cstrong_operator_topology cstrong_operator_topology
(λx :: 'd ⇒⇩C⇩L 'b. b o⇩C⇩L x)›
unfolding cstrong_operator_topology_def
apply (rule continuous_map_pullback')
subgoal
apply (subst asm_rl[of ‹(*⇩V) ∘ (o⇩C⇩L) b = (λa x. b *⇩V (a x)) ∘ (*⇩V)›])
subgoal by force
subgoal by (rule continuous_map_pullback) (use * in auto)
done
subgoal using * by auto
done
from continuous_map_compose[OF assms this, unfolded o_def]
show ?thesis
by -
qed
lemma continuous_cstrong_operator_topology_plus[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
assumes ‹continuous_map T cstrong_operator_topology g›
shows ‹continuous_map T cstrong_operator_topology (λx. f x + g x)›
using assms
by (auto intro!: continuous_map_add
simp: continuous_on_cstrong_operator_topo_iff_coordinatewise cblinfun.add_left)
lemma continuous_cstrong_operator_topology_uminus[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
shows ‹continuous_map T cstrong_operator_topology (λx. - f x)›
using assms
by (auto simp add: continuous_on_cstrong_operator_topo_iff_coordinatewise cblinfun.minus_left)
lemma continuous_cstrong_operator_topology_minus[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
assumes ‹continuous_map T cstrong_operator_topology g›
shows ‹continuous_map T cstrong_operator_topology (λx. f x - g x)›
apply (subst diff_conv_add_uminus)
by (intro continuous_intros assms)
lemma continuous_map_right_comp_sot[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
shows ‹continuous_map T cstrong_operator_topology (λx. f x o⇩C⇩L a)›
apply (rule continuous_map_compose[OF assms, unfolded o_def])
by (simp add: continuous_on_cstrong_operator_topo_iff_coordinatewise cstrong_operator_topology_continuous_evaluation)
lemma continuous_map_scaleC_sot[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
shows ‹continuous_map T cstrong_operator_topology (λx. c *⇩C f x)›
apply (subst asm_rl[of ‹scaleC c = (o⇩C⇩L) (c *⇩C id_cblinfun)›])
apply auto[1]
using assms by (rule continuous_map_left_comp_sot)
lemma continuous_scaleC_sot[continuous_intros]:
fixes f :: ‹'a::topological_space ⇒ (_,_) cblinfun_sot›
assumes ‹continuous_on X f›
shows ‹continuous_on X (λx. c *⇩C f x)›
apply (rule continuous_on_compose[OF assms, unfolded o_def])
apply (rule continuous_on_subset[rotated, where s=UNIV], simp)
apply (subst continuous_map_iff_continuous2[symmetric])
apply transfer
apply (rule continuous_map_scaleC_sot)
by simp
lemma sot_closure_is_csubspace[simp]:
fixes A::"('a::complex_normed_vector, 'b::complex_normed_vector) cblinfun_sot 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 ` A ⊆ closure A"
using csubspace_scaleC_invariant[of c A] assms False closure_subset[of A] by auto
hence "(*⇩C) c ` closure A ⊆ closure A"
by (intro image_closure_subset) (auto intro!: continuous_intros)
thus ?thesis
using that by blast
qed (use 0 in auto)
qed
lemma limitin_cstrong_operator_topology:
‹limitin cstrong_operator_topology f l F ⟷ (∀i. ((λj. f j *⇩V i) ⤏ l *⇩V i) F)›
by (simp add: cstrong_operator_topology_def limitin_pullback_topology
tendsto_coordinatewise)
lemma cstrong_operator_topology_in_closureI:
assumes ‹⋀M ε. ε > 0 ⟹ finite M ⟹ ∃a∈A. ∀v∈M. norm ((b-a) *⇩V v) ≤ ε›
shows ‹b ∈ cstrong_operator_topology closure_of A›
proof -
define F :: ‹('a set × real) filter› where ‹F = finite_subsets_at_top UNIV ×⇩F at_right 0›
obtain f where fA: ‹f M ε ∈ A› and f: ‹v ∈ M ⟹ norm ((f M ε - b) *⇩V v) ≤ ε› if ‹finite M› and ‹ε > 0› for M ε v
apply atomize_elim
apply (intro allI choice2)
using assms
by (metis cblinfun.diff_left norm_minus_commute)
have F_props: ‹∀⇩F (M,ε) in F. finite M ∧ ε > 0›
by (auto intro!: eventually_prodI simp: F_def case_prod_unfold eventually_at_right_less)
then have inA: ‹∀⇩F (M,ε) in F. f M ε ∈ A›
apply (rule eventually_rev_mp)
using fA by (auto intro!: always_eventually)
have ‹limitin cstrong_operator_topology (case_prod f) b F›
proof -
have ‹∀⇩F (M,ε) in F. norm (f M ε *⇩V v - b *⇩V v) < e› if ‹e > 0› for e v
proof -
have 1: ‹∀⇩F (M,ε) in F. (finite M ∧ v ∈ M) ∧ (ε > 0 ∧ ε < e)›
apply (unfold F_def case_prod_unfold, rule eventually_prodI)
using eventually_at_right that
by (auto simp add: eventually_finite_subsets_at_top)
have 2: ‹norm (f M ε *⇩V v - b *⇩V v) < e› if ‹(finite M ∧ v ∈ M) ∧ (ε > 0 ∧ ε < e)› for M ε
by (smt (verit) cblinfun.diff_left f that)
show ?thesis
using 1 apply (rule eventually_mono)
using 2 by auto
qed
then have ‹((λ(M,ε). f M ε *⇩V v) ⤏ b *⇩V v) F› for v
by (simp add: tendsto_iff dist_norm case_prod_unfold)
then show ?thesis
by (simp add: case_prod_unfold limitin_cstrong_operator_topology)
qed
then show ?thesis
apply (rule limitin_closure_of)
using inA by (auto simp: F_def case_prod_unfold prod_filter_eq_bot)
qed
lemma sot_weaker_than_norm_limitin: ‹limitin cstrong_operator_topology a A F› if ‹(a ⤏ A) F›
proof -
from that have ‹((λx. a x *⇩V ψ) ⤏ A ψ) F› for ψ
by (auto intro!: cblinfun.tendsto)
then show ?thesis
by (simp add: limitin_cstrong_operator_topology)
qed
lemma [transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_sot ===> (=)) csubspace csubspace›
unfolding complex_vector.subspace_def
by transfer_prover
lemma [transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_sot ===> (=)) (closedin cstrong_operator_topology) closed›
apply (simp add: closed_def[abs_def] closedin_def[abs_def] cstrong_operator_topology_topspace Compl_eq_Diff_UNIV)
by transfer_prover
lemma [transfer_rule]:
includes lifting_syntax
shows ‹(rel_set cr_cblinfun_sot ===> rel_set cr_cblinfun_sot) (Abstract_Topology.closure_of cstrong_operator_topology) closure›
apply (subst closure_of_hull[where X=cstrong_operator_topology, unfolded cstrong_operator_topology_topspace, simplified, abs_def])
apply (subst closure_hull[abs_def])
unfolding hull_def
by transfer_prover
lemma sot_closure_is_csubspace'[simp]:
fixes A::"('a::complex_normed_vector ⇒⇩C⇩L 'b::complex_normed_vector) set"
assumes ‹csubspace A›
shows ‹csubspace (cstrong_operator_topology closure_of A)›
using sot_closure_is_csubspace[of ‹Abs_cblinfun_sot ` A›] assms
apply (transfer fixing: A)
by simp
lemma has_sum_closed_cstrong_operator_topology:
assumes aA: ‹⋀i. a i ∈ A›
assumes closed: ‹closedin cstrong_operator_topology A›
assumes subspace: ‹csubspace A›
assumes has_sum: ‹⋀ψ. ((λi. a i *⇩V ψ) has_sum (b *⇩V ψ)) 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. a i *⇩V ψ) ⤏ b *⇩V ψ) (finite_subsets_at_top I)› for ψ
using has_sum_def by blast
then have ‹limitin cstrong_operator_topology (λF. ∑i∈F. a i) b (finite_subsets_at_top I)›
by (auto simp add: limitin_cstrong_operator_topology cblinfun.sum_left)
then show ‹b ∈ A›
using 1 closed apply (rule limitin_closedin)
by simp
qed
lemma has_sum_in_cstrong_operator_topology:
‹has_sum_in cstrong_operator_topology f A l ⟷ (∀ψ. ((λi. f i *⇩V ψ) has_sum (l *⇩V ψ)) A)›
by (simp add: cblinfun.sum_left has_sum_in_def limitin_cstrong_operator_topology has_sum_def)
lemma summable_sot_absI:
fixes b :: ‹'a ⇒ 'b::complex_normed_vector ⇒⇩C⇩L 'c::chilbert_space›
assumes ‹⋀F f. finite F ⟹ (∑n∈F. norm (b n *⇩V f)) ≤ K * norm f›
shows ‹summable_on_in cstrong_operator_topology b UNIV›
proof -
obtain B' where B': ‹((λn. b n *⇩V f) has_sum (B' f)) UNIV› for f
proof (atomize_elim, intro choice allI)
fix f
have ‹(λn. b n *⇩V f) abs_summable_on UNIV›
apply (rule nonneg_bdd_above_summable_on)
using assms by (auto intro!: bdd_aboveI[where M=‹K * norm f›])
then show ‹∃l. ((λn. b n *⇩V f) has_sum l) UNIV›
by (metis abs_summable_summable summable_on_def)
qed
have ‹bounded_clinear B'›
proof (intro bounded_clinearI allI)
fix x y :: 'b and c :: complex
from B'[of x] B'[of y]
have ‹((λn. b n *⇩V x + b n *⇩V y) has_sum B' x + B' y) UNIV›
by (simp add: has_sum_add)
with B'[of ‹x + y›]
show ‹B' (x + y) = B' x + B' y›
by (metis (no_types, lifting) cblinfun.add_right has_sum_cong infsumI)
from B'[of x]
have ‹((λn. c *⇩C (b n *⇩V x)) has_sum c *⇩C B' x) UNIV›
by (metis cblinfun_scaleC_right.rep_eq has_sum_cblinfun_apply)
with B'[of ‹c *⇩C x›]
show ‹B' (c *⇩C x) = c *⇩C B' x›
by (metis (no_types, lifting) cblinfun.scaleC_right has_sum_cong infsumI)
show ‹norm (B' x) ≤ norm x * K›
proof -
have *: ‹(λn. b n *⇩V x) abs_summable_on UNIV›
apply (rule nonneg_bdd_above_summable_on)
using assms by (auto intro!: bdd_aboveI[where M=‹K * norm x›])
have ‹norm (B' x) ≤ (∑⇩∞n. norm (b n *⇩V x))›
using _ B'[of x] apply (rule norm_has_sum_bound)
using * summable_iff_has_sum_infsum by blast
also have ‹(∑⇩∞n. norm (b n *⇩V x)) ≤ K * norm x›
using * apply (rule infsum_le_finite_sums)
using assms by simp
finally show ?thesis
by (simp add: mult.commute)
qed
qed
define B where ‹B = CBlinfun B'›
with ‹bounded_clinear B'› have BB': ‹B *⇩V f = B' f› for f
by (simp add: bounded_clinear_CBlinfun_apply)
have ‹has_sum_in cstrong_operator_topology b UNIV B›
using B' by (simp add: has_sum_in_cstrong_operator_topology BB')
then show ?thesis
using summable_on_in_def by blast
qed
declare cstrong_operator_topology_topspace[simp]
lift_definition cblinfun_compose_sot :: ‹('a::complex_normed_vector,'b::complex_normed_vector) cblinfun_sot ⇒ ('c::complex_normed_vector,'a) cblinfun_sot ⇒ ('c,'b) cblinfun_sot›
is cblinfun_compose .
lemma isCont_cblinfun_compose_sot_right[simp]: ‹isCont (λF. cblinfun_compose_sot F G) x›
apply (rule continuous_on_interior[where S=UNIV, rotated], simp)
apply (rule continuous_map_iff_continuous2[THEN iffD1])
apply transfer
by (simp add: continuous_map_right_comp_sot)
lemma isCont_cblinfun_compose_sot_left[simp]: ‹isCont (λF. cblinfun_compose_sot G F) x›
apply (rule continuous_on_interior[where S=UNIV, rotated], simp)
apply (rule continuous_map_iff_continuous2[THEN iffD1])
apply transfer
by (simp add: continuous_map_left_comp_sot)
lemma additive_cblinfun_compose_sot_right[simp]: ‹additive (λF. cblinfun_compose_sot F G)›
unfolding additive_def
apply transfer
by (simp add: cblinfun_compose_add_left)
lemma additive_cblinfun_compose_sot_left[simp]: ‹additive (λF. cblinfun_compose_sot G F)›
unfolding additive_def
apply transfer
by (simp add: cblinfun_compose_add_right)
lemma transfer_infsum_sot[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: ‹bi_unique R›
shows ‹((R ===> cr_cblinfun_sot) ===> rel_set R ===> cr_cblinfun_sot) (infsum_in cstrong_operator_topology) infsum›
apply (simp add: infsum_euclidean_eq[abs_def, symmetric])
by transfer_prover
lemma transfer_summable_on_sot[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: ‹bi_unique R›
shows ‹((R ===> cr_cblinfun_sot) ===> rel_set R ===> (⟷)) (summable_on_in cstrong_operator_topology) (summable_on)›
apply (simp add: summable_on_euclidean_eq[abs_def, symmetric])
by transfer_prover
lemma sandwich_sot_cont[continuous_intros]:
assumes ‹continuous_map T cstrong_operator_topology f›
shows ‹continuous_map T cstrong_operator_topology (λx. sandwich A (f x))›
apply (simp add: sandwich_apply)
by (intro continuous_intros assms)
lemma closed_map_sot_unitary_sandwich:
fixes U :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space›
assumes ‹unitary U›
shows ‹closed_map cstrong_operator_topology cstrong_operator_topology (λx. sandwich U x)›
apply (rule closed_eq_continuous_inverse_map[where g=‹sandwich (U*)›, THEN iffD2])
using assms
by (auto intro!: continuous_intros
simp flip: sandwich_compose cblinfun_apply_cblinfun_compose)
unbundle no cblinfun_syntax
end