Theory O2H_Additional_Lemmas

theory O2H_Additional_Lemmas
  imports Registers.Pure_States
begin

unbundle cblinfun_syntax
unbundle lattice_syntax

text ‹This theory contains additional lemmas on summability, trace, tensor product, sandwiching 
operator, arithmetic-quadratic mean inequality, matrices with norm less or equal one, projections
and more.›

text ‹An additional lemma›
lemma abs_summable_on_reindex:
  assumes ‹inj_on h A›
  shows ‹g abs_summable_on (h ` A) ⟷ (g ∘ h) abs_summable_on A›
proof -
  have "(norm ∘ g) summable_on (h ` A) ⟷ ((norm ∘ g) ∘ h) summable_on A"
    by (rule summable_on_reindex[OF assms])
  then show ?thesis unfolding comp_def by auto
qed


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 sandwich_tc_has_sum:
  assumes "(f has_sum x) A"
  shows "((sandwich_tc ρ o f) has_sum sandwich_tc ρ x) A"
  unfolding o_def by (intro has_sum_bounded_linear[OF _ assms]) 
    (auto simp add: bounded_clinear.bounded_linear bounded_clinear_sandwich_tc)

lemma sandwich_tc_abs_summable_on:
  assumes "f abs_summable_on A"
  shows "(sandwich_tc ρ o f) abs_summable_on A"
  by (intro abs_summable_on_bounded_linear) 
    (auto simp add: assms bounded_clinear.bounded_linear bounded_clinear_sandwich_tc)

lemma trace_tc_abs_summable_on:
  assumes "f abs_summable_on A"
  shows "(trace_tc o f) abs_summable_on A"
  by (intro abs_summable_on_bounded_linear) (auto simp add: assms bounded_clinear.bounded_linear)



text ‹Defining a self butterfly on trace class.›

lemma trace_selfbutter_norm:
  "trace (selfbutter A) = norm A ^2"
  by (simp add: power2_norm_eq_cinner trace_butterfly)


definition tc_selfbutter where "tc_selfbutter a = tc_butterfly a a"

lemma norm_tc_selfbutter[simp]:
  "norm (tc_selfbutter a) = (norm a)^2"
  unfolding tc_selfbutter_def using norm_tc_butterfly by (metis power2_eq_square)

lemma trace_tc_sandwich_tc_isometry: 
  assumes "isometry U" 
  shows "trace_tc (sandwich_tc U A) = trace_tc A"
  using assms by transfer auto

lemma norm_sandwich_tc_unitary:
  assumes "isometry U" "ρ ≥ 0"
  shows "norm (sandwich_tc U ρ) = norm ρ"
  using trace_tc_sandwich_tc_isometry[OF assms(1)] assms
  by (simp add: norm_tc_pos_Re sandwich_tc_pos)




text ‹Lemmas on const‹trace_tc››

lemma trace_tc_minus:
  "trace_tc (a-b) = trace_tc a - trace_tc b"
  by (metis add_implies_diff diff_add_cancel trace_tc_plus)

lemma trace_tc_sum:
  "trace_tc (sum a I) = (∑i∈I. trace_tc (a i))"
  by (simp add: from_trace_class_sum trace_sum trace_tc.rep_eq)


lemma selfbutter_sandwich:
  fixes A :: "'a ell2 ⇒CL 'a ell2" and B :: "'a ell2"
  shows "selfbutter (A *V B) = sandwich A *V selfbutter B"
  by (simp add: butterfly_comp_cblinfun cblinfun_comp_butterfly sandwich_apply)

lemma tc_tensor_sum_left:
  "tc_tensor (sum g S) x = (∑i∈S. tc_tensor (g i) x)"
  by transfer (auto simp add: tensor_op_cbilinear.sum_left)

lemma tc_tensor_sum_right:
  "tc_tensor x (sum g S) = (∑i∈S. tc_tensor x (g i))"
  by transfer (auto simp add: tensor_op_cbilinear.sum_right)

lemma complex_of_real_abs: "complex_of_real ¦f¦ = ¦complex_of_real f¦"
  by (simp add: abs_complex_def)




text ‹Additional Lemmas on Tensors›

lemma tensor_op_padding: 
  "(A ⊗o B) *V v = (A ⊗o id_cblinfun) *V (id_cblinfun ⊗o B) *V v"
  by (metis cblinfun_apply_cblinfun_compose cblinfun_compose_id_left cblinfun_compose_id_right 
      comp_tensor_op)

lemma tensor_op_padding': 
  "(A ⊗o B) *V v = (id_cblinfun ⊗o B) *V (A ⊗o id_cblinfun) *V v"
  by (subst cblinfun_apply_cblinfun_compose[symmetric], subst comp_tensor_op) auto

