Theory O2H_Theorem
theory O2H_Theorem
imports Mixed_O2H
begin
unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax
section ‹General O2H Setting and Theorem›
text ‹General O2H setting›
locale o2h_theorem = o2h_setting "TYPE('x)" "TYPE('y::group_add)" "TYPE('mem)" "TYPE('l)" +
fixes carrier :: "(('x ⇒ 'y)×('x ⇒ 'y)×('x ⇒ bool)×_) set"
fixes distr :: "(('x ⇒ 'y)×('x ⇒ 'y)×('x ⇒ bool)×_) ⇒ real"
assumes distr_pos: "∀(H,G,S,z)∈carrier. distr (H,G,S,z) ≥ 0"
and distr_sum_1: "(∑(H,G,S,z)∈carrier. distr (H,G,S,z)) = 1"
and finite_carrier: "finite carrier"
and H_G_same_upto_S:
"⋀H G S z. (H,G,S,z)∈carrier ⟹ x ∈ - Collect S ⟹ H x = G x"
fixes E:: "'mem kraus_adv"
assumes E_norm_id: "⋀i. i < d+1 ⟹ kf_bound (E i) ≤ id_cblinfun"
assumes E_nonzero: "⋀i. i < d+1 ⟹ Rep_kraus_family (E i) ≠ {}"
fixes P:: "'mem update"
assumes is_Proj_P: "is_Proj P"
begin
lemma Fst_E_nonzero:
"⋀i. i < d+1 ⟹ Rep_kraus_family (kf_Fst (E i)) ≠ {}"
using E_nonzero by (simp add: kf_Fst.rep_eq)
text ‹Some properties of the joint distribution.›
lemma Uquery_G_H_same_on_not_S_embed':
assumes "(H,G,S,z)∈carrier"
shows
"Uquery H o⇩C⇩L proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun =
Uquery G o⇩C⇩L proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun"
proof (intro equal_ket, safe, unfold tensor_ell2_ket[symmetric], goal_cases)
case (1 a b)
let ?P = "proj_classical_set (- (Collect S))"
have "(Uquery H o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b =
(Uquery G o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b"
if "¬ S a"
proof -
have "(Uquery H o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b = Uquery H *⇩V ket a ⊗⇩s ket b"
by (simp add: proj_classical_set_elem tensor_op_ell2 that)
also have "… = ket a ⊗⇩s ket (b + H a)" using Uquery_ket by auto
also have "… = ket a ⊗⇩s ket (b + G a)" using H_G_same_upto_S[OF assms] that by auto
also have "… = Uquery G *⇩V ket a ⊗⇩s ket b" using Uquery_ket by auto
also have "… = (Uquery G o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b"
by (simp add: proj_classical_set_elem tensor_op_ell2 that)
finally show ?thesis by auto
qed
moreover have "(Uquery H o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b =
(Uquery G o⇩C⇩L ?P ⊗⇩o id_cblinfun) *⇩V ket a ⊗⇩s ket b"
if "S a"
by (simp add: proj_classical_set_not_elem tensor_op_ell2 that)
ultimately show ?case by (cases "S a", auto)
qed
lemma Uquery_G_H_same_on_not_S_embed:
assumes "(H,G,S,z)∈carrier"
shows "((X;Y) (Uquery H) o⇩C⇩L (not_S_embed S)) = ((X;Y) (Uquery G) o⇩C⇩L (not_S_embed S))"
proof -
have "((X;Y) (Uquery H) o⇩C⇩L (not_S_embed S)) =
((X;Y) (Uquery H) o⇩C⇩L (X;Y) (proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun))"
unfolding not_S_embed_def by (simp add: Laws_Quantum.register_pair_apply)
also have "… = (X;Y) (Uquery H o⇩C⇩L proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun)"
by (simp add: Axioms_Quantum.register_mult)
also have "… = (X;Y) (Uquery G o⇩C⇩L proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun)"
using Uquery_G_H_same_on_not_S_embed' assms by auto
also have "… = ((X;Y) (Uquery G) o⇩C⇩L (X;Y) (proj_classical_set (- (Collect S)) ⊗⇩o id_cblinfun))"
by (simp add: Axioms_Quantum.register_mult)
also have "… = ((X;Y) (Uquery G) o⇩C⇩L (not_S_embed S))"
unfolding not_S_embed_def by (simp add: Laws_Quantum.register_pair_apply)
finally show ?thesis by auto
qed
lemma Uquery_G_H_same_on_not_S_embed_tensor:
assumes "(H,G,S,z)∈carrier"
shows "((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L Fst (not_S_embed S)) =
((X_for_B;Y_for_B) (Uquery G) o⇩C⇩L Fst (not_S_embed S))"
using Uquery_G_H_same_on_not_S_embed[OF assms] unfolding UqueryH_tensor_id_cblinfunB Fst_def
by (auto simp add: comp_tensor_op)
text ‹Instantiations of mixed o2h locale for H and G›
definition carrier_G where "carrier_G = (λ(H,G,S,z). (G,S,(H,z))) ` carrier"
definition distr_G where "distr_G = (λ(G,S,(H,z)). distr (H,G,S,z))"
lemma distr_G_pos: "∀(G,S,z)∈carrier_G. distr_G (G,S,z) ≥ 0"
unfolding carrier_G_def distr_G_def using distr_pos by auto
lemma distr_G_sum_1: "(∑(G,S,z)∈carrier_G. distr_G (G,S,z)) = 1"
unfolding carrier_G_def distr_G_def using distr_sum_1
by (subst sum.reindex, auto simp add: inj_on_def case_prod_beta)
lemma finite_carrier_G: "finite carrier_G"
unfolding carrier_G_def by (auto simp add: inj_on_def finite_carrier)
definition carrier_H where "carrier_H = (λ(H,G,S,z). (H,S,(G,z))) ` carrier"
definition distr_H where "distr_H = (λ(H,S,(G,z)). distr (H,G,S,z))"
lemma distr_H_pos: "∀(H,S,z)∈carrier_H. distr_H (H,S,z) ≥ 0"
unfolding carrier_H_def distr_H_def using distr_pos by auto
lemma distr_H_sum_1: "(∑(H,S,z)∈carrier_H. distr_H (H,S,z)) = 1"
unfolding carrier_H_def distr_H_def using distr_sum_1
by (subst sum.reindex[], auto simp add: inj_on_def case_prod_beta)
lemma finite_carrier_H: "finite carrier_H"
unfolding carrier_H_def by (auto simp add: inj_on_def finite_carrier)
interpretation mixed_H: mixed_o2h X Y d init flip bit valid empty carrier_H distr_H E P
apply unfold_locales
using distr_H_pos distr_H_sum_1 finite_carrier_H E_norm_id E_nonzero is_Proj_P
by auto
interpretation mixed_G: mixed_o2h X Y d init flip bit valid empty carrier_G distr_G E P
apply unfold_locales
using distr_G_pos distr_G_sum_1 finite_carrier_G E_norm_id E_nonzero is_Proj_P
by auto
text ‹Lemmas on \<^const>‹Proj_ket_upto› and ‹run_adv_mixed›. The adversary run upto i can be projected
to the first i ket states in the counting register.›
lemma length_has_bits_upto:
assumes "l∈has_bits_upto n"
shows "length l = d"
using assms unfolding has_bits_upto_def len_d_lists_def has_bits_def by auto
lemma empty_not_flip:
assumes "x ∈ list_to_l ` has_bits_upto n" "n<d"
shows "empty ≠ flip n x"
proof -
have "blog x" using assms using has_bits_upto_def surj_list_to_l by auto
obtain l where x: "x = list_to_l l" and l_in:"l∈has_bits_upto n" using assms(1) by blast
then have len: "length l = d" using length_has_bits_upto assms by auto
have "¬ l ! (length l - Suc n)" unfolding len using assms(2) has_bits_upto_elem l_in by auto
then have "bit x n = bit empty n" unfolding x by (subst bit_list_to_l) (auto simp add: assms len)
then have "bit (flip n x) n ≠ bit empty n" by (subst bit_flip_same[OF ‹n<d› ‹blog x›], auto)
then show ?thesis by auto
qed
lemma empty_not_flip':
assumes "x ≠ flip n empty" "n<d"
shows "empty ≠ flip n x"
proof (rule ccontr, safe)
assume "empty = flip n x"
then have "flip n empty = flip n (flip n x)" by auto
then have "flip n empty = x" by (metis assms(2) blog.intros(1) flip_flip not_blog_flip)
then show False using assms by auto
qed
lemma Proj_ket_upto_Snd:
"Proj_ket_upto A = Snd (proj_classical_set (list_to_l ` A))"
unfolding Proj_ket_upto_def Proj_ket_set_def Snd_def by auto
lemma from_trace_class_tc_selfbutter:
"from_trace_class (tc_selfbutter x) = selfbutter x"
by (simp add: tc_butterfly.rep_eq tc_selfbutter_def)
lemma selfbutter_empty_US_Proj_ket_upto:
assumes "i<d"
shows "Snd (selfbutter (ket empty)) o⇩C⇩L ((US S i) o⇩C⇩L Proj_ket_upto (has_bits_upto i)) =
Fst (not_S_embed S) o⇩C⇩L Snd (selfbutter (ket empty))"
proof (intro equal_ket, safe, goal_cases)
case (1 a b)
have split_a: "ket a = S_embed S (ket a) + not_S_embed S (ket a)"
using S_embed_not_S_embed_add by auto
have ?case (is "?left = ?right") if "b ∈ list_to_l ` has_bits_upto i"
proof -
have "Proj (ccspan (ket ` list_to_l ` has_bits_upto i)) *⇩V ket b = ket b"
using that by (simp add: Proj_fixes_image ccspan_superset')
then have proj: "proj_classical_set (list_to_l ` has_bits_upto i) *⇩V ket b = ket b"
unfolding proj_classical_set_def by auto
have "?left = (Snd (selfbutter (ket empty)) o⇩C⇩L (US S i)) *⇩V ket (a, b)"
using proj by (auto simp add: Proj_ket_upto_def Proj_ket_set_def tensor_ell2_ket[symmetric]
tensor_op_ell2)
also have "… = Snd (selfbutter (ket empty)) *⇩V
((S_embed S *⇩V ket a) ⊗⇩s (Ub i) *⇩V ket b + ((not_S_embed S *⇩V ket a) ⊗⇩s ket b))"
using US_ket_split by auto
also have "… = Snd (selfbutter (ket empty)) *⇩V ((not_S_embed S *⇩V ket a) ⊗⇩s ket b)"
proof -
obtain bs where b: "bs∈ has_bits_upto i" "b = list_to_l bs"
using ‹b ∈ list_to_l ` has_bits_upto i› by auto
then have bs: "length bs = d" "¬ (bs!(d-i-1))" unfolding has_bits_upto_def len_d_lists_def
using assms b(1) has_bits_upto_elem by auto
then have "bit b i = bit empty i" unfolding b(2)
by (subst bit_list_to_l) (auto simp add: ‹i<d›)
then have "flip i b ≠ empty" using assms bit_flip_same blog.intros(1) not_blog_flip by blast
then have "Snd (selfbutter (ket empty)) *⇩V ((S_embed S *⇩V ket a) ⊗⇩s (Ub i) *⇩V ket b) = 0"
by (simp add: Ub_def Snd_def classical_operator_ket[OF Ub_exists] tensor_op_ell2
tensor_ell2_scaleC2)
then show ?thesis by (simp add: cblinfun.real.add_right)
qed
also have "… = ?right" unfolding Fst_def Snd_def
by (auto simp add: tensor_ell2_ket[symmetric] cinner_ket tensor_op_ell2)
finally show ?thesis by blast
qed
moreover have ?case (is "?left = ?right") if "¬ (b ∈ list_to_l ` has_bits_upto i)" "blog b"
proof -
have "b ≠ empty" using that empty_list_to_l_has_bits_upto by force
have "b ∉ list_to_l ` has_bits_upto i" using that by auto
then have proj: "proj_classical_set (list_to_l ` has_bits_upto i) *⇩V ket b = 0"
unfolding proj_classical_set_def by (intro Proj_0_compl, intro mem_ortho_ccspanI) auto
then have "?left = 0"
by (auto simp add: Proj_ket_upto_def Proj_ket_set_def tensor_ell2_ket[symmetric]
tensor_op_ell2)
moreover have "?right = 0" using ‹b ≠ empty› unfolding Fst_def Snd_def
by (auto simp add: tensor_ell2_ket[symmetric] cinner_ket tensor_op_ell2)
ultimately show ?thesis by auto
qed
moreover have ?case (is "?left = ?right") if "¬ blog b"
proof -
have "b ≠ empty" using that blog.intros(1) by auto
have "b ∉ list_to_l ` has_bits_upto i"
using has_bits_upto_def surj_list_to_l that by fastforce
then have proj: "proj_classical_set (list_to_l ` has_bits_upto i) *⇩V ket b = 0"
unfolding proj_classical_set_def by (intro Proj_0_compl, intro mem_ortho_ccspanI) auto
then have "?left = 0"
by (auto simp add: Proj_ket_upto_def Proj_ket_set_def tensor_ell2_ket[symmetric]
tensor_op_ell2)
moreover have "?right = 0" using ‹b ≠ empty› unfolding Fst_def Snd_def
by (auto simp add: tensor_ell2_ket[symmetric] cinner_ket tensor_op_ell2)
ultimately show ?thesis by auto
qed
ultimately show ?case by (cases "b ∈ list_to_l ` has_bits_upto i", auto)
qed
lemma list_to_l_has_bits_upto_flip:
assumes "b ∈ list_to_l ` has_bits_upto n" "n<d"
shows "flip n b ∈ list_to_l ` has_bits_upto (Suc n)"
proof -
obtain lb where lb: "lb ∈ has_bits_upto n" and b: "b = list_to_l lb" using assms by blast
then have len:"length lb = d" unfolding has_bits_upto_def len_d_lists_def by auto
moreover have "¬ lb ! (length lb - Suc n)" using lb assms(2) calculation has_bits_upto_elem
by auto
ultimately have flip: "flip n b = list_to_l (lb[length lb - Suc n := True])"
unfolding b by (subst flip_list_to_l) (auto simp add: assms)
let ?lb' = "lb[length lb - Suc n := True]"
have len_lb': "?lb' ∈ len_d_lists" unfolding len_d_lists_def using len by auto
have "∀i∈{Suc n..<d}. ¬ lb!(d-i-1)" using lb unfolding has_bits_upto_def has_bits_def by auto
then have "∀i∈{Suc n..<d}. ¬ ?lb'!(d-i-1)" unfolding len by fastforce
then have "?lb' ∉ has_bits {Suc n..<d}" unfolding has_bits_def by auto
then have "?lb' ∈ has_bits_upto (Suc n)" using len_lb' unfolding has_bits_upto_def by auto
then show ?thesis using flip by auto
qed
lemma Proj_ket_upto_US:
assumes "n<d"
shows "US S n o⇩C⇩L Proj_ket_upto (has_bits_upto n) =
Proj_ket_upto (has_bits_upto (Suc n)) o⇩C⇩L US S n o⇩C⇩L Proj_ket_upto (has_bits_upto n)"
proof (intro equal_ket, safe, goal_cases)
case (1 a b)
have split_a: "ket a = S_embed S (ket a) + not_S_embed S (ket a)"
using S_embed_not_S_embed_add by auto
have ?case (is "?left = ?right") if "b ∈ list_to_l ` has_bits_upto n"
proof -
have "Proj (ccspan (ket ` list_to_l ` has_bits_upto n)) *⇩V ket b = ket b"
using that by (simp add: Proj_fixes_image ccspan_superset')
then have Proj: "Proj_ket_upto (has_bits_upto n) *⇩V ket (a,b) = ket (a,b)"
unfolding proj_classical_set_def Proj_ket_upto_Snd Snd_def
by (auto simp add: tensor_op_ell2 tensor_ell2_ket[symmetric])
have proj_Suc: "proj_classical_set (list_to_l ` has_bits_upto (Suc n)) *⇩V ket b = ket b"
unfolding proj_classical_set_def by (metis has_bits_upto_incl image_mono le_simps(1)
less_Suc_eq proj_classical_set_def proj_classical_set_elem subset_eq that)
have proj_Suc_flip: "proj_classical_set (list_to_l ` has_bits_upto (Suc n)) *⇩V ket (flip n b) =
ket (flip n b)"
using list_to_l_has_bits_upto_flip[OF that ‹n<d›] by (auto simp add: proj_classical_set_elem)
have "?left = US S n *⇩V ket (a, b)" using Proj by auto
also have "… = (S_embed S *⇩V ket a) ⊗⇩s ket (flip n b) + ((not_S_embed S *⇩V ket a) ⊗⇩s ket b)"
using US_ket_split Ub_ket by auto
also have "… = ((S_embed S *⇩V ket a) ⊗⇩s
proj_classical_set (list_to_l ` has_bits_upto (Suc n)) *⇩V ket (flip n b) +
((not_S_embed S *⇩V ket a) ⊗⇩s proj_classical_set (list_to_l ` has_bits_upto (Suc n)) *⇩V ket b))"
unfolding proj_Suc proj_Suc_flip by auto
also have "… = (Proj_ket_upto (has_bits_upto (Suc n)) o⇩C⇩L US S n) *⇩V ket (a,b)"
unfolding Proj_ket_upto_Snd Snd_def US_def
by (auto simp add: tensor_op_ell2 cblinfun.add_right cblinfun.add_left tensor_ell2_ket[symmetric]
Ub_ket)
also have "… = ?right" using Proj by auto
finally show ?thesis by blast
qed
moreover have ?case (is "?left = ?right") if "¬ (b ∈ list_to_l ` has_bits_upto n)"
proof -
have "b ∉ list_to_l ` has_bits_upto n" using that by auto
then have proj: "proj_classical_set (list_to_l ` has_bits_upto n) *⇩V ket b = 0"
unfolding proj_classical_set_def by (intro Proj_0_compl, intro mem_ortho_ccspanI) auto
then have Proj:"Proj_ket_upto (has_bits_upto n) *⇩V ket(a,b) = 0"
unfolding Proj_ket_upto_Snd Snd_def by (auto simp add: tensor_ell2_ket[symmetric] tensor_op_ell2)
then have "?left = 0" by auto
moreover have "?right = 0" using Proj by auto
ultimately show ?thesis by auto
qed
ultimately show ?case by (cases "b ∈ list_to_l ` has_bits_upto n", auto)
qed
lemma run_pure_adv_projection:
assumes "n<d+1"
and ρ: "ρ = run_pure_adv_tc n (λm. if m<n+1 then Fst (UA m) else UB m) (US S) init_B X_for_B Y_for_B H"
shows "sandwich_tc (Proj_ket_upto (has_bits_upto n)) ρ = ρ"
using assms proof (induct n arbitrary: ρ)
case 0
let ?P = "proj_classical_set (list_to_l ` has_bits_upto 0)"
have "sandwich (Snd ?P) (selfbutter init_B) = selfbutter init_B"
unfolding init_B_def Proj_ket_upto_Snd[symmetric]
by (metis Proj_ket_upto_vec empty_list_has_bits_upto empty_list_to_l selfbutter_sandwich)
then have "from_trace_class (sandwich_tc (Snd ?P) (tc_selfbutter init_B)) =
from_trace_class (tc_selfbutter init_B)"
unfolding from_trace_class_sandwich_tc from_trace_class_tc_selfbutter by auto
then have sand: "sandwich_tc (Snd ?P) (tc_selfbutter init_B) = tc_selfbutter init_B"
using from_trace_class_inject by blast
have *: "(if (0::nat)<0+1 then Fst (UA 0) else UB 0) = Fst (UA 0)" by auto
have "sandwich_tc (Proj_ket_upto (has_bits_upto 0)) ρ =
sandwich_tc (Fst (UA 0)) (sandwich_tc (Snd ?P) (tc_selfbutter init_B))"
unfolding Proj_ket_upto_Snd 0 run_pure_adv_tc.simps(1) unfolding *
by (metis Fst_def Snd_def from_trace_class_inject from_trace_class_sandwich_tc id_cblinfun.rep_eq
init_B_def from_trace_class_tc_selfbutter selfbutter_sandwich tensor_op_ell2)
also have "… = sandwich_tc (Fst (UA 0)) (tc_selfbutter init_B)"
unfolding sand by auto
finally show ?case unfolding 0(2) by auto
next
case (Suc n)
define run where "run = run_pure_adv_tc n (λm. if m<Suc n then Fst (UA m) else UB m) (US S)
init_B X_for_B Y_for_B H"
have *: "(λm. if m<(Suc n)+1 then Fst (UA m) else UB m) (Suc n) = Fst (UA (Suc n))" using Suc by auto
have "n<d" "n<d+1" using Suc(2) by auto
have rew: "(λm. if m < Suc (Suc n) then Fst (UA m) else UB m) =
(λm. if m < Suc n then Fst (UA m) else UB m)(Suc n:= Fst (UA(Suc n)))"
by auto
have over: "run_pure_adv_tc n (λm. if m < Suc (Suc n) then Fst (UA m) else UB m) (US S) init_B
X_for_B Y_for_B H = run" unfolding run_def rew by (intro run_pure_adv_tc_over) auto
have sand_run: "sandwich_tc (Proj_ket_upto (has_bits_upto n)) run = run" unfolding run_def
by (subst Suc(1)[OF ‹n<d+1›]) auto
have Suc': "sandwich_tc (Proj_ket_upto (has_bits_upto n)) run = run"
unfolding run_def using Suc ‹n<d+1› by auto
have "ρ = sandwich_tc (Fst (UA (Suc n)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S n o⇩C⇩L
Proj_ket_upto (has_bits_upto n)) run"
unfolding Suc(3) by (auto simp add: sand_run sandwich_tc_compose' ‹n<d› run_def[symmetric] over)
also have "… = sandwich_tc (Fst (UA (Suc n)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L
(Proj_ket_upto (has_bits_upto (Suc n)) o⇩C⇩L US S n o⇩C⇩L Proj_ket_upto (has_bits_upto n))) run"
using Proj_ket_upto_US[OF ‹n<d›] by (smt (verit, best) sandwich_tc_compose')
also have "… = sandwich_tc (Fst (UA (Suc n)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L
Proj_ket_upto (has_bits_upto (Suc n)) o⇩C⇩L US S n) run"
by (auto simp add: sand_run sandwich_tc_compose')
also have "… = sandwich_tc (Proj_ket_upto (has_bits_upto (Suc n)) o⇩C⇩L Fst (UA (Suc n)) o⇩C⇩L
((X_for_B;Y_for_B) (Uquery H)) o⇩C⇩L US S n) run"
unfolding Proj_ket_upto_Snd Snd_def UqueryH_tensor_id_cblinfunB Fst_def
by (auto simp add: comp_tensor_op sandwich_tc_compose')
also have "… = sandwich_tc (Proj_ket_upto (has_bits_upto (Suc n))) ρ"
unfolding Suc(3) by (auto simp add: sand_run sandwich_tc_compose' Suc ‹n<d› run_def[symmetric] over)
finally show ?case by auto
qed
lemma run_mixed_adv_projection_finite:
assumes "⋀i. i < n + 1 ⟹ finite (Rep_kraus_family (kf_Fst (F i)::
(('mem × 'l) ell2, ('mem × 'l) ell2, unit) kraus_family))"
and "⋀i. i < n + 1 ⟹ fst ` Rep_kraus_family (kf_Fst (F i)::
(('mem × 'l) ell2, ('mem × 'l) ell2, unit) kraus_family) ≠ {}"
assumes "n<d+1"
shows "sandwich_tc (Proj_ket_upto (has_bits_upto n))
(run_mixed_adv n (λn. kf_Fst (F n)) (US S) init_B X_for_B Y_for_B H) =
run_mixed_adv n (λn. kf_Fst (F n)) (US S) init_B X_for_B Y_for_B H"
proof -
have "sandwich_tc (Proj_ket_upto (has_bits_upto n))
(run_pure_adv_tc n x (US S) init_B X_for_B Y_for_B H) =
run_pure_adv_tc n x (US S) init_B X_for_B Y_for_B H"
if "x ∈ purify_comp_kraus n (λn. kf_Fst (F n))" for x
proof -
have *: "(⋀i. i < n + 1 ⟹ fst ` Rep_kraus_family (F i) ≠ {})"
using assms(2) unfolding fst_Rep_kf_Fst by auto
obtain UA where x:"x = (λa. if a < n+1 then Fst (UA a) else undefined)" using
purification_kf_Fst[OF * ‹x ∈ purify_comp_kraus n (λn. kf_Fst (F n))›]
by auto
show ?thesis using assms by (intro run_pure_adv_projection[of n _ UA "(λ_. undefined)" S H])
(auto simp add: x)
qed
then show ?thesis by (subst purification_run_mixed_adv[OF assms(1,2)], simp,
subst purification_run_mixed_adv[OF assms(1,2)], simp)
(use assms in ‹auto simp add: sandwich_tc_sum intro!: sum.cong›)
qed
lemma run_mixed_adv_projection:
assumes "⋀i. i < d + 1 ⟹ fst ` Rep_kraus_family (kf_Fst (F i)::
(('mem × 'l) ell2, ('mem × 'l) ell2, unit) kraus_family) ≠ {}"
assumes "n<d+1"
shows "sandwich_tc (Proj_ket_upto (has_bits_upto n))
(run_mixed_adv n (λn. kf_Fst (F n)) (US S) init_B X_for_B Y_for_B H) =
run_mixed_adv n (λn. kf_Fst (F n)) (US S) init_B X_for_B Y_for_B H"
proof -
define ρ where "ρ = run_mixed_adv n (λn. kf_Fst (F n)) (US S) init_B X_for_B Y_for_B H"
define ρsum where
"ρsum F' = run_mixed_adv n (λn. kf_Fst (F' n)) (US S) init_B X_for_B Y_for_B H" for F'
have ρ_has_sum': "((λF'. run_mixed_adv n F' (US S) init_B X_for_B Y_for_B H) has_sum ρ)
(finite_kraus_subadv (λm. kf_Fst (F m)) n)"
unfolding ρ_def using run_mixed_adv_has_sum by blast
then have ρ_has_sum: "(ρsum has_sum ρ) (finite_kraus_subadv F n)"
proof -
have inj: "inj_on (λf. λn∈{0..<n+1}. kf_Fst (f n)) (finite_kraus_subadv F n)"
using inj_on_kf_Fst by auto
have rew: "ρsum = (λf. run_mixed_adv n f (US S) init_B X_for_B Y_for_B H) o
(λf. λn∈{0..<n+1}. kf_Fst (f n))" unfolding ρsum_def
using run_mixed_adv_kf_Fst_restricted[where init' = init_B and X' = X_for_B and Y'=Y_for_B]
by auto
show ?thesis unfolding rew by (subst has_sum_reindex[OF inj, symmetric])
(unfold finite_kraus_subadv_Fst_invert[symmetric], rule ρ_has_sum')
qed
have elem: "(sandwich_tc (Proj_ket_upto (has_bits_upto n)) o ρsum) x = ρsum x"
if "x ∈ (finite_kraus_subadv F n)" for x unfolding ρsum_def o_def
proof (intro run_mixed_adv_projection_finite, goal_cases)
case (1 i)
then show ?case using finite_kf_Fst[OF fin_subadv_fin_Rep_kraus_family[OF that]] assms
by auto
next
case (2 i)
then show ?case using fin_subadv_nonzero[OF that] assms
unfolding fst_Rep_kf_Fst by auto
qed (use assms in ‹auto›)
have sand_has_sum_rho: "(sandwich_tc (Proj_ket_upto (has_bits_upto n)) o ρsum has_sum ρ)
(finite_kraus_subadv (F) n)"
by (subst has_sum_cong[where g = ρsum]) (use elem ρ_has_sum in ‹auto›)
have sand_has_sum_sand: "(sandwich_tc (Proj_ket_upto (has_bits_upto n)) o ρsum has_sum
(sandwich_tc (Proj_ket_upto (has_bits_upto n)) ρ))
(finite_kraus_subadv (F) n)" by (intro sandwich_tc_has_sum[OF ρ_has_sum])
have "sandwich_tc (Proj_ket_upto (has_bits_upto n)) ρ = ρ"
using has_sum_unique[OF sand_has_sum_sand sand_has_sum_rho] by auto
then show ?thesis unfolding ρ_def by auto
qed
text ‹Lemmas of commutation with non-Find event›
lemma Proj_commutes_with_Uquery:
"Snd (selfbutter (ket empty)) o⇩C⇩L (X_for_B;Y_for_B) (Uquery G) =
(X_for_B;Y_for_B) (Uquery G) o⇩C⇩L Snd (selfbutter (ket empty))"
unfolding Snd_def by (simp add: UqueryH_tensor_id_cblinfunB comp_tensor_op)
lemma run_mixed_adv_G_H_same:
assumes "(H,G,S,z)∈carrier" "n<d+1"
shows "sandwich_tc (Snd (selfbutter (ket empty)))
(run_mixed_adv n (λn. kf_Fst (E n)) (US S) init_B X_for_B Y_for_B H) =
sandwich_tc (Snd (selfbutter (ket empty)))
(run_mixed_adv n (λn. kf_Fst (E n)) (US S) init_B X_for_B Y_for_B G)"
using assms(2) proof (induct n)
case (Suc n)
have "n<d" "n<Suc d" using Suc by auto
let ?P = "Snd (selfbutter (ket empty))"
let ?P' = "Proj_ket_upto (has_bits_upto n)"
let ?ρ = "(λx Y. (run_mixed_adv x (λn. kf_Fst (E n)) (US S) init_B X_for_B Y_for_B Y))"
have "sandwich_tc ?P (?ρ (Suc n) H) = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc (?P o⇩C⇩L (X_for_B;Y_for_B) (Uquery H) o⇩C⇩L US S n) (?ρ n H))"
using sandwich_tc_kf_apply_Fst by (auto simp add: sandwich_tc_compose')
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc ((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L ?P o⇩C⇩L US S n o⇩C⇩L ?P') (?ρ n H))"
by (subst Proj_commutes_with_Uquery, subst run_mixed_adv_projection[symmetric])
(auto simp add: Fst_E_nonzero sandwich_tc_compose' ‹n<Suc d›)
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc ((X_for_B;Y_for_B) (Uquery H) o⇩C⇩L Fst (not_S_embed S) o⇩C⇩L ?P) (?ρ n H))"
using selfbutter_empty_US_Proj_ket_upto[OF ‹n<d›]
by (metis (no_types, lifting) sandwich_tc_compose')
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc ((X_for_B;Y_for_B) (Uquery G) o⇩C⇩L Fst (not_S_embed S) o⇩C⇩L ?P) (?ρ n H))"
using Uquery_G_H_same_on_not_S_embed_tensor assms by auto
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc ((X_for_B;Y_for_B) (Uquery G) o⇩C⇩L Fst (not_S_embed S) o⇩C⇩L ?P) (?ρ n G))"
using Suc by (auto simp add: sandwich_tc_compose')
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc ((X_for_B;Y_for_B) (Uquery G) o⇩C⇩L ?P o⇩C⇩L US S n o⇩C⇩L ?P') (?ρ n G))"
using selfbutter_empty_US_Proj_ket_upto[OF ‹n<d›]
by (metis (no_types, lifting) sandwich_tc_compose')
also have "… = kf_apply (kf_Fst (E (Suc n)))
(sandwich_tc (?P o⇩C⇩L (X_for_B;Y_for_B) (Uquery G) o⇩C⇩L US S n) (?ρ n G))"
by (subst Proj_commutes_with_Uquery, subst (2) run_mixed_adv_projection[symmetric])
(auto simp add: Fst_E_nonzero sandwich_tc_compose' ‹n<Suc d›)
also have "… = sandwich_tc ?P (?ρ (Suc n) G)"
using sandwich_tc_kf_apply_Fst[symmetric] by (auto simp add: sandwich_tc_compose')
finally show ?case by auto
qed auto
lemma run_mixed_B_G_H_same:
assumes "(H,G,S,z)∈carrier"
shows "sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E H S) =
sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E G S)"
proof -
have "sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E H S) =
sandwich_tc (Q ⊗⇩o id_cblinfun) (sandwich_tc (Snd (selfbutter (ket empty)))
(run_mixed_adv d (λn. kf_Fst (E n)) (US S) init_B X_for_B Y_for_B H))"
unfolding run_mixed_B_def
by (auto simp add: sandwich_tc_compose'[symmetric] Snd_def comp_tensor_op)
also have "… = sandwich_tc (Q ⊗⇩o id_cblinfun) (sandwich_tc (Snd (selfbutter (ket empty)))
(run_mixed_adv d (λn. kf_Fst (E n)) (US S) init_B X_for_B Y_for_B G))"
using run_mixed_adv_G_H_same[where n=d, OF assms] by auto
also have "… = sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E G S)"
unfolding run_mixed_B_def
by (auto simp add: sandwich_tc_compose'[symmetric] Snd_def comp_tensor_op)
finally show ?thesis by auto
qed
lemma ρright_G_H_same:
"sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (mixed_H.ρright E) =
sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (mixed_G.ρright E)"
proof -
have "sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (mixed_H.ρright E) =
(∑(H,G,S,z)∈carrier. distr (H,G,S,z) *⇩C
sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E H S))"
unfolding mixed_H.ρright_def unfolding carrier_H_def distr_H_def
by (subst sum.reindex) (auto simp add: inj_on_def case_prod_beta sandwich_tc_sum
sandwich_tc_scaleC_right intro!: sum.cong)
also have "… = (∑(H,G,S,z)∈carrier. distr (H,G,S,z) *⇩C
sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (run_mixed_B E G S))"
using run_mixed_B_G_H_same by (auto intro!: sum.cong)
also have "… = sandwich_tc (Q ⊗⇩o selfbutter (ket empty)) (mixed_G.ρright E)"
unfolding mixed_G.ρright_def unfolding carrier_G_def distr_G_def
by (subst sum.reindex) (auto simp add: inj_on_def case_prod_beta sandwich_tc_sum
sandwich_tc_scaleC_right intro!: sum.cong)
finally show ?thesis by auto
qed
lemma trace_compose_tcr_H_G_same:
"trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E)) =
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
proof -
have "trace (from_trace_class
(compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E)) o⇩C⇩L (Snd (selfbutter (ket empty)))*) =
trace (from_trace_class
(compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E)) o⇩C⇩L (Snd (selfbutter (ket empty)))*)"
by (metis (no_types, opaque_lifting) Snd_def ρright_G_H_same compose_tcr.rep_eq
from_trace_class_sandwich_tc sandwich_apply)
then have "trace (from_trace_class
(compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E))) =
trace (from_trace_class
(compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E)))"
by (smt (verit, best) Snd_def butterfly_is_Proj cblinfun_assoc_left(1) circularity_of_trace
compose_tcr.rep_eq is_Proj_algebraic is_Proj_id is_Proj_tensor_op norm_ket
trace_class_from_trace_class)
then show ?thesis unfolding trace_tc.rep_eq by auto
qed
text ‹The probability of not Find and the adversary succeeding for H\S and G\S are the same.
$Pr [b \and \not Find:b\leftarrow A^{H\backslash S}(z)] =
Pr [b \and \not Find:b\leftarrow A^{G\backslash S}(z)]$›
lemma Pright_G_H_same:
"mixed_H.Pright (Q ⊗⇩o selfbutter (ket empty)) = mixed_G.Pright (Q ⊗⇩o selfbutter (ket empty))"
unfolding mixed_H.Pright_def mixed_G.Pright_def mixed_G.PM_altdef
using ρright_G_H_same[where Q = Q] by auto
text ‹The finding event occurs with the same probability for G and H
if the overall norm stays the same.›
lemma Pfind_G_H_same:
assumes "norm (mixed_H.ρright E) = norm (mixed_G.ρright E)"
shows "mixed_H.Pfind E = mixed_G.Pfind E"
proof -
have "mixed_H.Pfind E = trace_tc (compose_tcr
(id_cblinfun - Snd (selfbutter (ket empty))::('mem×'l) update) (mixed_H.ρright E))"
unfolding mixed_H.Pfind_def mixed_G.end_measure_def Snd_def
by (auto simp add: tensor_op_right_minus)
also have "… = trace_tc (mixed_H.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E))"
by (simp add: compose_tcr.diff_left trace_tc_minus)
also have "… = norm (mixed_H.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E))"
by (simp add: mixed_H.ρright_pos norm_tc_pos)
also have "… = norm (mixed_G.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
unfolding assms using trace_compose_tcr_H_G_same by auto
also have "… = trace_tc (mixed_G.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
by (simp add: mixed_G.ρright_pos norm_tc_pos)
also have "… = trace_tc (compose_tcr
(id_cblinfun - Snd (selfbutter (ket empty))::('mem×'l) update) (mixed_G.ρright E))"
by (simp add: compose_tcr.diff_left trace_tc_minus)
also have "… = mixed_G.Pfind E"
unfolding mixed_G.Pfind_def mixed_G.end_measure_def Snd_def
by (auto simp add: tensor_op_right_minus)
finally show ?thesis by auto
qed
lemma Pfind_G_H_same_nonterm:
shows "(mixed_H.Pfind E - mixed_G.Pfind E) =
(norm (mixed_H.ρright E) - norm (mixed_G.ρright E))"
proof -
have "mixed_H.Pfind E = trace_tc (compose_tcr
(id_cblinfun - Snd (selfbutter (ket empty))::('mem×'l) update) (mixed_H.ρright E))"
unfolding mixed_H.Pfind_def mixed_G.end_measure_def Snd_def
by (auto simp add: tensor_op_right_minus)
also have "… = trace_tc (mixed_H.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E))"
by (simp add: compose_tcr.diff_left trace_tc_minus)
also have "… = norm (mixed_H.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_H.ρright E))"
by (simp add: mixed_H.ρright_pos norm_tc_pos)
finally have H: "mixed_H.Pfind E = norm (mixed_H.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
using trace_compose_tcr_H_G_same by auto
have "mixed_G.Pfind E = trace_tc (compose_tcr
(id_cblinfun - Snd (selfbutter (ket empty))::('mem×'l) update) (mixed_G.ρright E))"
unfolding mixed_G.Pfind_def mixed_G.end_measure_def Snd_def
by (auto simp add: tensor_op_right_minus)
also have "… = trace_tc (mixed_G.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
by (simp add: compose_tcr.diff_left trace_tc_minus)
finally have G: "mixed_G.Pfind E = norm (mixed_G.ρright E) -
trace_tc (compose_tcr (Snd (selfbutter (ket empty))) (mixed_G.ρright E))"
by (simp add: mixed_G.ρright_pos norm_tc_pos)
show ?thesis unfolding H G using complex_of_real_abs by auto
qed
text ‹The general version of the O2H with non-termination part.›
theorem mixed_o2h_nonterm:
shows
"¦mixed_H.Pleft P - mixed_G.Pleft P¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)
+ 2 * sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pleft P)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)
+ sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
proof -
let ?P = "P ⊗⇩o selfbutter (ket empty)"
have norm_P: "norm ?P ≤ 1"
by (simp add: butterfly_is_Proj is_Proj_tensor_op mixed_G.is_Proj_P norm_is_Proj)
have "¦mixed_H.Pleft P - mixed_G.Pleft P¦ =
¦mixed_H.Pleft' ?P - mixed_H.Pright ?P + mixed_G.Pright ?P - mixed_G.Pleft' ?P¦"
using Pright_G_H_same unfolding mixed_G.Pleft_Pleft'_empty mixed_H.Pleft_Pleft'_empty by auto
also have "… ≤ ¦mixed_H.Pleft' ?P - mixed_H.Pright ?P¦ +
¦mixed_G.Pleft' ?P - mixed_G.Pright ?P¦" by linarith
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E) +
2 * sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
using mixed_H.estimate_Pfind[OF norm_P] mixed_G.estimate_Pfind[OF norm_P]
by auto
finally show "¦mixed_H.Pleft P - mixed_G.Pleft P¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)
+ 2 * sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
by auto
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pleft P)¦ =
¦sqrt (mixed_H.Pleft' ?P) - sqrt (mixed_H.Pright ?P) +
sqrt (mixed_G.Pright ?P) - sqrt (mixed_G.Pleft' ?P)¦"
using Pright_G_H_same unfolding mixed_G.Pleft_Pleft'_empty mixed_H.Pleft_Pleft'_empty by auto
also have "… ≤ ¦sqrt (mixed_H.Pleft' ?P) - sqrt (mixed_H.Pright ?P)¦ +
¦sqrt (mixed_G.Pleft' ?P) - sqrt (mixed_G.Pright ?P)¦" by linarith
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)
+ sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_P] mixed_G.estimate_Pfind_sqrt[OF norm_P]
by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pleft P)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)
+ sqrt ((d+1) * Re (mixed_G.Pfind E) + d* mixed_G.P_nonterm E)"
by auto
qed
text ‹The general version of the O2H with terminating adversary. This formulation corresponds to
Theorem 1.›
theorem mixed_o2h_term:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_G.Pleft P¦ ≤ 4 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pleft P)¦ ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have normGright: "norm (mixed_G.ρright E) = 1"
by (rule mixed_G.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normGcount: "norm (mixed_G.ρcount E) = 1"
by (rule mixed_G.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have norm: "norm (mixed_H.ρright E) = norm (mixed_G.ρright E)" using normHright normGright by auto
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
have terminG: "mixed_G.P_nonterm E = 0"
unfolding mixed_G.P_nonterm_def using normGright normGcount
by (smt (verit, del_insts) Re_complex_of_real mixed_G.ρcount_pos mixed_G.ρright_pos norm_eq_zero
norm_le_zero_iff norm_of_real norm_pths(2) norm_tc_pos)
show "¦mixed_H.Pleft P - mixed_G.Pleft P¦ ≤ 4 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm(1) Pfind_G_H_same[OF norm] terminH terminG by auto
show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pleft P)¦ ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm(2) Pfind_G_H_same[OF norm] terminH terminG by auto
qed
text ‹Other formulations of the mixed o2h.›
text ‹Theorem 1, definition of Pright (2)›
definition Proj_2 :: "('mem × 'l) ell2 ⇒⇩C⇩L ('mem × 'l) ell2" where
"Proj_2 = P ⊗⇩o id_cblinfun"
lemma norm_Proj_2:
"norm Proj_2 ≤ 1"
unfolding Proj_2_def using mixed_H.norm_P by (simp add: tensor_op_norm)
theorem mixed_o2h_nonterm_2:
shows
"¦mixed_H.Pleft P - mixed_H.Pright Proj_2¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_2)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
proof -
have "¦mixed_H.Pleft P - mixed_H.Pright Proj_2¦ =
¦mixed_H.Pleft' Proj_2 - mixed_H.Pright Proj_2¦"
unfolding mixed_H.Pleft_Pleft'_id Proj_2_def by auto
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind[OF norm_Proj_2] by auto
finally show "¦mixed_H.Pleft P - mixed_H.Pright Proj_2¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_2)¦ =
¦sqrt (mixed_H.Pleft' Proj_2) - sqrt (mixed_H.Pright Proj_2)¦"
unfolding mixed_H.Pleft_Pleft'_id Proj_2_def by auto
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_Proj_2] by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_2)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
qed
theorem mixed_o2h_term_2:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_H.Pright Proj_2¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_2)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
show "¦mixed_H.Pleft P - mixed_H.Pright Proj_2¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_2(1) terminH by auto
show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_2)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_2(2) terminH by auto
qed
text ‹Theorem 1, definition of Pright (3)›
definition Proj_3 :: "('mem × 'l) ell2 ⇒⇩C⇩L ('mem × 'l) ell2" where
"Proj_3 = P ⊗⇩o selfbutter (ket empty)"
lemma is_Proj_3:
"is_Proj Proj_3"
unfolding Proj_3_def
by (simp add: butterfly_is_Proj is_Proj_tensor_op mixed_G.is_Proj_P)
lemma Proj_3_altdef:
"Proj_3 = Proj ((P ⊗⇩o id_cblinfun) *⇩S ⊤ ⊔ (id_cblinfun ⊗⇩o selfbutter (ket empty)) *⇩S ⊤)"
oops
lemma norm_Proj_3:
"norm Proj_3 ≤ 1"
unfolding Proj_3_def using mixed_H.norm_P by (simp add: norm_butterfly tensor_op_norm)
theorem mixed_o2h_nonterm_3:
shows
"¦mixed_H.Pleft P - mixed_H.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
proof -
have "¦mixed_H.Pleft P - mixed_H.Pright Proj_3¦ =
¦mixed_H.Pleft' Proj_3 - mixed_H.Pright Proj_3¦"
unfolding mixed_H.Pleft_Pleft'_empty Proj_3_def by auto
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind[OF norm_Proj_3] by auto
finally show "¦mixed_H.Pleft P - mixed_H.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_3)¦ =
¦sqrt (mixed_H.Pleft' Proj_3) - sqrt (mixed_H.Pright Proj_3)¦"
unfolding mixed_H.Pleft_Pleft'_empty Proj_3_def by auto
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_Proj_3] by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
qed
theorem mixed_o2h_term_3:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_H.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
show "¦mixed_H.Pleft P - mixed_H.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_3(1) terminH by auto
show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_3(2) terminH by auto
qed
text ‹Theorem 1, definition of Pright (4)›
theorem mixed_o2h_nonterm_4:
shows
"¦mixed_H.Pleft P - mixed_G.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
proof -
have "¦mixed_H.Pleft P - mixed_G.Pright Proj_3¦ =
¦mixed_H.Pleft' Proj_3 - mixed_H.Pright Proj_3¦"
using Pright_G_H_same unfolding mixed_G.Pleft_Pleft'_empty mixed_H.Pleft_Pleft'_empty
Proj_3_def by auto
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind[OF norm_Proj_3]
by auto
finally show "¦mixed_H.Pleft P - mixed_G.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_3)¦ =
¦sqrt (mixed_H.Pleft' Proj_3) - sqrt (mixed_H.Pright Proj_3)¦"
using Pright_G_H_same unfolding mixed_G.Pleft_Pleft'_empty mixed_H.Pleft_Pleft'_empty
Proj_3_def by auto
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_Proj_3] by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
qed
theorem mixed_o2h_term_4:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_G.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
show"¦mixed_H.Pleft P - mixed_G.Pright Proj_3¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_4(1) terminH by auto
show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_3)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_4(2) terminH by auto
qed
text ‹Theorem 1: the definition of Pright (5) is
‹Pright = P[find ∨ b=1 for b<- A^{H\S}] = P(find for b<- A^{H\S}) + P(¬ find ∧ b=1 for b<- A^{H\S})›
Careful: In general, we cannot state quantum events with and or or. However, in the case that the
two projectors commute, we may say
‹Pr(A ∧ B) ≡ PM_A o PM_B›
‹Pr(A ∨ B) ≡ PM_A + PM_B - PM_A o PM_B›
Still, for the projection, we need to joint the two projective spaces.
›
definition Proj_5 :: "('mem × 'l) ell2 ⇒⇩C⇩L ('mem × 'l) ell2" where
"Proj_5 = Proj (((P ⊗⇩o id_cblinfun) *⇩S ⊤) ⊔ ((id_cblinfun ⊗⇩o (id_cblinfun - selfbutter (ket empty))) *⇩S ⊤))"
lemma is_Proj_5:
"is_Proj Proj_5"
unfolding Proj_5_def by (simp)
lemma Proj_5_altdef:
"Proj_5 = Proj_3 + mixed_H.end_measure"
unfolding Proj_5_def Proj_3_def by (subst splitting_Proj_or[OF mixed_H.is_Proj_P])
(auto simp add: mixed_G.end_measure_def Snd_def butterfly_is_Proj)
lemma norm_Proj_5:
"norm Proj_5 ≤ 1"
unfolding Proj_5_def by (simp add: norm_is_Proj)
theorem mixed_o2h_nonterm_5:
shows
"¦mixed_H.Pleft P - (mixed_H.Pright Proj_5)¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
proof -
have "¦mixed_H.Pleft P - mixed_H.Pright Proj_5¦ =
¦mixed_H.Pleft' Proj_5 - mixed_H.Pright Proj_5¦"
unfolding Proj_5_altdef Proj_3_def mixed_H.Pleft_Pleft'_case5[OF mixed_H.is_Proj_P]
mixed_H.Pfind_Pright Fst_def by auto
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind[OF norm_Proj_5] by auto
finally show "¦mixed_H.Pleft P - mixed_H.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_5)¦ =
¦sqrt (mixed_H.Pleft' Proj_5) - sqrt (mixed_H.Pright Proj_5)¦"
unfolding mixed_H.Pleft_Pleft'_case5[OF mixed_H.is_Proj_P] Proj_5_altdef Proj_3_def by auto
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_Proj_5] by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
by auto
qed
theorem mixed_o2h_term_5:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_H.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
show "¦mixed_H.Pleft P - mixed_H.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_5(1) terminH by auto
show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_H.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_5(2) terminH by auto
qed
text ‹Theorem 1, definition of Pright (6)›
lemma Pright_G_H_case5_nonterm:
"mixed_H.Pright Proj_5 - mixed_G.Pright Proj_5 = norm (mixed_H.ρright E) - norm (mixed_G.ρright E)"
proof -
have "mixed_H.Pright Proj_5 - mixed_G.Pright Proj_5 =
Re (trace_tc (compose_tcr Proj_5 (mixed_H.ρright E))) -
Re (trace_tc (compose_tcr Proj_5 (mixed_G.ρright E)))"
unfolding mixed_H.Pright_def mixed_G.Pright_def mixed_H.PM_altdef mixed_G.PM_altdef
by (smt (verit, best) cblinfun_assoc_left(1) circularity_of_trace compose_tcr.rep_eq
from_trace_class_sandwich_tc is_Proj_5 is_Proj_algebraic sandwich_apply trace_class_from_trace_class
trace_tc.rep_eq)
also have "… = Re (trace_tc (compose_tcr Proj_3 (mixed_H.ρright E))) +
Re (trace_tc (compose_tcr mixed_G.end_measure (mixed_H.ρright E))) -
Re (trace_tc (compose_tcr Proj_3 (mixed_G.ρright E))) -
Re (trace_tc (compose_tcr mixed_G.end_measure (mixed_G.ρright E)))"
unfolding Proj_5_altdef by (auto simp add: compose_tcr.add_left trace_tc_plus)
also have "… = Re (trace_tc (sandwich_tc (P ⊗⇩o selfbutter (ket empty)) (mixed_H.ρright E))) +
Re (trace_tc (compose_tcr mixed_G.end_measure (mixed_H.ρright E))) -
Re (trace_tc (sandwich_tc (P ⊗⇩o selfbutter (ket empty)) (mixed_G.ρright E))) -
Re (trace_tc (compose_tcr mixed_G.end_measure (mixed_G.ρright E)))"
by (smt (verit, del_insts) Proj_3_def cblinfun_assoc_left(1) circularity_of_trace compose_tcr.rep_eq
from_trace_class_sandwich_tc is_Proj_3 is_Proj_algebraic sandwich_apply trace_class_from_trace_class
trace_tc.rep_eq)
also have "… = mixed_H.Pright Proj_3 - mixed_G.Pright Proj_3 + Re (mixed_H.Pfind E - mixed_G.Pfind E)"
by (simp add: Pright_G_H_same Proj_3_def ρright_G_H_same mixed_G.Pfind_def mixed_H.Pfind_def)
also have "… = Re (norm (mixed_H.ρright E) - norm (mixed_G.ρright E))"
unfolding Proj_3_def by (simp add: Pfind_G_H_same_nonterm Pright_G_H_same)
finally show ?thesis by auto
qed
lemma Pright_G_H_case5:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows "mixed_H.Pright Proj_5 = mixed_G.Pright Proj_5"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
moreover have normGright: "norm (mixed_G.ρright E) = 1"
by (rule mixed_G.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
ultimately show ?thesis using Pright_G_H_case5_nonterm by auto
qed
theorem mixed_o2h_nonterm_6:
shows
"¦mixed_H.Pleft P - mixed_G.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E) +
¦norm (mixed_H.ρright E) - norm (mixed_G.ρright E)¦"
proof -
have "¦mixed_H.Pleft P - mixed_G.Pright Proj_5¦ =
¦mixed_H.Pleft P - mixed_H.Pright Proj_5 + norm (mixed_H.ρright E) - norm (mixed_G.ρright E)¦"
using Pright_G_H_case5_nonterm by auto
also have "… ≤ ¦mixed_H.Pleft' Proj_5 - mixed_H.Pright Proj_5¦ +
¦norm (mixed_H.ρright E) - norm (mixed_G.ρright E)¦"
using Proj_3_def Proj_5_altdef mixed_G.is_Proj_P mixed_H.Pleft_Pleft'_case5 by force
also have "… ≤ 2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E) +
¦norm (mixed_H.ρright E) - norm (mixed_G.ρright E)¦"
using mixed_H.estimate_Pfind[OF norm_Proj_5] by auto
finally show "¦mixed_H.Pleft P - mixed_G.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E) +
¦norm (mixed_H.ρright E) - norm (mixed_G.ρright E)¦"
by auto
qed
theorem mixed_o2h_term_6:
assumes "⋀i. i<d+1 ⟹ km_trace_preserving (kf_apply (E i))"
shows
"¦mixed_H.Pleft P - mixed_G.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
and
"¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
proof -
have normHright: "norm (mixed_H.ρright E) = 1"
by (rule mixed_H.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normGright: "norm (mixed_G.ρright E) = 1"
by (rule mixed_G.trace_preserving_norm_ρright[OF trace_preserving_kf_Fst[OF assms]])
have normHcount: "norm (mixed_H.ρcount E) = 1"
by (rule mixed_H.trace_preserving_norm_ρcount[OF trace_preserving_kf_Fst[OF assms]])
have terminH: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
by (metis cmod_Re complex_of_real_nn_iff mixed_H.ρcount_pos mixed_H.ρright_pos norm_le_zero_iff
norm_pths(2) norm_tc_pos norm_zero of_real_0)
show"¦mixed_H.Pleft P - mixed_G.Pright Proj_5¦ ≤
2 * sqrt ((d+1) * Re (mixed_H.Pfind E))"
using mixed_o2h_nonterm_6(1) terminH unfolding normHright normGright by auto
have nonterm_zero: "mixed_H.P_nonterm E = 0"
unfolding mixed_H.P_nonterm_def using normHright normHcount
mixed_H.P_nonterm_def terminH by presburger
have "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_5)¦ =
¦sqrt (mixed_H.Pleft' Proj_5) - sqrt (mixed_H.Pright Proj_5)¦"
using Pright_G_H_case5[OF assms, symmetric]
unfolding mixed_H.Pleft_Pleft'_case5[OF mixed_H.is_Proj_P]
Proj_5_altdef Proj_3_def by auto
also have "… ≤ sqrt ((d+1) * Re (mixed_H.Pfind E) + d* mixed_H.P_nonterm E)"
using mixed_H.estimate_Pfind_sqrt[OF norm_Proj_5] by auto
finally show "¦sqrt (mixed_H.Pleft P) - sqrt (mixed_G.Pright Proj_5)¦ ≤
sqrt ((d+1) * Re (mixed_H.Pfind E))"
using nonterm_zero by auto
qed
end
unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax
end