Theory Axioms_Complement_Quantum
section ‹Quantum instantiation of complements›
theory Axioms_Complement_Quantum
imports
Laws_Quantum
Quantum_Extra
Hilbert_Space_Tensor_Product.Weak_Star_Topology
Hilbert_Space_Tensor_Product.Partial_Trace
With_Type.With_Type
Hilbert_Space_Tensor_Product.Misc_Tensor_Product_TTS
begin
unbundle no m_inv_syntax
unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax
no_notation Lattice.join (infixl "⊔ı" 65)
no_notation elt_set_eq (infix "=o" 50)
no_notation eq_closure_of ("closure'_ofı")
hide_const (open) Order.top
declare [[eta_contract]]
lemma register_decomposition_converse:
assumes ‹unitary U›
shows ‹register (λx. sandwich U (id_cblinfun ⊗⇩o x))›
using _ unitary_sandwich_register apply (rule register_comp[unfolded o_def])
using assms by auto
lemma iso_register_decomposition:
assumes [simp]: ‹iso_register F›
shows ‹∃U. unitary U ∧ F = sandwich U›
proof -
from register_decomposition
have ‹let 'c::type = register_decomposition_basis F in
∃U. unitary U ∧ F = sandwich U›
proof with_type_mp
show [simp]: ‹register F›
using assms iso_register_is_register by blast
with_type_case
let ?ida = ‹id_cblinfun :: 'c ell2 ⇒⇩C⇩L _›
from with_type_mp.premise
obtain V :: ‹('a × 'c) ell2 ⇒⇩C⇩L 'b ell2› where ‹unitary V›
and FV: ‹F θ = sandwich V (θ ⊗⇩o ?ida)› for θ
by auto
have inj_V: ‹inj ((*⇩V) (sandwich V))›
by (meson ‹unitary V› register_inj unitary_sandwich_register)
have ‹surj F›
by (meson assms iso_register_inv_comp2 surj_iff)
have surj_tensor: ‹surj (λa::'a ell2 ⇒⇩C⇩L 'a ell2. a ⊗⇩o ?ida)›
apply (rule surj_from_comp[where g=‹sandwich V›])
using ‹surj F› inj_V by (auto simp: FV)
then obtain a :: ‹'a ell2 ⇒⇩C⇩L 'a ell2›
where a: ‹a ⊗⇩o ?ida = butterfly (ket undefined) (ket undefined) ⊗⇩o butterfly (ket undefined) (ket undefined)›
by (smt (verit, best) surjD)
have ‹selfbutter (ket (undefined, undefined)) ≠ 0›
by (metis butterfly_apply cblinfun.zero_left complex_vector.scale_eq_0_iff ket_nonzero orthogonal_ket)
with a have ‹a ≠ 0›
by (auto simp: tensor_ell2_ket tensor_butterfly)
obtain γ where γ: ‹?ida = γ *⇩C butterfly (ket undefined) (ket undefined)›
apply atomize_elim
using a ‹a ≠ 0› by (rule tensor_op_almost_injective)
then have ‹?ida (ket undefined) = γ *⇩C (butterfly (ket undefined) (ket undefined) *⇩V ket undefined)›
by (simp add: ‹id_cblinfun = γ *⇩C butterfly (ket undefined) (ket undefined)› scaleC_cblinfun.rep_eq)
then have ‹ket undefined = γ *⇩C ket undefined›
by (metis butterfly_apply cinner_ket_same id_cblinfun_apply ket_nonzero scaleC_cancel_right scaleC_one)
then have ‹γ = 1›
by (smt (z3) γ butterfly_apply butterfly_scaleC_left cblinfun_id_cblinfun_apply complex_vector.scale_cancel_right cinner_ket_same ket_nonzero)
define T U where ‹T = CBlinfun (λψ. ψ ⊗⇩s ket undefined)› and ‹U = V o⇩C⇩L T›
have T: ‹T ψ = ψ ⊗⇩s ket undefined› for ψ
unfolding T_def
apply (subst bounded_clinear_CBlinfun_apply)
by (auto intro!: bounded_clinear_tensor_ell22)
have ‹sandwich T (butterfly (ket i) (ket j)) = butterfly (ket i) (ket j) ⊗⇩o id_cblinfun› for i j
by (simp add: T sandwich_apply cblinfun_comp_butterfly butterfly_comp_cblinfun γ ‹γ = 1› tensor_butterfly)
then have sandwich_T: ‹sandwich T a = a ⊗⇩o ?ida› for a
apply (rule_tac fun_cong[where x=a])
apply (rule weak_star_clinear_eq_butterfly_ketI[where T=weak_star_topology])
by auto
have ‹F (butterfly x y) = V o⇩C⇩L (butterfly x y ⊗⇩o ?ida) o⇩C⇩L V*› for x y
by (simp add: sandwich_apply FV)
also have ‹… x y = V o⇩C⇩L (butterfly (T x) (T y)) o⇩C⇩L V*› for x y
by (simp add: T γ ‹γ = 1› tensor_butterfly)
also have ‹… x y = U o⇩C⇩L (butterfly x y) o⇩C⇩L U*› for x y
by (simp add: U_def butterfly_comp_cblinfun cblinfun_comp_butterfly)
finally have F_rep: ‹F a = U o⇩C⇩L a o⇩C⇩L U*› for a
apply (rule_tac fun_cong[where x=a])
apply (rule weak_star_clinear_eq_butterfly_ketI[where T=weak_star_topology])
by (auto simp: clinear_register weak_star_cont_register simp flip: sandwich_apply)
have ‹isometry T›
apply (rule orthogonal_on_basis_is_isometry[where B=‹range ket›])
by (auto simp: T)
moreover have ‹T *⇩S ⊤ = ⊤›
proof -
have 1: ‹φ ⊗⇩s ξ ∈ range ((*⇩V) T)› for φ ξ
proof -
have ‹T *⇩V (cinner (ket undefined) ξ *⇩C φ) = φ ⊗⇩s (cinner (ket undefined) ξ *⇩C ket undefined)›
by (simp add: T tensor_ell2_scaleC1 tensor_ell2_scaleC2)
also have ‹… = φ ⊗⇩s (butterfly (ket undefined) (ket undefined) *⇩V ξ)›
by simp
also have ‹… = φ ⊗⇩s (?ida *⇩V ξ)›
by (simp add: γ ‹γ = 1›)
also have ‹… = φ ⊗⇩s ξ›
by simp
finally show ?thesis
by (metis range_eqI)
qed
have ‹⊤ ≤ ccspan {ket x | x. True}›
by (simp add: full_SetCompr_eq)
also have ‹… ≤ ccspan {φ ⊗⇩s ξ | φ ξ. True}›
apply (rule ccspan_mono)
by (auto simp flip: tensor_ell2_ket)
also from 1 have ‹… ≤ ccspan (range ((*⇩V) T))›
by (auto intro!: ccspan_mono)
also have ‹… = T *⇩S ⊤›
by (metis (mono_tags, opaque_lifting) calculation cblinfun_image_ccspan cblinfun_image_mono eq_iff top_greatest)
finally show ‹T *⇩S ⊤ = ⊤›
using top.extremum_uniqueI by blast
qed
ultimately have ‹unitary T›
by (rule surj_isometry_is_unitary)
then have ‹unitary U›
by (simp add: U_def ‹unitary V›)
from F_rep ‹unitary U› show ‹∃U. unitary U ∧ F = sandwich U›
by (auto simp: sandwich_apply[abs_def])
qed
from this[THEN with_type_prepare_cancel, cancel_type_definition, OF with_type_nonempty, OF this]
show ?thesis
by -
qed
lemma complement_exists:
fixes F :: ‹'a update ⇒ 'b update›
assumes ‹register F›
shows ‹let 'c::type = register_decomposition_basis F in
∃G :: 'c update ⇒ 'b update. compatible F G ∧ iso_register (F;G)›
proof (use register_decomposition[OF ‹register F›] in ‹rule with_type_mp›)
note [[simproc del: Laws_Quantum.compatibility_warn]]
assume register_decomposition: ‹∃U :: ('a × 'c) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧ (∀θ. F θ = Complex_Bounded_Linear_Function.sandwich U (θ ⊗⇩o id_cblinfun))›
then obtain U :: ‹('a × 'c) ell2 ⇒⇩C⇩L 'b ell2›
where [simp]: "unitary U" and F: ‹F a = sandwich U (a ⊗⇩o id_cblinfun)› for a
by auto
define G :: ‹'c update ⇒ 'b update› where ‹G b = sandwich U (id_cblinfun ⊗⇩o b)› for b
have [simp]: ‹register G›
unfolding G_def apply (rule register_decomposition_converse) by simp
have ‹F a o⇩C⇩L G b = G b o⇩C⇩L F a› for a b
proof -
have ‹F a o⇩C⇩L G b = sandwich U (a ⊗⇩o b)›
by (auto simp: F G_def sandwich_apply cblinfun_assoc_right
‹unitary U› lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op])
moreover have ‹G b o⇩C⇩L F a = sandwich U (a ⊗⇩o b)›
by (auto simp: F G_def sandwich_apply cblinfun_assoc_right
‹unitary U› lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op])
ultimately show ?thesis by simp
qed
then have [simp]: ‹compatible F G›
by (auto simp: compatible_def ‹register F›)
moreover have ‹iso_register (F;G)›
proof -
have ‹(F;G) (a ⊗⇩o b) = sandwich U (a ⊗⇩o b)› for a b
by (auto simp: register_pair_apply F G_def sandwich_apply cblinfun_assoc_right
‹unitary U› lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op])
then have FG: ‹(F;G) = sandwich U›
apply (rule tensor_extensionality[rotated -1])
by (simp_all add: unitary_sandwich_register)
define I where ‹I = sandwich (U*)› for x
have [simp]: ‹register I›
by (simp add: I_def unitary_sandwich_register)
have ‹I o (F;G) = id› and FGI: ‹(F;G) o I = id›
by (auto intro!:ext simp: I_def[abs_def] FG sandwich_apply cblinfun_assoc_right
‹unitary U› lift_cblinfun_comp[OF unitaryD1] lift_cblinfun_comp[OF unitaryD2]
lift_cblinfun_comp[OF comp_tensor_op])
then show ‹iso_register (F;G)›
by (auto intro!: iso_registerI)
qed
ultimately show ‹∃G :: 'c update ⇒ 'b update. compatible F G ∧ iso_register (F;G)›
apply (rule_tac exI[of _ G]) by auto
qed
lemma commutant_exchange:
fixes F :: ‹'a update ⇒ 'b update›
assumes ‹iso_register F›
shows ‹commutant (F ` X) = F ` commutant X›
proof (rule Set.set_eqI)
fix x :: ‹'b update›
from assms
obtain G where ‹F o G = id› and ‹G o F = id› and [simp]: ‹register G›
using iso_register_def by blast
from assms have [simp]: ‹register F›
using iso_register_def by blast
have ‹x ∈ commutant (F ` X) ⟷ (∀y ∈ F ` X. x o⇩C⇩L y = y o⇩C⇩L x)›
by (simp add: commutant_def)
also have ‹… ⟷ (∀y ∈ F ` X. G x o⇩C⇩L G y = G y o⇩C⇩L G x)›
by (metis (no_types, opaque_lifting) ‹F ∘ G = id› ‹G o F = id› ‹register G› comp_def eq_id_iff register_def)
also have ‹… ⟷ (∀y ∈ X. G x o⇩C⇩L y = y o⇩C⇩L G x)›
by (simp add: ‹G ∘ F = id› pointfree_idE)
also have ‹… ⟷ G x ∈ commutant X›
by (simp add: commutant_def)
also have ‹… ⟷ x ∈ F ` commutant X›
by (metis (no_types, opaque_lifting) ‹G ∘ F = id› ‹F ∘ G = id› image_iff pointfree_idE)
finally show ‹x ∈ commutant (F ` X) ⟷ x ∈ F ` commutant X›
by -
qed
lemma complement_range:
assumes [simp]: ‹compatible F G› and [simp]: ‹iso_register (F;G)›
shows ‹range G = commutant (range F)›
proof -
have [simp]: ‹register F› ‹register G›
using assms compatible_def by metis+
have [simp]: ‹(F;G) (a ⊗⇩o b) = F a o⇩C⇩L G b› for a b
using Laws_Quantum.register_pair_apply assms by blast
have [simp]: ‹range F = (F;G) ` range (λa. a ⊗⇩o id_cblinfun)›
by force
have [simp]: ‹range G = (F;G) ` range (λb. id_cblinfun ⊗⇩o b)›
by force
show ‹range G = commutant (range F)›
by (simp add: commutant_exchange commutant_tensor1)
qed
lemma register_inv_G_o_F:
assumes [simp]: ‹register F› and [simp]: ‹register G› and range_FG: ‹range F ⊆ range G›
shows ‹register (inv G ∘ F)›
proof -
note [[simproc del: Laws_Quantum.compatibility_warn]]
define GF where ‹GF = inv G o F›
have F_rangeG[simp]: ‹F x ∈ range G› for x
using range_FG by auto
have [simp]: ‹inj F› and [simp]: ‹inj G›
by (simp_all add: register_inj)
have [simp]: ‹bounded_clinear F› ‹bounded_clinear G›
by (simp_all add: register_bounded_clinear)
have [simp]: ‹clinear F› ‹clinear G›
by (simp_all add: bounded_clinear.clinear)
have addJ: ‹GF (x + y) = GF x + GF y› for x y
unfolding GF_def o_def
apply (rule injD[OF ‹inj G›])
apply (subst complex_vector.linear_add[OF ‹clinear G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
by (simp add: complex_vector.linear_add)
have scaleJ: ‹GF (r *⇩C x) = r *⇩C GF x› for r x
unfolding GF_def o_def
apply (rule injD[OF ‹inj G›])
apply (subst complex_vector.linear_scale[OF ‹clinear G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
by (simp add: complex_vector.linear_scale)
have unitalJ: ‹GF id_cblinfun = id_cblinfun›
unfolding GF_def o_def
apply (rule injD[OF ‹inj G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G])
by (auto intro!: range_eqI[of _ _ id_cblinfun])
have multJ: ‹GF (a o⇩C⇩L b) = GF a o⇩C⇩L GF b› for a b
unfolding GF_def o_def
apply (rule injD[OF ‹inj G›])
apply (subst register_mult[symmetric, OF ‹register G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
by (simp add: register_mult)
have adjJ: ‹GF (a*) = (GF a)*› for a
unfolding GF_def o_def
apply (rule injD[OF ‹inj G›])
apply (subst register_adjoint[OF ‹register G›])
apply (subst Hilbert_Choice.f_inv_into_f[where f=G], simp)+
using ‹register F› register_adjoint by blast
have normJ: ‹norm (GF a) = norm a› for a
unfolding GF_def
by (metis F_rangeG ‹register F› ‹register G› f_inv_into_f o_def register_norm)
have weak_star_J: ‹continuous_map weak_star_topology weak_star_topology GF›
proof -
have ‹continuous_map weak_star_topology weak_star_topology F›
by (simp add: weak_star_cont_register)
then have ‹continuous_map weak_star_topology (subtopology weak_star_topology (range F)) F›
by (simp add: continuous_map_into_subtopology)
moreover have ‹continuous_map (subtopology weak_star_topology (range G)) weak_star_topology (inv G)›
using ‹register G› register_inv_weak_star_continuous by blast
ultimately show ‹continuous_map weak_star_topology weak_star_topology GF›
by (simp add: GF_def range_FG continuous_map_compose continuous_map_from_subtopology_mono)
qed
from addJ scaleJ unitalJ multJ adjJ normJ weak_star_J
show ‹register GF›
unfolding register_def by (auto intro!: bounded_clinearI[where K=1])
qed
lemma same_range_equivalent:
fixes F :: ‹'a update ⇒ 'c update› and G :: ‹'b update ⇒ 'c update›
assumes [simp]: ‹register F› and [simp]: ‹register G›
assumes range_FG: ‹range F = range G›
shows ‹equivalent_registers F G›
proof -
note [[simproc del: Laws_Quantum.compatibility_warn]]
have regGF: ‹register (inv G o F)›
using assms by (auto intro!: register_inv_G_o_F)
have regFG: ‹register (inv F o G)›
using assms by (auto intro!: register_inv_G_o_F)
have ‹inj G›
by (simp add: register_inj)
with range_FG have GFFG: ‹(inv G o F) o (inv F o G) = id›
by (smt (verit) assms(1) f_inv_into_f invI isomorphism_expand o_def rangeI register_inj)
have ‹inj F›
by (simp add: register_inj)
with range_FG have FGGF: ‹(inv F o G) o (inv G o F) = id›
by (metis GFFG fun.set_map image_inv_f_f left_right_inverse_eq surj_iff)
from regGF regFG GFFG FGGF have iso_FG: ‹iso_register (inv F o G)›
using iso_registerI by auto
have FFG: ‹F o (inv F o G) = G›
by (smt (verit) FGGF GFFG fun.inj_map_strong fun.map_comp fun.set_map image_inv_f_f inj_on_imageI2 inv_id inv_into_injective inv_o_cancel o_inv_o_cancel range_FG surj_id surj_imp_inj_inv)
from FFG iso_FG show ‹equivalent_registers F G›
by (simp add: equivalent_registersI)
qed
lemma complement_unique:
assumes "compatible F G" and ‹iso_register (F;G)›
assumes "compatible F H" and ‹iso_register (F;H)›
shows ‹equivalent_registers G H›
by (metis assms compatible_def complement_range same_range_equivalent)
subsection ‹Finite dimensional complement›
typedef ('a, 'b::finite) complement_domain_simple = ‹{..< if CARD('b) div CARD('a) ≠ 0 then CARD('b) div CARD('a) else 1}›
by auto
instance complement_domain_simple :: (type, finite) finite
proof intro_classes
have ‹inj Rep_complement_domain_simple›
by (simp add: Rep_complement_domain_simple_inject inj_on_def)
moreover have ‹finite (range Rep_complement_domain_simple)›
by (metis finite_lessThan type_definition.Rep_range type_definition_complement_domain_simple)
ultimately show ‹finite (UNIV :: ('a,'b) complement_domain_simple set)›
using finite_image_iff by blast
qed
lemma CARD_complement_domain:
assumes ‹CARD('b::finite) = n * CARD('a)›
shows ‹CARD(('a,'b) complement_domain_simple) = n›
proof -
from assms have ‹n > 0›
by (metis nat_0_less_mult_iff zero_less_card_finite)
have *: ‹inj Rep_complement_domain_simple›
by (simp add: Rep_complement_domain_simple_inject inj_on_def)
moreover have ‹card (range (Rep_complement_domain_simple :: ('a,'b) complement_domain_simple ⇒ _)) = n›
apply (subst type_definition.Rep_range[OF type_definition_complement_domain_simple])
using assms ‹n > 0› apply simp
by force
ultimately show ?thesis
by (metis card_image)
qed
lemma register_decomposition_finite_aux:
fixes Φ :: ‹'a::finite update ⇒ 'b::finite update›
assumes [simp]: ‹register Φ›
shows ‹∃U :: ('a × ('a, 'b) complement_domain_simple) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧
(∀θ. Φ θ = sandwich U (θ ⊗⇩o id_cblinfun))›
proof -
note [[simproc del: compatibility_warn]]
fix ξ0 :: 'a
have [simp]: ‹clinear Φ›
by (simp add: clinear_register)
define P where ‹P i = Proj (ccspan {ket i})› for i :: 'a
have P_butter: ‹P i = butterfly (ket i) (ket i)› for i
by (simp add: P_def butterfly_eq_proj)
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 register_projector)
have ‹(∑i∈UNIV. P i) = id_cblinfun›
using sum_butterfly_ket P_butter by simp
then have sumP'id: ‹(∑i∈UNIV. P' i) = id_cblinfun›
unfolding P'_def
apply (subst complex_vector.linear_sum[OF ‹clinear Φ›, symmetric])
by auto
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)
obtain B0 where finiteB0: ‹finite (B0 i)› and cspanB0: ‹cspan (B0 i) = space_as_set (S i)› for i
apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice)
by (meson cfinite_dim_finite_subspace_basis csubspace_space_as_set)
obtain B where orthoB: ‹is_ortho_set (B i)›
and normalB: ‹⋀b. b ∈ B i ⟹ norm b = 1›
and cspanB: ‹cspan (B i) = cspan (B0 i)›
and finiteB: ‹finite (B i)› for i
apply atomize_elim apply (simp flip: all_conj_distrib) apply (rule choice)
using orthonormal_basis_of_cspan[OF finiteB0] by blast
from cspanB cspanB0 have cspanB: ‹cspan (B i) = space_as_set (S i)› for i
by simp
then have ccspanB: ‹ccspan (B i) = S i› for i
by (metis ccspan.rep_eq closure_finite_cspan finiteB space_as_set_inject)
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 -
from ‹x ∈ B i› obtain x' where x: ‹x = P' i *⇩V x'›
by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P')
from ‹y ∈ B j› obtain y' where y: ‹y = P' j *⇩V y'›
by (metis S_def cblinfun_fixes_range complex_vector.span_base cspanB is_Proj_idempotent proj_P')
have ‹cinner x y = cinner (P' i *⇩V x') (P' j *⇩V y')›
using x y by simp
also have ‹… = cinner (P' j *⇩V P' i *⇩V x') y'›
by (metis cinner_adj_left is_Proj_algebraic proj_P')
also have ‹… = cinner (Φ (P j o⇩C⇩L P i) *⇩V x') y'›
unfolding P'_def register_mult[OF ‹register Φ›, symmetric] by simp
also have ‹… = cinner (Φ (butterfly (ket j) (ket j) o⇩C⇩L butterfly (ket i) (ket i)) *⇩V x') y'›
unfolding P_butter by simp
also have ‹… = cinner (Φ 0 *⇩V x') y'›
by (metis butterfly_comp_butterfly complex_vector.scale_eq_0_iff orthogonal_ket that(3))
also have ‹… = 0›
by (simp add: complex_vector.linear_0)
finally show ?thesis
by -
qed
define B' where ‹B' = (⋃i∈UNIV. B i)›
have P'B: ‹P' i = Proj (ccspan (B i))› for i
unfolding ccspanB S_def
using proj_P' Proj_on_own_range'[symmetric] is_Proj_algebraic by blast
have ‹(∑i∈UNIV. P' i) = Proj (ccspan B')›
proof (unfold B'_def, use finite[of UNIV] in induction)
case empty
show ?case by auto
next
case (insert j M)
have ‹(∑i∈insert j M. P' i) = P' j + (∑i∈M. P' i)›
by (meson insert.hyps(1) insert.hyps(2) sum.insert)
also have ‹… = Proj (ccspan (B j)) + Proj (ccspan (⋃i∈M. B i))›
unfolding P'B insert.IH[symmetric] by simp
also have ‹… = Proj (ccspan (B j ∪ (⋃i∈M. B i)))›
apply (rule Proj_orthog_ccspan_union[symmetric])
using orthoBiBj insert.hyps(2) by auto
also have ‹… = Proj (ccspan (⋃i∈insert j M. B i))›
by auto
finally show ?case
by simp
qed
with sumP'id
have ccspanB': ‹ccspan B' = ⊤›
by (metis Proj_range cblinfun_image_id)
hence cspanB': ‹cspan B' = UNIV›
by (metis B'_def finiteB ccspan.rep_eq finite_UN_I finite_class.finite_UNIV closure_finite_cspan top_ccsubspace.rep_eq)
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
have cardB': ‹card B' = CARD('b)›
apply (subst complex_vector.dim_span_eq_card_independent[symmetric])
apply (rule indepB')
apply (subst cspanB')
using cdim_UNIV_ell2 by auto
from orthoBiBj orthoB
have Bdisj: ‹B i ∩ B j = {}› if ‹i ≠ j› for i j
unfolding is_ortho_set_def
using that by fastforce
have cardBsame: ‹card (B i) = card (B j)› for i j
proof -
define Si_to_Sj where ‹Si_to_Sj i j ψ = Φ (butterfly (ket j) (ket i)) *⇩V ψ› for i j ψ
have S2S2S: ‹Si_to_Sj j i (Si_to_Sj i j ψ) = ψ› if ‹ψ ∈ space_as_set (S i)› for i j ψ
using that P'id
by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def)
also have lin[simp]: ‹clinear (Si_to_Sj i j)› for i j
unfolding Si_to_Sj_def by simp
have S2S: ‹Si_to_Sj i j x ∈ space_as_set (S j)› for i j x
proof -
have ‹Si_to_Sj i j x = P' j *⇩V Si_to_Sj i j x›
by (simp add: Si_to_Sj_def cblinfun_apply_cblinfun_compose[symmetric] register_mult P_butter P'_def)
also have ‹P' j *⇩V Si_to_Sj i j x ∈ space_as_set (S j)›
by (simp add: S_def)
finally show ?thesis by -
qed
have bij: ‹bij_betw (Si_to_Sj i j) (space_as_set (S i)) (space_as_set (S j))›
apply (rule bij_betwI[where g=‹Si_to_Sj j i›])
using S2S S2S2S by (auto intro!: funcsetI)
have ‹cdim (space_as_set (S i)) = cdim (space_as_set (S j))›
using lin apply (rule isomorphic_equal_cdim[where f=‹Si_to_Sj i j›])
using bij by (auto simp: bij_betw_def)
then show ?thesis
by (metis complex_vector.dim_span_eq_card_independent cspanB indepB)
qed
have CARD'b: ‹CARD('b) = card (B ξ0) * CARD('a)›
proof -
have ‹CARD('b) = card B'›
using cardB' by simp
also have ‹… = (∑i∈UNIV. card (B i))›
unfolding B'_def apply (rule card_UN_disjoint)
using finiteB Bdisj by auto
also have ‹… = (∑(i::'a)∈UNIV. card (B ξ0))›
using cardBsame by metis
also have ‹… = card (B ξ0) * CARD('a)›
by auto
finally show ?thesis by -
qed
obtain f where bij_f: ‹bij_betw f (UNIV::('a,'b) complement_domain_simple set) (B ξ0)›
apply atomize_elim apply (rule finite_same_card_bij)
using finiteB CARD_complement_domain[OF CARD'b] by auto
define u where ‹u = (λ(ξ,α). Φ (butterfly (ket ξ) (ket ξ0)) *⇩V f α)› for ξ :: 'a and α :: ‹('a,'b) complement_domain_simple›
obtain U where Uapply: ‹U *⇩V ket ξα = u ξα› for ξα
apply atomize_elim
apply (rule exI[of _ ‹cblinfun_extension (range ket) (λk. u (inv ket k))›])
apply (subst cblinfun_extension_apply)
apply (rule cblinfun_extension_exists_finite_dim)
by (auto simp add: inj_ket cindependent_ket)
define eqa where ‹eqa a b = (if a = b then 1 else 0 :: complex)› for a b :: 'a
define eqc where ‹eqc a b = (if a = b then 1 else 0 :: complex)› for a b :: ‹('a,'b) complement_domain_simple›
define eqac where ‹eqac a b = (if a = b then 1 else 0 :: complex)› for a b :: ‹'a * ('a,'b) complement_domain_simple›
have ‹cinner (U *⇩V ket ξα) (U *⇩V ket ξ'α') = eqac ξα ξ'α'› for ξα ξ'α'
proof -
obtain ξ α ξ' α' where ξα: ‹ξα = (ξ,α)› and ξ'α': ‹ξ'α' = (ξ',α')›
apply atomize_elim by auto
have ‹cinner (U *⇩V ket (ξ,α)) (U *⇩V ket (ξ', α')) = cinner (Φ (butterfly (ket ξ) (ket ξ0)) *⇩V f α) (Φ (butterfly (ket ξ') (ket ξ0)) *⇩V f α')›
unfolding Uapply u_def by simp
also have ‹… = cinner ((Φ (butterfly (ket ξ') (ket ξ0)))* *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V f α) (f α')›
by (simp add: cinner_adj_left)
also have ‹… = cinner (Φ (butterfly (ket ξ') (ket ξ0) *) *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V f α) (f α')›
by (metis (no_types, lifting) assms register_def)
also have ‹… = cinner (Φ (butterfly (ket ξ0) (ket ξ') o⇩C⇩L butterfly (ket ξ) (ket ξ0)) *⇩V f α) (f α')›
by (simp add: register_mult cblinfun_apply_cblinfun_compose[symmetric])
also have ‹… = cinner (Φ (eqa ξ' ξ *⇩C butterfly (ket ξ0) (ket ξ0)) *⇩V f α) (f α')›
by (simp add: eqa_def cinner_ket)
also have ‹… = eqa ξ' ξ * cinner (Φ (butterfly (ket ξ0) (ket ξ0)) *⇩V f α) (f α')›
by (smt (verit, ccfv_threshold) ‹clinear Φ› eqa_def cblinfun.scaleC_left cinner_commute
cinner_scaleC_left cinner_zero_right complex_cnj_one complex_vector.linear_scale)
also have ‹… = eqa ξ' ξ * cinner (P' ξ0 *⇩V f α) (f α')›
using P_butter P'_def by simp
also have ‹… = eqa ξ' ξ * cinner (f α) (f α')›
apply (subst P'id)
apply (metis bij_betw_imp_surj_on bij_f complex_vector.span_base cspanB rangeI)
by simp
also have ‹… = eqa ξ' ξ * eqc α α'›
proof -
from normalB bij_f
have aux1: ‹f α' ∙⇩C f α' ≠ 1 ⟹ eqa ξ' ξ = 0›
by (metis bij_betw_imp_surj_on cnorm_eq_1 rangeI)
from orthoB bij_f have aux2: ‹α ≠ α' ⟹ f α ∙⇩C f α' ≠ 0 ⟹ eqa ξ' ξ = 0›
by (smt (z3) bij_betw_iff_bijections iso_tuple_UNIV_I is_ortho_set_def)
from aux1 aux2 show ?thesis
unfolding eqc_def by auto
qed
finally show ?thesis
by (simp add: eqa_def eqac_def eqc_def ξ'α' ξα)
qed
then have [simp]: ‹isometry U›
apply (rule_tac orthogonal_on_basis_is_isometry[where B=‹range ket›])
using eqac_def by auto
have ‹sandwich (U*) (Φ (butterfly (ket ξ) (ket η))) = butterfly (ket ξ) (ket η) ⊗⇩o id_cblinfun› for ξ η
proof (rule equal_ket, rename_tac ξ1α)
fix ξ1α obtain ξ1 :: 'a and α :: ‹('a,'b) complement_domain_simple› where ξ1α: ‹ξ1α = (ξ1,α)›
apply atomize_elim by auto
have ‹sandwich (U*) (Φ (butterfly (ket ξ) (ket η))) *⇩V ket ξ1α = U* *⇩V Φ (butterfly (ket ξ) (ket η)) *⇩V Φ (butterfly (ket ξ1) (ket ξ0)) *⇩V f α›
by (simp add: sandwich_apply[abs_def] cblinfun_apply_cblinfun_compose ξ1α Uapply u_def)
also have ‹… = U* *⇩V Φ (butterfly (ket ξ) (ket η) o⇩C⇩L butterfly (ket ξ1) (ket ξ0)) *⇩V f α›
by (metis (no_types, lifting) assms butterfly_comp_butterfly lift_cblinfun_comp(4) register_mult)
also have ‹… = U* *⇩V Φ (eqa η ξ1 *⇩C butterfly (ket ξ) (ket ξ0)) *⇩V f α›
by (simp add: eqa_def cinner_ket)
also have ‹… = eqa η ξ1 *⇩C U* *⇩V Φ (butterfly (ket ξ) (ket ξ0)) *⇩V f α›
by (simp add: complex_vector.linear_scale)
also have ‹… = eqa η ξ1 *⇩C U* *⇩V U *⇩V ket (ξ, α)›
unfolding Uapply u_def by simp
also from ‹isometry U› have ‹… = eqa η ξ1 *⇩C ket (ξ, α)›
unfolding cblinfun_apply_cblinfun_compose[symmetric] by simp
also have ‹… = (butterfly (ket ξ) (ket η) *⇩V ket ξ1) ⊗⇩s ket α›
by (simp add: eqa_def 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 ‹sandwich (U*) (Φ (butterfly (ket ξ) (ket η))) *⇩V ket ξ1α = (butterfly (ket ξ) (ket η) ⊗⇩o id_cblinfun) *⇩V ket ξ1α›
by -
qed
then have 1: ‹sandwich (U*) (Φ θ) = θ ⊗⇩o id_cblinfun› for θ
apply (rule clinear_eq_butterfly_ketI[THEN fun_cong, where x=θ, rotated -1])
by (auto intro: bounded_clinear.clinear bounded_linear_intros register_bounded_clinear ‹register Φ›)
have [simp]: ‹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 f b)›])
apply (simp add: u_def, metis bij_betw_inv_into_right bij_f 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_butter)
also have ‹… = Φ (butterfly (ket ξ) (ket ξ0)) *⇩S ccspan (B ξ0)›
by (simp add: ccspanB)
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
moreover have ‹Φ id_cblinfun *⇩S ⊤ ≤ (SUP ξ∈UNIV. Φ (butterfly (ket ξ) (ket ξ)) *⇩S ⊤)›
unfolding sum_butterfly_ket[symmetric]
apply (subst complex_vector.linear_sum, simp)
by (rule cblinfun_sum_image_distr)
ultimately have ‹Φ id_cblinfun *⇩S ⊤ ≤ U *⇩S ⊤›
by (metis (no_types, lifting) Proj_range Proj_top SUP_le_iff assms register_of_id top_le)
then have ‹U *⇩S ⊤ = ⊤›
using top.extremum_unique by auto
with ‹isometry U› show ‹unitary U›
by (rule surj_isometry_is_unitary)
qed
have ‹Φ θ = sandwich U (θ ⊗⇩o id_cblinfun)› for θ
proof -
from 1 have ‹sandwich U (sandwich (U*) *⇩V Φ θ) = sandwich U (θ ⊗⇩o id_cblinfun)›
by simp
then show ?thesis
by (simp flip: sandwich_compose cblinfun_apply_cblinfun_compose)
qed
then show ?thesis
apply (rule_tac exI[of _ U])
by simp
qed
lemma register_decomposition_finite:
fixes Φ :: ‹'a update ⇒ 'b::finite update›
assumes [simp]: ‹register Φ›
shows ‹∃U :: ('a × ('a, 'b) complement_domain_simple) ell2 ⇒⇩C⇩L 'b ell2. unitary U ∧
(∀θ. Φ θ = sandwich U (θ ⊗⇩o id_cblinfun))›
proof -
have inj_butterket: ‹inj (λa. butterfly (ket a) (ket a) :: 'a update)›
proof (rule injI)
fix x y :: 'a
assume ‹butterfly (ket x) (ket x) = butterfly (ket y) (ket y)›
then have ‹butterfly (ket x) (ket x) *⇩V ket x = butterfly (ket y) (ket y) *⇩V ket x›
by simp
then show ‹x = y›
apply (cases ‹x = y›)
by (auto simp: cinner_ket)
qed
from cindependent_butterfly_ket
have ‹cindependent (range (λa. butterfly (ket a) (ket a)) :: 'a update set)›
apply (subgoal_tac ‹(range (λa. butterfly (ket a) (ket a)) :: 'a update set) ⊆ {butterfly (ket i) (ket j) |i j. True}›)
by (auto intro: complex_vector.dependent_mono)
then have ‹cindependent (Φ ` range (λa. butterfly (ket a) (ket a)))›
apply (rule complex_vector.linear_independent_injective_image[rotated])
by (simp_all add: register_inj clinear_register)
then have ‹finite (Φ ` range (λa. butterfly (ket a) (ket a)))›
using cindependent_cfinite_dim_finite by blast
then have ‹finite (range (λa. butterfly (ket a) (ket a)) :: 'a update set)›
apply (rule Finite_Set.inj_on_finite[rotated -1, where f=Φ])
by (simp_all add: register_inj)
then have ‹finite (UNIV :: 'a set)›
apply (rule Finite_Set.inj_on_finite[rotated -1, where f=‹λa. butterfly (ket a) (ket a)›])
apply (rule inj_butterket)
by simp
then have ‹class.finite TYPE('a)›
by intro_classes
from register_decomposition_finite_aux[unoverload_type 'a, OF this]
show ?thesis
using assms by metis
qed
hide_fact register_decomposition_finite_aux
lemma complement_exists_simple:
fixes F :: ‹'a update ⇒ 'b::finite update›
assumes ‹register F›
shows ‹∃G :: ('a, 'b) complement_domain_simple update ⇒ 'b update. compatible F G ∧ iso_register (F;G)›
proof -
note [[simproc del: Laws_Quantum.compatibility_warn]]
obtain U :: ‹('a × ('a, 'b) complement_domain_simple) ell2 ⇒⇩C⇩L 'b ell2›
where [simp]: "unitary U" and F: ‹F a = sandwich U (a ⊗⇩o id_cblinfun)› for a
apply atomize_elim using assms by (rule register_decomposition_finite)
define G :: ‹(('a, 'b) complement_domain_simple) update ⇒ 'b update› where ‹G b = sandwich U (id_cblinfun ⊗⇩o b)› for b
have [simp]: ‹register G›
unfolding G_def apply (rule register_decomposition_converse) by simp
have ‹F a o⇩C⇩L G b = G b o⇩C⇩L F a› for a b
proof -
have ‹F a o⇩C⇩L G b = sandwich U (a ⊗⇩o b)›
by (auto simp: F G_def sandwich_apply cblinfun_assoc_left lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op] ‹unitary U›)
moreover have ‹G b o⇩C⇩L F a = sandwich U (a ⊗⇩o b)›
by (auto simp: F G_def sandwich_apply cblinfun_assoc_left lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op] ‹unitary U›)
ultimately show ?thesis by simp
qed
then have [simp]: ‹compatible F G›
by (auto simp: compatible_def ‹register F› ‹register G›)
moreover have ‹iso_register (F;G)›
proof -
have ‹(F;G) (a ⊗⇩o b) = sandwich U (a ⊗⇩o b)› for a b
by (auto simp: register_pair_apply F G_def sandwich_apply cblinfun_assoc_left lift_cblinfun_comp[OF unitaryD1]
lift_cblinfun_comp[OF comp_tensor_op] ‹unitary U›)
then have FG: ‹(F;G) = sandwich U›
apply (rule tensor_extensionality[rotated -1])
by (simp_all add: bounded_cbilinear.add_left bounded_cbilinear_cblinfun_compose bounded_cbilinear.add_right clinearI unitary_sandwich_register)
define I where ‹I = sandwich (U*)› for x
have [simp]: ‹register I›
by (simp add: I_def unitary_sandwich_register)
have IFG: ‹I o (F;G) = id›
by (auto intro!:ext simp: I_def[abs_def] FG sandwich_apply lift_cblinfun_comp[OF unitaryD1]
‹unitary U› cblinfun_assoc_left)
have FGI: ‹(F;G) o I = id›
by (auto intro!:ext simp: I_def[abs_def] FG sandwich_apply cblinfun_assoc_left
lift_cblinfun_comp[OF unitaryD1] lift_cblinfun_comp[OF unitaryD2] ‹unitary U›)
from IFG FGI show ‹iso_register (F;G)›
by (auto intro!: iso_registerI)
qed
ultimately show ?thesis
apply (rule_tac exI[of _ G]) by (auto)
qed
unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax
end