lemma tensor_op_left_minus: "(x - y) ⊗o b = x ⊗o b - y ⊗o b"
  by (metis ordered_field_class.sign_simps(10) tensor_op_left_add)

lemma tensor_op_right_minus: "b ⊗o (x - y) = b ⊗o x - b ⊗o y"
  by (metis ordered_field_class.sign_simps(10) tensor_op_right_add)

lemma id_cblinfun_selfbutter_tensor_ell2_right:
  "id_cblinfun ⊗o selfbutter (ket i) = (tensor_ell2_right (ket i)) oCL (tensor_ell2_right (ket i)*)"
  by (intro equal_ket) (auto simp add: tensor_ell2_ket[symmetric] tensor_op_ell2 
      tensor_ell2_scaleC2 tensor_ell2_scaleC1)



text ‹A lot lof lemmas on limit processes with several functions.›

lemma tendsto_Re:
  assumes "(f ⤏ x) F"
  shows "((λx. Re (f x)) ⤏ Re x) F"
  using assms by (simp add: tendsto_Re)

lemma tendsto_tc_tensor:
  assumes "(f ⤏ x) F"
  shows "((λx. tc_tensor (f x) a) ⤏ tc_tensor x a) F"
  using bounded_linear.tendsto[OF bounded_clinear.bounded_linear[OF bounded_clinear_tc_tensor_left] assms]
  by auto


lemma tc_tensor_has_sum:
  assumes "(f has_sum x) A"
  shows "((λy. tc_tensor y a) o f has_sum tc_tensor x a) A"
  unfolding o_def using has_sum_bounded_linear bounded_clinear_tc_tensor_left 
    assms bounded_clinear.bounded_linear by blast


lemma Re_has_sum:
  assumes "(f has_sum x) A"
  shows "((λn. Re n) o f has_sum Re x) A"
  by (metis assms(1) has_sum_Re has_sum_cong o_def)

text ‹Relationship norm and condition›

lemma norm_1_to_cond:
  fixes A :: "'a ell2 ⇒CL 'a ell2"
  assumes "norm A ≤ 1"
  shows "A* oCL A ≤ id_cblinfun"
proof -
  have "norm (A *V Ψ) ≤ norm Ψ" for Ψ :: "'a ell2"
    by (meson assms basic_trans_rules(23) mult_left_le_one_le norm_cblinfun norm_ge_zero)
  then have ineq: "norm (A *V Ψ)^2 ≤ norm Ψ^2" for  Ψ :: "'a ell2" by simp 
  have left: "norm (A *V Ψ)^2 = Ψ ∙C ((A* oCL A) *V Ψ)" for Ψ:: "'a ell2"
    by (simp add: cdot_square_norm cinner_adj_right)
  have right: "norm Ψ^2 = Ψ ∙C (id_cblinfun *V Ψ)" for Ψ:: "'a ell2"
    by (simp add: cdot_square_norm)
  have "Ψ ∙C ((A* oCL A) *V Ψ) ≤ Ψ ∙C (id_cblinfun *V Ψ)" for Ψ:: "'a ell2"
    using ineq left right by (simp add: cnorm_le)
  then show "A* oCL A ≤ id_cblinfun" using cblinfun_leI by blast
qed

lemma cond_to_norm_1:
  fixes A :: "'a ell2 ⇒CL 'a ell2"
  assumes "A* oCL A ≤ id_cblinfun"
  shows "norm A ≤ 1"
proof -
  have left: "norm (A *V Ψ)^2 = Ψ ∙C ((A* oCL A) *V Ψ)" for Ψ:: "'a ell2"
    by (simp add: cdot_square_norm cinner_adj_right)
  have right: "norm Ψ^2 = Ψ ∙C (id_cblinfun *V Ψ)" for Ψ:: "'a ell2"
    by (simp add: cdot_square_norm)
  have "Ψ ∙C ((A* oCL A) *V Ψ) ≤ Ψ ∙C (id_cblinfun *V Ψ)" for Ψ:: "'a ell2"
    using assms less_eq_cblinfun_def by blast
  then have ineq: "norm (A *V Ψ)^2 ≤ norm Ψ^2" for  Ψ :: "'a ell2"
    by (metis complex_of_real_mono_iff left right)
  then have "norm (A *V Ψ) ≤ norm Ψ" for Ψ :: "'a ell2" by simp
  then show "norm A ≤ 1" by (simp add: norm_cblinfun_bound)
qed


text ‹Arithmetic mean - quadratic mean inequality (AM-QM)›

lemma arith_quad_mean_ineq:
  fixes n::nat and x :: "nat ⇒ real"
  assumes "⋀i. i∈I ⟹ x i ≥ 0"
  shows "(∑i∈I. x i)^2 ≤ (card I) * (∑i∈I. (x i) ^2)"
  using Cauchy_Schwarz_ineq_sum[of "(λ_. 1)" x I] by auto

