Theory Misc_Kraus_Maps

section ‹Miscelleanous missing theorems›

theory Misc_Kraus_Maps
  imports
    Hilbert_Space_Tensor_Product.Hilbert_Space_Tensor_Product
    Hilbert_Space_Tensor_Product.Von_Neumann_Algebras
begin

unbundle cblinfun_syntax

lemma abs_summable_norm:
  assumes ‹f abs_summable_on A›
  shows ‹(λx. norm (f x)) abs_summable_on A›
  using assms by simp

lemma abs_summable_on_add:
  assumes ‹f abs_summable_on A› and ‹g abs_summable_on A›
  shows ‹(λx. f x + g x) abs_summable_on A›
proof -
  from assms have ‹(λx. norm (f x) + norm (g x)) summable_on A›
    using summable_on_add by blast
  then show ?thesis
    apply (rule Infinite_Sum.abs_summable_on_comparison_test')
    using norm_triangle_ineq by blast
qed

lemma bdd_above_transform_mono_pos:
  assumes bdd: ‹bdd_above ((λx. g x) ` M)›
  assumes gpos: ‹⋀x. x ∈ M ⟹ g x ≥ 0›
  assumes mono: ‹mono_on (Collect ((≤) 0)) f›
  shows ‹bdd_above ((λx. f (g x)) ` M)›
proof (cases ‹M = {}›)
  case True
  then show ?thesis
    by simp
next
  case False
  from bdd obtain B where B: ‹g x ≤ B› if ‹x ∈ M› for x
  by (meson bdd_above.unfold imageI)
  with gpos False have ‹B ≥ 0›
    using dual_order.trans by blast
  have ‹f (g x) ≤ f B› if ‹x ∈ M› for x
    using mono _ _ B
    apply (rule mono_onD)
    by (auto intro!: gpos that  ‹B ≥ 0›)
  then show ?thesis
    by fast
qed

lemma Ex_iffI:
  assumes ‹⋀x. P x ⟹ Q (f x)›
  assumes ‹⋀x. Q x ⟹ P (g x)›
  shows ‹Ex P ⟷ Ex Q›
  using assms(1) assms(2) by auto

lemma has_sum_Sigma'_banach:
  fixes A :: "'a set" and B :: "'a ⇒ 'b set"
    and f :: ‹'a ⇒ 'b ⇒ 'c::banach›
  assumes "((λ(x,y). f x y) has_sum S) (Sigma A B)"
  shows ‹((λx. infsum (f x) (B x)) has_sum S) A›
  by (metis (no_types, lifting) assms has_sum_cong has_sum_imp_summable has_sum_infsum infsumI infsum_Sigma'_banach summable_on_Sigma_banach)

lemma infsum_Sigma_topological_monoid:
  fixes A :: "'a set" and B :: "'a ⇒ 'b set"
    and f :: ‹'a × 'b ⇒ 'c::{topological_comm_monoid_add, t3_space}›
  assumes summableAB: "f summable_on (Sigma A B)"
  assumes summableB: ‹⋀x. x∈A ⟹ (λy. f (x, y)) summable_on (B x)›
  shows "infsum f (Sigma A B) = (∑⇩∞x∈A. ∑⇩∞y∈B x. f (x, y))"
proof -
  have 1: ‹(f has_sum infsum f (Sigma A B)) (Sigma A B)›
    by (simp add: assms)
  define b where ‹b x = (∑⇩∞y∈B x. f (x, y))› for x
  have 2: ‹((λy. f (x, y)) has_sum b x) (B x)› if ‹x ∈ A› for x
    using b_def assms(2) that by auto
  have 3: ‹(b has_sum (∑⇩∞x∈A. b x)) A›
    using 1 2 by (metis has_sum_SigmaD infsumI)
  have 4: ‹(f has_sum (∑⇩∞x∈A. b x)) (Sigma A B)›
    using 2 3 apply (rule has_sum_SigmaI)
    using assms by auto
  from 1 4 show ?thesis
    using b_def[abs_def] infsumI by blast
qed

lemma flip_eq_const: ‹(λy. y = x) = ((=) x)›
  by auto

lemma sgn_ket[simp]: ‹sgn (ket x) = ket x›
  by (simp add: sgn_div_norm)

lemma tensor_op_in_tensor_vn:
  assumes ‹a ∈ A› and ‹b ∈ B›
  shows ‹a ⊗⇩o b ∈ A ⊗⇩v⇩N B›
proof -
  have ‹a ⊗⇩o id_cblinfun ∈ A ⊗⇩v⇩N B›
    by (metis (no_types, lifting) Un_iff assms(1) double_commutant_grows' image_iff tensor_vn_def)
  moreover have ‹id_cblinfun ⊗⇩o b ∈ A ⊗⇩v⇩N B›
    by (simp add: assms(2) double_commutant_grows' tensor_vn_def)
  ultimately have ‹(a ⊗⇩o id_cblinfun) o⇩C⇩L (id_cblinfun ⊗⇩o b) ∈ A ⊗⇩v⇩N B›
    using commutant_mult tensor_vn_def by blast
  then show ?thesis
    by (simp add: comp_tensor_op)
qed

lemma commutant_tensor_vn_subset: 
  assumes ‹von_neumann_algebra A› and ‹von_neumann_algebra B›
  shows ‹commutant A ⊗⇩v⇩N commutant B ⊆ commutant (A ⊗⇩v⇩N B)›
proof -
  have 1: ‹a ⊗⇩o id_cblinfun ∈ commutant (A ⊗⇩v⇩N B)› if ‹a ∈ commutant A› for a
    apply (simp add: tensor_vn_def)
    using that by (auto intro!: simp: commutant_def comp_tensor_op)
  have 2: ‹id_cblinfun ⊗⇩o b ∈ commutant (A ⊗⇩v⇩N B)› if ‹b ∈ commutant B› for b
    apply (simp add: tensor_vn_def)
    using that by (auto intro!: simp: commutant_def comp_tensor_op)
  show ?thesis
    apply (subst tensor_vn_def)
    apply (rule double_commutant_in_vn_algI)
    using 1 2
    by (auto intro!: von_neumann_algebra_commutant von_neumann_algebra_tensor_vn assms)
qed

lemma commutant_span[simp]: ‹commutant (span X) = commutant X›
proof (rule order_antisym)
  have ‹commutant X ⊆ commutant (cspan X)›
    by (simp add: commutant_cspan)
  also have ‹… ⊆ commutant (span X)›
    by (simp add: commutant_antimono span_subset_cspan)
  finally show ‹commutant X ⊆ commutant (span X)›
    by -
  show ‹commutant (span X) ⊆ commutant X›
    by (simp add: commutant_antimono span_superset)
qed


lemma explicit_cblinfun_exists_0[simp]: ‹explicit_cblinfun_exists (λ_ _. 0)›
  by (auto intro!: explicit_cblinfun_exists_bounded[where B=0] simp: explicit_cblinfun_def)

lemma explicit_cblinfun_0[simp]: ‹explicit_cblinfun (λ_ _. 0) = 0›
  by (auto intro!: equal_ket Rep_ell2_inject[THEN iffD1] ext simp: Rep_ell2_explicit_cblinfun_ket zero_ell2.rep_eq)

lemma cnj_of_bool[simp]: ‹cnj (of_bool b) = of_bool b›
  by simp

lemma has_sum_single: 
  fixes f :: ‹_ ⇒ _::{comm_monoid_add,t2_space}›
  assumes "⋀j. j ≠ i ⟹ j∈A ⟹ f j = 0"
  assumes ‹s = (if i∈A then f i else 0)›
  shows "HAS_SUM f A s"
  apply (subst has_sum_cong_neutral[where T=‹A ∩ {i}› and g=f])
  using assms by auto

lemma classical_operator_None[simp]: ‹classical_operator (λ_. None) = 0›
  by (auto intro!: equal_ket simp: classical_operator_ket inj_map_def classical_operator_exists_inj)

lemma has_sum_in_in_closedsubspace:
  assumes ‹has_sum_in T f A l›
  assumes ‹⋀x. x∈A ⟹ f x ∈ S›
  assumes ‹closedin T S›
  assumes ‹csubspace S›
  shows ‹l ∈ S›
proof -
  from assms
  have ‹limitin T (sum f) l (finite_subsets_at_top A)›
    by (simp add: has_sum_in_def)
  then have ‹limitin T (λF. if F⊆A then sum f F else 0) l (finite_subsets_at_top A)›
    apply (rule limitin_transform_eventually[rotated])
    apply (rule eventually_finite_subsets_at_top_weakI)
    by simp
  then show ‹l ∈ S›
    apply (rule limitin_closedin)
    using assms by (auto intro!: complex_vector.subspace_0 simp: complex_vector.subspace_sum subsetD)
qed


lemma has_sum_coordinatewise:
  ‹(f has_sum s) A ⟷ (∀i. ((λx. f x i) has_sum s i) A)›
proof -
  have ‹(f has_sum s) A ⟷ ((λF. (∑x∈F. f x)) ⤏ s) (finite_subsets_at_top A)›
    by (simp add: has_sum_def)
  also  have ‹… ⟷ (∀i. ((λF. (∑x∈F. f x) i) ⤏ s i) (finite_subsets_at_top A))›
    by (simp add: tendsto_coordinatewise)
  also have ‹… ⟷ (∀i. ((λF. ∑x∈F. f x i) ⤏ s i) (finite_subsets_at_top A))›
  proof (rewrite at ‹∑x∈F. f x i› at ‹λF. ⌑› in ‹∀i. ⌑› to ‹(∑x∈F. f x) i› DEADID.rel_mono_strong)
    fix i
    show ‹(∑x∈F. f x i) = (∑x∈F. f x) i› for F
      apply (induction F rule:infinite_finite_induct)
      by auto
    show ‹P = P› for P :: bool
      by simp
  qed
  also have ‹… ⟷ (∀i. ((λx. f x i) has_sum s i) A)›
    by (simp add: has_sum_def)
  finally show ?thesis
    by - 
qed


lemma one_dim_butterfly:
  ‹butterfly g h = (one_dim_iso g * cnj (one_dim_iso h)) *⇩C 1›
  apply (rule cblinfun_eq_on_canonical_basis)
  apply simp
  by (smt (verit, del_insts) Groups.mult_ac(2) cblinfun.scaleC_left of_complex_def of_complex_inner_1
      of_complex_inner_1' one_cblinfun_apply_one one_dim_apply_is_times_def one_dim_iso_def
      one_dim_scaleC_1)



lemma one_dim_tc_butterfly:
  fixes g :: ‹'a :: one_dim› and h :: ‹'b :: one_dim›
  shows ‹tc_butterfly g h = (one_dim_iso g * cnj (one_dim_iso h)) *⇩C 1›
proof -
  have ‹tc_butterfly g h = one_dim_iso (butterfly g h)›
  by (metis (mono_tags, lifting) from_trace_class_one_dim_iso one_dim_iso_inj one_dim_iso_is_of_complex
      one_dim_iso_of_complex tc_butterfly.rep_eq)
  also have ‹… = (one_dim_iso g * cnj (one_dim_iso h)) *⇩C 1›
    by (simp add: one_dim_butterfly)
  finally show ?thesis
    by -
qed

lemma one_dim_iso_of_real[simp]: ‹one_dim_iso (of_real x) = of_real x›
  apply (simp add: of_real_def)
  by (simp add: scaleR_scaleC del: of_complex_of_real_eq)

lemma filter_insert_if:
  ‹Set.filter P (insert x M) = (if P x then insert x (Set.filter P M) else Set.filter P M)›
  by auto

lemma filter_empty[simp]: ‹Set.filter P {} = {}›
  by auto

lemma has_sum_in_cong_neutral:
  fixes f g :: ‹'a ⇒ 'b::comm_monoid_add›
  assumes ‹⋀x. x∈T-S ⟹ g x = 0›
  assumes ‹⋀x. x∈S-T ⟹ f x = 0›
  assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
  shows "has_sum_in X f S x ⟷ has_sum_in X g T x"
proof -
  have ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))
      = eventually P (filtermap (sum g) (finite_subsets_at_top T))› for P
  proof 
    assume ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))›
    then obtain F0 where ‹finite F0› and ‹F0 ⊆ S› and F0_P: ‹⋀F. finite F ⟹ F ⊆ S ⟹ F ⊇ F0 ⟹ P (sum f F)›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where ‹F0' = F0 ∩ T›
    have [simp]: ‹finite F0'› ‹F0' ⊆ T›
      by (simp_all add: F0'_def ‹finite F0›)
    have ‹P (sum g F)› if ‹finite F› ‹F ⊆ T› ‹F ⊇ F0'› for F
    proof -
      have ‹P (sum f ((F∩S) ∪ (F0∩S)))›
        by (intro F0_P) (use ‹F0 ⊆ S› ‹finite F0› that in auto)
      also have ‹sum f ((F∩S) ∪ (F0∩S)) = sum g F›
        by (intro sum.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
      finally show ?thesis .
    qed
    with ‹F0' ⊆ T› ‹finite F0'› show ‹eventually P (filtermap (sum g) (finite_subsets_at_top T))›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  next
    assume ‹eventually P (filtermap (sum g) (finite_subsets_at_top T))›
    then obtain F0 where ‹finite F0› and ‹F0 ⊆ T› and F0_P: ‹⋀F. finite F ⟹ F ⊆ T ⟹ F ⊇ F0 ⟹ P (sum g F)›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
    define F0' where ‹F0' = F0 ∩ S›
    have [simp]: ‹finite F0'› ‹F0' ⊆ S›
      by (simp_all add: F0'_def ‹finite F0›)
    have ‹P (sum f F)› if ‹finite F› ‹F ⊆ S› ‹F ⊇ F0'› for F
    proof -
      have ‹P (sum g ((F∩T) ∪ (F0∩T)))›
        by (intro F0_P) (use ‹F0 ⊆ T› ‹finite F0› that in auto)
      also have ‹sum g ((F∩T) ∪ (F0∩T)) = sum f F›
        by (intro sum.mono_neutral_cong) (use that ‹finite F0› F0'_def assms in auto)
      finally show ?thesis .
    qed
    with ‹F0' ⊆ S› ‹finite F0'› show ‹eventually P (filtermap (sum f) (finite_subsets_at_top S))›
      by (metis (no_types, lifting) eventually_filtermap eventually_finite_subsets_at_top)
  qed

  then have tendsto_x: "limitin X (sum f) x (finite_subsets_at_top S) ⟷ limitin X (sum g) x (finite_subsets_at_top T)" for x
    by (simp add: le_filter_def filterlim_def flip: filterlim_nhdsin_iff_limitin)
  then show ?thesis
    by (simp add: has_sum_in_def)
qed


lemma infsum_in_cong_neutral: 
  fixes f g :: ‹'a ⇒ 'b::comm_monoid_add›
  assumes ‹⋀x. x∈T-S ⟹ g x = 0›
  assumes ‹⋀x. x∈S-T ⟹ f x = 0›
  assumes ‹⋀x. x∈S∩T ⟹ f x = g x›
  shows ‹infsum_in X f S = infsum_in X g T›
  apply (rule infsum_in_eqI')
  apply (rule has_sum_in_cong_neutral)
  using assms by auto

lemma filter_image: ‹Set.filter P (f ` X) = f ` (Set.filter (λx. P (f x)) X)›
  by auto

lemma Sigma_image_left: ‹(SIGMA x:f`A. B x) = (λ(x,y). (f x, y)) ` (SIGMA x:A. B (f x))›
  by (auto intro!: image_eqI simp: split: prod.split)

lemma finite_subset_filter_image:
  assumes "finite B"
  assumes ‹B ⊆ Set.filter P (f ` A)›
  shows "∃C⊆A. finite C ∧ B = f ` C"
proof -
  from assms have ‹B ⊆ f ` A›
    by auto
  then show ?thesis
    by (simp add: assms(1) finite_subset_image)
qed

definition ‹card_le_1 M ⟷ (∃x. M ⊆ {x})›

lemma card_le_1_empty[iff]: ‹card_le_1 {}›
  by (simp add: card_le_1_def)

lemma card_le_1_signleton[iff]: ‹card_le_1 {x}›
  using card_le_1_def by fastforce

lemma sgn_tensor_ell2: ‹sgn (h ⊗⇩s k) = sgn h ⊗⇩s sgn k›
  by (simp add: sgn_div_norm norm_tensor_ell2 scaleR_scaleC tensor_ell2_scaleC1 tensor_ell2_scaleC2)

lemma is_ortho_set_tensor:
  assumes ‹is_ortho_set B›
  assumes ‹is_ortho_set C›
  shows ‹is_ortho_set ((λ(x, y). x ⊗⇩s y) ` (B × C))›
proof (intro is_ortho_set_def[THEN iffD2] conjI notI ballI impI)
  fix bc bc' :: ‹('a × 'b) ell2›
  assume ‹bc ∈ (λ(x, y). x ⊗⇩s y) ` (B × C)› 
  then obtain b c where ‹b ∈ B› ‹c ∈ C› and bc: ‹bc = b ⊗⇩s c›
    by fast
  assume ‹bc' ∈ (λ(x, y). x ⊗⇩s y) ` (B × C)›
  then obtain b' c' where ‹b' ∈ B› ‹c' ∈ C› and bc': ‹bc' = b' ⊗⇩s c'›
    by fast
  assume ‹bc ≠ bc'›
  then consider (neqb) ‹b ≠ b'› | (neqc) ‹c ≠ c'›
    using bc bc' by blast
  then show ‹is_orthogonal bc bc'›
  proof cases
    case neqb
    with ‹b ∈ B› ‹b' ∈ B› ‹is_ortho_set B›
    have ‹b ∙⇩C b' = 0›
      by (simp add: is_ortho_setD)
    then show ?thesis
      by (simp add: bc bc')
  next
    case neqc
    with ‹c ∈ C› ‹c' ∈ C› ‹is_ortho_set C›
    have ‹c ∙⇩C c' = 0›
      by (simp add: is_ortho_setD)
    then show ?thesis
      by (simp add: bc bc')
  qed
next
  assume ‹0 ∈ (λ(x, y). x ⊗⇩s y) ` (B × C)›
  then obtain b c where ‹b ∈ B› ‹c ∈ C› and ‹b ⊗⇩s c = 0›
    by auto
  then show False
    by (metis assms(1,2) is_ortho_set_def tensor_ell2_nonzero)
qed



end