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 E ⟷ (∃EE :: ('a,'b,unit) kraus_family. E = kf_apply EE)›

lemma kraus_map_def: ‹kraus_map E ⟷ (∃EE :: ('a::chilbert_space,'b::chilbert_space,'x) kraus_family. E = kf_apply EE)›
  ― ‹Has a more general type than the original definition›
proof (rule iffI)
  assume ‹kraus_map E›
  then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = 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. E = kf_apply EE›
    by metis
next
  assume ‹∃EE :: ('a,'b,'x) kraus_family. E = kf_apply EE›
  then obtain EE :: ‹('a,'b,'x) kraus_family› where EE: ‹E = 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 E›
    apply (simp add: kraus_map_def_raw)
    by metis
qed

lemma kraus_mapI:
  assumes ‹E = kf_apply E'›
  shows ‹kraus_map E›
  using assms kraus_map_def by blast

lemma kraus_map_bounded_clinear: 
  ‹bounded_clinear E› if ‹kraus_map E›
  by (metis kf_apply_bounded_clinear kraus_map_def that)

lemma kraus_map_pos:
  assumes ‹kraus_map E› and ‹ρ ≥ 0›
  shows ‹E ρ ≥ 0›
proof -
  from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
    using kraus_map_def by blast
  show ?thesis
    by (simp add: E' assms(2) kf_apply_pos)
qed

lemma kraus_map_mono:
  assumes ‹kraus_map E› and ‹ρ ≥ τ›
  shows ‹E ρ ≥ E τ›
  by (metis assms kf_apply_mono_right kraus_map_def_raw)

lemma kraus_map_kf_apply[iff]: ‹kraus_map (kf_apply E)›
  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 E = (if kraus_map E then SOME F. E = kf_apply F else 0)›

lemma kf_apply_km_some_kraus_family[simp]:
  assumes ‹kraus_map E›
  shows ‹kf_apply (km_some_kraus_family E) = E›
  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 E›
  shows ‹km_some_kraus_family E = 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 →_CL 'b) set → bool› where
  ‹km_operators_in E S ⟷ (∃F :: ('a,'b,unit) kraus_family. kf_apply F = E ∧ kf_operators F ⊆ S)›

lemma km_operators_in_mono: ‹S ⊆ T ==> km_operators_in E S ==> km_operators_in E T›
  by (metis basic_trans_rules(23) km_operators_in_def)

lemma km_operators_in_kf_apply:
  assumes ‹span (kf_operators E) ⊆ S›
  shows ‹km_operators_in (kf_apply E) S›
proof (unfold km_operators_in_def, intro conjI exI[where x=‹kf_flatten E›])
  show ‹(*\<^sub>k\<^sub>r) (kf_flatten \) = (*\<^sub>k\<^sub>r) \\
 by simp
 from assms show ‹kf_operators (kf_flatten E) ⊆ S›
 using kf_operators_kf_map by fastforce
 

  km_operators_in_kf_apply_flattened:
 fixes E :: ‹('a::chilbert_space,'b::chilbert_space,'x::CARD_1) kraus_family›
 assumes ‹kf_operators E ⊆ S›
 shows ‹km_operators_in (kf_apply E) S›
  (unfold km_operators_in_def, intro conjI exI[where x=‹kf_map_inj (λx.()) E›])
 show ‹(*\<^sub>k\<^sub>r) (kf_map_inj (\\. ()) \) = (*\<^sub>k\<^sub>r) \\
 by (auto intro!: ext kf_apply_map_inj inj_onI)
 have ‹kf_operators (kf_map_inj (λF. ()) E) = kf_operators E›
 by simp
 with assms show ‹kf_operators (kf_map_inj (λF. ()) E) ⊆ S›
 by blast
 

  km_commute:
 assumes ‹km_operators_in E S›
 assumes ‹km_operators_in F T›
 assumes ‹S ⊆ commutant T›
 shows ‹F o E = E o F›
  -
 from assms obtain E' :: ‹(_,_,unit) kraus_family› where E': ‹E = kf_apply E'› and E'S: ‹kf_operators E' ⊆ S›
 by (metis km_operators_in_def)
 from assms obtain F' :: ‹(_,_,unit) kraus_family› where F': ‹F = kf_apply F'› and F'T: ‹kf_operators F' ⊆ T›
 by (metis km_operators_in_def)

 have ‹kf_operators E' ⊆ S›
 by (rule E'S)
 also have ‹S ⊆ commutant T›
 by (rule assms)
 also have ‹commutant T ⊆ commutant (kf_operators F')›
 apply (rule commutant_antimono)
 by (rule F'T)
 finally show ?thesis
 unfolding E' F'
 by (rule kf_apply_commute[symmetric])
 

  km_operators_in_UNIV:
 assumes ‹kraus_map E›
 shows ‹km_operators_in E UNIV›
 by (metis assms kf_apply_km_some_kraus_family km_operators_in_def top.extremum)

  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)

  ‹Bound and norm›

  km_bound :: ‹(('a::chilbert_space, 'a) trace_class → ('b::chilbert_space, 'b) trace_class) → ('a, 'a) cblinfun› where
 ‹km_bound E = (if ∃E' :: (_, _, unit) kraus_family. E = kf_apply E' then kf_bound (SOME E' :: (_, _, unit) kraus_family. E = kf_apply E') else 0)›

  km_bound_kf_bound:
 assumes ‹E = kf_apply F›
 shows ‹km_bound E = kf_bound F›
  -
 wlog ex: ‹∃E' :: (_, _, unit) kraus_family. E = kf_apply E'›
 using assms kraus_map_def_raw negation by blast
 define E' where ‹E' = (SOME E' :: (_, _, unit) kraus_family. E = kf_apply E')›
 have ‹E = kf_apply (kf_flatten F)›
 by (simp add: assms)
 then have ‹E = kf_apply E'›
 by (metis (mono_tags, lifting) E'_def someI_ex)
 then have ‹E' =_kr F›
 using assms kf_eq_weak_def by force
 then have ‹kf_bound E' = kf_bound F›
 using kf_bound_cong by blast
 then show ?thesis
 by (metis E'_def km_bound_def ex)
 

 
  km_norm :: ‹(('a::chilbert_space, 'a) trace_class → ('b::chilbert_space, 'b) trace_class) → real› where
 ‹km_norm E = norm (km_bound E)›

  km_norm_kf_norm:
 assumes ‹E = kf_apply F›
 shows ‹km_norm E = kf_norm F›
 by (simp add: assms kf_norm_def km_bound_kf_bound km_norm_def)

  km_bound_invalid:
 assumes ‹¬ kraus_map E›
 shows ‹km_bound E = 0›
 by (metis assms km_bound_def kraus_map_def_raw)

  km_norm_invalid:
 assumes ‹¬ kraus_map E›
 shows ‹km_norm E = 0›
 by (simp add: assms km_bound_invalid km_norm_def)



  km_norm_geq0[iff]: ‹km_norm E ≥ 0›
 by (simp add: km_norm_def)

  kf_bound_pos[iff]: ‹km_bound E ≥ 0›
 apply (cases ‹kraus_map E›)
 apply (simp add: km_bound_def)
 by (simp add: km_bound_invalid)

  km_bounded_pos:
 assumes ‹kraus_map E› and ‹ρ ≥ 0›
 shows ‹norm (E ρ) ≤ km_norm E * norm ρ›
  -
 from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
 using kraus_map_def by blast
 show ?thesis
 by (simp add: E' assms(2) kf_apply_bounded_pos km_norm_kf_norm)
 

  km_bounded:
 assumes ‹kraus_map E›
 shows ‹norm (E ρ) ≤ 4 * km_norm E * norm ρ›
  -
 from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
 using kraus_map_def by blast
 show ?thesis
 by (simp add: E' kf_apply_bounded km_norm_kf_norm)
 

  km_bound_from_map:
 assumes ‹kraus_map E›
 shows ‹ψ ∙_C km_bound E φ = trace_tc (E (tc_butterfly φ ψ))›
 by (metis assms kf_bound_from_map km_bound_kf_bound kraus_map_def_raw)

  trace_from_km_bound:
 assumes ‹kraus_map E›
 shows ‹trace_tc (E ρ) = trace_tc (compose_tcr (km_bound E) ρ)›
 by (metis assms km_bound_kf_bound kraus_map_def_raw trace_from_kf_bound)

  km_bound_selfadjoint[iff]: ‹selfadjoint (km_bound E)›
 by (simp add: pos_selfadjoint)

  km_bound_leq_km_norm_id: ‹km_bound E ≤ km_norm E *_R id_cblinfun›
 by (simp add: km_norm_def less_eq_scaled_id_norm)

  kf_norm_km_some_kraus_family[simp]: ‹kf_norm (km_some_kraus_family E) = km_norm E›
 apply (cases ‹kraus_map E›)
 by (auto intro!: km_norm_kf_norm[symmetric] simp: km_some_kraus_family_invalid km_norm_invalid)

  ‹Basic Kraus maps›

  ‹Zero map and constant maps. Addition and rescaling and composition of maps.›

  kraus_map_0[iff]: ‹kraus_map 0›
 by (metis kf_apply_0 kraus_mapI)

  kraus_map_0'[iff]: ‹kraus_map (λ_. 0)›
 using kraus_map_0 unfolding func_zero by simp
  km_bound_0[simp]: ‹km_bound 0 = 0›
 using km_bound_kf_bound[of 0 0]
 by simp

  km_norm_0[simp]: ‹km_norm 0 = 0›
 by (simp add: km_norm_def)

  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)

  kraus_map_id[iff]: ‹kraus_map id›
 by (auto intro!: ext kraus_mapI[of _ kf_id])

  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)

  km_norm_id_leq1[iff]: ‹km_norm id ≤ 1›
 by (simp add: km_norm_def norm_cblinfun_id_le)

  km_norm_id_eq1[simp]: ‹km_norm (id :: ('a :: {chilbert_space, not_singleton}, 'a) trace_class → _) = 1›
 by (simp add: km_norm_def)

  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)

  kraus_map_add[iff]:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹kraus_map (λρ. E ρ + F ρ)›
  -
 from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
 using kraus_map_def by blast
 from assms obtain F' :: ‹('a, 'b, unit) kraus_family› where F': ‹F = kf_apply F'›
 using kraus_map_def by blast
 show ?thesis
 apply (rule kraus_mapI[of _ ‹E' + F'›])
 by (auto intro!: ext simp: E' F' kf_plus_apply')
 

  kraus_map_plus'[iff]:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹kraus_map (E + F)›
 using assms by (simp add: plus_fun_def)

  km_bound_plus:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹km_bound (E + F) = km_bound E + km_bound F›
  -
 from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
 using kraus_map_def_raw by blast
 from assms obtain FF :: ‹('a,'b,unit) kraus_family› where FF: ‹F = kf_apply FF›
 using kraus_map_def_raw by blast
 show ?thesis
 apply (rule km_bound_kf_bound[where F=‹EE + FF›, THEN trans])
 by (auto intro!: ext simp: EE FF kf_plus_apply' kf_plus_bound' km_bound_kf_bound)
 

  km_norm_triangle:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹km_norm (E + F) ≤ km_norm E + km_norm F›
 by (simp add: km_norm_def km_bound_plus assms norm_triangle_ineq)


  kraus_map_constant[iff]: ‹kraus_map (λσ. trace_tc σ *_C ρ)› if ‹ρ ≥ 0›
 apply (rule kraus_mapI[where E'=‹kf_constant ρ›])
 by (simp add: kf_constant_apply[OF that, abs_def])

  kraus_map_constant_invalid:
 ‹¬ kraus_map (λσ :: ('a::{chilbert_space,not_singleton},'a) trace_class. trace_tc σ *_C ρ)› if ‹~ ρ ≥ 0›
  (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
 

  kraus_map_scale:
 assumes ‹kraus_map E› and ‹c ≥ 0›
 shows ‹kraus_map (λρ. c *_R E ρ)›
  -
 from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
 using kraus_map_def by blast
 then show ?thesis
 apply (rule_tac kraus_mapI[where E'=‹c *_R E'›])
 by (auto intro!: ext simp add: E' kf_scale_apply assms)
 

  km_bound_scale[simp]: ‹km_bound (λρ. c *_R E ρ) = c *_R km_bound E› if ‹c ≥ 0›
  -
 consider (km) ‹kraus_map E› | (c0) ‹c = 0› | (not_km) ‹¬ kraus_map E› ‹c > 0›
 using ‹0 ≤ c› by argo
 then show ?thesis
 proof cases
 case km
 then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = 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 E ρ› ‹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 E ρ)›
 proof (rule ccontr)
 assume ‹¬ ¬ kraus_map (λρ. c *_R E ρ)›
 then have ‹kraus_map (λρ. inverse c *_R (c *_R E ρ))›
 apply (rule_tac kraus_map_scale)
 using not_km by auto
 then have ‹kraus_map E›
 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
 


  km_norm_scale[simp]: ‹km_norm (λρ. c *_R E ρ) = c * km_norm E› if ‹c ≥ 0›
 using that by (simp add: km_norm_def)



  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

  km_bound_sandwich[simp]: ‹km_bound (sandwich_tc A) = A* o_CL 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

  km_norm_sandwich[simp]: ‹km_norm (sandwich_tc A) = (norm A)²›
 by (simp add: km_norm_def)

  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

  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)

  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)

  km_constant_norm_leq[simp]: ‹km_norm (λσ::('a::chilbert_space,'a) trace_class. trace_tc σ *_C ρ) ≤ norm ρ›
  -
 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
 

  kraus_map_comp:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹kraus_map (E o F)›
  -
 from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
 using kraus_map_def_raw by blast
 from assms obtain FF :: ‹('c,'a,unit) kraus_family› where FF: ‹F = kf_apply FF›
 using kraus_map_def_raw by blast
 show ?thesis
 apply (rule kraus_mapI[where E'=‹kf_comp EE FF›])
 by (simp add: EE FF kf_comp_apply)
 

  km_comp_norm_leq:
 assumes ‹kraus_map E› and ‹kraus_map F›
 shows ‹km_norm (E o F) ≤ km_norm E * km_norm F›
  -
 from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
 using kraus_map_def_raw by blast
 from assms obtain FF :: ‹('c,'a,unit) kraus_family› where FF: ‹F = kf_apply FF›
 using kraus_map_def_raw by blast
 have ‹km_norm (E o F) = 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 E * km_norm F›
 by (simp add: EE FF km_norm_kf_norm)
 finally show ?thesis
 by -
 

  km_bound_comp_sandwich:
 assumes ‹kraus_map E›
  shows \<open>km_bound (\<lambda>\<rho>. \<EE> (sandwich_tc U \<rho>)) = sandwich (U*) (km_bound E)›
proof -
  from assms obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  have \<open>km_bound (\<lambda>\<rho>. \<EE> (sandwich_tc U \<rho>)) = kf_bound (kf_comp EE (kf_of_op U))\<close>
    apply (rule km_bound_kf_bound)
    by (simp add: kf_comp_apply o_def EE kf_of_op_apply)
  also have \<open>\<dots> = sandwich (U*) *_V kf_bound EE›
    by (simp add: kf_bound_comp_of_op)
  also have ‹… = sandwich (U*) (km_bound E)›
    by (simp add: EE km_bound_kf_bound)
  finally show ?thesis
    by -
qed

(* lemma sandwich_tc_compose: \<open>sandwich_tc A (sandwich_tc B \<rho>) = sandwich_tc (A o\<^sub>C\<^sub>L B) \<rho>\<close>
  apply transfer'
  by (simp add: sandwich_compose) *)



lemma km_norm_comp_sandwich_coiso:
  assumes ‹isometry (U*)›
  shows ‹km_norm (λρ. E (sandwich_tc U ρ)) = km_norm E›
proof (cases ‹kraus_map E›)
  case True
  then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  have ‹km_norm (λρ. E (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 E›
    by (simp add: EE km_norm_kf_norm)
  finally show ?thesis
    by -
next
  case False
  have ‹¬ kraus_map (λρ. E (sandwich_tc U ρ))›
  proof (rule ccontr)
    assume ‹¬ ¬ kraus_map (λρ. E (sandwich_tc U ρ))›
    then have ‹kraus_map (λρ. E (sandwich_tc U ρ))›
      by blast
    then have ‹kraus_map (λρ. E (sandwich_tc U (sandwich_tc (U*) ρ)))›
      apply (rule kraus_map_comp[unfolded o_def])
      by fastforce
    then have ‹kraus_map E›
      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 (E ρ)) = km_bound E›
proof (cases ‹kraus_map E›)
  case True
  then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  have ‹km_bound (λρ. sandwich_tc U (E ρ)) = 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 E›
    by (simp add: EE km_bound_kf_bound)
  finally show ?thesis
    by -
next
  case False
  have ‹¬ kraus_map (λρ. sandwich_tc U (E ρ))›
  proof (rule ccontr)
    assume ‹¬ ¬ kraus_map (λρ. sandwich_tc U (E ρ))›
    then have ‹kraus_map (λρ. sandwich_tc U (E ρ))›
      by blast
    then have ‹kraus_map (λρ. sandwich_tc (U*) (sandwich_tc U (E ρ)))›
      apply (rule kraus_map_comp[unfolded o_def, rotated])
      by fastforce
    then have ‹kraus_map E›
      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 (E ρ)) = km_norm E›
proof (cases ‹kraus_map E›)
  case True
  then obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  have ‹km_norm (λρ. sandwich_tc U (E ρ)) = 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 E›
    by (simp add: EE km_norm_kf_norm)
  finally show ?thesis
    by -
next
  case False
  have ‹¬ kraus_map (λρ. sandwich_tc U (E ρ))›
  proof (rule ccontr)
    assume ‹¬ ¬ kraus_map (λρ. sandwich_tc U (E ρ))›
    then have ‹kraus_map (λρ. sandwich_tc U (E ρ))›
      by blast
    then have ‹kraus_map (λρ. sandwich_tc (U*) (sandwich_tc U (E ρ)))›
      apply (rule kraus_map_comp[unfolded o_def, rotated])
      by fastforce
    then have ‹kraus_map E›
      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 (E x)›
  shows ‹kraus_map (∑x∈A. E x)›
  apply (insert assms, induction A rule:infinite_finite_induct)
  by auto

lemma km_bound_sum:
  assumes ‹∧x. x∈A ==> kraus_map (E x)›
  shows ‹km_bound (∑x∈A. E x) = (∑x∈A. km_bound (E 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. E x) = km_bound (E x + (∑x∈F. E x))›
    by (simp add: insert.hyps)
  also have ‹… = km_bound (E x) + km_bound (∑x∈F. E x)›
    by (simp add: km_bound_plus kraus_map_sum insert.prems)
  also have ‹… = km_bound (E x) + (∑x∈F. km_bound (E x))›
    by (simp add: insert)
  also have ‹… = (∑x∈insert x F. km_bound (E x))›
    using insert.hyps by fastforce
  finally show ?case
    by -
qed




subsection ‹Infinite sums›

lemma
  assumes ‹∧ρ. ((λa. sandwich_tc (f a) ρ) has_sum E ρ) A›
  defines ‹EE ≡ Set.filter (λ(E,_). E≠0) ((λa. (f a, a)) ` A)›
  shows kraus_mapI_sum: ‹kraus_map E›
    and kraus_map_sum_kraus_family: ‹kraus_family EE›
    and kraus_map_sum_kf_apply: ‹E = 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 ‹E = kf_apply (Abs_kraus_family EE)›
    unfolding EE_def
    apply (rule kf_reconstruction[symmetric])
    by (fact assms(1))
  then show ‹kraus_map E›
    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 E›
  shows ‹∃M. ∀ρ. ((λE. sandwich_tc E ρ) has_sum E ρ) M›
proof -
  from assms obtain E' :: ‹('a, 'b, unit) kraus_family› where E': ‹E = kf_apply E'›
    using kraus_map_def by blast
  define M where ‹M = fst ` Rep_kraus_family E'›
  have ‹((λE. sandwich_tc E ρ) has_sum E ρ) M› for ρ
  proof -
    have [simp]: ‹inj_on fst (Rep_kraus_family E')›
      by (auto intro!: inj_onI)
    from kf_apply_has_sum[of ρ E']
    have ‹((λ(E, x). sandwich_tc E ρ) has_sum kf_apply E' ρ) (Rep_kraus_family E')›
      by -
    then show ?thesis
      by (simp add: M_def has_sum_reindex o_def case_prod_unfold E')
  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 E A ⟷ summable_on_in cweak_operator_topology (λa. km_bound (E a)) A›

lemma km_summable_kf_summable:
  assumes ‹∧a ρ. a ∈ A ==> E a ρ = F a *_kr ρ›
  shows ‹km_summable E A ⟷ kf_summable F A›
proof -
  have ‹km_summable E A ⟷ summable_on_in cweak_operator_topology (λa. km_bound (E a)) A›
    using km_summable_def by blast
  also have ‹… ⟷ summable_on_in cweak_operator_topology (λa. kf_bound (F a)) A›
    apply (rule summable_on_in_cong)
    apply (rule km_bound_kf_bound)
    using assms by fastforce
  also have ‹… ⟷ kf_summable F A›
    using kf_summable_def by blast
  finally show ?thesis
    by -
qed

lemma km_summable_summable:
  assumes km: ‹∧a. a∈A ==> kraus_map (E a)›
  assumes sum: ‹km_summable E A›
  shows ‹(λa. E a ρ) summable_on A›
proof -
  from km
  obtain EE :: ‹_ → (_,_,unit) kraus_family› where EE: ‹E 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 *_kr ρ) 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 (E a)›
  assumes sum: ‹km_summable E A›
  shows ‹kraus_map (λρ. ∑_\∞a∈A. E a ρ)›
proof -
  from km
  obtain EE :: ‹_ → (_,_,unit) kraus_family› where EE: ‹E 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 *_kr ρ = (∑_\∞a∈A. EE a *_kr ρ)› for ρ
    by (metis kf_infsum_apply)
  also have ‹… ρ = (∑_\∞a∈A. E 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 (E a)›
  assumes sum: ‹km_summable E A›
  shows ‹km_bound (λρ. ∑_\∞a∈A. E a ρ) = infsum_in cweak_operator_topology (λa. km_bound (E a)) A›
proof -
  from km
  obtain EE :: ‹_ → (_,_,unit) kraus_family› where EE: ‹E 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. E a ρ) = km_bound (λρ. ∑_\∞a∈A. EE a *_kr ρ)›
    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 (E 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 (E a)›
  assumes sum: ‹(λa. km_norm (E a)) summable_on A›
  shows ‹km_norm (λρ. ∑_\∞a∈A. E a ρ) ≤ (∑_\∞a∈A. km_norm (E a))›
proof -
  from km
  obtain EE :: ‹_ → (_,_,unit) kraus_family› where EE: ‹E 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. E a ρ) = km_norm (λρ. ∑_\∞a∈A. EE a *_kr ρ)›
    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 (E 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 (E x)›
  assumes ‹km_summable E A›
  assumes ‹(E has_sum F) A›
  shows ‹kraus_map F›
proof -
  from ‹(E has_sum F) A›
  have ‹((λx. E x t) has_sum F t) A› for t
    by (simp add: has_sum_coordinatewise)
  then have ‹F t = (∑_\∞a∈A. E a t)› for t
    by (metis infsumI)
  with kraus_map_infsum[OF assms(1,2)]
  show ‹kraus_map F›
    by presburger
qed

lemma km_summable_iff_sums_to_kraus_map:
  assumes ‹∧a. a∈A ==> kraus_map (E a)›
  shows ‹km_summable E A ⟷ (∃F. (∀t. ((λx. E x t) has_sum F t) A) ∧ kraus_map F)›
proof (rule iffI)
  assume asm: ‹km_summable E A›
  define F where ‹F t = (∑_\∞a∈A. E a t)› for t
  from km_summable_summable[OF assms asm]
  have ‹((λx. E x t) has_sum F t) A› for t
    using F_def by fastforce
  moreover from kraus_map_infsum[OF assms asm]
  have ‹kraus_map F›
    by (simp add: F_def[abs_def])
  ultimately show ‹(∃F. (∀t. ((λx. E x t) has_sum F t) A) ∧ kraus_map F)›
    by auto
next
  assume ‹∃F. (∀t. ((λx. E x t) has_sum F t) A) ∧ kraus_map F›
  then obtain F where ‹kraus_map F› and ‹((λx. E x t) has_sum F t) A› for t
    by auto
  then have ‹((λx. trace_tc (E x (tc_butterfly k h))) has_sum trace_tc (F (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 (E x (tc_butterfly k h))) has_sum h ∙_C (km_bound F *_V k)) A› for h k
    by (simp add: km_bound_from_map ‹kraus_map F›)
  then have ‹((λx. h ∙_C (km_bound (E x) *_V k)) has_sum h ∙_C (km_bound F *_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 (E a)) A (km_bound F)›
    by (simp add: has_sum_in_cweak_operator_topology_pointwise)
  then show ‹km_summable E 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 E F ⟷ (∃EF. bounded_clinear EF ∧ (∀ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ)))›


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 E F = (if km_tensor_exists E F
 then SOME EF. bounded_clinear EF ∧ (∀ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ))
 else 0)›

lemma km_tensor_invalid:
  assumes ‹¬ km_tensor_exists E F›
  shows ‹km_tensor E F = 0›
  by (simp add: assms km_tensor_def)


lemma km_tensor_exists_bounded_clinear[iff]:
  assumes ‹km_tensor_exists E F›
  shows ‹bounded_clinear (km_tensor E F)›
  unfolding km_tensor_def
  apply (rule someI2_ex[where P=‹λEF. bounded_clinear EF ∧ (∀ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ))›])
  using assms
  by (simp_all add: km_tensor_exists_def)

lemma km_tensor_apply[simp]:
  assumes ‹km_tensor_exists E F›
  shows ‹km_tensor E F (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ)›
  unfolding km_tensor_def
  apply (rule someI2_ex[where P=‹λEF. bounded_clinear EF ∧ (∀ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ))›])
  using assms
  by (simp_all add: km_tensor_exists_def)

lemma km_tensor_unique:
  assumes ‹bounded_clinear EF›
  assumes ‹∧ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ)›
  shows ‹EF = km_tensor E F›
proof -
  define P where ‹P EF ⟷ bounded_clinear EF ∧ (∀ρ σ. EF (tc_tensor ρ σ) = tc_tensor (E ρ) (F σ))› for EF
  have ‹P EF›
    using P_def assms by presburger
  then have ‹km_tensor_exists E F›
    using P_def km_tensor_exists_def by blast
  with ‹P EF› have Ptensor: ‹P (km_tensor E F)›
    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 E) (kf_apply F) = kf_apply (kf_tensor E F)›
  by (metis kf_apply_bounded_clinear kf_apply_tensor km_tensor_unique)

lemma km_tensor_kraus_map:
  assumes ‹kraus_map E› and ‹kraus_map F›
  shows ‹kraus_map (km_tensor E F)›
proof -
  from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹F = 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 E› and ‹kraus_map F›
  shows ‹km_tensor_exists E F›
proof -
  from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹F = 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 E ρ) I›
  assumes ‹∧ρ. ((λj. sandwich_tc (F j) ρ) has_sum F ρ) J›
  shows ‹km_tensor E F ρ = (∑_\∞(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 ‹E = kf_apply (Abs_kraus_family EE)› and ‹F = kf_apply (Abs_kraus_family FF)›
    using assms kraus_map_sum_kf_apply EE_def FF_def
    by blast+
  then have ‹km_tensor E F ρ = 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 E› and ‹kraus_map F›
  shows ‹km_bound (km_tensor E F) = km_bound E ⊗_o km_bound F›
proof -
  from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹F = 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 E› and ‹kraus_map F›
  shows ‹km_norm (km_tensor E F) = km_norm E * km_norm F›
proof -
  from assms obtain EE :: ‹(_,_,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  from assms obtain FF :: ‹(_,_,unit) kraus_family› where FF: ‹F = 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 E G› and ‹km_tensor_exists F H›
  shows ‹km_tensor (E o F) (G o H) = km_tensor E G o km_tensor F H›
  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 E S›
  assumes ‹km_operators_in F T›
  shows ‹km_operators_in (km_tensor E F) (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 E' :: ‹(_,_,unit) kraus_family› where E_def: ‹E = kf_apply E'› and E'S: ‹kf_operators E' ⊆ S›
    by (metis km_operators_in_def)
  from assms obtain F' :: ‹(_,_,unit) kraus_family› where F_def: ‹F = kf_apply F'› and F'T: ‹kf_operators F' ⊆ T›
    by (metis km_operators_in_def)
  define EF where ‹EF = kf_map_inj (λ((),()). ()) (kf_tensor E' F')›
  then have ‹kf_operators EF = kf_operators (kf_tensor E' F')›
    by (simp add: EF_def)
  also have ‹kf_operators (kf_tensor E' F') ⊆ span {E ⊗_o F | E F. E ∈ kf_operators E' ∧ F ∈ kf_operators F'}›
    using kf_operators_tensor by force
  also have ‹… ⊆ span {E ⊗_o F | E F. E ∈ S ∧ F ∈ T}›
    by (smt (verit) Collect_mono_iff E'S F'T span_mono subset_iff)
  finally have ‹kf_operators EF ⊆ span {s ⊗_o t |s t. s ∈ S ∧ t ∈ T}›
    using EF_def by blast
  moreover have ‹kf_apply EF = km_tensor E F›
    by (simp add: EF_def E_def F_def kf_apply_bounded_clinear kf_apply_tensor km_tensor_unique)
  ultimately show ?thesis
    by (auto intro!: exI[of _ EF] 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 E ⟷ (∃F::(_,_,unit) kraus_family. E = kf_apply F ∧ kf_trace_preserving F)›
lemma km_trace_preserving_def': ‹km_trace_preserving E ⟷ (∃F::(_, _, 'c) kraus_family. E = kf_apply F ∧ kf_trace_preserving F)›
  ― ‹Has a more general type than @{thm [source] km_trace_preserving_def}›
proof (rule iffI)
  assume ‹km_trace_preserving E›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_preserving F›
    using km_trace_preserving_def by blast
  from EF have ‹E = kf_apply (kf_map (λ_. undefined :: 'c) F)›
    by simp
  moreover from tpF have ‹kf_trace_preserving (kf_map (λ_. undefined :: 'c) F)›
    by (metis EF calculation kf_trace_preserving_iff_bound_id km_bound_kf_bound)
  ultimately show ‹∃F::(_, _, 'c) kraus_family. E = (*_kr) F ∧ kf_trace_preserving F›
    by blast
next
  assume ‹∃F::(_, _, 'c) kraus_family. E = (*_kr) F ∧ kf_trace_preserving F›
  then obtain F :: ‹(_,_,'c) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_preserving F›
    by blast
  from EF have ‹E = kf_apply (kf_flatten F)›
    by simp
  moreover from tpF have ‹kf_trace_preserving (kf_flatten F)›
    by (metis EF calculation kf_trace_preserving_iff_bound_id km_bound_kf_bound)
  ultimately show ‹km_trace_preserving E›
    using km_trace_preserving_def by blast
qed

definition km_trace_reducing_def: ‹km_trace_reducing E ⟷ (∃F::(_,_,unit) kraus_family. E = kf_apply F ∧ kf_trace_reducing F)›
lemma km_trace_reducing_def': ‹km_trace_reducing E ⟷ (∃F::(_, _, 'c) kraus_family. E = kf_apply F ∧ kf_trace_reducing F)›
proof (rule iffI)
  assume ‹km_trace_reducing E›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_reducing F›
    using km_trace_reducing_def by blast
  from EF have ‹E = kf_apply (kf_map (λ_. undefined :: 'c) F)›
    by simp
  moreover from tpF have ‹kf_trace_reducing (kf_map (λ_. undefined :: 'c) F)›
    by (simp add: kf_trace_reducing_iff_norm_leq1)
  ultimately show ‹∃F::(_, _, 'c) kraus_family. E = (*_kr) F ∧ kf_trace_reducing F›
    by blast
next
  assume ‹∃F::(_, _, 'c) kraus_family. E = (*_kr) F ∧ kf_trace_reducing F›
  then obtain F :: ‹(_,_,'c) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_reducing F›
    by blast
  from EF have ‹E = kf_apply (kf_flatten F)›
    by simp
  moreover from tpF have ‹kf_trace_reducing (kf_flatten F)›
    by (simp add: kf_trace_reducing_iff_norm_leq1)
  ultimately show ‹km_trace_reducing E›
    using km_trace_reducing_def by blast
qed

lemma km_trace_preserving_apply[simp]: ‹km_trace_preserving (kf_apply E) = kf_trace_preserving E›
  using kf_trace_preserving_def km_trace_preserving_def' by auto

lemma km_trace_reducing_apply[simp]: ‹km_trace_reducing (kf_apply E) = kf_trace_reducing E›
  by (metis kf_trace_reducing_iff_norm_leq1 km_norm_kf_norm km_trace_reducing_def')

lemma km_trace_preserving_iff: ‹km_trace_preserving E ⟷ kraus_map E ∧ (∀ρ. trace_tc (E ρ) = trace_tc ρ)›
proof (intro iffI conjI allI)
  assume tp: ‹km_trace_preserving E›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_preserving F›
    by (metis kf_trace_preserving_def kf_trace_reducing_def km_trace_preserving_def order.refl)
  then show ‹kraus_map E›
    by blast
  from tpF show ‹trace_tc (E ρ) = trace_tc ρ› for ρ
    by (simp add: EF kf_trace_preserving_def)
next
  assume asm: ‹kraus_map E ∧ (∀ρ. trace_tc (E ρ) = trace_tc ρ)›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F›
    using kraus_map_def_raw by blast
  from asm EF have ‹trace_tc (kf_apply F ρ) = trace_tc ρ› for ρ
    by blast
  then have ‹kf_trace_preserving F›
    using kf_trace_preserving_def by blast
  with EF show ‹km_trace_preserving E›
    using km_trace_preserving_def by blast
qed


lemma km_trace_reducing_iff: ‹km_trace_reducing E ⟷ kraus_map E ∧ (∀ρ≥0. trace_tc (E ρ) ≤ trace_tc ρ)›
proof (intro iffI conjI allI impI)
  assume tp: ‹km_trace_reducing E›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F› and tpF: ‹kf_trace_reducing F›
    by (metis kf_trace_reducing_def kf_trace_reducing_def km_trace_reducing_def order.refl)
  then show ‹kraus_map E›
    by blast
  from tpF EF show ‹trace_tc (E ρ) ≤ trace_tc ρ› if ‹ρ ≥ 0› for ρ
    using kf_trace_reducing_def that by blast
next
  assume asm: ‹kraus_map E ∧ (∀ρ≥0. trace_tc (E ρ) ≤ trace_tc ρ)›
  then obtain F :: ‹(_,_,unit) kraus_family› where EF: ‹E = kf_apply F›
    using kraus_map_def_raw by blast
  from asm EF have ‹trace_tc (kf_apply F ρ) ≤ trace_tc ρ› if ‹ρ ≥ 0› for ρ
    using that by blast
  then have ‹kf_trace_reducing F›
    using kf_trace_reducing_def by blast
  with EF show ‹km_trace_reducing E›
    using km_trace_reducing_def by blast
qed

lemma km_trace_preserving_imp_reducing:
  assumes ‹km_trace_preserving E›
  shows ‹km_trace_reducing E›
  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 E ⟷ kraus_map E ∧ km_norm E ≤ 1›
proof (intro iffI conjI)
  assume ‹km_trace_reducing E›
  then show ‹kraus_map E›
    using km_trace_reducing_iff by blast
  then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  with ‹km_trace_reducing E›
  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 E ≤ 1›
    by (simp add: EE km_norm_kf_norm)
next
  assume asm: ‹kraus_map E ∧ km_norm E ≤ 1›
  then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  from asm have ‹km_norm E ≤ 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 E›
    using EE km_trace_reducing_def by blast
qed


lemma km_trace_preserving_iff_bound_id: ‹km_trace_preserving E ⟷ kraus_map E ∧ km_bound E = id_cblinfun›
proof (intro iffI conjI)
  assume ‹km_trace_preserving E›
  then show ‹kraus_map E›
    using km_trace_preserving_iff by blast
  then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = kf_apply EE›
    using kraus_map_def_raw by blast
  with ‹km_trace_preserving E›
  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 E = id_cblinfun›
    by (simp add: EE km_bound_kf_bound)
next
  assume asm: ‹kraus_map E ∧ km_bound E = id_cblinfun›
  then have ‹kraus_map E›
    by simp
  then obtain EE :: ‹('a,'b,unit) kraus_family› where EE: ‹E = 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 E›
    using EE km_trace_preserving_def by blast
qed

lemma km_trace_preserving_iff_bound_id':
  fixes E :: ‹('a::{chilbert_space, not_singleton}, 'a) trace_class → _›
  shows ‹km_trace_preserving E ⟷ km_bound E = id_cblinfun›
  using km_bound_invalid km_trace_preserving_iff_bound_id by fastforce

lemma km_trace_norm_preserving: ‹km_norm E ≤ 1› if ‹km_trace_preserving E›
  using km_trace_preserving_imp_reducing km_trace_reducing_iff_norm_leq1 that by blast

lemma km_trace_norm_preserving_eq: 
  fixes E :: ‹('a::{chilbert_space,not_singleton},'a) trace_class → ('b::chilbert_space,'b) trace_class›
  assumes ‹km_trace_preserving E›
  shows ‹km_norm E = 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 E›
  assumes ‹kraus_map F›
  shows ‹partial_trace (km_tensor F E ρ) = F (partial_trace ρ)›
proof -
  from assms
  obtain EE :: ‹(_,_,unit) kraus_family› where EE_def: ‹E = kf_apply EE› and tpEE: ‹kf_trace_preserving EE›
    using km_trace_preserving_def by blast
  obtain FF :: ‹(_,_,unit) kraus_family› where FF_def: ‹F = kf_apply FF›
    using assms(2) kraus_map_def_raw by blast
  have ‹partial_trace (km_tensor F E ρ) = partial_trace (kf_tensor FF EE *_kr ρ)›
    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 *_kr partial_trace ρ›
    by (simp add: partial_trace_ignores_kraus_family tpEE)
  also have ‹… = F (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 E› and ‹km_trace_preserving F›
  shows ‹km_trace_preserving (km_tensor E F)›
proof -
  from assms obtain EE :: ‹('a ell2, 'b ell2, unit) kraus_family› where EE: ‹E = 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: ‹F = 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 E› and ‹km_trace_reducing F›
  shows ‹km_trace_reducing (km_tensor E F)›
  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))² *_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) E = 0›
proof (cases ‹km_tensor_exists (0 :: ('a ell2, 'b ell2) trace_class → ('c ell2, 'd ell2) trace_class) E›)
  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 E (0 :: ('a ell2, 'b ell2) trace_class → ('c ell2, 'd ell2) trace_class) = 0›
proof (cases ‹km_tensor_exists E (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