Theory Limit_Process
theory Limit_Process
imports Run_Adversary
begin
unbundle cblinfun_syntax
unbundle lattice_syntax
unbundle register_syntax
section ‹Limit Processes›
text ‹We need some concept of limes of Kraus families, i.e.\ finite Kraus maps tending to a
Kraus map. Therefore, we define a filter on the Kraus family.›
text ‹‹kf_elems› is the set of Kraus maps with only one element that are part of the
original Kraus map.›
lift_definition kf_elems ::
"('a::chilbert_space, 'b::chilbert_space, unit) kraus_family ⇒ ('a, 'b, unit) kraus_family set" is
"λE. (λx. {x}) ` E"
apply (intro CollectI kraus_family_if_finite)
by (auto simp: kraus_family_def)
lemma kf_elems_Rep_kraus_family:
"kf_elems 𝔈 = (λx. Abs_kraus_family {x}) ` Rep_kraus_family 𝔈"
unfolding kf_elems_def by auto
lemma kf_elems_finite:
assumes "F ∈ kf_elems 𝔈"
shows "finite (Rep_kraus_family F)"
using assms by transfer auto
lemma kf_bound_of_elems:
assumes "F ∈ kf_elems E"
shows "kf_bound F ≤ kf_bound E"
proof -
have subset: "Rep_kraus_family F ⊆ Rep_kraus_family E" using assms by transfer auto
have "kf_bound F = (∑(E, u)∈Rep_kraus_family F. E* o⇩C⇩L E)"
using assms kf_bound_finite kf_elems_finite by blast
also have "… ≤ kf_bound E" using kf_bound_geq_sum[OF subset] by auto
finally show ?thesis by linarith
qed
lemma kf_elems_card_1:
assumes "F ∈ kf_elems E"
shows "card (Rep_kraus_family F) = 1"
using assms by transfer auto
lemma inj_on_kf_singleton:
"inj_on (λx. Abs_kraus_family {x}) (Rep_kraus_family 𝔈)"
apply (rule inj_onI)
apply (subst (asm) Abs_kraus_family_inject)
using Rep_kraus_family kraus_family_def by auto
lemma kf_apply_singleton:
fixes E :: ‹'a::chilbert_space ⇒⇩C⇩L 'b::chilbert_space × 'x›
assumes ‹fst E ≠ 0›
shows "kf_apply (Abs_kraus_family {E}) ρ = sandwich_tc (fst E) ρ"
apply (subst kf_apply.abs_eq)
using assms
apply (simp add: eq_onp_same_args)
by simp
lemma kf_apply_summable_on_kf_elems:
fixes 𝔈 :: "('a::chilbert_space,'b::chilbert_space,unit) kraus_family"
shows "(λ𝔉. kf_apply 𝔉 ρ) summable_on (kf_elems 𝔈)"
proof -
have *: ‹kf_apply (Abs_kraus_family {E}) ρ = sandwich_tc (fst E) ρ›
if ‹E ∈ Rep_kraus_family 𝔈› for E
apply (subst kf_apply_singleton)
using that Rep_kraus_family
apply (force intro!: simp: kraus_family_def)
by simp
show ?thesis
unfolding kf_elems_Rep_kraus_family
apply (subst summable_on_reindex[OF inj_on_kf_singleton])
apply (rule summable_on_cong[where g=‹λE. sandwich_tc (fst E) ρ›, THEN iffD2])
using *
apply force
using kf_apply_summable
by (force simp: case_prod_unfold)
qed
lemma kf_apply_has_sum_kf_elems:
fixes 𝔈 :: "('a::chilbert_space,'b::chilbert_space,unit) kraus_family"
shows "((λ𝔉. kf_apply 𝔉 ρ) has_sum (kf_apply 𝔈 ρ)) (kf_elems 𝔈)"
proof -
have *: ‹kf_apply (Abs_kraus_family {E}) ρ = sandwich_tc (fst E) ρ›
if ‹E ∈ Rep_kraus_family 𝔈› for E
apply (subst kf_apply_singleton)
using that Rep_kraus_family
apply (force intro!: simp: kraus_family_def)
by simp
show ?thesis
unfolding kf_elems_Rep_kraus_family
apply (subst has_sum_reindex[OF inj_on_kf_singleton])
apply (rule has_sum_cong[where g=‹λE. sandwich_tc (fst E) ρ›, THEN iffD2])
using *
apply force
by (metis (no_types, lifting) has_sum_cong kf_apply_has_sum split_def)
qed
lemma kf_apply_abs_summable_on_kf_elems:
fixes 𝔈 :: "('a::chilbert_space,'b::chilbert_space,unit) kraus_family"
shows "(λ𝔉. kf_apply 𝔉 ρ) abs_summable_on (kf_elems 𝔈)"
proof -
have *: ‹kf_apply (Abs_kraus_family {E}) ρ = sandwich_tc (fst E) ρ›
if ‹E ∈ Rep_kraus_family 𝔈› for E
apply (subst kf_apply_singleton)
using that Rep_kraus_family
apply (force intro!: simp: kraus_family_def)
by simp
show ?thesis
unfolding kf_elems_Rep_kraus_family
apply (subst summable_on_reindex[OF inj_on_kf_singleton])
apply (subst o_def)
apply (rule summable_on_cong[where g=‹λE. norm (sandwich_tc (fst E) ρ)›, THEN iffD2])
using *
apply force
using Rep_kraus_family kf_apply_abs_summable
by (force simp: case_prod_unfold)
qed
text ‹Now, we can define a sub-adversary. An adversary is modeled by a sequence of $n$ Kraus maps.
A sub-adversary is then defined as a sequence of $n$ elements of the respective Kraus maps.
Adding all sub-adversaries together yields the original Kraus map.›
definition finite_kraus_subadv :: "'a kraus_adv ⇒ nat ⇒ 'a kraus_adv set" where
"finite_kraus_subadv 𝔈 n = PiE {0..<n+1} (λi. kf_elems (𝔈 i))"
lemma finite_kraus_subadv_I:
assumes "f ∈ finite_kraus_subadv 𝔈 n" "i<n+1"
shows "f i ∈ kf_elems (𝔈 i)"
using assms unfolding finite_kraus_subadv_def by auto
lemma finite_kraus_subadv_rewrite:
"finite_kraus_subadv 𝔈 (Suc n) =
(λ(x,f). fun_upd f (Suc n) x) ` (kf_elems (𝔈 (Suc n)) × finite_kraus_subadv 𝔈 n)"
by (metis PiE_insert_eq Suc_eq_plus1 finite_kraus_subadv_def set_upt_Suc)
lemma finite_kraus_subadv_rewrite_inj:
"inj_on (λ(x, f). f(Suc n := x)) (kf_elems (𝔈 (Suc n)) × finite_kraus_subadv 𝔈 n)"
unfolding inj_on_def proof (safe, goal_cases)
case (1 a b aa ba) then show ?case by (metis fun_upd_eqD)
next
case (2 a b aa b')
then have "b x = b' x" if "x<Suc n" for x
by (metis fun_upd_eqD fun_upd_triv fun_upd_twist nat_neq_iff that)
moreover have "b x = undefined" and "b' x = undefined" if "x ≥ Suc n" for x
using 2(2,4) unfolding finite_kraus_subadv_def
by (metis PiE_arb Suc_eq_plus1 atLeastLessThan_iff not_le that)+
ultimately show ?case by (intro ext) (metis not_le)
qed
lemma norm_kf_apply_singleton_trace_tc:
assumes "0 ≤ ρ" and ‹fst x ≠ 0›
shows "norm (kf_apply (Abs_kraus_family {x}) ρ) = trace_tc (sandwich_tc (fst x) ρ)"
apply (subst norm_tc_pos)
apply (rule kf_apply_pos[OF assms(1)])
using kf_apply_singleton
apply (subst kf_apply_singleton)
using assms by auto
lemma infsum_norm_kf_apply_step:
assumes ρn_summable: "ρn summable_on finite_kraus_subadv 𝔈 n"
and pos: "⋀x. x ∈ finite_kraus_subadv 𝔈 n ⟹ 0 ≤ ρn x"
shows "(λx. ∑⇩∞y∈finite_kraus_subadv 𝔈 n. norm (kf_apply x (ρn y)))
abs_summable_on kf_elems (𝔈 (Suc n))"
proof -
define ρ where "ρ = infsum ρn (finite_kraus_subadv 𝔈 n)"
have "((λy. trace_tc (sandwich_tc E y)) o (λy. ρn y) has_sum trace_tc (sandwich_tc E ρ))
(finite_kraus_subadv 𝔈 n)" for E::"'a ell2 ⇒⇩C⇩L 'a ell2"
unfolding o_def by (subst has_sum_bounded_linear[OF bounded_linear_trace_norm_sandwich_tc])
(auto simp add: ρ_def ρn_summable)
then have sandwich_tc_lim: "(∑⇩∞y∈finite_kraus_subadv 𝔈 n. trace_tc (sandwich_tc E (ρn y))) =
trace_tc (sandwich_tc E (∑⇩∞y∈finite_kraus_subadv 𝔈 n. ρn y))"
for E::"'a ell2 ⇒⇩C⇩L 'a ell2"
by (intro infsumI) (auto simp add: o_def ρ_def)
let ?f1 = "(λ(E,x). ¦∑⇩∞y∈finite_kraus_subadv 𝔈 n. trace_tc (sandwich_tc E (ρn y))¦)"
let ?f2 = "(λx. ¦∑⇩∞y∈finite_kraus_subadv 𝔈 n. norm (kf_apply (Abs_kraus_family {x}) (ρn y))¦)"
have "(λ(E, x). sandwich_tc E ρ) abs_summable_on Rep_kraus_family (𝔈 (Suc n))"
using Rep_kraus_family kf_apply_abs_summable by blast
then have f1_summable: "?f1 summable_on Rep_kraus_family (𝔈 (Suc n))"
unfolding sandwich_tc_lim ρ_def[symmetric] using trace_tc_abs_summable_on o_def
by (metis (mono_tags, lifting) abs_summable_summable norm_abs split_def summable_on_cong)
then have "?f2 summable_on Rep_kraus_family (𝔈 (Suc n))"
proof -
have "(?f1 summable_on Rep_kraus_family (𝔈 (Suc n))) = (?f2 summable_on Rep_kraus_family (𝔈 (Suc n)))"
proof (subst summable_on_cong[of "Rep_kraus_family (𝔈 (Suc n))" ?f1 ?f2], goal_cases)
case (1 x)
then have neq0: ‹fst x ≠ 0›
using Rep_kraus_family
by (force simp: kraus_family_def)
have infsum: "(∑⇩∞y∈finite_kraus_subadv 𝔈 n. trace_tc (sandwich_tc (fst x) (ρn y))) =
(∑⇩∞y∈finite_kraus_subadv 𝔈 n. norm (kf_apply (Abs_kraus_family {x}) (ρn y)))"
apply (subst infsum_of_real[symmetric])
apply (rule infsum_cong)
apply (subst norm_kf_apply_singleton_trace_tc)
using pos neq0 by auto
then show ?case by (auto simp add: split_def abs_complex_def)
next
case 2
then show ?case using summable_on_iff_abs_summable_on_complex by force
qed
then show ?thesis using f1_summable by auto
qed
then show ?thesis unfolding kf_elems_Rep_kraus_family
by (subst summable_on_reindex[OF inj_on_kf_singleton])
(use kf_apply_singleton in ‹auto simp add: o_def› )
qed
text ‹Run of adversary is summable on sub-adversaries.›
lemma run_mixed_adv_greater_indifferent:
assumes "m > n"
shows "run_mixed_adv n (f(m := x)) UB init X Y H = run_mixed_adv n f UB init X Y H"
using assms by (induct n arbitrary: f m) auto
lemma run_mixed_adv_Suc_indifferent:
"run_mixed_adv n (f(Suc n := x)) UB init X Y H = run_mixed_adv n f UB init X Y H"
by (intro run_mixed_adv_greater_indifferent) auto
lemma run_mixed_adv_abs_summable:
fixes 𝔈 :: "'a kraus_adv"
shows "(λf. run_mixed_adv n f UB init X Y H) abs_summable_on (finite_kraus_subadv 𝔈 n)"
proof (induct n)
case 0
have "inj_on (λf. f 0) (Π⇩E i∈{0}. kf_elems (𝔈 i))"
unfolding PiE_over_singleton_iff inj_on_def by auto
then have inj: "inj_on (λf. f 0) (finite_kraus_subadv 𝔈 0)"
unfolding finite_kraus_subadv_def by simp
have "(λ𝔉. kf_apply 𝔉 (tc_selfbutter init)) abs_summable_on
(kf_elems (𝔈 0))" using kf_apply_abs_summable_on_kf_elems by auto
moreover {
have "x ∈ kf_elems (𝔈 0) ⟹
x ∈ (λx. x 0) ` (Π⇩E i∈{0}. kf_elems (𝔈 i))" for x
unfolding PiE_over_singleton_iff by (simp add: image_iff)
then have "(λf. f 0) ` finite_kraus_subadv 𝔈 0 = kf_elems (𝔈 0)"
by (auto simp add: finite_kraus_subadv_I finite_kraus_subadv_def)
}
ultimately have "(λ𝔉. kf_apply 𝔉 (tc_selfbutter init)) o (λf. f 0) abs_summable_on (finite_kraus_subadv 𝔈 0)"
by (subst abs_summable_on_reindex[OF inj, symmetric]) auto
then show ?case by auto
next
case (Suc n)
define ρn where "ρn f = sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n)(run_mixed_adv n f UB init X Y H)"
for f
have ρn_Suc_indiff:"ρn (f(Suc n := x)) = ρn f" for f x
unfolding ρn_def run_mixed_adv_Suc_indifferent by auto
have ρn_abs_summable_on:
"(λf. ρn f) abs_summable_on finite_kraus_subadv 𝔈 n"
unfolding ρn_def using sandwich_tc_abs_summable_on[OF Suc] by (auto simp add: o_def)
have one: "(λxa. kf_apply x (ρn (xa(Suc n := x)))) abs_summable_on finite_kraus_subadv 𝔈 n"
if "x ∈ kf_elems (𝔈 (Suc n))" for x
using ρn_Suc_indiff ρn_abs_summable_on finite_kf_apply_abs_summable_on by fastforce
have ρn_summable: "ρn summable_on finite_kraus_subadv 𝔈 n"
using Suc ρn_def ρn_abs_summable_on abs_summable_summable by blast
have pos: "x ∈ finite_kraus_subadv 𝔈 n ⟹ 0 ≤ ρn x" for x
by (simp add: ρn_def run_mixed_adv_pos sandwich_tc_pos)
have two: "(λx. ∑⇩∞y∈finite_kraus_subadv 𝔈 n. norm (kf_apply x (ρn (y(Suc n := x)))))
abs_summable_on kf_elems (𝔈 (Suc n))"
unfolding ρn_Suc_indiff by (rule infsum_norm_kf_apply_step[OF ρn_summable pos])
have lim: "(λx. kf_apply (x (Suc n)) (ρn x)) abs_summable_on finite_kraus_subadv 𝔈 (Suc n)"
apply (subst finite_kraus_subadv_rewrite)
apply (subst abs_summable_on_reindex[OF finite_kraus_subadv_rewrite_inj])
apply (unfold o_def case_prod_beta)
apply (subst abs_summable_on_Sigma_iff)
using one two by auto
then have "(λf. kf_apply (f (Suc n)) (sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n)
(run_mixed_adv n f UB init X Y H))) abs_summable_on
(finite_kraus_subadv 𝔈 (Suc n))"
unfolding ρn_def[symmetric] by auto
then show ?case by auto
qed
lemma run_mixed_adv_summable:
fixes 𝔈 :: "'a kraus_adv"
shows "(λf. run_mixed_adv n f UB init X Y H) summable_on (finite_kraus_subadv 𝔈 n)"
using abs_summable_summable[OF run_mixed_adv_abs_summable] by blast
lemma run_mixed_adv_has_sum:
fixes 𝔈 :: "'a kraus_adv"
shows "((λf. run_mixed_adv n f UB init X Y H) has_sum run_mixed_adv n 𝔈 UB init X Y H)
(finite_kraus_subadv 𝔈 n)"
proof (induct n)
case 0
have "inj_on (λf. f 0) (Π⇩E i∈{0}. kf_elems (𝔈 i))"
unfolding PiE_over_singleton_iff inj_on_def by auto
then have inj: "inj_on (λf. f 0) (finite_kraus_subadv 𝔈 0)"
unfolding finite_kraus_subadv_def by simp
have rew: "(λf. kf_apply (f 0) (tc_selfbutter init)) =
(λ𝔉. kf_apply 𝔉 (tc_selfbutter init)) o (λf. f 0)" by auto
have "((λ𝔉. kf_apply 𝔉 (tc_selfbutter init)) has_sum
kf_apply (𝔈 0) (tc_selfbutter init))
(kf_elems (𝔈 0))" using kf_apply_has_sum_kf_elems by auto
moreover {
have "x ∈ kf_elems (𝔈 0) ⟹
x ∈ (λx. x 0) ` (Π⇩E i∈{0}. kf_elems (𝔈 i))" for x
unfolding PiE_over_singleton_iff by (simp add: image_iff)
then have "(λf. f 0) ` finite_kraus_subadv 𝔈 0 = kf_elems (𝔈 0)"
by (auto simp add: finite_kraus_subadv_I finite_kraus_subadv_def)
}
ultimately have "((λf. kf_apply (f 0) (tc_selfbutter init)) has_sum
kf_apply (𝔈 0) (tc_selfbutter init)) (finite_kraus_subadv 𝔈 0)"
unfolding rew by (subst has_sum_reindex[OF inj, symmetric]) auto
then show ?case by auto
next
case (Suc n)
define ρn where "ρn f = sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n)(run_mixed_adv n f UB init X Y H)"
for f
have ρn_Suc_indiff:"ρn (f(Suc n := x)) = ρn f" for f x
unfolding ρn_def run_mixed_adv_Suc_indifferent by auto
define ρ where "ρ = sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n) (run_mixed_adv n 𝔈 UB init X Y H)"
have ρn_has_sum_ρ: "((λf. ρn f) has_sum ρ) (finite_kraus_subadv 𝔈 n)"
unfolding ρn_def ρ_def by (use sandwich_tc_has_sum[OF Suc] in ‹auto simp add: o_def›)
have ρn_abs_summable_on:
"(λf. ρn f) abs_summable_on finite_kraus_subadv 𝔈 n"
proof -
have "∀f c F. (λfa. sandwich_tc c (f fa)) abs_summable_on F ∨ ¬ f abs_summable_on F"
using sandwich_tc_abs_summable_on by auto
then show ?thesis
unfolding ρn_def by (metis (no_types) run_mixed_adv_abs_summable)
qed
have one: "((λy. kf_apply x (ρn (y(Suc n := x)))) has_sum kf_apply x ρ)
(finite_kraus_subadv 𝔈 n)" if "x ∈ kf_elems (𝔈 (Suc n))" for x
unfolding ρn_Suc_indiff by (smt (verit, best) ρn_has_sum_ρ comp_eq_dest_lhs
finite_kf_apply_has_sum has_sum_cong)
have two: "((λx. kf_apply x ρ) has_sum kf_apply (𝔈 (Suc n)) ρ)
(kf_elems (𝔈 (Suc n)))"
by (simp add: kf_apply_has_sum_kf_elems)
have "(λ(x,f). kf_apply x (ρn (f(Suc n := x)))) abs_summable_on
kf_elems (𝔈 (Suc n)) × finite_kraus_subadv 𝔈 n"
proof (unfold ρn_Suc_indiff, subst abs_summable_on_Sigma_iff, safe, goal_cases)
case (1 x)
then show ?case using ρn_abs_summable_on finite_kf_apply_abs_summable_on by auto
next
case 2
then show ?case
by (intro infsum_norm_kf_apply_step[OF abs_summable_summable[OF ρn_abs_summable_on]])
(auto simp add: ρn_def run_mixed_adv_pos sandwich_tc_pos)
qed
then have "(λ(x,f). kf_apply x (ρn (f(Suc n := x)))) summable_on
kf_elems (𝔈 (Suc n)) × finite_kraus_subadv 𝔈 n"
using abs_summable_summable by blast
then have three: "(λx. kf_apply (fst x) (ρn ((snd x)(Suc n := fst x)))) summable_on
kf_elems (𝔈 (Suc n)) × finite_kraus_subadv 𝔈 n"
by (metis (no_types, lifting) split_def summable_on_cong)
have lim:
"((λf. kf_apply (f (Suc n)) (ρn f)) has_sum kf_apply (𝔈 (Suc n)) ρ)
(finite_kraus_subadv 𝔈 (Suc n))"
apply (subst finite_kraus_subadv_rewrite)
apply (subst has_sum_reindex[OF finite_kraus_subadv_rewrite_inj])
apply (unfold o_def case_prod_beta)
apply (intro has_sum_SigmaI[where g = "(λx. kf_apply x ρ)"])
by (auto simp add: one two three)
then have "((λf. kf_apply (f (Suc n)) (sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n)
(run_mixed_adv n f UB init X Y H))) has_sum kf_apply (𝔈 (Suc n))
(sandwich_tc ((X;Y) (Uquery H) o⇩C⇩L UB n) (run_mixed_adv n 𝔈 UB init X Y H)))
(finite_kraus_subadv 𝔈 (Suc n))"
unfolding ρn_def ρ_def by auto
then show ?case by auto
qed
text ‹Now, we cover limits for adversary runs in the O2H setting.›
context o2h_setting
begin
lemma run_mixed_A_has_sum:
"((λf. run_mixed_A f H) has_sum run_mixed_A kraus_A H) (finite_kraus_subadv kraus_A d)"
unfolding run_mixed_A_def by (rule run_mixed_adv_has_sum)
lemma run_mixed_B_has_sum:
"((λf. run_mixed_adv d f (US S) init_B X_for_B Y_for_B H) has_sum run_mixed_B kraus_B H S)
(finite_kraus_subadv (λn. kf_Fst (kraus_B n)) d)"
unfolding run_mixed_B_def by (rule run_mixed_adv_has_sum)
lemma run_mixed_B_count_has_sum:
"((λf. run_mixed_adv d f (λ_. U_S' S) init_B_count X_for_C Y_for_C H) has_sum run_mixed_B_count kraus_B H S)
(finite_kraus_subadv (λn. kf_Fst (kraus_B n)) d)"
unfolding run_mixed_B_count_def by (rule run_mixed_adv_has_sum)
lemma kf_elems_kf_Fst:
"kf_elems (kf_Fst 𝔈) = (λf. kf_Fst f) ` kf_elems 𝔈"
by transfer auto
lemma finite_kraus_subadv_Fst_invert:
"finite_kraus_subadv (λm. (kf_Fst :: _⇒(('a × 'c) ell2,_,_) kraus_family) (𝔈 m)) n =
(λf. λi∈{0..<n+1}. kf_Fst (f i)) ` (finite_kraus_subadv 𝔈 n)"
unfolding finite_kraus_subadv_def kf_elems_kf_Fst
proof (induct n)
case 0
have " (Π⇩E i∈{0..<0 + 1}. kf_Fst ` kf_elems (𝔈 i)) =
(Π⇩E i∈{0}. kf_Fst ` kf_elems (𝔈 i))" by auto
also have "… = (⋃b∈kf_elems (𝔈 0). {λx∈{0}. kf_Fst b})"
unfolding PiE_over_singleton_iff by auto
also have "… = (⋃b∈kf_elems (𝔈 0). (λf. λi∈{0}. kf_Fst (f i)) ` {λx∈{0}. b})"
proof -
have "(λx∈{0}. kf_Fst b) = (λa∈{0}. kf_Fst (if a = 0 then b else undefined))" for b
by fastforce
then show ?thesis by (intro Union_cong) auto
qed
also have "… = (λf. λi∈{0}. kf_Fst (f i)) `(⋃b∈kf_elems (𝔈 0). {λx∈{0}. b})"
unfolding image_UN by auto
also have "… = (λf. λi∈{0..<0+1}. kf_Fst (f i)) ` (Π⇩E i∈{0}. kf_elems (𝔈 i))"
unfolding PiE_over_singleton_iff by auto
also have "… = (λf. λi∈{0..<0+1}. kf_Fst (f i)) ` (Π⇩E i∈{0..<0+1}. kf_elems (𝔈 i))"
by auto
finally show ?case by blast
next
case (Suc n)
let ?prodset = "kf_elems (𝔈 (Suc n)) ×(Π⇩E i∈{0..<n+1}. kf_elems (𝔈 i))"
have "(Π⇩E i∈{0..<Suc n + 1}. (kf_Fst :: _⇒(('a × 'c) ell2,_,_) kraus_family) `
kf_elems (𝔈 i)) =
(Π⇩E i∈(insert (Suc n) {0..<Suc n}). kf_Fst ` kf_elems (𝔈 i))"
by (auto simp add: set_upt_Suc)
also have "… = (λ(y, g). g(Suc n := y)) ` (kf_Fst ` kf_elems (𝔈 (Suc n)) ×
(Π⇩E i∈{0..<n+1}. kf_Fst ` kf_elems (𝔈 i)))"
by (subst PiE_insert_eq) auto
also have "… = (λ(y, g). g(Suc n := y)) ` (kf_Fst ` kf_elems (𝔈 (Suc n)) ×
((λf. λi∈{0..<n+1}. kf_Fst (f i)) ` (Π⇩E i∈{0..<n+1}. kf_elems (𝔈 i))))"
by (subst Suc) auto
also have "… = (λ(y, g). g(Suc n := y)) `
(λ(a,x). (kf_Fst a, restrict (λi. kf_Fst (x i)) {0..<n+1})) ` ?prodset"
by (simp add: image_paired_Times)
also have "… = (λ(y, g). (restrict (λi. kf_Fst (g i)) {0..<n+1})
(Suc n := kf_Fst y)) ` ?prodset"
by (subst image_image) (simp add: split_def)
also have "… = (λ(y, g). restrict ((λi. kf_Fst (g i))(Suc n := kf_Fst y))
(insert (Suc n) {0..<n+1})) ` ?prodset"
by (subst restrict_upd) auto
also have "… = (λ(y, g). restrict ((λi. kf_Fst (g i))(Suc n := kf_Fst y))
{0..<Suc n + 1}) ` ?prodset" using semiring_norm(174) set_upt_Suc by presburger
also have "… = (λ(y, g). restrict (λi. kf_Fst ((g(Suc n:=y)) i))
{0..<Suc n + 1}) ` ?prodset"
proof -
have rew: "(λi. kf_Fst (g i))(Suc n := kf_Fst y) =
(λi. (kf_Fst :: _⇒(('a × 'c) ell2,_,_) kraus_family) ((g(Suc n:=y)) i))" for g y
by fastforce
show ?thesis by (subst rew) auto
qed
also have "… = (λf. restrict (λi. kf_Fst (f i)) {0..<Suc n + 1}) `
(λ(a,g). g(Suc n:= a)) ` ?prodset"
by (smt (verit, best) image_cong image_image restrict_ext split_def)
also have "… = (λf. restrict (λi. kf_Fst (f i)) {0..<Suc n + 1}) `
(Π⇩E i∈(insert (Suc n) {0..<Suc n}). kf_elems (𝔈 i))"
by (metis Suc_eq_plus1 finite_kraus_subadv_def finite_kraus_subadv_rewrite set_upt_Suc)
also have "… = (λf. λi∈{0..<Suc n + 1}. kf_Fst (f i)) `
(Π⇩E i∈{0..<Suc n+1}. kf_elems (𝔈 i))" by (simp add: set_upt_Suc)
finally show ?case by blast
qed
lemma inj_kf_Fst: ‹E = F› if ‹kf_Fst E = kf_Fst F›
proof (insert that, transfer)
fix E F :: ‹('a ell2 ⇒⇩C⇩L 'c ell2 × unit) set›
assume asm: ‹(λ(x, _). (x ⊗⇩o id_cblinfun, ())) ` E = (λ(x, _). (x ⊗⇩o id_cblinfun, ())) ` F›
have ‹inj (λ(x::'a ell2 ⇒⇩C⇩L 'c ell2, _::unit). (x ⊗⇩o id_cblinfun, ()))›
apply (rewrite at ‹inj ⌑› to ‹map_prod (λx. x ⊗⇩o id_cblinfun) id› DEADID.rel_mono_strong)
apply (force intro!: simp:)
apply (rule prod.inj_map)
by (simp_all add: inj_tensor_left)
from inj_image_eq_iff[OF this] asm
show ‹E = F›
by blast
qed
lemma inj_on_kf_Fst:
"inj_on (λf. λn∈{0..<n+1}. (kf_Fst (f n) :: (('a × 'b) ell2, _, _) kraus_family))
(finite_kraus_subadv 𝔈 n)"
proof (rule inj_onI, rename_tac E F)
fix E F :: ‹nat ⇒ ('a ell2, 'a ell2, unit) kraus_family›
assume finE: ‹E ∈ finite_kraus_subadv 𝔈 n› and finF: ‹F ∈ finite_kraus_subadv 𝔈 n›
assume eq: ‹(λi∈{0..<n + 1}. kf_Fst (E i) :: (('a × 'b) ell2, _, _) kraus_family) = (λn∈{0..<n + 1}. kf_Fst (F n))›
have ‹(kf_Fst (E i) :: (('a × 'b) ell2, _, _) kraus_family) = kf_Fst (F i)› if ‹i ∈ {0..<n+1}› for i
using eq[unfolded fun_eq_iff, rule_format, of i]
unfolding restrict_def
using that by (auto intro!: simp: fun_eq_iff)
then have ‹E i = F i› if ‹i ∈ {0..<n+1}› for i
using inj_kf_Fst that by blast
moreover from finE finF
have ‹E i = F i› if ‹i ∉ {0..<n+1}› for i
using that
by (simp add: finite_kraus_subadv_def PiE_def extensional_def)
ultimately show ‹E = F›
by blast
qed
lemma run_mixed_adv_kf_Fst_restricted:
"run_mixed_adv m (λn. kf_Fst (f n)) U init' X' Y' H =
run_mixed_adv m (λn∈{0..<m + 1}. kf_Fst (f n)) U init' X' Y' H"
proof (induct m arbitrary: f)
case (Suc m)
let ?f1 = "(λa. if a < Suc m then (kf_Fst ::_⇒(('a × 'b) ell2,_,_) kraus_family) (f a)
else undefined)"
let ?f2 = "(λa. if a < Suc (Suc m) then (kf_Fst ::_⇒(('a × 'b) ell2,_,_) kraus_family) (f a)
else undefined)"
have f12: "?f1(Suc m:= kf_Fst (f (Suc m))) = ?f2" by fastforce
have eq: "run_mixed_adv m ?f1 U init' X' Y' H =
run_mixed_adv m ?f2 U init' X' Y' H"
unfolding f12[symmetric] by (subst run_mixed_adv_Suc_indifferent) auto
show ?case by (auto simp add: eq Suc)
qed auto
lemma run_mixed_B_has_sum':
"((λf. run_mixed_B f H S) has_sum run_mixed_B kraus_B H S) (finite_kraus_subadv kraus_B d)"
(is "(?f has_sum ?x) ?A")
proof -
have inj: "inj_on (λf. λn∈{0..<d + 1}. kf_Fst (f n)) (finite_kraus_subadv kraus_B d)"
using inj_on_kf_Fst by auto
have rew: "?f = (λf. run_mixed_adv d f (US S) init_B X_for_B Y_for_B H) o
(λf. λn∈{0..<d + 1}. kf_Fst (f n))" unfolding run_mixed_B_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 run_mixed_B_has_sum)
qed
lemma run_mixed_B_count_has_sum':
"((λf. run_mixed_B_count f H S) has_sum run_mixed_B_count kraus_B H S) (finite_kraus_subadv kraus_B d)"
(is "(?f has_sum ?x) ?A")
proof -
have inj: "inj_on (λf. λn∈{0..<d + 1}. kf_Fst (f n)) (finite_kraus_subadv kraus_B d)"
using inj_on_kf_Fst by auto
have rew: "?f = (λf. run_mixed_adv d f (λ_. U_S' S) init_B_count X_for_C Y_for_C H) o
(λf. λn∈{0..<d + 1}. kf_Fst (f n))" unfolding run_mixed_B_count_def
using run_mixed_adv_kf_Fst_restricted[where init' = init_B_count and X' = X_for_C and Y'=Y_for_C]
by auto
show ?thesis unfolding rew by (subst has_sum_reindex[OF inj, symmetric])
(unfold finite_kraus_subadv_Fst_invert[symmetric], rule run_mixed_B_count_has_sum)
qed
text ‹Limit with finite sums›
lemma has_sum_finite_sum:
fixes f :: "'a ⇒ 'b ⇒ 'c:: {comm_monoid_add,topological_space, topological_comm_monoid_add}"
assumes "⋀val. (f val has_sum g val) A" "finite S"
shows "((λx. (∑val ∈ S. f val x)) has_sum (∑val ∈ S. g val)) A"
using assms(2) proof (induct S)
case empty
show "((λx. ∑val∈{}. f val x) has_sum sum g {}) A" by auto
next
case (insert x F)
show "((λxa. ∑val∈insert x F. f val xa) has_sum sum g (insert x F)) A"
unfolding sum.insert_remove[OF ‹finite F›] by (intro has_sum_add[of "f x"])
(use assms insert in ‹auto›)
qed
lemma fin_subadv_fin_Rep_kraus_family:
assumes "F ∈ finite_kraus_subadv E n" "i < n+1" "n<d+1"
shows "finite (Rep_kraus_family (F i))"
using assms unfolding finite_kraus_subadv_def using kf_elems_finite by fastforce
lemma fin_subadv_bound_leq_id:
assumes "F ∈ finite_kraus_subadv E d"
assumes "i < d+1"
assumes E_norm_id: "⋀i. i < d+1 ⟹ kf_bound (E i) ≤ id_cblinfun"
shows "kf_bound (F i) ≤ id_cblinfun"
proof -
have "F i ∈ kf_elems (E i)" using assms unfolding finite_kraus_subadv_def by auto
then have "kf_bound (F i) ≤ kf_bound (E i)"
using kf_bound_of_elems by auto
then show ?thesis using E_norm_id[OF assms(2)] by auto
qed
lemma fin_subadv_nonzero:
assumes "F ∈ finite_kraus_subadv E n" "i < n+1" "n<d+1"
shows "Rep_kraus_family (F i) ≠ {}"
proof -
have "F i ∈ kf_elems (E i)" using assms unfolding finite_kraus_subadv_def by auto
then show ?thesis using kf_elems_card_1 by fastforce
qed
end
unbundle no cblinfun_syntax
unbundle no lattice_syntax
unbundle no register_syntax
end