Theory Axioms_Quantum
section ‹Quantum instantiation of registers›
theory Axioms_Quantum
imports Jordan_Normal_Form.Matrix_Impl "HOL-Library.Rewrite"
Complex_Bounded_Operators.Complex_L2
Hilbert_Space_Tensor_Product.Hilbert_Space_Tensor_Product
Hilbert_Space_Tensor_Product.Weak_Star_Topology
Hilbert_Space_Tensor_Product.Partial_Trace
Hilbert_Space_Tensor_Product.Von_Neumann_Algebras
With_Type.With_Type
Misc
begin
unbundle cblinfun_syntax
unbundle no m_inv_syntax
type_synonym 'a update = ‹('a ell2, 'a ell2) cblinfun›
definition preregister :: ‹('a update ⇒ 'b update) ⇒ bool› where
‹preregister F ⟷ bounded_clinear F ∧ continuous_map weak_star_topology weak_star_topology F›
lemma preregister_mult_right: ‹preregister (λa. a o⇩C⇩L z)›
by (auto simp add: bounded_cbilinear.bounded_clinear_left bounded_cbilinear_cblinfun_compose
preregister_def continuous_map_right_comp_weak_star)
lemma preregister_mult_left: ‹preregister (λa. z o⇩C⇩L a)›
by (auto simp add: bounded_cbilinear.bounded_clinear_right bounded_cbilinear_cblinfun_compose
preregister_def continuous_map_left_comp_weak_star)
lemma comp_preregister: "preregister F ⟹ preregister G ⟹ preregister (G ∘ F)"
by (auto simp add: preregister_def continuous_map_compose comp_bounded_clinear)
lemma id_preregister: ‹preregister id›
unfolding preregister_def by auto
lemma tensor_extensionality:
‹preregister F ⟹ preregister G ⟹ (⋀a b. F (tensor_op a b) = G (tensor_op a b)) ⟹ F = G›
apply (rule weak_star_clinear_eq_butterfly_ketI)
by (auto intro!: bounded_clinear.clinear simp: preregister_def simp flip: tensor_ell2_ket tensor_butterfly)
definition register :: ‹('a update ⇒ 'b update) ⇒ bool› where
"register F ⟷
bounded_clinear F
∧ continuous_map weak_star_topology weak_star_topology F
∧ F id_cblinfun = id_cblinfun
∧ (∀a b. F(a o⇩C⇩L b) = F a o⇩C⇩L F b)
∧ (∀a. F (a*) = (F a)*)"
lemma register_of_id: ‹register F ⟹ F id_cblinfun = id_cblinfun›
by (simp add: register_def)
lemma register_id: ‹register id›
by (simp add: register_def complex_vector.module_hom_id)
lemma register_preregister: "register F ⟹ preregister F"
unfolding register_def preregister_def by auto
lemma register_comp: "register F ⟹ register G ⟹ register (G ∘ F)"
using bounded_clinear_compose continuous_map_compose
apply (simp add: o_def register_def)
by blast
lemma register_mult: "register F ⟹ cblinfun_compose (F a) (F b) = F (cblinfun_compose a b)"
unfolding register_def
by auto
lemma register_tensor_left: ‹register (λa. tensor_op a id_cblinfun)›
by (auto simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint
intro!: tensor_op_cbilinear.bounded_clinear_left)
lemma register_tensor_right: ‹register (λa. tensor_op id_cblinfun a)›
by (auto simp add: comp_tensor_op register_def tensor_op_cbilinear tensor_op_adjoint
bounded_cbilinear_apply_bounded_clinear tensor_op_bounded_cbilinear)
definition register_pair ::
‹('a update ⇒ 'c update) ⇒ ('b update ⇒ 'c update)
⇒ (('a×'b) update ⇒ 'c update)› where
‹register_pair F G = (if register F ∧ register G ∧ (∀a b. F a o⇩C⇩L G b = G b o⇩C⇩L F a) then
SOME R. (∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b) else (λ_. 0))›
lemma cbilinear_F_comp_G[simp]: ‹clinear F ⟹ clinear G ⟹ cbilinear (λa b. F a o⇩C⇩L G b)›
unfolding cbilinear_def
by (auto simp add: clinear_iff bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right)
lemma register_projector:
assumes "register F"
assumes "is_Proj a"
shows "is_Proj (F a)"
using assms unfolding register_def is_Proj_algebraic by metis
lemma register_unitary:
assumes "register F"
assumes "unitary a"
shows "unitary (F a)"
using assms by (smt (verit, best) register_def unitary_def)
definition ‹register_decomposition_basis Φ = (SOME B. is_ortho_set B ∧ (∀b∈B. norm b = 1) ∧ ccspan B = Φ (butterfly (ket undefined) (ket undefined)) *⇩S ⊤)›
for Φ :: ‹'a update ⇒ 'b update›
lemma register_decomposition:
fixes Φ :: ‹'a update ⇒ 'b update›
assumes [simp]: ‹register Φ›
shows ‹let 'c::type = register_decomposition_basis Φ in
(∃U :: ('a × 'c) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧
(∀θ. Φ θ = sandwich U (θ ⊗⇩o id_cblinfun)))›
proof with_type_intro
define ξ0 :: 'a where ‹ξ0 = undefined›
have ‹bounded_clinear Φ›
using assms register_def by blast
then have [simp]: ‹clinear Φ›
by (simp add: bounded_clinear.clinear)
define P where ‹P i = butterfly (ket i) (ket i)› for i :: 'a
note blinfun_cblinfun_eq_bi_unique[transfer_rule del]
note cblinfun.bi_unique[transfer_rule del]
note cblinfun.left_unique[transfer_rule del]
note cblinfun.right_unique[transfer_rule del]
note cblinfun.right_total[transfer_rule del]
note id_cblinfun.transfer[transfer_rule del]
define P' where ‹P' i = Φ (P i)› for i :: 'a
have proj_P': ‹is_Proj (P' i)› for i
by (simp add: P_def P'_def butterfly_is_Proj register_projector)
have sumP'id2: ‹has_sum_in weak_star_topology (λi. P' i) UNIV id_cblinfun›
proof -
from has_sum_butterfly_ket
have ‹has_sum_in weak_star_topology (Φ o (λx. butterfly (ket x) (ket x))) UNIV (Φ id_cblinfun)›
apply (rule has_sum_in_comm_additive[rotated -1])
using assms
by (auto simp: complex_vector.linear_add register_def Modules.additive_def
intro!: continuous_map_is_continuous_at_point complex_vector.linear_0 ‹clinear Φ›)
then show ?thesis
by (simp add: P'_def P_def o_def register_of_id)
qed
define S where ‹S i = P' i *⇩S ⊤› for i :: 'a
have P'id: ‹P' i *⇩V ψ = ψ› if ‹ψ ∈ space_as_set (S i)› for i ψ
using S_def that proj_P'
by (metis cblinfun_fixes_range is_Proj_algebraic)
define S_iso' :: ‹'a ⇒ 'a ⇒ 'a update› where ‹S_iso' i j = classical_operator (Some o Transposition.transpose i j)› for i j :: 'a
have S_iso'_apply: ‹S_iso' i j *⇩V ket i = ket j› for i j
by (simp add: S_iso'_def classical_operator_ket classical_operator_exists_inj)
have S_iso'_unitary: ‹unitary (S_iso' i j)› for i j
by (simp add: S_iso'_def unitary_classical_operator)
have S_iso'_id: ‹S_iso' i i = id_cblinfun› for i
by (auto intro!: equal_ket simp: S_iso'_def classical_operator_ket classical_operator_exists_inj)
have S_iso'_adj_apply: ‹(S_iso' i j)* *⇩V ket j = ket i› for i j
by (metis S_iso'_apply S_iso'_unitary cblinfun_apply_cblinfun_compose id_cblinfun_apply unitaryD1)
define S_iso where ‹S_iso i j = Φ (S_iso' i j)› for i j
have uni_S_iso: ‹unitary (S_iso i j)› for i j
by (simp add: S_iso_def S_iso'_unitary register_unitary)
have S_iso_S: ‹S_iso i j *⇩S S i = S j› for i j
proof -
have ‹S_iso i j *⇩S S i = S_iso i j *⇩S P' i *⇩S S_iso j i *⇩S ⊤›
by (simp add: S_def uni_S_iso)
also have ‹… = S j›
by (simp add: S_def P'_def S_iso_def P_def register_mult butterfly_comp_cblinfun cblinfun_comp_butterfly S_iso'_apply S_iso'_adj_apply
flip: cblinfun_compose_image)
finally show ?thesis
by -
qed
have S_iso_id[simp]: ‹S_iso i i = id_cblinfun› for i
by (simp add: S_iso'_id S_iso_def register_of_id)
obtain B⇩0 where B⇩0: ‹is_ortho_set B⇩0› ‹⋀b. b ∈ B⇩0 ⟹ norm b = 1› ‹ccspan B⇩0 = S ξ0›
using orthonormal_subspace_basis_exists[where S="{}" and V=‹S ξ0›]
apply atomize_elim by auto
have register_decomposition_basis_Φ: ‹is_ortho_set (register_decomposition_basis Φ) ∧
(∀b∈register_decomposition_basis Φ. norm b = 1) ∧
ccspan (register_decomposition_basis Φ) = S ξ0›
unfolding register_decomposition_basis_def
apply (rule someI2[where a=B⇩0])
using B⇩0 by (auto simp: S_def P'_def P_def ξ0_def)
define B where ‹B i = S_iso ξ0 i ` register_decomposition_basis Φ› for i
have Bξ0: ‹B ξ0 = register_decomposition_basis Φ›
using B_def by force
have orthoB: ‹is_ortho_set (B i)› for i
proof -
have 1: ‹x ∈ register_decomposition_basis Φ ⟹
y ∈ register_decomposition_basis Φ ⟹
S_iso ξ0 i *⇩V x ≠ S_iso ξ0 i *⇩V y ⟹ is_orthogonal (S_iso ξ0 i *⇩V x) (S_iso ξ0 i *⇩V y)› for x y
by (metis (no_types, lifting) register_decomposition_basis_Φ UNIV_I cblinfun_apply_cblinfun_compose cblinfun_fixes_range cinner_adj_left id_cblinfun_adjoint is_ortho_set_def top_ccsubspace.rep_eq uni_S_iso unitaryD1 unitary_id unitary_range)
have 2: ‹x ∈ register_decomposition_basis Φ ⟹ S_iso ξ0 i *⇩V x ≠ 0› for x
by (metis register_decomposition_basis_Φ cinner_ket_same cinner_zero_left cnorm_eq_1 isometry_preserves_norm orthogonal_ket uni_S_iso unitary_isometry)
from 1 2 show ?thesis
by (auto simp add: B_def is_ortho_set_def)
qed
have normalB: ‹⋀b. b ∈ B i ⟹ norm b = 1› for i
by (metis (no_types, lifting) register_decomposition_basis_Φ B_def imageE isometry_preserves_norm uni_S_iso unitary_twosided_isometry)
have cspanB: ‹ccspan (B i) = S i› for i
by (simp add: B_def register_decomposition_basis_Φ Bξ0 S_iso_S flip: cblinfun_image_ccspan)
from orthoB have indepB: ‹cindependent (B i)› for i
by (simp add: Complex_Inner_Product.is_ortho_set_cindependent)
have orthoBiBj: ‹is_orthogonal x y› if ‹x ∈ B i› and ‹y ∈ B j› and ‹i ≠ j› for x y i j
proof -
have ‹P' i o⇩C⇩L P' j = 0›
using ‹i ≠ j›
by (simp add: P'_def P_def register_mult butterfly_comp_butterfly cinner_ket
‹clinear Φ› complex_vector.linear_0)
then have *: ‹Proj (ccspan (B i)) o⇩C⇩L Proj (ccspan (B j)) = 0›
by (simp add: Proj_on_own_range S_def cspanB proj_P')
then show ‹is_orthogonal x y›
by (meson orthogonal_projectors_orthogonal_spaces orthogonal_spaces_ccspan that(1) that(2))
qed
define B' where ‹B' = (⋃i∈UNIV. B i)›
have P'B: ‹P' i = Proj (ccspan (B i))› for i
unfolding cspanB S_def
using proj_P' Proj_on_own_range'[symmetric] is_Proj_algebraic by blast
show ‹register_decomposition_basis Φ ≠ {}›
proof (rule ccontr)
assume ‹¬ register_decomposition_basis Φ ≠ {}›
then have ‹B i = {}› for i
by (simp add: B_def)
then have ‹S i = 0› for i
using cspanB by force
then have ‹P' i = 0› for i
by (simp add: P'B cspanB)
with sumP'id2
have ‹has_sum_in weak_star_topology (λi. 0) UNIV id_cblinfun›
by (metis (no_types, lifting) UNIV_I has_sum_in_0 has_sum_in_cong has_sum_in_unique hausdorff_weak_star id_cblinfun_not_0 weak_star_topology_topspace)
then have ‹id_cblinfun = 0›
using has_sum_in_0 has_sum_in_unique hausdorff_weak_star id_cblinfun_not_0 weak_star_topology_topspace by fast
then show False
using id_cblinfun_not_0 by blast
qed
from orthoBiBj orthoB have orthoB': ‹is_ortho_set B'›
unfolding B'_def is_ortho_set_def by blast
then have indepB': ‹cindependent B'›
using is_ortho_set_cindependent by blast
from orthoBiBj orthoB
have Bdisj: ‹B i ∩ B j = {}› if ‹i ≠ j› for i j
unfolding is_ortho_set_def
using cinner_eq_zero_iff that
by fastforce
fix rep_c :: ‹'c ⇒ 'b ell2›
assume bij_rep_c: ‹bij_betw rep_c UNIV (register_decomposition_basis Φ)›
then interpret type_definition rep_c ‹inv rep_c› ‹register_decomposition_basis Φ›
by (simp add: type_definition_bij_betw_iff)
from bij_rep_c have bij_rep_c: ‹bij_betw rep_c (UNIV :: 'c set) (B ξ0)›
unfolding Bξ0 by simp
define u where ‹u = (λ(ξ,α). Φ (butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α)› for ξ :: 'a and α :: ‹'c›
have cinner_u: ‹cinner (u ξα) (u ξ'α') = of_bool (ξα = ξ'α')› for ξα ξ'α'
proof -
obtain ξ α ξ' α' where ξα: ‹ξα = (ξ,α)› and ξ'α': ‹ξ'α' = (ξ',α')›
apply atomize_elim by auto
have ‹cinner (u (ξ,α)) (u (ξ', α')) = cinner (Φ (butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α) (Φ (butterfly (ket ξ') (ket ξ0)) *⇩V rep_c α')›
unfolding u_def by simp
also have ‹… = cinner ((Φ (butterfly (ket ξ') (ket ξ0)))* *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α) (rep_c α')›
by (simp add: cinner_adj_left)
also have ‹… = cinner (Φ (butterfly (ket ξ') (ket ξ0) *) *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α) (rep_c α')›
by (metis (no_types, lifting) assms register_def)
also have ‹… = cinner (Φ (butterfly (ket ξ0) (ket ξ') o⇩C⇩L butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α) (rep_c α')›
by (simp add: register_mult cblinfun_apply_cblinfun_compose[symmetric])
also have ‹… = cinner (Φ (of_bool (ξ'=ξ) *⇩C butterfly (ket ξ0) (ket ξ0)) *⇩V rep_c α) (rep_c α')›
by (simp add: cinner_ket_left ket.rep_eq)
also have ‹… = of_bool (ξ'=ξ) * cinner (Φ (butterfly (ket ξ0) (ket ξ0)) *⇩V rep_c α) (rep_c α')›
by (simp add: complex_vector.linear_0)
also have ‹… = of_bool (ξ'=ξ) * cinner (P' ξ0 *⇩V rep_c α) (rep_c α')›
using P_def P'_def by simp
also have ‹… = of_bool (ξ'=ξ) * cinner (rep_c α) (rep_c α')›
apply (subst P'id)
apply (metis Bξ0 Rep ccspan_superset cspanB in_mono)
by simp
also have ‹… = of_bool (ξ'=ξ) * of_bool (α=α')›
using bij_rep_c orthoB normalB unfolding is_ortho_set_def
by (smt (verit, best) Bξ0 Rep Rep_inject cnorm_eq_1 of_bool_eq(1) of_bool_eq(2))
finally show ?thesis
by (simp add: ξ'α' ξα)
qed
define U where ‹U = cblinfun_extension (range ket) (u o inv ket)›
have Uapply: ‹U *⇩V ket ξα = u ξα› for ξα
proof -
have aux: ‹(⋀a b aa ba. u (a, b) ∙⇩C u (aa, ba) = of_bool (a = aa ∧ b = ba)) ⟹ norm (u (a, b)) ≤ 1› for a b
by (metis (full_types) cinner_u cnorm_eq_1 of_bool_eq_1_iff order_refl)
then show ?thesis
unfolding U_def
apply (subst cblinfun_extension_apply)
using cinner_u by (auto intro!: cblinfun_extension_exists_ortho[where B=1])
qed
have ‹isometry U›
apply (rule_tac orthogonal_on_basis_is_isometry[where B=‹range ket›])
by (auto simp: Uapply cinner_u)
have 1: ‹U* o⇩C⇩L Φ θ o⇩C⇩L U = θ ⊗⇩o id_cblinfun› for θ
proof -
have *: ‹U* o⇩C⇩L Φ (butterfly (ket ξ) (ket η)) o⇩C⇩L U = butterfly (ket ξ) (ket η) ⊗⇩o id_cblinfun› for ξ η
proof (rule equal_ket, rename_tac ξ1α)
fix ξ1α obtain ξ1 :: 'a and α :: ‹'c› where ξ1α: ‹ξ1α = (ξ1,α)›
apply atomize_elim by auto
have ‹(U* o⇩C⇩L Φ (butterfly (ket ξ) (ket η)) o⇩C⇩L U) *⇩V ket ξ1α = U* *⇩V Φ (butterfly (ket ξ) (ket η)) *⇩V Φ (butterfly (ket ξ1) (ket ξ0)) *⇩V rep_c α›
unfolding cblinfun_apply_cblinfun_compose ξ1α Uapply u_def by simp
also have ‹… = U* *⇩V Φ (butterfly (ket ξ) (ket η) o⇩C⇩L butterfly (ket ξ1) (ket ξ0)) *⇩V rep_c α›
by (metis assms register_mult simp_a_oCL_b')
also have ‹… = U* *⇩V Φ (of_bool (η=ξ1) *⇩C butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α›
by (simp add: cinner_ket)
also have ‹… = of_bool (η=ξ1) *⇩C U* *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V rep_c α›
by (simp add: complex_vector.linear_scale)
also have ‹… = of_bool (η=ξ1) *⇩C U* *⇩V U *⇩V ket (ξ, α)›
unfolding Uapply u_def by simp
also from ‹isometry U› have ‹… = of_bool (η=ξ1) *⇩C ket (ξ, α)›
unfolding cblinfun_apply_cblinfun_compose[symmetric] by simp
also have ‹… = (butterfly (ket ξ) (ket η) *⇩V ket ξ1) ⊗⇩s ket α›
by (simp add: tensor_ell2_scaleC1 tensor_ell2_ket)
also have ‹… = (butterfly (ket ξ) (ket η) ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
by (simp add: ξ1α tensor_op_ket)
finally show ‹(U* o⇩C⇩L Φ (butterfly (ket ξ) (ket η)) o⇩C⇩L U) *⇩V ket ξ1α = (butterfly (ket ξ) (ket η) ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
by -
qed
have cont1: ‹continuous_map weak_star_topology weak_star_topology (λa. U* o⇩C⇩L Φ a o⇩C⇩L U)›
apply (subst asm_rl[of ‹(λa. U* o⇩C⇩L Φ a o⇩C⇩L U) = (λx. x o⇩C⇩L U) o (λx. U* o⇩C⇩L x) o Φ›])
apply force
apply (intro continuous_map_compose[where X'=weak_star_topology])
using assms register_def continuous_map_left_comp_weak_star continuous_map_right_comp_weak_star by blast+
have *: ‹U* o⇩C⇩L Φ θ o⇩C⇩L U = θ ⊗⇩o id_cblinfun› if ‹θ ∈ cspan (range (λ(ξ, η). butterfly (ket ξ) (ket η)))› for θ
apply (rule complex_vector.linear_eq_on[where x=θ, OF _ _ that])
apply (intro ‹clinear Φ›
clinear_compose[OF _ clinear_cblinfun_compose_left, unfolded o_def]
clinear_compose[OF _ clinear_cblinfun_compose_right, unfolded o_def])
apply simp
using * by fast
have ‹U* o⇩C⇩L Φ θ o⇩C⇩L U = θ ⊗⇩o id_cblinfun›
if ‹θ ∈ (weak_star_topology closure_of (cspan (range (λ(ξ, η). butterfly (ket ξ) (ket η)))))› for θ
apply (rule closure_of_eqI[OF _ _ that])
using * cont1 left_amplification_weak_star_cont by auto
with butterkets_weak_star_dense show ?thesis
by auto
qed
have ‹unitary U›
proof -
have ‹Φ (butterfly (ket ξ) (ket ξ1)) *⇩S ⊤ ≤ U *⇩S ⊤› for ξ ξ1
proof -
have *: ‹Φ (butterfly (ket ξ) (ket ξ0)) *⇩V b ∈ space_as_set (U *⇩S ⊤)› if ‹b ∈ B ξ0› for b
apply (subst asm_rl[of ‹Φ (butterfly (ket ξ) (ket ξ0)) *⇩V b = u (ξ, inv rep_c b)›])
apply (simp add: u_def, metis bij_betw_inv_into_right bij_rep_c that)
by (metis Uapply cblinfun_apply_in_image)
have ‹Φ (butterfly (ket ξ) (ket ξ1)) *⇩S ⊤ = Φ (butterfly (ket ξ) (ket ξ0)) *⇩S Φ (butterfly (ket ξ0) (ket ξ0)) *⇩S Φ (butterfly (ket ξ0) (ket ξ1)) *⇩S ⊤›
unfolding cblinfun_compose_image[symmetric] register_mult[OF assms]
by simp
also have ‹… ≤ Φ (butterfly (ket ξ) (ket ξ0)) *⇩S Φ (butterfly (ket ξ0) (ket ξ0)) *⇩S ⊤›
by (meson cblinfun_image_mono top_greatest)
also have ‹… = Φ (butterfly (ket ξ) (ket ξ0)) *⇩S S ξ0›
by (simp add: S_def P'_def P_def)
also have ‹… = Φ (butterfly (ket ξ) (ket ξ0)) *⇩S ccspan (B ξ0)›
by (simp add: cspanB)
also have ‹… = ccspan (Φ (butterfly (ket ξ) (ket ξ0)) ` B ξ0)›
by (meson cblinfun_image_ccspan)
also have ‹… ≤ U *⇩S ⊤›
by (rule ccspan_leqI, use * in auto)
finally show ?thesis by -
qed
then have ‹ccspan {Φ (butterfly (ket ξ) (ket ξ)) *⇩V α |ξ α. True} ≤ U *⇩S ⊤›
apply (rule_tac ccspan_leqI)
using cblinfun_apply_in_image less_eq_ccsubspace.rep_eq by blast
moreover have ‹ccspan {Φ (butterfly (ket ξ) (ket ξ)) *⇩V α |ξ α. True} = ⊤›
proof -
define Q where ‹Q = Proj (- ccspan {Φ (butterfly (ket ξ) (ket ξ)) *⇩V α |ξ α. True})›
have ‹has_sum_in weak_star_topology (λξ. Q o⇩C⇩L Φ (butterfly (ket ξ) (ket ξ))) UNIV (Q o⇩C⇩L id_cblinfun)›
apply (rule has_sum_in_comm_additive[where g=‹cblinfun_compose Q› and T=weak_star_topology, unfolded o_def])
using sumP'id2
by (auto simp add: continuous_map_left_comp_weak_star P'_def P_def cblinfun_compose_add_right Modules.additive_def)
moreover have ‹Q o⇩C⇩L Φ (butterfly (ket ξ) (ket ξ)) = 0› for ξ
apply (rule equal_ket)
apply (simp add: Q_def Proj_ortho_compl cblinfun.diff_left)
apply (subst Proj_fixes_image)
by (auto intro!: ccspan_superset[THEN set_mp])
ultimately have ‹Q = 0›
apply (rule_tac has_sum_in_unique)
by auto
then show ?thesis
by (smt (verit, del_insts) Q_def Proj_ortho_compl Proj_range cblinfun_image_id right_minus_eq)
qed
ultimately have ‹U *⇩S ⊤ = ⊤›
by (simp add: top.extremum_unique)
with ‹isometry U› show ‹unitary U›
by (rule surj_isometry_is_unitary)
qed
have ‹Φ θ = U o⇩C⇩L (θ ⊗⇩o id_cblinfun) o⇩C⇩L U*› for θ
proof -
from ‹unitary U›
have ‹Φ θ = (U o⇩C⇩L U*) o⇩C⇩L Φ θ o⇩C⇩L (U o⇩C⇩L U*)›
by simp
also have ‹… = U o⇩C⇩L (U* o⇩C⇩L Φ θ o⇩C⇩L U) o⇩C⇩L U*›
by (simp add: cblinfun_assoc_left)
also have ‹… = U o⇩C⇩L (θ ⊗⇩o id_cblinfun) o⇩C⇩L U*›
using 1 by simp
finally show ?thesis
by -
qed
with ‹unitary U› show ‹∃U :: ('a × 'c) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧ (∀θ. Φ θ = sandwich U (θ ⊗⇩o id_cblinfun))›
by (auto simp: sandwich_apply)
qed
lemma register_bounded_clinear: ‹register F ⟹ bounded_clinear F›
using preregister_def register_preregister by blast
lemma clinear_register: ‹register F ⟹ clinear F›
using bounded_clinear.clinear register_bounded_clinear by blast
lemma weak_star_cont_register: ‹register F ⟹ continuous_map weak_star_topology weak_star_topology F›
using register_def by blast
lemma register_inv_weak_star_continuous:
assumes ‹register F›
shows ‹continuous_map (subtopology weak_star_topology (range F)) weak_star_topology (inv F)›
proof (rule continuous_map_iff_preserves_convergence, rename_tac K a)
fix K a
assume limit_id: ‹limitin (subtopology weak_star_topology (range F)) id a K›
from register_decomposition
have ‹let 'c::type = register_decomposition_basis F in
limitin weak_star_topology (inv F) (inv F a) K›
proof with_type_mp
from assms show ‹register F› by -
next
with_type_case
then obtain U :: ‹('a × 'c) ell2 ⇒⇩C⇩L 'b ell2›
where ‹unitary U› and FU: ‹F θ = sandwich U (θ ⊗⇩o id_cblinfun)› for θ
by auto
define δ :: ‹'c ell2 ⇒⇩C⇩L 'c ell2› where ‹δ = selfbutter (ket (undefined))›
then have [simp]: ‹trace_class δ›
by simp
define u where ‹u t = U o⇩C⇩L (from_trace_class t ⊗⇩o δ) o⇩C⇩L U*› for t
have [simp]: ‹trace_class (u t)› for t
unfolding u_def
apply (rule trace_class_comp_left)
apply (rule trace_class_comp_right)
by (simp add: trace_class_tensor)
have uF: ‹trace (from_trace_class t o⇩C⇩L a) = trace (u t o⇩C⇩L F a)› for t a
proof -
have ‹trace (from_trace_class t o⇩C⇩L a) = trace (from_trace_class t o⇩C⇩L a) * trace (δ o⇩C⇩L id_cblinfun)›
by (simp add: δ_def trace_butterfly)
also have ‹… = trace ((from_trace_class t o⇩C⇩L a) ⊗⇩o (δ o⇩C⇩L id_cblinfun))›
by (simp add: trace_class_comp_left trace_tensor)
also have ‹… = trace ((from_trace_class t ⊗⇩o δ) o⇩C⇩L (a ⊗⇩o id_cblinfun))›
by (simp add: comp_tensor_op)
also have ‹… = trace (U* o⇩C⇩L u t o⇩C⇩L U o⇩C⇩L (a ⊗⇩o id_cblinfun))›
using ‹unitary U›
by (simp add: u_def lift_cblinfun_comp[OF unitaryD1] cblinfun_compose_assoc)
also have ‹… = trace (u t o⇩C⇩L U o⇩C⇩L (a ⊗⇩o id_cblinfun) o⇩C⇩L U*)›
apply (subst (2) circularity_of_trace)
by (simp_all add: trace_class_comp_left cblinfun_compose_assoc)
also have ‹… = trace (u t o⇩C⇩L F a)›
by (simp add: sandwich_apply FU cblinfun_compose_assoc)
finally show ?thesis
by -
qed
from limit_id
have ‹a ∈ range F› and KrangeF: ‹∀⇩F a in K. a ∈ range F› and limit_id': ‹limitin weak_star_topology id a K›
unfolding limitin_subtopology by auto
from ‹a ∈ range F› have FiFa: ‹F (inv F a) = a›
by (simp add: f_inv_into_f)
from KrangeF
have *: ‹∀⇩F x in K. trace (from_trace_class t o⇩C⇩L F (inv F x)) = trace (from_trace_class t o⇩C⇩L x)› for t
apply (rule eventually_mono)
by (simp add: f_inv_into_f)
from limit_id' have ‹((λa'. trace (from_trace_class t o⇩C⇩L a')) ⤏ trace (from_trace_class t o⇩C⇩L a)) K› for t
unfolding limitin_weak_star_topology' by simp
then have *: ‹((λa'. trace (from_trace_class t o⇩C⇩L F (inv F a'))) ⤏ trace (from_trace_class t o⇩C⇩L F (inv F a))) K› for t
unfolding FiFa using * by (rule tendsto_cong[THEN iffD2, rotated])
have ‹((λa'. trace (u t o⇩C⇩L F (inv F a'))) ⤏ trace (u t o⇩C⇩L F (inv F a))) K› for t
using *[of ‹Abs_trace_class (u t)›]
by (simp add: Abs_trace_class_inverse)
then have ‹((λa'. trace (from_trace_class t o⇩C⇩L inv F a')) ⤏ trace (from_trace_class t o⇩C⇩L inv F a)) K› for t
by (simp add: uF[symmetric])
then show ‹limitin weak_star_topology (inv F) (inv F a) K›
by (simp add: limitin_weak_star_topology')
qed
note this[cancel_with_type]
then show ‹limitin weak_star_topology (inv F) (inv F a) K›
by -
qed
lemma register_inj: ‹inj_on F X› if [simp]: ‹register F›
proof -
have ‹let 'c::type = register_decomposition_basis F in inj F›
using register_decomposition[OF ‹register F›]
proof with_type_mp
with_type_case
then obtain U :: ‹('a × 'c) ell2 ⇒⇩C⇩L 'b ell2›
where ‹unitary U› and F: ‹F a = Complex_Bounded_Linear_Function.sandwich U (a ⊗⇩o id_cblinfun)› for a
apply atomize_elim by auto
have ‹inj (Complex_Bounded_Linear_Function.sandwich U)›
by (smt (verit, best) ‹unitary U› cblinfun_assoc_left inj_onI sandwich_apply cblinfun_compose_id_right cblinfun_compose_id_left unitary_def)
moreover have ‹inj (λa::'a ell2 ⇒⇩C⇩L _. a ⊗⇩o id_cblinfun)›
by (rule inj_tensor_left, simp)
ultimately show ‹inj F›
unfolding F
by (smt (z3) inj_def)
qed
from this[THEN with_type_prepare_cancel, cancel_type_definition, OF with_type_nonempty, OF this]
show ‹inj_on F X›
by (simp add: inj_on_def)
qed
lemma register_norm: ‹norm (F a) = norm a› if ‹register F›
proof -
from register_decomposition[OF that]
have ‹let 'c::type = register_decomposition_basis F in
norm (F a) = norm a›
proof with_type_mp
with_type_case
then obtain U :: ‹('a × 'c) ell2 ⇒⇩C⇩L 'b ell2› where ‹unitary U›
and FU: ‹F θ = sandwich U (θ ⊗⇩o id_cblinfun)› for θ
by metis
show ‹norm (F a) = norm a›
using ‹unitary U›
by (simp add: FU sandwich_apply norm_isometry_compose norm_isometry_compose' norm_isometry tensor_op_norm)
qed
note this[cancel_with_type]
then show ?thesis
by simp
qed
lemma unitary_sandwich_register: ‹unitary a ⟹ register (sandwich a)›
by (auto simp: sandwich_apply register_def cblinfun.bounded_clinear_right
lift_cblinfun_comp[OF unitaryD1] lift_cblinfun_comp[OF unitaryD2]
cblinfun_assoc_left)
lemma register_adj: ‹register F ⟹ F (a*) = (F a)*›
using register_def by blast
lemma right_register_tensor_ex: ‹∃T :: ('a × 'b) update ⇒ ('a × 'c) update.
register T ∧ (∀a b. T (a ⊗⇩o b) = a ⊗⇩o F b)› if ‹register F›
proof -
from register_decomposition[OF ‹register F›]
have ‹let 'g::type = register_decomposition_basis F in
∃T :: ('a × 'b) update ⇒ ('a × 'c) update.
register T ∧ (∀a b. T (a ⊗⇩o b) = a ⊗⇩o F b)›
proof with_type_mp
with_type_case
then obtain U :: ‹('b × 'g) ell2 ⇒⇩C⇩L 'c ell2›
where [simp]: ‹unitary U› and F: ‹F θ = sandwich U *⇩V θ ⊗⇩o id_cblinfun› for θ
by auto
define T :: ‹('a × 'b) update ⇒ ('a × 'c) update›
where ‹T = sandwich (id_cblinfun ⊗⇩o U) o sandwich assoc_ell2 o (λab. ab ⊗⇩o id_cblinfun)›
have ‹register T›
by (auto intro!: register_comp register_tensor_left unitary_sandwich_register unitary_tensor_op simp add: T_def)
moreover have ‹T (a ⊗⇩o b) = a ⊗⇩o F b› for a b
by (simp add: T_def F sandwich_tensor_op)
ultimately show ‹∃T :: ('a × 'b) update ⇒ ('a × 'c) update. register T ∧ (∀a b. T (a ⊗⇩o b) = a ⊗⇩o F b)›
by auto
qed
from this[cancel_with_type]
show ?thesis
by -
qed
lemma
fixes F :: ‹'a update ⇒ 'c update› and G
assumes [simp]: ‹register F› ‹register G›
assumes FG_comm: ‹⋀a b. F a o⇩C⇩L G b = G b o⇩C⇩L F a›
shows register_pair_apply: ‹(register_pair F G) (tensor_op a b) = F a o⇩C⇩L G b›
and register_pair_is_register: ‹register (register_pair F G)›
proof -
have *: ‹register_pair F G = (SOME R. ∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b)›
using assms unfolding register_pair_def by simp
from register_decomposition[OF ‹register F›]
have ‹let 'd::type = register_decomposition_basis F in
∃R. ∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b›
proof with_type_mp
with_type_case
then obtain U :: ‹('a × 'd) ell2 ⇒⇩C⇩L 'c ell2› where [simp]: ‹unitary U›
and FU: ‹F θ = sandwich U (θ ⊗⇩o id_cblinfun)› for θ
by metis
from register_decomposition[OF ‹register G›]
have ‹let 'f::type = register_decomposition_basis G in
∃R. ∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b›
proof with_type_mp
with_type_case
then obtain V :: ‹('b × 'f) ell2 ⇒⇩C⇩L 'c ell2› where [simp]: ‹unitary V›
and GU: ‹G θ = sandwich V (θ ⊗⇩o id_cblinfun)› for θ
by metis
show ‹∃FG. ∀a b. register FG ∧ FG (a ⊗⇩o b) = F a o⇩C⇩L G b›
proof -
define G' and ι :: ‹'d update ⇒ ('a × 'd) update› and G⇩1
where ‹G' = sandwich (U*) o G› and ‹ι d = id_cblinfun ⊗⇩o d› and ‹G⇩1 = inv ι o G'› for d
have [simp]: ‹register G'›
by (simp add: G'_def register_comp unitary_sandwich_register)
then have [simp]: ‹bounded_clinear G'›
by (meson register_bounded_clinear)
then have [simp]: ‹clinear G'›
by (simp add: bounded_clinear.axioms(1))
have ‹range G' = sandwich (U*) ` range G›
by (simp add: GU G'_def image_image)
also have ‹… ⊆ sandwich (U*) ` commutant (range F)›
by (auto intro!: image_mono simp: commutant_def FG_comm)
also have ‹… = commutant (sandwich (U*) ` range F)›
by (simp add: sandwich_unitary_commutant)
also have ‹… = commutant (range (λa. a ⊗⇩o id_cblinfun))›
apply (rule arg_cong[where f=commutant])
by (simp add: FU image_image flip: sandwich_compose cblinfun_apply_cblinfun_compose)
also have ‹… = range (λd. id_cblinfun ⊗⇩o d)›
by (rule commutant_tensor1)
also have ‹… = range ι›
by (simp add: ι_def[abs_def])
finally have range_G': ‹range G' ⊆ range ι›
by -
have ‹continuous_map weak_star_topology weak_star_topology G'›
by (auto intro!: continuous_map_compose[where X'=weak_star_topology] simp: G'_def weak_star_cont_register)
then have cont_G': ‹continuous_map weak_star_topology (subtopology weak_star_topology (range ι)) G'›
using range_G' by (auto intro!: continuous_map_into_subtopology)
have [simp]: ‹register ι›
by (simp add: ι_def[abs_def] register_tensor_right)
then have cont_invι: ‹continuous_map (subtopology weak_star_topology (range ι)) weak_star_topology (inv ι)›
by (rule register_inv_weak_star_continuous)
have ι_inj: ‹x = y› if ‹ι x = ι y› for x y
by (metis ‹register ι› invI register_inj that)
have [simp]: ‹register G⇩1›
proof (unfold register_def, intro conjI allI)
from cont_G' cont_invι
show cont_G⇩1: ‹continuous_map weak_star_topology weak_star_topology G⇩1›
using G⇩1_def continuous_map_compose by blast
have ι_cancel: ‹ι (inv ι x) = x› if ‹x ∈ range G'› for x
by (meson f_inv_into_f range_G' subsetD that)
show ‹bounded_clinear G⇩1›
using range_G'
by (auto intro!: bounded_clinearI[where K=1] ι_inj
simp: G⇩1_def complex_vector.linear_add[of ι] bounded_clinear.clinear clinear_register
ι_cancel range_subsetD complex_vector.linear_scale[of ι] register_norm[of G']
simp flip: complex_vector.linear_add[of G'] complex_vector.linear_scale[of G']
register_norm[of ι])
show ‹G⇩1 id_cblinfun = id_cblinfun›
by (auto intro!: ι_inj register_of_id[of G'] simp add: G⇩1_def ι_cancel register_of_id[of ι])
show adj_G⇩1: ‹G⇩1 (a*) = (G⇩1 a)*› for a
using range_G'
by (auto intro!: ι_inj
simp: G⇩1_def ι_cancel register_adj[of ι]
simp flip: register_adj[of G'])
show mult_G⇩1: ‹G⇩1 (a o⇩C⇩L b) = G⇩1 a o⇩C⇩L G⇩1 b› for a b
using range_G'
by (auto intro!: bounded_clinearI[where K=1] ι_inj
simp: G⇩1_def ι_cancel register_mult[of G']
simp flip: register_mult[of ι])
qed
obtain T :: ‹('a × 'b) update ⇒ ('a × 'd) update›
where [simp]: ‹register T› and T_apply: ‹T (a ⊗⇩o b) = a ⊗⇩o G⇩1 b› for a b
using ‹register G⇩1› right_register_tensor_ex by blast
define FG where ‹FG = sandwich U o T›
then have [simp]: ‹register FG›
by (auto intro!: register_comp unitary_sandwich_register simp add: FG_def)
have ‹FG (a ⊗⇩o b) = F a o⇩C⇩L G b› for a b
proof -
have FG_a: ‹FG (a ⊗⇩o id_cblinfun) = F a›
by (simp add: FG_def T_apply register_of_id FU)
have ‹FG (id_cblinfun ⊗⇩o b) = sandwich U (ι (G⇩1 b))›
by (simp add: FG_def T_apply ι_def)
also have ‹… = sandwich U (G' b)›
apply (rule arg_cong[where f=‹cblinfun_apply _›])
by (metis G⇩1_def UNIV_I f_inv_into_f image_subset_iff o_def range_G')
also have ‹… = G b›
by (smt (verit) G'_def ‹unitary U› cblinfun_apply_cblinfun_compose cblinfun_compose_id_left cblinfun_compose_id_right comp_def id_cblinfun_adjoint sandwich.rep_eq sandwich_compose unitaryD2)
finally have FG_b: ‹FG (id_cblinfun ⊗⇩o b) = G b›
by -
have ‹FG (a ⊗⇩o b) = FG (a ⊗⇩o id_cblinfun) o⇩C⇩L FG (id_cblinfun ⊗⇩o b)›
by (simp add: comp_tensor_op register_mult)
also have ‹… = F a o⇩C⇩L G b›
by (simp add: FG_a FG_b)
finally show ?thesis
by -
qed
with ‹register FG› show ?thesis
by metis
qed
qed
from this[cancel_with_type]
show ‹∃R. ∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b›
by -
qed
from this[cancel_with_type]
have ‹∃R. ∀a b. register R ∧ R (a ⊗⇩o b) = F a o⇩C⇩L G b›
by -
then have ‹∀a b. register (register_pair F G) ∧ (register_pair F G) (a ⊗⇩o b) = F a o⇩C⇩L G b›
unfolding * by (smt (verit) someI_ex)
then show ‹(register_pair F G) (tensor_op a b) = F a o⇩C⇩L G b› and ‹register (register_pair F G)›
by auto
qed
unbundle no cblinfun_syntax
end