Theory Kraus_Maps.Kraus_Maps
section ‹Kraus maps›
theory Kraus_Maps
imports Kraus_Families
begin
subsection ‹Kraus maps›
unbundle kraus_map_syntax
unbundle cblinfun_syntax
definition kraus_map :: ‹(('a::chilbert_space,'a) trace_class ⇒ ('b::chilbert_space,'b) trace_class) ⇒ bool› where
kraus_map_def_raw: ‹kraus_map 𝔈 ⟷ (∃EE :: ('a,'b,unit) kraus_family. 𝔈 = kf_apply EE)›
lemma kraus_map_def: ‹kraus_map 𝔈 ⟷ (∃EE :: ('a::chilbert_space,'b::chilbert_space,'x) kraus_family. 𝔈 = kf_apply EE)›
proof (rule iffI)
assume ‹kraus_map 𝔈›
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
define EE' :: ‹('a,'b,'x) kraus_family› where ‹EE' = kf_map (λ_. undefined) EE›
have ‹kf_apply EE' = kf_apply EE›
by (simp add: EE'_def kf_apply_map)
with EE show ‹∃EE :: ('a,'b,'x) kraus_family. 𝔈 = kf_apply EE›
by metis
next
assume ‹∃EE :: ('a,'b,'x) kraus_family. 𝔈 = kf_apply EE›
then obtain EE :: ‹('a,'b,'x) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
define EE' :: ‹('a,'b,unit) kraus_family› where ‹EE' = kf_map (λ_. ()) EE›
have ‹kf_apply EE' = kf_apply EE›
by (simp add: EE'_def kf_apply_map)
with EE show ‹kraus_map 𝔈›
apply (simp add: kraus_map_def_raw)
by metis
qed
lemma kraus_mapI:
assumes ‹𝔈 = kf_apply 𝔈'›
shows ‹kraus_map 𝔈›
using assms kraus_map_def by blast
lemma kraus_map_bounded_clinear:
‹bounded_clinear 𝔈› if ‹kraus_map 𝔈›
by (metis kf_apply_bounded_clinear kraus_map_def that)
lemma kraus_map_pos:
assumes ‹kraus_map 𝔈› and ‹ρ ≥ 0›
shows ‹𝔈 ρ ≥ 0›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
show ?thesis
by (simp add: 𝔈' assms(2) kf_apply_pos)
qed
lemma kraus_map_mono:
assumes ‹kraus_map 𝔈› and ‹ρ ≥ τ›
shows ‹𝔈 ρ ≥ 𝔈 τ›
by (metis assms kf_apply_mono_right kraus_map_def_raw)
lemma kraus_map_kf_apply[iff]: ‹kraus_map (kf_apply 𝔈)›
using kraus_map_def by blast
definition km_some_kraus_family :: ‹(('a::chilbert_space, 'a) trace_class ⇒ ('b::chilbert_space, 'b) trace_class) ⇒ ('a, 'b, unit) kraus_family› where
‹km_some_kraus_family 𝔈 = (if kraus_map 𝔈 then SOME 𝔉. 𝔈 = kf_apply 𝔉 else 0)›
lemma kf_apply_km_some_kraus_family[simp]:
assumes ‹kraus_map 𝔈›
shows ‹kf_apply (km_some_kraus_family 𝔈) = 𝔈›
unfolding km_some_kraus_family_def
apply (rule someI2_ex)
using assms kraus_map_def by auto
lemma km_some_kraus_family_invalid:
assumes ‹¬ kraus_map 𝔈›
shows ‹km_some_kraus_family 𝔈 = 0›
by (simp add: assms km_some_kraus_family_def)
definition km_operators_in :: ‹(('a::chilbert_space,'a) trace_class ⇒ ('b::chilbert_space,'b) trace_class) ⇒ ('a ⇒⇩C⇩L 'b) set ⇒ bool› where
‹km_operators_in 𝔈 S ⟷ (∃𝔉 :: ('a,'b,unit) kraus_family. kf_apply 𝔉 = 𝔈 ∧ kf_operators 𝔉 ⊆ S)›
lemma km_operators_in_mono: ‹S ⊆ T ⟹ km_operators_in 𝔈 S ⟹ km_operators_in 𝔈 T›
by (metis basic_trans_rules(23) km_operators_in_def)
lemma km_operators_in_kf_apply:
assumes ‹span (kf_operators 𝔈) ⊆ S›
shows ‹km_operators_in (kf_apply 𝔈) S›
proof (unfold km_operators_in_def, intro conjI exI[where x=‹kf_flatten 𝔈›])
show ‹(*⇩k⇩r) (kf_flatten 𝔈) = (*⇩k⇩r) 𝔈›
by simp
from assms show ‹kf_operators (kf_flatten 𝔈) ⊆ S›
using kf_operators_kf_map by fastforce
qed
lemma km_operators_in_kf_apply_flattened:
fixes 𝔈 :: ‹('a::chilbert_space,'b::chilbert_space,'x::CARD_1) kraus_family›
assumes ‹kf_operators 𝔈 ⊆ S›
shows ‹km_operators_in (kf_apply 𝔈) S›
proof (unfold km_operators_in_def, intro conjI exI[where x=‹kf_map_inj (λx.()) 𝔈›])
show ‹(*⇩k⇩r) (kf_map_inj (λ𝔉. ()) 𝔈) = (*⇩k⇩r) 𝔈›
by (auto intro!: ext kf_apply_map_inj inj_onI)
have ‹kf_operators (kf_map_inj (λ𝔉. ()) 𝔈) = kf_operators 𝔈›
by simp
with assms show ‹kf_operators (kf_map_inj (λ𝔉. ()) 𝔈) ⊆ S›
by blast
qed
lemma km_commute:
assumes ‹km_operators_in 𝔈 S›
assumes ‹km_operators_in 𝔉 T›
assumes ‹S ⊆ commutant T›
shows ‹𝔉 o 𝔈 = 𝔈 o 𝔉›
proof -
from assms obtain 𝔈' :: ‹(_,_,unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'› and 𝔈'S: ‹kf_operators 𝔈' ⊆ S›
by (metis km_operators_in_def)
from assms obtain 𝔉' :: ‹(_,_,unit) kraus_family› where 𝔉': ‹𝔉 = kf_apply 𝔉'› and 𝔉'T: ‹kf_operators 𝔉' ⊆ T›
by (metis km_operators_in_def)
have ‹kf_operators 𝔈' ⊆ S›
by (rule 𝔈'S)
also have ‹S ⊆ commutant T›
by (rule assms)
also have ‹commutant T ⊆ commutant (kf_operators 𝔉')›
apply (rule commutant_antimono)
by (rule 𝔉'T)
finally show ?thesis
unfolding 𝔈' 𝔉'
by (rule kf_apply_commute[symmetric])
qed
lemma km_operators_in_UNIV:
assumes ‹kraus_map 𝔈›
shows ‹km_operators_in 𝔈 UNIV›
by (metis assms kf_apply_km_some_kraus_family km_operators_in_def top.extremum)
lemma separating_kraus_map_bounded_clinear:
fixes S :: ‹('a::chilbert_space,'a) trace_class set›
assumes ‹separating_set (bounded_clinear :: (_ ⇒ ('b::chilbert_space,'b) trace_class) ⇒ _) S›
shows ‹separating_set (kraus_map :: (_ ⇒ ('b::chilbert_space,'b) trace_class) ⇒ _) S›
by (metis (mono_tags, lifting) assms kraus_map_bounded_clinear separating_set_def)
subsection ‹Bound and norm›
definition km_bound :: ‹(('a::chilbert_space, 'a) trace_class ⇒ ('b::chilbert_space, 'b) trace_class) ⇒ ('a, 'a) cblinfun› where
‹km_bound 𝔈 = (if ∃𝔈' :: (_, _, unit) kraus_family. 𝔈 = kf_apply 𝔈' then kf_bound (SOME 𝔈' :: (_, _, unit) kraus_family. 𝔈 = kf_apply 𝔈') else 0)›
lemma km_bound_kf_bound:
assumes ‹𝔈 = kf_apply 𝔉›
shows ‹km_bound 𝔈 = kf_bound 𝔉›
proof -
wlog ex: ‹∃𝔈' :: (_, _, unit) kraus_family. 𝔈 = kf_apply 𝔈'›
using assms kraus_map_def_raw negation by blast
define 𝔈' where ‹𝔈' = (SOME 𝔈' :: (_, _, unit) kraus_family. 𝔈 = kf_apply 𝔈')›
have ‹𝔈 = kf_apply (kf_flatten 𝔉)›
by (simp add: assms)
then have ‹𝔈 = kf_apply 𝔈'›
by (metis (mono_tags, lifting) 𝔈'_def someI_ex)
then have ‹𝔈' =⇩k⇩r 𝔉›
using assms kf_eq_weak_def by force
then have ‹kf_bound 𝔈' = kf_bound 𝔉›
using kf_bound_cong by blast
then show ?thesis
by (metis 𝔈'_def km_bound_def ex)
qed
definition km_norm :: ‹(('a::chilbert_space, 'a) trace_class ⇒ ('b::chilbert_space, 'b) trace_class) ⇒ real› where
‹km_norm 𝔈 = norm (km_bound 𝔈)›
lemma km_norm_kf_norm:
assumes ‹𝔈 = kf_apply 𝔉›
shows ‹km_norm 𝔈 = kf_norm 𝔉›
by (simp add: assms kf_norm_def km_bound_kf_bound km_norm_def)
lemma km_bound_invalid:
assumes ‹¬ kraus_map 𝔈›
shows ‹km_bound 𝔈 = 0›
by (metis assms km_bound_def kraus_map_def_raw)
lemma km_norm_invalid:
assumes ‹¬ kraus_map 𝔈›
shows ‹km_norm 𝔈 = 0›
by (simp add: assms km_bound_invalid km_norm_def)
lemma km_norm_geq0[iff]: ‹km_norm 𝔈 ≥ 0›
by (simp add: km_norm_def)
lemma kf_bound_pos[iff]: ‹km_bound 𝔈 ≥ 0›
apply (cases ‹kraus_map 𝔈›)
apply (simp add: km_bound_def)
by (simp add: km_bound_invalid)
lemma km_bounded_pos:
assumes ‹kraus_map 𝔈› and ‹ρ ≥ 0›
shows ‹norm (𝔈 ρ) ≤ km_norm 𝔈 * norm ρ›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
show ?thesis
by (simp add: 𝔈' assms(2) kf_apply_bounded_pos km_norm_kf_norm)
qed
lemma km_bounded:
assumes ‹kraus_map 𝔈›
shows ‹norm (𝔈 ρ) ≤ 4 * km_norm 𝔈 * norm ρ›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
show ?thesis
by (simp add: 𝔈' kf_apply_bounded km_norm_kf_norm)
qed
lemma km_bound_from_map:
assumes ‹kraus_map 𝔈›
shows ‹ψ ∙⇩C km_bound 𝔈 φ = trace_tc (𝔈 (tc_butterfly φ ψ))›
by (metis assms kf_bound_from_map km_bound_kf_bound kraus_map_def_raw)
lemma trace_from_km_bound:
assumes ‹kraus_map 𝔈›
shows ‹trace_tc (𝔈 ρ) = trace_tc (compose_tcr (km_bound 𝔈) ρ)›
by (metis assms km_bound_kf_bound kraus_map_def_raw trace_from_kf_bound)
lemma km_bound_selfadjoint[iff]: ‹selfadjoint (km_bound 𝔈)›
by (simp add: pos_selfadjoint)
lemma km_bound_leq_km_norm_id: ‹km_bound 𝔈 ≤ km_norm 𝔈 *⇩R id_cblinfun›
by (simp add: km_norm_def less_eq_scaled_id_norm)
lemma kf_norm_km_some_kraus_family[simp]: ‹kf_norm (km_some_kraus_family 𝔈) = km_norm 𝔈›
apply (cases ‹kraus_map 𝔈›)
by (auto intro!: km_norm_kf_norm[symmetric] simp: km_some_kraus_family_invalid km_norm_invalid)
subsection ‹Basic Kraus maps›
text ‹Zero map and constant maps. Addition and rescaling and composition of maps.›
lemma kraus_map_0[iff]: ‹kraus_map 0›
by (metis kf_apply_0 kraus_mapI)
lemma kraus_map_0'[iff]: ‹kraus_map (λ_. 0)›
using kraus_map_0 unfolding func_zero by simp
lemma km_bound_0[simp]: ‹km_bound 0 = 0›
using km_bound_kf_bound[of 0 0]
by simp
lemma km_norm_0[simp]: ‹km_norm 0 = 0›
by (simp add: km_norm_def)
lemma km_some_kraus_family_0[simp]: ‹km_some_kraus_family 0 = 0›
apply (rule kf_eq_0_iff_eq_0[THEN iffD1])
by (simp add: kf_eq_weak_def)
lemma kraus_map_id[iff]: ‹kraus_map id›
by (auto intro!: ext kraus_mapI[of _ kf_id])
lemma km_bound_id[simp]: ‹km_bound id = id_cblinfun›
using km_bound_kf_bound[of id kf_id]
by (simp add: kf_id_apply[abs_def] id_def)
lemma km_norm_id_leq1[iff]: ‹km_norm id ≤ 1›
by (simp add: km_norm_def norm_cblinfun_id_le)
lemma km_norm_id_eq1[simp]: ‹km_norm (id :: ('a :: {chilbert_space, not_singleton}, 'a) trace_class ⇒ _) = 1›
by (simp add: km_norm_def)
lemma km_operators_in_id[iff]: ‹km_operators_in id {id_cblinfun}›
apply (subst asm_rl[of ‹id = kf_apply kf_id›])
by (auto simp: km_operators_in_kf_apply_flattened)
lemma kraus_map_add[iff]:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹kraus_map (λρ. 𝔈 ρ + 𝔉 ρ)›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
from assms obtain 𝔉' :: ‹('a, 'b, unit) kraus_family› where 𝔉': ‹𝔉 = kf_apply 𝔉'›
using kraus_map_def by blast
show ?thesis
apply (rule kraus_mapI[of _ ‹𝔈' + 𝔉'›])
by (auto intro!: ext simp: 𝔈' 𝔉' kf_plus_apply')
qed
lemma kraus_map_plus'[iff]:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹kraus_map (𝔈 + 𝔉)›
using assms by (simp add: plus_fun_def)
lemma km_bound_plus:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_bound (𝔈 + 𝔉) = km_bound 𝔈 + km_bound 𝔉›
proof -
from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹('a,'b,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
apply (rule km_bound_kf_bound[where 𝔉=‹EE + FF›, THEN trans])
by (auto intro!: ext simp: EE FF kf_plus_apply' kf_plus_bound' km_bound_kf_bound)
qed
lemma km_norm_triangle:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_norm (𝔈 + 𝔉) ≤ km_norm 𝔈 + km_norm 𝔉›
by (simp add: km_norm_def km_bound_plus assms norm_triangle_ineq)
lemma kraus_map_constant[iff]: ‹kraus_map (λσ. trace_tc σ *⇩C ρ)› if ‹ρ ≥ 0›
apply (rule kraus_mapI[where 𝔈'=‹kf_constant ρ›])
by (simp add: kf_constant_apply[OF that, abs_def])
lemma kraus_map_constant_invalid:
‹¬ kraus_map (λσ :: ('a::{chilbert_space,not_singleton},'a) trace_class. trace_tc σ *⇩C ρ)› if ‹~ ρ ≥ 0›
proof (rule ccontr)
assume ‹¬ ¬ kraus_map (λσ :: ('a,'a) trace_class. trace_tc σ *⇩C ρ)›
then have km: ‹kraus_map (λσ :: ('a,'a) trace_class. trace_tc σ *⇩C ρ)›
by simp
obtain h :: 'a where ‹norm h = 1›
using ex_norm1_not_singleton by blast
from km have ‹trace_tc (tc_butterfly h h) *⇩C ρ ≥ 0›
using kraus_map_pos by fastforce
with ‹norm h = 1›
have ‹ρ ≥ 0›
by (metis mult_cancel_left2 norm_tc_butterfly norm_tc_pos of_real_1 scaleC_one tc_butterfly_pos)
with that show False
by simp
qed
lemma kraus_map_scale:
assumes ‹kraus_map 𝔈› and ‹c ≥ 0›
shows ‹kraus_map (λρ. c *⇩R 𝔈 ρ)›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
then show ?thesis
apply (rule_tac kraus_mapI[where 𝔈'=‹c *⇩R 𝔈'›])
by (auto intro!: ext simp add: 𝔈' kf_scale_apply assms)
qed
lemma km_bound_scale[simp]: ‹km_bound (λρ. c *⇩R 𝔈 ρ) = c *⇩R km_bound 𝔈› if ‹c ≥ 0›
proof -
consider (km) ‹kraus_map 𝔈› | (c0) ‹c = 0› | (not_km) ‹¬ kraus_map 𝔈› ‹c > 0›
using ‹0 ≤ c› by argo
then show ?thesis
proof cases
case km
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
with ‹c ≥ 0 ›have ‹kf_bound (c *⇩R EE) = c *⇩R kf_bound EE›
by simp
then show ?thesis
using km_bound_kf_bound[of ‹λρ. c *⇩R 𝔈 ρ› ‹c *⇩R EE›, symmetric]
using kf_scale_apply[OF ‹c ≥ 0›, of EE, abs_def]
by (simp add: EE km_bound_kf_bound)
next
case c0
then show ?thesis
by (simp flip: func_zero)
next
case not_km
have ‹¬ kraus_map (λρ. c *⇩R 𝔈 ρ)›
proof (rule ccontr)
assume ‹¬ ¬ kraus_map (λρ. c *⇩R 𝔈 ρ)›
then have ‹kraus_map (λρ. inverse c *⇩R (c *⇩R 𝔈 ρ))›
apply (rule_tac kraus_map_scale)
using not_km by auto
then have ‹kraus_map 𝔈›
using not_km by (simp add: scaleR_scaleR field.field_inverse)
with not_km show False
by simp
qed
with not_km show ?thesis
by (simp add: km_bound_invalid)
qed
qed
lemma km_norm_scale[simp]: ‹km_norm (λρ. c *⇩R 𝔈 ρ) = c * km_norm 𝔈› if ‹c ≥ 0›
using that by (simp add: km_norm_def)
lemma kraus_map_sandwich[iff]: ‹kraus_map (sandwich_tc A)›
apply (rule kraus_mapI[of _ ‹kf_of_op A›])
using kf_of_op_apply[of A, abs_def]
by simp
lemma km_bound_sandwich[simp]: ‹km_bound (sandwich_tc A) = A* o⇩C⇩L A›
using km_bound_kf_bound[of ‹sandwich_tc A› ‹kf_of_op A›, symmetric]
using kf_bound_of_op[of A]
using kf_of_op_apply[of A]
by fastforce
lemma km_norm_sandwich[simp]: ‹km_norm (sandwich_tc A) = (norm A)⇧2›
by (simp add: km_norm_def)
lemma km_operators_in_sandwich: ‹km_operators_in (sandwich_tc U) {U}›
apply (subst kf_of_op_apply[abs_def, symmetric])
apply (rule km_operators_in_kf_apply_flattened)
by simp
lemma km_constant_bound[simp]: ‹km_bound (λσ. trace_tc σ *⇩C ρ) = norm ρ *⇩R id_cblinfun› if ‹ρ ≥ 0›
apply (rule km_bound_kf_bound[THEN trans])
using that apply (rule kf_constant_apply[symmetric, THEN ext])
using that by (rule kf_bound_constant)
lemma km_constant_norm[simp]: ‹km_norm (λσ::('a::{chilbert_space,not_singleton},'a) trace_class. trace_tc σ *⇩C ρ) = norm ρ› if ‹ρ ≥ 0›
apply (subst km_norm_kf_norm[of ‹(λσ::('a,'a) trace_class. trace_tc σ *⇩C ρ)› ‹kf_constant ρ›])
apply (subst kf_constant_apply[OF that, abs_def], rule refl)
apply (rule kf_norm_constant)
by (fact that)
lemma km_constant_norm_leq[simp]: ‹km_norm (λσ::('a::chilbert_space,'a) trace_class. trace_tc σ *⇩C ρ) ≤ norm ρ›
proof -
consider (pos) ‹ρ ≥ 0› | (singleton) ‹¬ class.not_singleton TYPE('a)› | (nonpos) ‹¬ ρ ≥ 0› ‹class.not_singleton TYPE('a)›
by blast
then show ?thesis
proof cases
case pos
show ?thesis
apply (subst km_norm_kf_norm[of ‹(λσ::('a,'a) trace_class. trace_tc σ *⇩C ρ)› ‹kf_constant ρ›])
apply (subst kf_constant_apply[OF pos, abs_def], rule refl)
by (rule kf_norm_constant_leq)
next
case nonpos
have ‹¬ kraus_map (λσ::('a,'a) trace_class. trace_tc σ *⇩C ρ)›
apply (rule kraus_map_constant_invalid[internalize_sort' 'a])
apply (rule chilbert_space_axioms)
using nonpos by -
then have ‹km_norm (λσ::('a,'a) trace_class. trace_tc σ *⇩C ρ) = 0›
using km_norm_invalid by blast
then show ?thesis
by (metis norm_ge_zero)
next
case singleton
then have ‹(λσ::('a,'a) trace_class. trace_tc σ *⇩C ρ) = 0›
apply (subst not_not_singleton_tc_zero)
by auto
then show ?thesis
by simp
qed
qed
lemma kraus_map_comp:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹kraus_map (𝔈 o 𝔉)›
proof -
from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹('c,'a,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
apply (rule kraus_mapI[where 𝔈'=‹kf_comp EE FF›])
by (simp add: EE FF kf_comp_apply)
qed
lemma km_comp_norm_leq:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_norm (𝔈 o 𝔉) ≤ km_norm 𝔈 * km_norm 𝔉›
proof -
from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹('c,'a,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
have ‹km_norm (𝔈 o 𝔉) = kf_norm (kf_comp EE FF)›
by (simp add: EE FF kf_comp_apply km_norm_kf_norm)
also have ‹… ≤ kf_norm EE * kf_norm FF›
by (simp add: kf_comp_norm_leq)
also have ‹… = km_norm 𝔈 * km_norm 𝔉›
by (simp add: EE FF km_norm_kf_norm)
finally show ?thesis
by -
qed
lemma km_bound_comp_sandwich:
assumes ‹kraus_map 𝔈›
shows ‹km_bound (λρ. 𝔈 (sandwich_tc U ρ)) = sandwich (U*) (km_bound 𝔈)›
proof -
from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
have ‹km_bound (λρ. 𝔈 (sandwich_tc U ρ)) = kf_bound (kf_comp EE (kf_of_op U))›
apply (rule km_bound_kf_bound)
by (simp add: kf_comp_apply o_def EE kf_of_op_apply)
also have ‹… = sandwich (U*) *⇩V kf_bound EE›
by (simp add: kf_bound_comp_of_op)
also have ‹… = sandwich (U*) (km_bound 𝔈)›
by (simp add: EE km_bound_kf_bound)
finally show ?thesis
by -
qed
lemma km_norm_comp_sandwich_coiso:
assumes ‹isometry (U*)›
shows ‹km_norm (λρ. 𝔈 (sandwich_tc U ρ)) = km_norm 𝔈›
proof (cases ‹kraus_map 𝔈›)
case True
then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
have ‹km_norm (λρ. 𝔈 (sandwich_tc U ρ)) = kf_norm (kf_comp EE (kf_of_op U))›
apply (rule km_norm_kf_norm)
by (auto intro!: simp: kf_comp_apply o_def EE kf_of_op_apply)
also have ‹… = kf_norm EE›
by (simp add: assms kf_norm_comp_of_op_coiso)
also have ‹… = km_norm 𝔈›
by (simp add: EE km_norm_kf_norm)
finally show ?thesis
by -
next
case False
have ‹¬ kraus_map (λρ. 𝔈 (sandwich_tc U ρ))›
proof (rule ccontr)
assume ‹¬ ¬ kraus_map (λρ. 𝔈 (sandwich_tc U ρ))›
then have ‹kraus_map (λρ. 𝔈 (sandwich_tc U ρ))›
by blast
then have ‹kraus_map (λρ. 𝔈 (sandwich_tc U (sandwich_tc (U*) ρ)))›
apply (rule kraus_map_comp[unfolded o_def])
by fastforce
then have ‹kraus_map 𝔈›
using isometryD[OF assms]
by (simp flip: sandwich_tc_compose[unfolded o_def, THEN fun_cong])
then show False
using False by blast
qed
with False show ?thesis
by (simp add: km_norm_invalid)
qed
lemma km_bound_comp_sandwich_iso:
assumes ‹isometry U›
shows ‹km_bound (λρ. sandwich_tc U (𝔈 ρ)) = km_bound 𝔈›
proof (cases ‹kraus_map 𝔈›)
case True
then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
have ‹km_bound (λρ. sandwich_tc U (𝔈 ρ)) = kf_bound (kf_comp (kf_of_op U) EE)›
apply (rule km_bound_kf_bound)
by (auto intro!: simp: kf_comp_apply o_def EE kf_of_op_apply)
also have ‹… = kf_bound EE›
by (simp add: assms kf_bound_comp_iso)
also have ‹… = km_bound 𝔈›
by (simp add: EE km_bound_kf_bound)
finally show ?thesis
by -
next
case False
have ‹¬ kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
proof (rule ccontr)
assume ‹¬ ¬ kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
then have ‹kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
by blast
then have ‹kraus_map (λρ. sandwich_tc (U*) (sandwich_tc U (𝔈 ρ)))›
apply (rule kraus_map_comp[unfolded o_def, rotated])
by fastforce
then have ‹kraus_map 𝔈›
using isometryD[OF assms]
by (simp flip: sandwich_tc_compose[unfolded o_def, THEN fun_cong])
then show False
using False by blast
qed
with False show ?thesis
by (simp add: km_bound_invalid)
qed
lemma km_norm_comp_sandwich_iso:
assumes ‹isometry U›
shows ‹km_norm (λρ. sandwich_tc U (𝔈 ρ)) = km_norm 𝔈›
proof (cases ‹kraus_map 𝔈›)
case True
then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
have ‹km_norm (λρ. sandwich_tc U (𝔈 ρ)) = kf_norm (kf_comp (kf_of_op U) EE)›
apply (rule km_norm_kf_norm)
by (auto intro!: simp: kf_comp_apply o_def EE kf_of_op_apply)
also have ‹… = kf_norm EE›
by (simp add: assms kf_norm_comp_iso)
also have ‹… = km_norm 𝔈›
by (simp add: EE km_norm_kf_norm)
finally show ?thesis
by -
next
case False
have ‹¬ kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
proof (rule ccontr)
assume ‹¬ ¬ kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
then have ‹kraus_map (λρ. sandwich_tc U (𝔈 ρ))›
by blast
then have ‹kraus_map (λρ. sandwich_tc (U*) (sandwich_tc U (𝔈 ρ)))›
apply (rule kraus_map_comp[unfolded o_def, rotated])
by fastforce
then have ‹kraus_map 𝔈›
using isometryD[OF assms]
by (simp flip: sandwich_tc_compose[unfolded o_def, THEN fun_cong])
then show False
using False by blast
qed
with False show ?thesis
by (simp add: km_norm_invalid)
qed
lemma kraus_map_sum:
assumes ‹⋀x. x∈A ⟹ kraus_map (𝔈 x)›
shows ‹kraus_map (∑x∈A. 𝔈 x)›
apply (insert assms, induction A rule:infinite_finite_induct)
by auto
lemma km_bound_sum:
assumes ‹⋀x. x∈A ⟹ kraus_map (𝔈 x)›
shows ‹km_bound (∑x∈A. 𝔈 x) = (∑x∈A. km_bound (𝔈 x))›
proof (insert assms, induction A rule:infinite_finite_induct)
case (infinite A)
then show ?case
by (metis km_bound_0 sum.infinite)
next
case empty
then show ?case
by (metis km_bound_0 sum.empty)
next
case (insert x F)
have ‹km_bound (∑x∈insert x F. 𝔈 x) = km_bound (𝔈 x + (∑x∈F. 𝔈 x))›
by (simp add: insert.hyps)
also have ‹… = km_bound (𝔈 x) + km_bound (∑x∈F. 𝔈 x)›
by (simp add: km_bound_plus kraus_map_sum insert.prems)
also have ‹… = km_bound (𝔈 x) + (∑x∈F. km_bound (𝔈 x))›
by (simp add: insert)
also have ‹… = (∑x∈insert x F. km_bound (𝔈 x))›
using insert.hyps by fastforce
finally show ?case
by -
qed
subsection ‹Infinite sums›
lemma
assumes ‹⋀ρ. ((λa. sandwich_tc (f a) ρ) has_sum 𝔈 ρ) A›
defines ‹EE ≡ Set.filter (λ(E,_). E≠0) ((λa. (f a, a)) ` A)›
shows kraus_mapI_sum: ‹kraus_map 𝔈›
and kraus_map_sum_kraus_family: ‹kraus_family EE›
and kraus_map_sum_kf_apply: ‹𝔈 = kf_apply (Abs_kraus_family EE)›
proof -
show ‹kraus_family EE›
unfolding EE_def
apply (rule kf_reconstruction_is_kraus_family)
by (fact assms(1))
show ‹𝔈 = kf_apply (Abs_kraus_family EE)›
unfolding EE_def
apply (rule kf_reconstruction[symmetric])
by (fact assms(1))
then show ‹kraus_map 𝔈›
by (rule kraus_mapI)
qed
lemma kraus_map_infsum_sandwich:
assumes ‹⋀ρ. (λa. sandwich_tc (f a) ρ) summable_on A›
shows ‹kraus_map (λρ. ∑⇩∞a∈A. sandwich_tc (f a) ρ)›
apply (rule kraus_mapI_sum)
using assms by (rule has_sum_infsum)
lemma kraus_map_sum_sandwich: ‹kraus_map (λρ. ∑a∈A. sandwich_tc (f a) ρ)›
apply (cases ‹finite A›)
apply (simp add: kraus_map_infsum_sandwich flip: infsum_finite)
by simp
lemma kraus_map_as_infsum:
assumes ‹kraus_map 𝔈›
shows ‹∃M. ∀ρ. ((λE. sandwich_tc E ρ) has_sum 𝔈 ρ) M›
proof -
from assms obtain 𝔈' :: ‹('a, 'b, unit) kraus_family› where 𝔈': ‹𝔈 = kf_apply 𝔈'›
using kraus_map_def by blast
define M where ‹M = fst ` Rep_kraus_family 𝔈'›
have ‹((λE. sandwich_tc E ρ) has_sum 𝔈 ρ) M› for ρ
proof -
have [simp]: ‹inj_on fst (Rep_kraus_family 𝔈')›
by (auto intro!: inj_onI)
from kf_apply_has_sum[of ρ 𝔈']
have ‹((λ(E, x). sandwich_tc E ρ) has_sum kf_apply 𝔈' ρ) (Rep_kraus_family 𝔈')›
by -
then show ?thesis
by (simp add: M_def has_sum_reindex o_def case_prod_unfold 𝔈')
qed
then show ?thesis
by auto
qed
definition km_summable :: ‹('a ⇒ ('b::chilbert_space,'b) trace_class ⇒ ('c::chilbert_space,'c) trace_class) ⇒ 'a set ⇒ bool› where
‹km_summable 𝔈 A ⟷ summable_on_in cweak_operator_topology (λa. km_bound (𝔈 a)) A›
lemma km_summable_kf_summable:
assumes ‹⋀a ρ. a ∈ A ⟹ 𝔈 a ρ = 𝔉 a *⇩k⇩r ρ›
shows ‹km_summable 𝔈 A ⟷ kf_summable 𝔉 A›
proof -
have ‹km_summable 𝔈 A ⟷ summable_on_in cweak_operator_topology (λa. km_bound (𝔈 a)) A›
using km_summable_def by blast
also have ‹… ⟷ summable_on_in cweak_operator_topology (λa. kf_bound (𝔉 a)) A›
apply (rule summable_on_in_cong)
apply (rule km_bound_kf_bound)
using assms by fastforce
also have ‹… ⟷ kf_summable 𝔉 A›
using kf_summable_def by blast
finally show ?thesis
by -
qed
lemma km_summable_summable:
assumes km: ‹⋀a. a∈A ⟹ kraus_map (𝔈 a)›
assumes sum: ‹km_summable 𝔈 A›
shows ‹(λa. 𝔈 a ρ) summable_on A›
proof -
from km
obtain EE :: ‹_ ⇒ (_,_,unit) kraus_family› where EE: ‹𝔈 a = kf_apply (EE a)› if ‹a ∈ A› for a
apply atomize_elim
apply (rule_tac choice)
by (simp add: kraus_map_def_raw)
from sum
have ‹kf_summable EE A›
by (simp add: EE km_summable_kf_summable)
then have ‹(λa. EE a *⇩k⇩r ρ) summable_on A›
by (rule kf_infsum_apply_summable)
then show ?thesis
by (metis (mono_tags, lifting) EE summable_on_cong)
qed
lemma kraus_map_infsum:
assumes km: ‹⋀a. a∈A ⟹ kraus_map (𝔈 a)›
assumes sum: ‹km_summable 𝔈 A›
shows ‹kraus_map (λρ. ∑⇩∞a∈A. 𝔈 a ρ)›
proof -
from km
obtain EE :: ‹_ ⇒ (_,_,unit) kraus_family› where EE: ‹𝔈 a = kf_apply (EE a)› if ‹a ∈ A› for a
apply atomize_elim
apply (rule_tac choice)
by (simp add: kraus_map_def_raw)
from sum
have ‹kf_summable EE A›
by (simp add: EE km_summable_kf_summable)
then have ‹kf_infsum EE A *⇩k⇩r ρ = (∑⇩∞a∈A. EE a *⇩k⇩r ρ)› for ρ
by (metis kf_infsum_apply)
also have ‹… ρ = (∑⇩∞a∈A. 𝔈 a ρ)› for ρ
by (metis (mono_tags, lifting) EE infsum_cong)
finally show ?thesis
apply (rule_tac kraus_mapI[of _ ‹kf_infsum EE A›])
by auto
qed
lemma km_bound_infsum:
assumes km: ‹⋀a. a∈A ⟹ kraus_map (𝔈 a)›
assumes sum: ‹km_summable 𝔈 A›
shows ‹km_bound (λρ. ∑⇩∞a∈A. 𝔈 a ρ) = infsum_in cweak_operator_topology (λa. km_bound (𝔈 a)) A›
proof -
from km
obtain EE :: ‹_ ⇒ (_,_,unit) kraus_family› where EE: ‹𝔈 a = kf_apply (EE a)› if ‹a ∈ A› for a
apply atomize_elim
apply (rule_tac choice)
by (simp add: kraus_map_def_raw)
from sum have ‹kf_summable EE A›
by (simp add: EE km_summable_kf_summable)
have ‹km_bound (λρ. ∑⇩∞a∈A. 𝔈 a ρ) = km_bound (λρ. ∑⇩∞a∈A. EE a *⇩k⇩r ρ)›
apply (rule arg_cong[where f=km_bound])
by (auto intro!: infsum_cong simp add: EE)
also have ‹… = kf_bound (kf_infsum EE A)›
apply (rule km_bound_kf_bound)
using kf_infsum_apply[OF ‹kf_summable EE A›]
by auto
also have ‹… = infsum_in cweak_operator_topology (λa. kf_bound (EE a)) A›
using ‹kf_summable EE A› kf_bound_infsum by fastforce
also have ‹… = infsum_in cweak_operator_topology (λa. km_bound (𝔈 a)) A›
by (metis (mono_tags, lifting) EE infsum_in_cong km_bound_kf_bound)
finally show ?thesis
by -
qed
lemma km_norm_infsum:
assumes km: ‹⋀a. a∈A ⟹ kraus_map (𝔈 a)›
assumes sum: ‹(λa. km_norm (𝔈 a)) summable_on A›
shows ‹km_norm (λρ. ∑⇩∞a∈A. 𝔈 a ρ) ≤ (∑⇩∞a∈A. km_norm (𝔈 a))›
proof -
from km
obtain EE :: ‹_ ⇒ (_,_,unit) kraus_family› where EE: ‹𝔈 a = kf_apply (EE a)› if ‹a ∈ A› for a
apply atomize_elim
apply (rule_tac choice)
by (simp add: kraus_map_def_raw)
from sum have sum1: ‹(λa. kf_norm (EE a)) summable_on A›
by (metis (mono_tags, lifting) EE km_norm_kf_norm summable_on_cong)
then have sum2: ‹kf_summable EE A›
using kf_summable_from_abs_summable by blast
have ‹km_norm (λρ. ∑⇩∞a∈A. 𝔈 a ρ) = km_norm (λρ. ∑⇩∞a∈A. EE a *⇩k⇩r ρ)›
apply (rule arg_cong[where f=km_norm])
apply (rule ext)
apply (rule infsum_cong)
by (simp add: EE)
also have ‹… = kf_norm (kf_infsum EE A)›
apply (subst kf_infsum_apply[OF sum2, abs_def, symmetric])
using km_norm_kf_norm by blast
also have ‹… ≤ (∑⇩∞a∈A. kf_norm (EE a))›
by (metis kf_norm_infsum sum1)
also have ‹… = (∑⇩∞a∈A. km_norm (𝔈 a))›
by (metis (mono_tags, lifting) EE infsum_cong km_norm_kf_norm)
finally show ?thesis
by -
qed
lemma kraus_map_has_sum:
assumes ‹⋀x. x ∈ A ⟹ kraus_map (𝔈 x)›
assumes ‹km_summable 𝔈 A›
assumes ‹(𝔈 has_sum 𝔉) A›
shows ‹kraus_map 𝔉›
proof -
from ‹(𝔈 has_sum 𝔉) A›
have ‹((λx. 𝔈 x t) has_sum 𝔉 t) A› for t
by (simp add: has_sum_coordinatewise)
then have ‹𝔉 t = (∑⇩∞a∈A. 𝔈 a t)› for t
by (metis infsumI)
with kraus_map_infsum[OF assms(1,2)]
show ‹kraus_map 𝔉›
by presburger
qed
lemma km_summable_iff_sums_to_kraus_map:
assumes ‹⋀a. a∈A ⟹ kraus_map (𝔈 a)›
shows ‹km_summable 𝔈 A ⟷ (∃𝔉. (∀t. ((λx. 𝔈 x t) has_sum 𝔉 t) A) ∧ kraus_map 𝔉)›
proof (rule iffI)
assume asm: ‹km_summable 𝔈 A›
define 𝔉 where ‹𝔉 t = (∑⇩∞a∈A. 𝔈 a t)› for t
from km_summable_summable[OF assms asm]
have ‹((λx. 𝔈 x t) has_sum 𝔉 t) A› for t
using 𝔉_def by fastforce
moreover from kraus_map_infsum[OF assms asm]
have ‹kraus_map 𝔉›
by (simp add: 𝔉_def[abs_def])
ultimately show ‹(∃𝔉. (∀t. ((λx. 𝔈 x t) has_sum 𝔉 t) A) ∧ kraus_map 𝔉)›
by auto
next
assume ‹∃𝔉. (∀t. ((λx. 𝔈 x t) has_sum 𝔉 t) A) ∧ kraus_map 𝔉›
then obtain 𝔉 where ‹kraus_map 𝔉› and ‹((λx. 𝔈 x t) has_sum 𝔉 t) A› for t
by auto
then have ‹((λx. trace_tc (𝔈 x (tc_butterfly k h))) has_sum trace_tc (𝔉 (tc_butterfly k h))) A› for h k
using bounded_clinear.bounded_linear bounded_clinear_trace_tc has_sum_bounded_linear by blast
then have ‹((λx. trace_tc (𝔈 x (tc_butterfly k h))) has_sum h ∙⇩C (km_bound 𝔉 *⇩V k)) A› for h k
by (simp add: km_bound_from_map ‹kraus_map 𝔉›)
then have ‹((λx. h ∙⇩C (km_bound (𝔈 x) *⇩V k)) has_sum h ∙⇩C (km_bound 𝔉 *⇩V k)) A› for h k
apply (rule has_sum_cong[THEN iffD1, rotated 1])
by (simp add: km_bound_from_map assms)
then have ‹has_sum_in cweak_operator_topology (λa. km_bound (𝔈 a)) A (km_bound 𝔉)›
by (simp add: has_sum_in_cweak_operator_topology_pointwise)
then show ‹km_summable 𝔈 A›
using summable_on_in_def km_summable_def by blast
qed
subsection ‹Tensor products›
definition km_tensor_exists :: ‹(('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class)
⇒ (('e ell2, 'f ell2) trace_class ⇒ ('g ell2, 'h ell2) trace_class) ⇒ bool› where
‹km_tensor_exists 𝔈 𝔉 ⟷ (∃𝔈𝔉. bounded_clinear 𝔈𝔉 ∧ (∀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ)))›
definition km_tensor :: ‹(('a ell2, 'c ell2) trace_class ⇒ ('e ell2, 'g ell2) trace_class)
⇒ (('b ell2, 'd ell2) trace_class ⇒ ('f ell2, 'h ell2) trace_class)
⇒ (('a × 'b) ell2, ('c × 'd) ell2) trace_class ⇒ (('e × 'f) ell2, ('g × 'h) ell2) trace_class› where
‹km_tensor 𝔈 𝔉 = (if km_tensor_exists 𝔈 𝔉
then SOME 𝔈𝔉. bounded_clinear 𝔈𝔉 ∧ (∀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ))
else 0)›
lemma km_tensor_invalid:
assumes ‹¬ km_tensor_exists 𝔈 𝔉›
shows ‹km_tensor 𝔈 𝔉 = 0›
by (simp add: assms km_tensor_def)
lemma km_tensor_exists_bounded_clinear[iff]:
assumes ‹km_tensor_exists 𝔈 𝔉›
shows ‹bounded_clinear (km_tensor 𝔈 𝔉)›
unfolding km_tensor_def
apply (rule someI2_ex[where P=‹λ𝔈𝔉. bounded_clinear 𝔈𝔉 ∧ (∀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ))›])
using assms
by (simp_all add: km_tensor_exists_def)
lemma km_tensor_apply[simp]:
assumes ‹km_tensor_exists 𝔈 𝔉›
shows ‹km_tensor 𝔈 𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ)›
unfolding km_tensor_def
apply (rule someI2_ex[where P=‹λ𝔈𝔉. bounded_clinear 𝔈𝔉 ∧ (∀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ))›])
using assms
by (simp_all add: km_tensor_exists_def)
lemma km_tensor_unique:
assumes ‹bounded_clinear 𝔈𝔉›
assumes ‹⋀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ)›
shows ‹𝔈𝔉 = km_tensor 𝔈 𝔉›
proof -
define P where ‹P 𝔈𝔉 ⟷ bounded_clinear 𝔈𝔉 ∧ (∀ρ σ. 𝔈𝔉 (tc_tensor ρ σ) = tc_tensor (𝔈 ρ) (𝔉 σ))› for 𝔈𝔉
have ‹P 𝔈𝔉›
using P_def assms by presburger
then have ‹km_tensor_exists 𝔈 𝔉›
using P_def km_tensor_exists_def by blast
with ‹P 𝔈𝔉› have Ptensor: ‹P (km_tensor 𝔈 𝔉)›
by (simp add: P_def)
show ?thesis
apply (rule eq_from_separatingI2)
apply (rule separating_set_bounded_clinear_tc_tensor)
using assms Ptensor by (simp_all add: P_def)
qed
lemma km_tensor_kf_tensor: ‹km_tensor (kf_apply 𝔈) (kf_apply 𝔉) = kf_apply (kf_tensor 𝔈 𝔉)›
by (metis kf_apply_bounded_clinear kf_apply_tensor km_tensor_unique)
lemma km_tensor_kraus_map:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹kraus_map (km_tensor 𝔈 𝔉)›
proof -
from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
by (simp add: EE FF km_tensor_kf_tensor)
qed
lemma km_tensor_kraus_map_exists:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_tensor_exists 𝔈 𝔉›
proof -
from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
using EE FF kf_apply_bounded_clinear kf_apply_tensor km_tensor_exists_def by blast
qed
lemma km_tensor_as_infsum:
assumes ‹⋀ρ. ((λi. sandwich_tc (E i) ρ) has_sum 𝔈 ρ) I›
assumes ‹⋀ρ. ((λj. sandwich_tc (F j) ρ) has_sum 𝔉 ρ) J›
shows ‹km_tensor 𝔈 𝔉 ρ = (∑⇩∞(i,j)∈I×J. sandwich_tc (E i ⊗⇩o F j) ρ)›
proof -
define EE FF where ‹EE = Set.filter (λ(E,_). E≠0) ((λa. (E a, a)) ` I)› and ‹FF = Set.filter (λ(E,_). E≠0) ((λa. (F a, a)) ` J)›
then have [simp]: ‹kraus_family EE› ‹kraus_family FF›
using assms kraus_map_sum_kraus_family
by blast+
have ‹𝔈 = kf_apply (Abs_kraus_family EE)› and ‹𝔉 = kf_apply (Abs_kraus_family FF)›
using assms kraus_map_sum_kf_apply EE_def FF_def
by blast+
then have ‹km_tensor 𝔈 𝔉 ρ = kf_apply (kf_tensor (Abs_kraus_family EE) (Abs_kraus_family FF)) ρ›
by (simp add: km_tensor_kf_tensor)
also have ‹… = (∑⇩∞((E, x), (F, y))∈EE × FF. sandwich_tc (E ⊗⇩o F) ρ)›
by (simp add: kf_apply_tensor_as_infsum Abs_kraus_family_inverse)
also have ‹… = (∑⇩∞((E, x), (F, y))∈(λ(i,j). ((E i, i), (F j, j)))`(I×J). sandwich_tc (E ⊗⇩o F) ρ)›
apply (rule infsum_cong_neutral)
by (auto simp: EE_def FF_def)
also have ‹… = (∑⇩∞(i,j)∈I×J. sandwich_tc (E i ⊗⇩o F j) ρ)›
by (simp add: infsum_reindex inj_on_def o_def case_prod_unfold)
finally show ?thesis
by -
qed
lemma km_bound_tensor:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_bound (km_tensor 𝔈 𝔉) = km_bound 𝔈 ⊗⇩o km_bound 𝔉›
proof -
from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
by (simp add: EE FF km_tensor_kf_tensor kf_bound_tensor km_bound_kf_bound)
qed
lemma km_norm_tensor:
assumes ‹kraus_map 𝔈› and ‹kraus_map 𝔉›
shows ‹km_norm (km_tensor 𝔈 𝔉) = km_norm 𝔈 * km_norm 𝔉›
proof -
from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹𝔉 = kf_apply FF›
using kraus_map_def_raw by blast
show ?thesis
by (simp add: EE FF km_tensor_kf_tensor kf_norm_tensor km_norm_kf_norm)
qed
lemma km_tensor_compose_distrib:
assumes ‹km_tensor_exists 𝔈 𝔊› and ‹km_tensor_exists 𝔉 ℌ›
shows ‹km_tensor (𝔈 o 𝔉) (𝔊 o ℌ) = km_tensor 𝔈 𝔊 o km_tensor 𝔉 ℌ›
by (smt (verit, del_insts) assms(1,2) comp_bounded_clinear km_tensor_exists_def km_tensor_unique o_apply)
lemma kraus_map_tensor_right[simp]:
assumes ‹ρ ≥ 0›
shows ‹kraus_map (λσ. tc_tensor σ ρ)›
apply (rule kraus_mapI[of _ ‹kf_tensor_right ρ›])
by (auto intro!: ext simp: kf_apply_tensor_right assms)
lemma kraus_map_tensor_left[simp]:
assumes ‹ρ ≥ 0›
shows ‹kraus_map (λσ. tc_tensor ρ σ)›
apply (rule kraus_mapI[of _ ‹kf_tensor_left ρ›])
by (auto intro!: ext simp: kf_apply_tensor_left assms)
lemma km_bound_tensor_right[simp]:
assumes ‹ρ ≥ 0›
shows ‹km_bound (λσ. tc_tensor σ ρ) = norm ρ *⇩C id_cblinfun›
apply (subst km_bound_kf_bound)
apply (rule ext)
apply (subst kf_apply_tensor_right[OF assms])
by (auto intro!: simp: kf_bound_tensor_right assms)
lemma km_bound_tensor_left[simp]:
assumes ‹ρ ≥ 0›
shows ‹km_bound (λσ. tc_tensor ρ σ) = norm ρ *⇩C id_cblinfun›
apply (subst km_bound_kf_bound)
apply (rule ext)
apply (subst kf_apply_tensor_left[OF assms])
by (auto intro!: simp: kf_bound_tensor_left assms)
lemma kf_norm_tensor_right[simp]:
assumes ‹ρ ≥ 0›
shows ‹km_norm (λσ. tc_tensor σ ρ) = norm ρ›
by (simp add: km_norm_def km_bound_tensor_right assms)
lemma kf_norm_tensor_left[simp]:
assumes ‹ρ ≥ 0›
shows ‹km_norm (λσ. tc_tensor ρ σ) = norm ρ›
by (simp add: km_norm_def km_bound_tensor_left assms)
lemma km_operators_in_tensor:
assumes ‹km_operators_in 𝔈 S›
assumes ‹km_operators_in 𝔉 T›
shows ‹km_operators_in (km_tensor 𝔈 𝔉) (span {s ⊗⇩o t | s t. s∈S ∧ t∈T})›
proof -
have [iff]: ‹inj_on (λ((),()). ()) X› for X
by (simp add: inj_on_def)
from assms obtain 𝔈' :: ‹(_,_,unit) kraus_family› where 𝔈_def: ‹𝔈 = kf_apply 𝔈'› and 𝔈'S: ‹kf_operators 𝔈' ⊆ S›
by (metis km_operators_in_def)
from assms obtain 𝔉' :: ‹(_,_,unit) kraus_family› where 𝔉_def: ‹𝔉 = kf_apply 𝔉'› and 𝔉'T: ‹kf_operators 𝔉' ⊆ T›
by (metis km_operators_in_def)
define 𝔈𝔉 where ‹𝔈𝔉 = kf_map_inj (λ((),()). ()) (kf_tensor 𝔈' 𝔉')›
then have ‹kf_operators 𝔈𝔉 = kf_operators (kf_tensor 𝔈' 𝔉')›
by (simp add: 𝔈𝔉_def)
also have ‹kf_operators (kf_tensor 𝔈' 𝔉') ⊆ span {E ⊗⇩o F | E F. E ∈ kf_operators 𝔈' ∧ F ∈ kf_operators 𝔉'}›
using kf_operators_tensor by force
also have ‹… ⊆ span {E ⊗⇩o F | E F. E ∈ S ∧ F ∈ T}›
by (smt (verit) Collect_mono_iff 𝔈'S 𝔉'T span_mono subset_iff)
finally have ‹kf_operators 𝔈𝔉 ⊆ span {s ⊗⇩o t |s t. s ∈ S ∧ t ∈ T}›
using 𝔈𝔉_def by blast
moreover have ‹kf_apply 𝔈𝔉 = km_tensor 𝔈 𝔉›
by (simp add: 𝔈𝔉_def 𝔈_def 𝔉_def kf_apply_bounded_clinear kf_apply_tensor km_tensor_unique)
ultimately show ?thesis
by (auto intro!: exI[of _ 𝔈𝔉] simp add: km_operators_in_def)
qed
lemma km_tensor_sandwich_tc:
‹km_tensor (sandwich_tc A) (sandwich_tc B) = sandwich_tc (A ⊗⇩o B)›
by (metis bounded_clinear_sandwich_tc km_tensor_unique sandwich_tc_tensor)
subsection ‹Trace and partial trace›
definition ‹km_trace_preserving 𝔈 ⟷ (∃𝔉::(_,_,unit) kraus_family. 𝔈 = kf_apply 𝔉 ∧ kf_trace_preserving 𝔉)›
lemma km_trace_preserving_def': ‹km_trace_preserving 𝔈 ⟷ (∃𝔉::(_, _, 'c) kraus_family. 𝔈 = kf_apply 𝔉 ∧ kf_trace_preserving 𝔉)›
proof (rule iffI)
assume ‹km_trace_preserving 𝔈›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_preserving 𝔉›
using km_trace_preserving_def by blast
from 𝔈𝔉 have ‹𝔈 = kf_apply (kf_map (λ_. undefined :: 'c) 𝔉)›
by simp
moreover from tp𝔉 have ‹kf_trace_preserving (kf_map (λ_. undefined :: 'c) 𝔉)›
by (metis 𝔈𝔉 calculation kf_trace_preserving_iff_bound_id km_bound_kf_bound)
ultimately show ‹∃𝔉::(_, _, 'c) kraus_family. 𝔈 = (*⇩k⇩r) 𝔉 ∧ kf_trace_preserving 𝔉›
by blast
next
assume ‹∃𝔉::(_, _, 'c) kraus_family. 𝔈 = (*⇩k⇩r) 𝔉 ∧ kf_trace_preserving 𝔉›
then obtain 𝔉 :: ‹(_,_,'c) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_preserving 𝔉›
by blast
from 𝔈𝔉 have ‹𝔈 = kf_apply (kf_flatten 𝔉)›
by simp
moreover from tp𝔉 have ‹kf_trace_preserving (kf_flatten 𝔉)›
by (metis 𝔈𝔉 calculation kf_trace_preserving_iff_bound_id km_bound_kf_bound)
ultimately show ‹km_trace_preserving 𝔈›
using km_trace_preserving_def by blast
qed
definition km_trace_reducing_def: ‹km_trace_reducing 𝔈 ⟷ (∃𝔉::(_,_,unit) kraus_family. 𝔈 = kf_apply 𝔉 ∧ kf_trace_reducing 𝔉)›
lemma km_trace_reducing_def': ‹km_trace_reducing 𝔈 ⟷ (∃𝔉::(_, _, 'c) kraus_family. 𝔈 = kf_apply 𝔉 ∧ kf_trace_reducing 𝔉)›
proof (rule iffI)
assume ‹km_trace_reducing 𝔈›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_reducing 𝔉›
using km_trace_reducing_def by blast
from 𝔈𝔉 have ‹𝔈 = kf_apply (kf_map (λ_. undefined :: 'c) 𝔉)›
by simp
moreover from tp𝔉 have ‹kf_trace_reducing (kf_map (λ_. undefined :: 'c) 𝔉)›
by (simp add: kf_trace_reducing_iff_norm_leq1)
ultimately show ‹∃𝔉::(_, _, 'c) kraus_family. 𝔈 = (*⇩k⇩r) 𝔉 ∧ kf_trace_reducing 𝔉›
by blast
next
assume ‹∃𝔉::(_, _, 'c) kraus_family. 𝔈 = (*⇩k⇩r) 𝔉 ∧ kf_trace_reducing 𝔉›
then obtain 𝔉 :: ‹(_,_,'c) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_reducing 𝔉›
by blast
from 𝔈𝔉 have ‹𝔈 = kf_apply (kf_flatten 𝔉)›
by simp
moreover from tp𝔉 have ‹kf_trace_reducing (kf_flatten 𝔉)›
by (simp add: kf_trace_reducing_iff_norm_leq1)
ultimately show ‹km_trace_reducing 𝔈›
using km_trace_reducing_def by blast
qed
lemma km_trace_preserving_apply[simp]: ‹km_trace_preserving (kf_apply 𝔈) = kf_trace_preserving 𝔈›
using kf_trace_preserving_def km_trace_preserving_def' by auto
lemma km_trace_reducing_apply[simp]: ‹km_trace_reducing (kf_apply 𝔈) = kf_trace_reducing 𝔈›
by (metis kf_trace_reducing_iff_norm_leq1 km_norm_kf_norm km_trace_reducing_def')
lemma km_trace_preserving_iff: ‹km_trace_preserving 𝔈 ⟷ kraus_map 𝔈 ∧ (∀ρ. trace_tc (𝔈 ρ) = trace_tc ρ)›
proof (intro iffI conjI allI)
assume tp: ‹km_trace_preserving 𝔈›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_preserving 𝔉›
by (metis kf_trace_preserving_def kf_trace_reducing_def km_trace_preserving_def order.refl)
then show ‹kraus_map 𝔈›
by blast
from tp𝔉 show ‹trace_tc (𝔈 ρ) = trace_tc ρ› for ρ
by (simp add: 𝔈𝔉 kf_trace_preserving_def)
next
assume asm: ‹kraus_map 𝔈 ∧ (∀ρ. trace_tc (𝔈 ρ) = trace_tc ρ)›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉›
using kraus_map_def_raw by blast
from asm 𝔈𝔉 have ‹trace_tc (kf_apply 𝔉 ρ) = trace_tc ρ› for ρ
by blast
then have ‹kf_trace_preserving 𝔉›
using kf_trace_preserving_def by blast
with 𝔈𝔉 show ‹km_trace_preserving 𝔈›
using km_trace_preserving_def by blast
qed
lemma km_trace_reducing_iff: ‹km_trace_reducing 𝔈 ⟷ kraus_map 𝔈 ∧ (∀ρ≥0. trace_tc (𝔈 ρ) ≤ trace_tc ρ)›
proof (intro iffI conjI allI impI)
assume tp: ‹km_trace_reducing 𝔈›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉› and tp𝔉: ‹kf_trace_reducing 𝔉›
by (metis kf_trace_reducing_def kf_trace_reducing_def km_trace_reducing_def order.refl)
then show ‹kraus_map 𝔈›
by blast
from tp𝔉 𝔈𝔉 show ‹trace_tc (𝔈 ρ) ≤ trace_tc ρ› if ‹ρ ≥ 0› for ρ
using kf_trace_reducing_def that by blast
next
assume asm: ‹kraus_map 𝔈 ∧ (∀ρ≥0. trace_tc (𝔈 ρ) ≤ trace_tc ρ)›
then obtain 𝔉 :: ‹(_,_,unit) kraus_family› where 𝔈𝔉: ‹𝔈 = kf_apply 𝔉›
using kraus_map_def_raw by blast
from asm 𝔈𝔉 have ‹trace_tc (kf_apply 𝔉 ρ) ≤ trace_tc ρ› if ‹ρ ≥ 0› for ρ
using that by blast
then have ‹kf_trace_reducing 𝔉›
using kf_trace_reducing_def by blast
with 𝔈𝔉 show ‹km_trace_reducing 𝔈›
using km_trace_reducing_def by blast
qed
lemma km_trace_preserving_imp_reducing:
assumes ‹km_trace_preserving 𝔈›
shows ‹km_trace_reducing 𝔈›
using assms km_trace_preserving_iff km_trace_reducing_iff by fastforce
lemma km_trace_preserving_id[iff]: ‹km_trace_preserving id›
by (simp add: km_trace_preserving_iff)
lemma km_trace_reducing_iff_norm_leq1: ‹km_trace_reducing 𝔈 ⟷ kraus_map 𝔈 ∧ km_norm 𝔈 ≤ 1›
proof (intro iffI conjI)
assume ‹km_trace_reducing 𝔈›
then show ‹kraus_map 𝔈›
using km_trace_reducing_iff by blast
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
with ‹km_trace_reducing 𝔈›
have ‹kf_trace_reducing EE›
using kf_trace_reducing_def km_trace_reducing_iff by blast
then have ‹kf_norm EE ≤ 1›
using kf_trace_reducing_iff_norm_leq1 by blast
then show ‹km_norm 𝔈 ≤ 1›
by (simp add: EE km_norm_kf_norm)
next
assume asm: ‹kraus_map 𝔈 ∧ km_norm 𝔈 ≤ 1›
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from asm have ‹km_norm 𝔈 ≤ 1›
by blast
then have ‹kf_norm EE ≤ 1›
by (simp add: EE km_norm_kf_norm)
then have ‹kf_trace_reducing EE›
by (simp add: kf_trace_reducing_iff_norm_leq1)
then show ‹km_trace_reducing 𝔈›
using EE km_trace_reducing_def by blast
qed
lemma km_trace_preserving_iff_bound_id: ‹km_trace_preserving 𝔈 ⟷ kraus_map 𝔈 ∧ km_bound 𝔈 = id_cblinfun›
proof (intro iffI conjI)
assume ‹km_trace_preserving 𝔈›
then show ‹kraus_map 𝔈›
using km_trace_preserving_iff by blast
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
with ‹km_trace_preserving 𝔈›
have ‹kf_trace_preserving EE›
using kf_trace_preserving_def km_trace_preserving_iff by blast
then have ‹kf_bound EE = id_cblinfun›
by (simp add: kf_trace_preserving_iff_bound_id)
then show ‹km_bound 𝔈 = id_cblinfun›
by (simp add: EE km_bound_kf_bound)
next
assume asm: ‹kraus_map 𝔈 ∧ km_bound 𝔈 = id_cblinfun›
then have ‹kraus_map 𝔈›
by simp
then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹𝔈 = kf_apply EE›
using kraus_map_def_raw by blast
from asm have ‹kf_bound EE = id_cblinfun›
by (simp add: EE km_bound_kf_bound)
then have ‹kf_trace_preserving EE›
by (simp add: kf_trace_preserving_iff_bound_id)
then show ‹km_trace_preserving 𝔈›
using EE km_trace_preserving_def by blast
qed
lemma km_trace_preserving_iff_bound_id':
fixes 𝔈 :: ‹('a::{chilbert_space, not_singleton}, 'a) trace_class ⇒ _›
shows ‹km_trace_preserving 𝔈 ⟷ km_bound 𝔈 = id_cblinfun›
using km_bound_invalid km_trace_preserving_iff_bound_id by fastforce
lemma km_trace_norm_preserving: ‹km_norm 𝔈 ≤ 1› if ‹km_trace_preserving 𝔈›
using km_trace_preserving_imp_reducing km_trace_reducing_iff_norm_leq1 that by blast
lemma km_trace_norm_preserving_eq:
fixes 𝔈 :: ‹('a::{chilbert_space,not_singleton},'a) trace_class ⇒ ('b::chilbert_space,'b) trace_class›
assumes ‹km_trace_preserving 𝔈›
shows ‹km_norm 𝔈 = 1›
using assms
by (simp add: km_trace_preserving_iff_bound_id' km_norm_def)
lemma kraus_map_trace: ‹kraus_map (one_dim_iso o trace_tc)›
by (auto intro!: ext kraus_mapI[of _ ‹kf_trace some_chilbert_basis›]
simp: kf_trace_is_trace)
lemma trace_preserving_trace_kraus_map[iff]: ‹km_trace_preserving (one_dim_iso o trace_tc)›
using km_trace_preserving_iff kraus_map_trace by fastforce
lemma km_trace_bound[simp]: ‹km_bound (one_dim_iso o trace_tc) = id_cblinfun›
using km_trace_preserving_iff_bound_id by blast
lemma km_trace_norm_eq1[simp]: ‹km_norm (one_dim_iso o trace_tc :: ('a::{chilbert_space,not_singleton},'a) trace_class ⇒ _) = 1›
using km_trace_norm_preserving_eq by blast
lemma km_trace_norm_leq1[simp]: ‹km_norm (one_dim_iso o trace_tc) ≤ 1›
using km_trace_norm_preserving by blast
lemma kraus_map_partial_trace[iff]: ‹kraus_map partial_trace›
by (auto intro!: ext kraus_mapI[of _ ‹kf_partial_trace_right›] simp flip: partial_trace_is_kf_partial_trace)
lemma partial_trace_ignores_kraus_map:
assumes ‹km_trace_preserving 𝔈›
assumes ‹kraus_map 𝔉›
shows ‹partial_trace (km_tensor 𝔉 𝔈 ρ) = 𝔉 (partial_trace ρ)›
proof -
from assms
obtain EE :: ‹(_,_,unit) kraus_family› where EE_def: ‹𝔈 = kf_apply EE› and tpEE: ‹kf_trace_preserving EE›
using km_trace_preserving_def by blast
obtain FF :: ‹(_,_,unit) kraus_family› where FF_def: ‹𝔉 = kf_apply FF›
using assms(2) kraus_map_def_raw by blast
have ‹partial_trace (km_tensor 𝔉 𝔈 ρ) = partial_trace (kf_tensor FF EE *⇩k⇩r ρ)›
using assms
by (simp add: km_trace_preserving_def partial_trace_ignores_kraus_family
km_tensor_kf_tensor EE_def kf_id_apply[abs_def] id_def FF_def
flip: km_tensor_kf_tensor)
also have ‹… = FF *⇩k⇩r partial_trace ρ›
by (simp add: partial_trace_ignores_kraus_family tpEE)
also have ‹… = 𝔉 (partial_trace ρ)›
using FF_def by presburger
finally show ?thesis
by -
qed
lemma km_partial_trace_bound[simp]: ‹km_bound partial_trace = id_cblinfun›
apply (subst km_bound_kf_bound[of _ kf_partial_trace_right])
using partial_trace_is_kf_partial_trace by auto
lemma km_partial_trace_norm[simp]:
shows ‹km_norm partial_trace = 1›
by (simp add: km_norm_def)
lemma km_trace_preserving_tensor:
assumes ‹km_trace_preserving 𝔈› and ‹km_trace_preserving 𝔉›
shows ‹km_trace_preserving (km_tensor 𝔈 𝔉)›
proof -
from assms obtain EE :: ‹('a ell2, 'b ell2, unit) kraus_family› where EE: ‹𝔈 = kf_apply EE› and tE: ‹kf_trace_preserving EE›
using km_trace_preserving_def by blast
from assms obtain FF :: ‹('c ell2, 'd ell2, unit) kraus_family› where FF: ‹𝔉 = kf_apply FF› and tF: ‹kf_trace_preserving FF›
using km_trace_preserving_def by blast
show ?thesis
by (auto intro!: kf_trace_preserving_tensor simp: EE FF km_tensor_kf_tensor tE tF)
qed
lemma km_trace_reducing_tensor:
assumes ‹km_trace_reducing 𝔈› and ‹km_trace_reducing 𝔉›
shows ‹km_trace_reducing (km_tensor 𝔈 𝔉)›
by (smt (z3) assms(1,2) km_norm_geq0 km_norm_tensor km_tensor_kraus_map km_trace_reducing_iff_norm_leq1
mult_left_le_one_le)
subsection ‹Complete measurements›
definition ‹km_complete_measurement B ρ = (∑⇩∞x∈B. sandwich_tc (selfbutter (sgn x)) ρ)›
abbreviation ‹km_complete_measurement_ket ≡ km_complete_measurement (range ket)›
lemma km_complete_measurement_kf_complete_measurement: ‹km_complete_measurement B = kf_apply (kf_complete_measurement B)› if ‹is_ortho_set B›
by (simp add: kf_complete_measurement_apply[OF that, abs_def] km_complete_measurement_def[abs_def])
lemma km_complete_measurement_ket_kf_complete_measurement_ket: ‹km_complete_measurement_ket = kf_apply kf_complete_measurement_ket›
by (metis Complex_L2.is_ortho_set_ket kf_apply_map kf_complete_measurement_ket_kf_map kf_eq_imp_eq_weak kf_eq_weak_def
km_complete_measurement_kf_complete_measurement)
lemma km_complete_measurement_has_sum:
assumes ‹is_ortho_set B›
shows ‹((λx. sandwich_tc (selfbutter (sgn x)) ρ) has_sum km_complete_measurement B ρ) B›
using kf_complete_measurement_has_sum[OF assms] and assms
by (simp add: kf_complete_measurement_apply km_complete_measurement_def)
lemma km_complete_measurement_ket_has_sum:
‹((λx. sandwich_tc (selfbutter (ket x)) ρ) has_sum km_complete_measurement_ket ρ) UNIV›
by (smt (verit) has_sum_cong has_sum_reindex inj_ket is_onb_ket is_ortho_set_ket kf_complete_measurement_apply
kf_complete_measurement_has_sum_onb km_complete_measurement_def o_def)
lemma km_bound_complete_measurement:
assumes ‹is_ortho_set B›
shows ‹km_bound (km_complete_measurement B) ≤ id_cblinfun›
apply (subst km_bound_kf_bound[of _ ‹kf_complete_measurement B›])
using assms kf_complete_measurement_apply km_complete_measurement_def apply fastforce
by (simp add: assms kf_bound_complete_measurement)
lemma km_norm_complete_measurement:
assumes ‹is_ortho_set B›
shows ‹km_norm (km_complete_measurement B) ≤ 1›
apply (subst km_norm_kf_norm[of _ ‹kf_complete_measurement B›])
apply (simp add: assms km_complete_measurement_kf_complete_measurement)
by (simp_all add: assms kf_norm_complete_measurement)
lemma km_bound_complete_measurement_onb[simp]:
assumes ‹is_onb B›
shows ‹km_bound (km_complete_measurement B) = id_cblinfun›
apply (subst km_bound_kf_bound[of _ ‹kf_complete_measurement B›])
using assms
by (auto intro!: ext simp: kf_complete_measurement_apply is_onb_def km_complete_measurement_def)
lemma km_bound_complete_measurement_ket[simp]: ‹km_bound km_complete_measurement_ket = id_cblinfun›
by fastforce
lemma km_norm_complete_measurement_onb[simp]:
fixes B :: ‹'a::{not_singleton, chilbert_space} set›
assumes ‹is_onb B›
shows ‹km_norm (km_complete_measurement B) = 1›
apply (subst km_norm_kf_norm[of _ ‹kf_complete_measurement B›])
using assms
by (auto intro!: ext simp: kf_complete_measurement_apply is_onb_def km_complete_measurement_def)
lemma km_norm_complete_measurement_ket[simp]:
shows ‹km_norm km_complete_measurement_ket = 1›
by fastforce
lemma kraus_map_complete_measurement:
assumes ‹is_ortho_set B›
shows ‹kraus_map (km_complete_measurement B)›
apply (rule kraus_mapI[of _ ‹kf_complete_measurement B›])
by (auto intro!: ext simp add: assms kf_complete_measurement_apply km_complete_measurement_def)
lemma kraus_map_complete_measurement_ket[iff]:
shows ‹kraus_map km_complete_measurement_ket›
by (simp add: kraus_map_complete_measurement)
lemma km_complete_measurement_idem[simp]:
assumes ‹is_ortho_set B›
shows ‹km_complete_measurement B (km_complete_measurement B ρ) = km_complete_measurement B ρ›
using kf_complete_measurement_idem[of B]
kf_complete_measurement_apply[OF assms] km_complete_measurement_def
by (metis (no_types, lifting) ext kf_comp_apply kf_complete_measurement_idem_weak kf_eq_weak_def o_def)
lemma km_complete_measurement_ket_idem[simp]:
‹km_complete_measurement_ket (km_complete_measurement_ket ρ) = km_complete_measurement_ket ρ›
by fastforce
lemma km_complete_measurement_has_sum_onb:
assumes ‹is_onb B›
shows ‹((λx. sandwich_tc (selfbutter x) ρ) has_sum km_complete_measurement B ρ) B›
using kf_complete_measurement_has_sum_onb[OF assms] and assms
by (simp add: kf_complete_measurement_apply km_complete_measurement_def is_onb_def)
lemma km_complete_measurement_ket_diagonal_operator[simp]:
‹km_complete_measurement_ket (diagonal_operator_tc f) = diagonal_operator_tc f›
using kf_complete_measurement_ket_diagonal_operator[of f]
by (metis (no_types, lifting) is_ortho_set_ket kf_apply_map kf_apply_on_UNIV kf_apply_on_eqI kf_complete_measurement_apply
kf_complete_measurement_ket_kf_map km_complete_measurement_def)
lemma km_operators_complete_measurement:
assumes ‹is_ortho_set B›
shows ‹km_operators_in (km_complete_measurement B) (span (selfbutter ` B))›
proof -
have ‹span ((selfbutter ∘ sgn) ` B) ⊆ span (selfbutter ` B)›
proof (intro real_vector.span_minimal[OF _ real_vector.subspace_span] subsetI)
fix a
assume ‹a ∈ (selfbutter ∘ sgn) ` B›
then obtain h where ‹a = selfbutter (sgn h)› and ‹h ∈ B›
by force
then have ‹a = (inverse (norm h))⇧2 *⇩R selfbutter h›
by (simp add: sgn_div_norm scaleR_scaleC power2_eq_square)
with ‹h ∈ B›
show ‹a ∈ span (selfbutter ` B)›
by (simp add: span_clauses(1) span_mul)
qed
then show ?thesis
by (simp add: km_complete_measurement_kf_complete_measurement assms km_operators_in_kf_apply
kf_operators_complete_measurement)
qed
lemma km_operators_complete_measurement_ket:
shows ‹km_operators_in km_complete_measurement_ket (span (range (λc. (selfbutter (ket c)))))›
by (metis (no_types, lifting) image_cong is_ortho_set_ket km_operators_complete_measurement range_composition)
lemma km_complete_measurement_ket_butterket[simp]:
‹km_complete_measurement_ket (tc_butterfly (ket c) (ket c)) = tc_butterfly (ket c) (ket c)›
by (simp add: km_complete_measurement_ket_kf_complete_measurement_ket kf_complete_measurement_ket_apply_butterfly)
lemma km_complete_measurement_tensor:
assumes ‹is_ortho_set B› and ‹is_ortho_set C›
shows ‹km_tensor (km_complete_measurement B) (km_complete_measurement C)
= km_complete_measurement ((λ(b,c). b ⊗⇩s c) ` (B × C))›
by (simp add: km_complete_measurement_kf_complete_measurement assms is_ortho_set_tensor km_tensor_kf_tensor
flip: kf_complete_measurement_tensor)
lemma km_complete_measurement_ket_tensor:
shows ‹km_tensor (km_complete_measurement_ket :: ('a ell2, _) trace_class ⇒ _) (km_complete_measurement_ket :: ('b ell2, _) trace_class ⇒ _)
= km_complete_measurement_ket›
by (simp add: km_complete_measurement_ket_kf_complete_measurement_ket km_tensor_kf_tensor kf_complete_measurement_ket_tensor)
lemma km_tensor_0_left[simp]: ‹km_tensor (0 :: ('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class) 𝔈 = 0›
proof (cases ‹km_tensor_exists (0 :: ('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class) 𝔈›)
case True
then show ?thesis
apply (rule_tac eq_from_separatingI2[OF separating_set_bounded_clinear_tc_tensor])
by (simp_all add: km_tensor_apply)
next
case False
then show ?thesis
using km_tensor_invalid by blast
qed
lemma km_tensor_0_right[simp]: ‹km_tensor 𝔈 (0 :: ('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class) = 0›
proof (cases ‹km_tensor_exists 𝔈 (0 :: ('a ell2, 'b ell2) trace_class ⇒ ('c ell2, 'd ell2) trace_class)›)
case True
then show ?thesis
apply (rule_tac eq_from_separatingI2[OF separating_set_bounded_clinear_tc_tensor])
by (simp_all add: km_tensor_apply)
next
case False
then show ?thesis
using km_tensor_invalid by blast
qed
unbundle no kraus_map_syntax
unbundle no cblinfun_syntax
end