lemma sqrt_binom:
  assumes "a ≥ 0" "b ≥ 0"
  shows "¦a - b¦ = ¦sqrt a - sqrt b¦ * ¦sqrt a + sqrt b¦"
  by (metis abs_mult abs_pos assms(1) assms(2) cross3_simps(11) real_sqrt_abs2 real_sqrt_mult 
      square_diff_square_factored)





text ‹Lemmas on const‹sandwich_tc››

lemma sandwich_tc_compose':
  "sandwich_tc (A oCL B) ρ = sandwich_tc A (sandwich_tc B ρ)"
  using sandwich_tc_compose unfolding o_def by metis


lemma sandwich_tc_sum:
  "sandwich_tc E (sum f A) = sum (sandwich_tc E o f) A"
  by (metis sandwich_tc_0_right sandwich_tc_plus sum_comp_morphism)


lemma isCont_sandwich_tc:
  "isCont (sandwich_tc A) x"
  by (intro linear_continuous_at) 
    (simp add: bounded_clinear.bounded_linear bounded_clinear_sandwich_tc)

lemma bounded_linear_trace_norm_sandwich_tc:
  "bounded_linear (λy. trace_tc (sandwich_tc E y))"
  unfolding bounded_linear_def by (metis bounded_clinear.bounded_linear bounded_clinear_sandwich_tc 
      bounded_clinear_trace_tc bounded_linear_compose bounded_linear_def)

lemma sandwich_add1:
  "sandwich (A+B) C = sandwich A C + sandwich B C + A oCL C oCL B* + B oCL C oCL A*"
  by (simp add: adj_plus cblinfun_compose_add_left cblinfun_compose_add_right sandwich.rep_eq)

lemma sandwich_tc_add1:
  "sandwich_tc (A+B) C = sandwich_tc A C + sandwich_tc B C + 
  compose_tcl (compose_tcr B C) (A*) + compose_tcl (compose_tcr A C) (B*)"
  unfolding sandwich_tc_def 
  by (auto simp add: compose_tcr.add_left compose_tcl.add_left compose_tcl.add_right adj_plus)

lemma sandwich_add2:
  "sandwich A (B+C) = sandwich A B + sandwich A C"
  by (simp add: cblinfun.add_right)


text ‹On the spaces of projections with and/or or events.›

lemma splitting_Proj_and:
  assumes "is_Proj P" "is_Proj Q"
  shows "Proj (((P ⊗o id_cblinfun) *S ⊤) ⊓ ((id_cblinfun ⊗o Q) *S ⊤)) = P ⊗o Q"
proof -
  have tensor1: "(P ⊗o (id_cblinfun::'b ell2 ⇒CL 'b ell2)) *S ⊤ = (P *S ⊤) ⊗S ⊤"
    and tensor2: "((id_cblinfun::'a ell2 ⇒CL 'a ell2) ⊗o Q) *S ⊤ = ⊤ ⊗S (Q *S ⊤)"
    by (auto simp add: Proj_on_own_range assms tensor_ccsubspace_via_Proj)

  have "((P ⊗o id_cblinfun) *S ⊤) ⊓ ((id_cblinfun ⊗o Q) *S ⊤) =
    ((P *S ⊤) ⊗S ⊤) ⊓ (⊤ ⊗S (Q *S ⊤))"
    using tensor1 tensor2 by auto
  also have "… = (P *S ⊤) ⊗S (Q *S ⊤)"
    by (smt (z3) Proj_image_leq Proj_o_Proj_subspace_right Proj_on_own_range Proj_range assms 
        boolean_algebra_cancel.inf1 cblinfun_assoc_left(2) cblinfun_image_id inf.orderE 
        inf_commute inf_le2 is_Proj_id is_Proj_tensor_op isometry_cblinfun_image_inf_distrib' 
        tensor_ccsubspace_image tensor_ccsubspace_top)
  finally have rew: "((P ⊗o id_cblinfun) *S ⊤) ⊓ ((id_cblinfun ⊗o Q) *S ⊤) = 
    ((P ⊗o Q) *S ⊤)"
    by (simp add: tensor_ccsubspace_image)
  show ?thesis unfolding rew 
    by (simp add: Proj_on_own_range assms(1) assms(2) is_Proj_tensor_op)
qed


lemma splitting_Proj_or:
  assumes "is_Proj P" "is_Proj Q"
  shows "Proj (((P ⊗o id_cblinfun) *S ⊤) ⊔ ((id_cblinfun ⊗o Q) *S ⊤)) = 
  P ⊗o (id_cblinfun - Q) + id_cblinfun ⊗o Q"
