Theory More_Kraus_Maps
theory More_Kraus_Maps
imports Kraus_Maps.Kraus_Maps
O2H_Additional_Lemmas
begin
unbundle cblinfun_syntax
unbundle lattice_syntax
text ‹Fst on kraus families.›
lemma inj_Fst_alt:
assumes "c≠0"
shows "a ⊗⇩o c = b ⊗⇩o c ⟹ a = b"
using inj_tensor_left[OF assms] unfolding inj_def by auto
lift_definition kf_Fst :: "('a ell2, 'c ell2, unit) kraus_family ⇒
(('a × 'b) ell2, ('c × 'b) ell2, unit) kraus_family" is
"λE. (λ(x,_). (x ⊗⇩o id_cblinfun, ())) ` E"
proof (rename_tac 𝔈, intro CollectI)
fix 𝔈 :: ‹('a ell2 ⇒⇩C⇩L 'c ell2 × unit) set›
assume ‹𝔈 ∈ Collect kraus_family›
then have ‹kraus_family 𝔈› by auto
define f :: ‹('a ell2 ⇒⇩C⇩L 'c ell2 × unit) ⇒ _› where ‹f = (λ(E,x). (E ⊗⇩o id_cblinfun, ()))›
define Fst where ‹Fst = f ` 𝔈›
show ‹kraus_family Fst›
proof (intro kraus_familyI)
from ‹kraus_family 𝔈›
obtain B where B: ‹(∑(E, x)∈S. E* o⇩C⇩L E) ≤ B› if ‹finite S› and ‹S ⊆ 𝔈› for S
apply atomize_elim
by (auto simp: kraus_family_def bdd_above_def)
from B[of ‹{}›] have [simp]: ‹B ≥ 0› by simp
have ‹(∑(G, z)∈U. G* o⇩C⇩L G) ≤ B ⊗⇩o id_cblinfun› if ‹finite U› and ‹U ⊆ Fst› for U
proof -
from that
obtain V where V_subset: ‹V ⊆ 𝔈› and [simp]: ‹finite V› and ‹U = f ` V›
apply (simp only: Fst_def flip: f_def)
by (meson finite_subset_image)
have ‹inj_on f V› by (auto intro!: inj_onI simp: f_def inj_Fst_alt[OF id_cblinfun_not_0])
have ‹(∑(G, z)∈U. G* o⇩C⇩L G) = (∑(G, z)∈f ` V. G* o⇩C⇩L G)›
using ‹U = f ` V› by (auto)
also have ‹… = (∑(E,x)∈V. (E ⊗⇩o id_cblinfun)* o⇩C⇩L (E ⊗⇩o id_cblinfun))›
by (subst sum.reindex) (use ‹inj_on f V› in ‹auto simp: case_prod_unfold f_def›)
also have ‹… = (∑(E,x)∈V. (E* o⇩C⇩L E)) ⊗⇩o id_cblinfun›
by (subst tensor_op_cbilinear.sum_left)
(simp add: case_prod_unfold comp_tensor_op tensor_op_adjoint)
also have ‹… ≤ B ⊗⇩o id_cblinfun›
using V_subset by (auto intro!: tensor_op_mono B)
finally show ?thesis by-
qed
then show ‹bdd_above ((λF. ∑(E, x)∈F. E* o⇩C⇩L E) ` {F. finite F ∧ F ⊆ Fst})›
by fast
show ‹0 ∉ fst ` Fst› (is ‹?zero ∉ _›)
proof (rule notI)
assume ‹?zero ∈ fst ` Fst›
then have ‹?zero ∈ (λx. fst x ⊗⇩o id_cblinfun) ` 𝔈›
by (simp add: Fst_def f_def image_image case_prod_unfold)
then obtain E where ‹E ∈ 𝔈› and ‹?zero = fst E ⊗⇩o id_cblinfun›
by blast
then have ‹fst E = 0›
by (metis id_cblinfun_not_0 tensor_op_nonzero)
with ‹E ∈ 𝔈›
show False
using ‹kraus_family 𝔈›
by (simp add: kraus_family_def)
qed
qed
qed
lemma summable_on_in_kf_Fst:
fixes f :: "'c ⇒ 'a ell2 ⇒⇩C⇩L 'a ell2"
and b :: "'b ell2 ⇒⇩C⇩L 'b ell2"
shows "summable_on_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) (Rep_kraus_family G)"
proof -
have "bdd_above (sum (λ(E, x). E* o⇩C⇩L E) ` {F. finite F ∧ F ⊆ Rep_kraus_family G})"
by (intro summable_wot_bdd_above[OF kf_bound_summable positive_cblinfun_squareI])
(auto simp add: case_prod_beta)
then obtain B where B: ‹(∑x∈S. fst x* o⇩C⇩L fst x) ≤ B› if ‹finite S› and
‹S ⊆ (Rep_kraus_family G)› for S
apply atomize_elim unfolding bdd_above_def by (auto simp: case_prod_beta)
have bound: "(∑x∈F. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) ≤ B ⊗⇩o id_cblinfun"
if "finite F" "F ⊆ (Rep_kraus_family G)" for F
by (subst tensor_op_cbilinear.sum_left[symmetric], intro tensor_op_mono_left)
(auto simp add: B that)
have pos: "x ∈ (Rep_kraus_family G) ⟹ 0 ≤ (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun" for x
using positive_cblinfun_squareI positive_id_cblinfun tensor_op_pos by blast
show ?thesis by (auto intro!: summable_wot_boundedI[OF bound pos])
qed
lemma infsum_in_kf_Fst:
fixes f :: "'c ⇒ 'a ell2 ⇒⇩C⇩L 'a ell2"
and b :: "'b ell2 ⇒⇩C⇩L 'b ell2"
shows "infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) (Rep_kraus_family G) ≤
(infsum_in cweak_operator_topology (λx. fst x* o⇩C⇩L fst x) (Rep_kraus_family G)) ⊗⇩o id_cblinfun"
proof -
have sum: "summable_on_in cweak_operator_topology (λx. fst x* o⇩C⇩L fst x) (Rep_kraus_family G)"
using kf_bound_summable
by (metis (mono_tags, lifting) cond_case_prod_eta fst_conv)
have pos_f: "x ∈ Rep_kraus_family G ⟹ 0 ≤ fst x* o⇩C⇩L fst x" for x
using positive_cblinfun_squareI by blast
have pos: "x ∈ Rep_kraus_family G ⟹ 0 ≤ (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun" for x
by (simp add: positive_cblinfun_squareI tensor_op_pos)
define s where "s = infsum_in cweak_operator_topology (λx. fst x* o⇩C⇩L fst x) (Rep_kraus_family G)"
have "sum (λx. fst x* o⇩C⇩L fst x) F ≤ s" if "finite F" and "F ⊆ (Rep_kraus_family G)" for F
unfolding s_def
using that infsum_wot_is_Sup[OF sum pos_f] unfolding is_Sup_def by auto
then have "sum (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) F ≤ s ⊗⇩o id_cblinfun"
if "finite F" and "F ⊆ Rep_kraus_family G" for F
apply (subst tensor_op_cbilinear.sum_left[symmetric])
apply (intro tensor_op_mono_left[OF _ positive_id_cblinfun])
by (use that in ‹auto›)
moreover have "is_Sup (sum (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) `
{F. finite F ∧ F ⊆ (Rep_kraus_family G)})
(infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) (Rep_kraus_family G))"
by (intro infsum_wot_is_Sup[OF summable_on_in_kf_Fst pos], auto)
ultimately have "infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun)
(Rep_kraus_family G) ≤ s ⊗⇩o id_cblinfun"
by (smt (verit, ccfv_threshold) image_iff is_Sup_def mem_Collect_eq)
then show ?thesis unfolding s_def by auto
qed
lemma kf_bound_kf_Fst:
"kf_bound (kf_Fst F:: (('a × 'b) ell2, ('c × 'b) ell2, unit) kraus_family) ≤
kf_bound F ⊗⇩o id_cblinfun"
proof -
have inj: "inj_on (λ(x, _). (x ⊗⇩o id_cblinfun, ())) (Rep_kraus_family F)"
unfolding inj_on_def by (auto simp add: inj_Fst_alt[OF id_cblinfun_not_0])
have "infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun) (Rep_kraus_family F) ≤
infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x)) (Rep_kraus_family F) ⊗⇩o id_cblinfun"
by (rule infsum_in_kf_Fst)
then have "infsum_in cweak_operator_topology (λx. (fst x* o⇩C⇩L fst x) ⊗⇩o id_cblinfun)(Rep_kraus_family F)
≤ infsum_in cweak_operator_topology (λ(E, x). E* o⇩C⇩L E) (Rep_kraus_family F) ⊗⇩o id_cblinfun"
by (metis (mono_tags, lifting) infsum_in_cong prod.case_eq_if)
then have "infsum_in cweak_operator_topology (λ(E, x). E* o⇩C⇩L E) ((λ(x,_).
(x ⊗⇩o (id_cblinfun ::'b update), ())) ` (Rep_kraus_family F)) ≤
(infsum_in cweak_operator_topology (λ(E, x). E* o⇩C⇩L E) (Rep_kraus_family F)) ⊗⇩o id_cblinfun"
by (subst infsum_in_reindex[OF inj])
(auto simp add: o_def case_prod_beta tensor_op_adjoint comp_tensor_op)
then show ?thesis
by (simp add: kf_Fst.rep_eq kf_bound.rep_eq)
qed
lemma sandwich_tc_kf_apply_Fst:
"sandwich_tc (Snd (Q::'d update)) (kf_apply (kf_Fst F::
(('a×'d) ell2, ('a×'d) ell2, unit) kraus_family) ρ) =
kf_apply (kf_Fst F) (sandwich_tc (Snd Q) ρ)"
proof -
have sand: "sandwich_tc (Snd Q) (sandwich_tc a ρ) =
sandwich_tc a (sandwich_tc (Snd Q) ρ)"
if "(a, ()) ∈ Rep_kraus_family (kf_Fst F)" for a
proof -
obtain x where a: "a = x ⊗⇩o id_cblinfun"
using ‹(a, ()) ∈ Rep_kraus_family (kf_Fst F)› unfolding kf_Fst.rep_eq by auto
show ?thesis unfolding a sandwich_tc_compose'[symmetric] Snd_def by (auto simp add: comp_tensor_op)
qed
have 1: "sum (sandwich_tc (Snd Q) o (λE. (sandwich_tc (fst E) ρ))) F' =
sandwich_tc (Snd Q) (∑E∈F'. sandwich_tc (fst E) ρ)"
if "finite F'" "F' ⊆ Rep_kraus_family (kf_Fst F ::
(('a×'d) ell2, ('a×'d) ell2, unit) kraus_family)" for F'
by (auto simp add: sandwich_tc_sum sandwich_tc_tensor intro!: sum.cong)
have 2: "isCont (sandwich_tc (Snd Q))
(∑⇩∞E∈Rep_kraus_family (kf_Fst F). sandwich_tc (fst E) ρ)"
using isCont_sandwich_tc by auto
have 3: " (λE. sandwich_tc (fst E) ρ) summable_on Rep_kraus_family (kf_Fst F)"
by (metis (no_types, lifting) cond_case_prod_eta fst_conv kf_apply_summable)
then show ?thesis unfolding kf_apply.rep_eq
by (subst infsum_comm_additive_general[OF 1 2 3, symmetric])
(auto intro!: infsum_cong simp add: sand)
qed
text ‹kraus family Fst is trace preserving.›
lemma kf_apply_Fst_tensor:
‹kf_apply (kf_Fst 𝔈 ::(('c × 'b) ell2, ('a × 'b) ell2, unit) kraus_family)
(tc_tensor ρ σ) = tc_tensor (kf_apply 𝔈 ρ) σ›
proof -
have inj: ‹inj_on (λ(E, x). (E ⊗⇩o id_cblinfun, ())) (Rep_kraus_family 𝔈)›
unfolding inj_on_def by (auto simp add: inj_Fst_alt[OF id_cblinfun_not_0])
have [simp]: ‹bounded_linear (λx. tc_tensor x σ)›
by (intro bounded_linear_intros)
have [simp]: ‹bounded_linear (tc_tensor (sandwich_tc E ρ))› for E
by (intro bounded_linear_intros)
have sum2: ‹(λ(E, x). sandwich_tc E ρ) summable_on Rep_kraus_family 𝔈›
using kf_apply_summable by blast
have ‹kf_apply (kf_Fst 𝔈 ::(('c × 'b) ell2, ('a × 'b) ell2, unit) kraus_family)
(tc_tensor ρ σ)
= (∑⇩∞(E,x)∈Rep_kraus_family 𝔈. sandwich_tc (E ⊗⇩o id_cblinfun) (tc_tensor ρ σ))›
unfolding kf_apply.rep_eq kf_Fst.rep_eq
by (subst infsum_reindex[OF inj]) (simp add: case_prod_unfold o_def)
also have ‹… = (∑⇩∞(E,x)∈Rep_kraus_family 𝔈. tc_tensor (sandwich_tc E ρ) σ)›
by (simp add: sandwich_tc_tensor)
finally have ‹kf_apply (kf_Fst 𝔈 ::(('c × 'b) ell2, ('a × 'b) ell2, unit) kraus_family)
(tc_tensor ρ σ) = (∑⇩∞(E,x)∈Rep_kraus_family 𝔈. tc_tensor (sandwich_tc E ρ) σ)›
by (simp add: kf_apply_def case_prod_unfold)
also have ‹… = tc_tensor (∑⇩∞(E,x)∈Rep_kraus_family 𝔈. sandwich_tc E ρ) σ›
by (subst infsum_bounded_linear[where h=‹λx. tc_tensor x σ›, symmetric])
(use sum2 in ‹auto simp add: o_def case_prod_unfold›)
also have ‹… = tc_tensor (kf_apply 𝔈 ρ) σ›
by (simp add: kf_apply_def case_prod_unfold)
finally show ?thesis by auto
qed
lemma partial_trace_ignore_trace_preserving_map_Fst:
assumes ‹kf_trace_preserving 𝔈›
shows ‹partial_trace (kf_apply (kf_Fst 𝔈) ρ) =
kf_apply 𝔈 (partial_trace ρ)›
proof (rule fun_cong[where x=ρ], rule eq_from_separatingI2[OF separating_set_bounded_clinear_tc_tensor])
show ‹bounded_clinear (λa. partial_trace (kf_apply (kf_Fst 𝔈) a))›
by (intro bounded_linear_intros)
show ‹bounded_clinear (λa. kf_apply 𝔈 (partial_trace a))›
by (intro bounded_linear_intros)
fix ρ :: ‹('a ell2, 'a ell2) trace_class› and σ :: ‹('c ell2, 'c ell2) trace_class›
from assms
show ‹partial_trace (kf_apply (kf_Fst 𝔈) (tc_tensor ρ σ)) =
kf_apply 𝔈 (partial_trace (tc_tensor ρ σ))›
by (simp add: kf_apply_Fst_tensor kf_apply_scaleC partial_trace_tensor)
qed
lemma trace_preserving_kf_Fst:
assumes "km_trace_preserving (kf_apply E)"
shows "km_trace_preserving (kf_apply (
kf_Fst E ::(('a × 'c) ell2, ('a × 'c) ell2, unit) kraus_family))"
proof -
have bounded: "bounded_clinear (λρ. trace_tc (kf_apply (kf_Fst E) ρ))"
by (simp add: bounded_clinear_compose kf_apply_bounded_clinear)
have trace: "trace_tc (kf_apply (kf_Fst E ::
(('a × 'c) ell2, ('a × 'c) ell2, unit) kraus_family) (tc_tensor x y)) =
trace_tc (tc_tensor x y)" for x y using assms
apply (simp add: kf_apply_Fst_tensor tc_tensor.rep_eq trace_tc.rep_eq trace_tensor km_trace_preserving_def)
by (metis kf_trace_preserving_def trace_tc.rep_eq)
have "(λρ. trace_tc (kf_apply (kf_Fst E ::
(('a × 'c) ell2, ('a × 'c) ell2, unit) kraus_family) ρ)) = trace_tc"
by (rule eq_from_separatingI2[OF separating_set_bounded_clinear_tc_tensor])
(auto simp add: bounded trace)
then show ?thesis
using assms unfolding km_trace_preserving_def
by (metis kf_trace_preserving_def)
qed
text ‹Summability on Kraus maps›
lemma finite_kf_apply_has_sum:
assumes "(f has_sum x) A"
shows "((kf_apply 𝔉 o f) has_sum kf_apply 𝔉 x) A"
unfolding o_def by (intro has_sum_bounded_linear[OF _ assms])
(auto simp add: bounded_clinear.bounded_linear kf_apply_bounded_clinear)
lemma finite_kf_apply_abs_summable_on:
assumes "f abs_summable_on A"
shows "(kf_apply 𝔉 o f) abs_summable_on A"
by (intro abs_summable_on_bounded_linear)
(auto simp add: assms bounded_clinear.bounded_linear kf_apply_bounded_clinear)
unbundle no cblinfun_syntax
unbundle no lattice_syntax
end