proof -
  have tensor1: "(P ⊗o (id_cblinfun::'b ell2 ⇒CL 'b ell2)) *S ⊤ = (P *S ⊤) ⊗S ⊤"
    and tensor2: "((id_cblinfun::'a ell2 ⇒CL 'a ell2) ⊗o Q) *S ⊤ = ⊤ ⊗S (Q *S ⊤)"
    by (auto simp add: Proj_on_own_range assms tensor_ccsubspace_via_Proj)
  have "((P ⊗o id_cblinfun) *S ⊤) ⊔ ((id_cblinfun ⊗o Q) *S ⊤) = 
    ((P *S ⊤) ⊗S ⊤) ⊔ (⊤ ⊗S (Q *S ⊤))" using tensor1 tensor2 by auto
  also have "… = ((P *S ⊤) ⊗S (Q *S ⊤)) ⊔ ((P *S ⊤) ⊗S - (Q *S ⊤)) ⊔ 
    ((P *S ⊤) ⊗S (Q *S ⊤)) ⊔ (-(P *S ⊤) ⊗S (Q *S ⊤))"
    by (smt (z3) cblinfun_image_id cblinfun_image_sup complemented_lattice_class.sup_compl_top 
        ortho_tensor_ccsubspace_left ortho_tensor_ccsubspace_right sup_aci(2) tensor1 tensor2 
        tensor_ccsubspace_image)
  also have "… = ((P *S ⊤) ⊗S - (Q *S ⊤)) ⊔ ((P *S ⊤) ⊗S (Q *S ⊤)) ⊔ 
    (-(P *S ⊤) ⊗S (Q *S ⊤))" by (simp add: inf_sup_aci(5))
  also have "… = ((P *S ⊤) ⊗S - (Q *S ⊤)) ⊔ (⊤ ⊗S (Q *S ⊤))"
    by (smt (verit, del_insts) cblinfun_image_id cblinfun_image_sup complemented_lattice_class.compl_sup_top 
        inf_sup_aci(5) ortho_tensor_ccsubspace_left sup_aci(2) tensor2 tensor_ccsubspace_image)
  finally have rew: "((P ⊗o id_cblinfun) *S ⊤) ⊔ ((id_cblinfun ⊗o Q) *S ⊤) = 
    ((P ⊗o (id_cblinfun - Q)) *S ⊤) ⊔ ((id_cblinfun ⊗o Q) *S ⊤)"
    by (simp add: Proj_on_own_range assms(2) range_cblinfun_code_def tensor2 
        tensor_ccsubspace_image uminus_Span_code)
  have "Proj (((P ⊗o id_cblinfun) *S ⊤) ⊔ ((id_cblinfun ⊗o Q) *S ⊤)) =
    Proj ((P ⊗o (id_cblinfun - Q)) *S ⊤) + Proj ((id_cblinfun ⊗o Q) *S ⊤)" 
    unfolding rew by (intro Proj_sup) (smt (verit, del_insts) Proj_image_leq Proj_on_own_range
        Proj_ortho_compl assms(1) assms(2) ortho_tensor_ccsubspace_right orthogonal_spaces_leq_compl 
        range_cblinfun_code_def tensor2 tensor_ccsubspace_mono tensor_ccsubspace_via_Proj top_greatest 
        uminus_Span_code)
  also have "… = P ⊗o (id_cblinfun - Q) + id_cblinfun ⊗o Q"
    by (simp add: Proj_on_own_range assms(1) assms(2) is_Proj_tensor_op)
  finally show ?thesis by auto
qed


text ‹Additional stuff›

lemma Union_cong:
  assumes "⋀i. i∈A ⟹ f i = g i"
  shows "(⋃i∈A. f i) = (⋃ i∈A. g i)"
  using assms by auto


lemma proj_ket_apply:
  "proj (ket i) *V ket j = (if i=j then ket i else 0)"
  by (metis Proj_fixes_image ccspan_superset' insertI1 kernel_Proj kernel_memberD 
      mem_ortho_ccspanI orthogonal_ket singletonD)





text ‹Missing lemmas for Kraus maps›
  (* This is a subset of the Missing2.thy file from the qrhl-tool Kraus map implementation. *)

lemma infsum_in_finite:
  assumes "finite F"
  assumes ‹Hausdorff_space T›
  assumes ‹sum f F ∈ topspace T›
  shows "infsum_in T f F = sum f F"
  using has_sum_in_finite[OF assms(1,3)]
  using assms(2) has_sum_in_infsum_in has_sum_in_unique summable_on_in_def by blast


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 clinear_of_complex[iff]: ‹clinear of_complex›
  by (simp add: clinearI)

lemma inj_on_CARD_1[iff]: ‹inj_on f X› for X :: ‹'a::CARD_1 set›
  by (auto intro!: inj_onI)

unbundle no cblinfun_syntax
unbundle no lattice_syntax


end