# Theory Finite_Tensor_Product

```section ‹Tensor products (finite dimensional)›

theory Finite_Tensor_Product
imports Complex_Bounded_Operators.Complex_L2 Misc
begin

declare cblinfun.scaleC_right[simp]

unbundle cblinfun_notation
no_notation m_inv ("invı _" [81] 80)

lift_definition tensor_ell2 :: ‹'a::finite ell2 ⇒ 'b::finite ell2 ⇒ ('a×'b) ell2› (infixr "⊗⇩s" 70) is
‹λψ φ (i,j). ψ i * φ j›
by simp

lemma tensor_ell2_add2: ‹tensor_ell2 a (b + c) = tensor_ell2 a b + tensor_ell2 a c›
apply transfer apply (rule ext) apply (auto simp: case_prod_beta)
by (meson algebra_simps)

lemma tensor_ell2_add1: ‹tensor_ell2 (a + b) c = tensor_ell2 a c + tensor_ell2 b c›
apply transfer apply (rule ext) apply (auto simp: case_prod_beta)
by (simp add: vector_space_over_itself.scale_left_distrib)

lemma tensor_ell2_scaleC2: ‹tensor_ell2 a (c *⇩C b) = c *⇩C tensor_ell2 a b›
apply transfer apply (rule ext) by (auto simp: case_prod_beta)

lemma tensor_ell2_scaleC1: ‹tensor_ell2 (c *⇩C a) b = c *⇩C tensor_ell2 a b›
apply transfer apply (rule ext) by (auto simp: case_prod_beta)

lemma tensor_ell2_inner_prod[simp]: ‹⟨tensor_ell2 a b, tensor_ell2 c d⟩ = ⟨a,c⟩ * ⟨b,d⟩›
apply transfer
by (auto simp: case_prod_beta sum_product sum.cartesian_product mult.assoc mult.left_commute)

lemma clinear_tensor_ell21: "clinear (λb. tensor_ell2 a b)"
apply (rule clinearI; transfer)
apply (auto simp: case_prod_beta)
by (simp add: cond_case_prod_eta algebra_simps)

lemma clinear_tensor_ell22: "clinear (λa. tensor_ell2 a b)"
apply (rule clinearI; transfer)
apply (auto simp: case_prod_beta)
by (simp add: case_prod_beta' algebra_simps)

lemma tensor_ell2_ket[simp]: "tensor_ell2 (ket i) (ket j) = ket (i,j)"
apply transfer by auto

definition tensor_op :: ‹('a ell2, 'b::finite ell2) cblinfun ⇒ ('c ell2, 'd::finite ell2) cblinfun
⇒ (('a×'c) ell2, ('b×'d) ell2) cblinfun› (infixr "⊗⇩o" 70) where
‹tensor_op M N = (SOME P. ∀a c. P *⇩V (ket (a,c))
= tensor_ell2 (M *⇩V ket a) (N *⇩V ket c))›

lemma tensor_op_ket:
fixes a :: ‹'a::finite› and b :: ‹'b› and c :: ‹'c::finite› and d :: ‹'d›
shows ‹tensor_op M N *⇩V (ket (a,c)) = tensor_ell2 (M *⇩V ket a) (N *⇩V ket c)›
proof -
define S :: ‹('a×'c) ell2 set› where "S = ket ` UNIV"
define φ where ‹φ = (λ(a,c). tensor_ell2 (M *⇩V ket a) (N *⇩V ket c))›
define φ' where ‹φ' = φ ∘ inv ket›

have def: ‹tensor_op M N = (SOME P. ∀a c. P *⇩V (ket (a,c)) = φ (a,c))›
unfolding tensor_op_def φ_def by auto

have ‹cindependent S›
using S_def cindependent_ket by blast
moreover have ‹cspan S = UNIV›
using S_def cspan_range_ket_finite by blast
ultimately have "cblinfun_extension_exists S φ'"
by (rule cblinfun_extension_exists_finite_dim)
then have "∃P. ∀x∈S. P *⇩V x = φ' x"
unfolding cblinfun_extension_exists_def by auto
then have ex: ‹∃P. ∀a c. P *⇩V ket (a,c) = φ (a,c)›
by (metis S_def φ'_def comp_eq_dest_lhs inj_ket inv_f_f rangeI)

then have ‹tensor_op M N *⇩V (ket (a,c)) = φ (a,c)›
unfolding def apply (rule someI2_ex[where P=‹λP. ∀a c. P *⇩V (ket (a,c)) = φ (a,c)›])
by auto
then show ?thesis
unfolding φ_def by auto
qed

lemma tensor_op_ell2: "tensor_op A B *⇩V tensor_ell2 ψ φ = tensor_ell2 (A *⇩V ψ) (B *⇩V φ)"
proof -
have 1: ‹clinear (λa. tensor_op A B *⇩V tensor_ell2 a (ket b))› for b
by (auto intro!: clinearI simp: tensor_ell2_add1 tensor_ell2_scaleC1 cblinfun.add_right)
have 2: ‹clinear (λa. tensor_ell2 (A *⇩V a) (B *⇩V ket b))› for b
by (auto intro!: clinearI simp: tensor_ell2_add1 tensor_ell2_scaleC1 cblinfun.add_right)
have 3: ‹clinear (λa. tensor_op A B *⇩V tensor_ell2 ψ a)›
by (auto intro!: clinearI simp: tensor_ell2_add2 tensor_ell2_scaleC2 cblinfun.add_right)
have 4: ‹clinear (λa. tensor_ell2 (A *⇩V ψ) (B *⇩V a))›
by (auto intro!: clinearI simp: tensor_ell2_add2 tensor_ell2_scaleC2 cblinfun.add_right)

have eq_ket_ket: ‹tensor_op A B *⇩V tensor_ell2 (ket a) (ket b) = tensor_ell2 (A *⇩V ket a) (B *⇩V ket b)› for a b
by (simp add: tensor_op_ket)
have eq_ket: ‹tensor_op A B *⇩V tensor_ell2 ψ (ket b) = tensor_ell2 (A *⇩V ψ) (B *⇩V ket b)› for b
apply (rule fun_cong[where x=ψ])
using 1 2 eq_ket_ket by (rule clinear_equal_ket)
show ?thesis
apply (rule fun_cong[where x=φ])
using 3 4 eq_ket by (rule clinear_equal_ket)
qed

lemma comp_tensor_op: "(tensor_op a b) o⇩C⇩L (tensor_op c d) = tensor_op (a o⇩C⇩L c) (b o⇩C⇩L d)"
for a :: "'e::finite ell2 ⇒⇩C⇩L 'c::finite ell2" and b :: "'f::finite ell2 ⇒⇩C⇩L 'd::finite ell2" and
c :: "'a::finite ell2 ⇒⇩C⇩L 'e ell2" and d :: "'b::finite ell2 ⇒⇩C⇩L 'f ell2"
apply (rule equal_ket)
apply (rename_tac ij, case_tac ij, rename_tac i j, hypsubst_thin)
by (simp flip: tensor_ell2_ket add: tensor_op_ell2 cblinfun_apply_cblinfun_compose)

lemma tensor_op_cbilinear: ‹cbilinear (tensor_op :: 'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2
⇒ 'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2 ⇒ _)›
proof -
have ‹clinear (λb::'c ell2 ⇒⇩C⇩L 'd ell2. tensor_op a b)› for a :: ‹'a ell2 ⇒⇩C⇩L 'b ell2›
apply (rule clinearI)
apply (rule equal_ket, rename_tac ij, case_tac ij, rename_tac i j, hypsubst_thin)
apply (rule equal_ket, rename_tac ij, case_tac ij, rename_tac i j, hypsubst_thin)
by (simp add: scaleC_cblinfun.rep_eq tensor_ell2_scaleC2 tensor_op_ket)

moreover have ‹clinear (λa::'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2. tensor_op a b)› for b :: ‹'c ell2 ⇒⇩C⇩L 'd ell2›
apply (rule clinearI)
apply (rule equal_ket, rename_tac ij, case_tac ij, rename_tac i j, hypsubst_thin)
apply (rule equal_ket, rename_tac ij, case_tac ij, rename_tac i j, hypsubst_thin)
by (simp add: scaleC_cblinfun.rep_eq tensor_ell2_scaleC1 tensor_op_ket)

ultimately show ?thesis
unfolding cbilinear_def by auto
qed

lemma tensor_butter: ‹tensor_op (butterket i j) (butterket k l) = butterket (i,k) (j,l)›
for i :: "_" and j :: "_::finite" and k :: "_" and l :: "_::finite"
apply (rule equal_ket, rename_tac x, case_tac x)
apply (auto simp flip: tensor_ell2_ket simp: cblinfun_apply_cblinfun_compose tensor_op_ell2 butterfly_def)
by (auto simp: tensor_ell2_scaleC1 tensor_ell2_scaleC2)

lemma cspan_tensor_op: ‹cspan {tensor_op (butterket i j) (butterket k l)| i (j::_::finite) k (l::_::finite). True} = UNIV›
unfolding tensor_butter
apply (subst cspan_butterfly_ket[symmetric])
by (metis surj_pair)

lemma cindependent_tensor_op: ‹cindependent {tensor_op (butterket i j) (butterket k l)| i (j::_::finite) k (l::_::finite). True}›
unfolding tensor_butter
using cindependent_butterfly_ket
by (smt (z3) Collect_mono_iff complex_vector.independent_mono)

lemma tensor_extensionality:
fixes F G :: ‹((('a::finite × 'b::finite) ell2) ⇒⇩C⇩L (('c::finite × 'd::finite) ell2)) ⇒ 'e::complex_vector›
assumes [simp]: "clinear F" "clinear G"
assumes tensor_eq: "(⋀a b. F (tensor_op a b) = G (tensor_op a b))"
shows "F = G"
proof (rule ext, rule complex_vector.linear_eq_on_span[where f=F and g=G])
show ‹clinear F› and ‹clinear G›
using assms by (simp_all add: cbilinear_def)
show ‹x ∈ cspan  {tensor_op (butterket i j) (butterket k l)| i j k l. True}›
for x :: ‹('a × 'b) ell2 ⇒⇩C⇩L ('c × 'd) ell2›
using cspan_tensor_op by auto
show ‹F x = G x› if ‹x ∈ {tensor_op (butterket i j) (butterket k l) |i j k l. True}› for x
using that by (auto simp: tensor_eq)
qed

lemma tensor_id[simp]: ‹tensor_op id_cblinfun id_cblinfun = id_cblinfun›
apply (rule equal_ket, rename_tac x, case_tac x)
by (simp flip: tensor_ell2_ket add: tensor_op_ell2)

lemma tensor_op_adjoint: ‹(tensor_op a b)* = tensor_op (a*) (b*)›
apply (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma tensor_butterfly[simp]: "tensor_op (butterfly ψ ψ') (butterfly φ φ') = butterfly (tensor_ell2 ψ φ) (tensor_ell2 ψ' φ')"
apply (rule equal_ket, rename_tac x, case_tac x)
by (simp flip: tensor_ell2_ket add: tensor_op_ell2 butterfly_def
cblinfun_apply_cblinfun_compose tensor_ell2_scaleC1 tensor_ell2_scaleC2)

definition tensor_lift :: ‹(('a1::finite ell2 ⇒⇩C⇩L 'a2::finite ell2) ⇒ ('b1::finite ell2 ⇒⇩C⇩L 'b2::finite ell2) ⇒ 'c)
⇒ ((('a1×'b1) ell2 ⇒⇩C⇩L ('a2×'b2) ell2) ⇒ 'c::complex_vector)› where
"tensor_lift F2 = (SOME G. clinear G ∧ (∀a b. G (tensor_op a b) = F2 a b))"

lemma
fixes F2 :: "'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2
⇒ 'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2
⇒ 'e::complex_normed_vector"
assumes "cbilinear F2"
shows tensor_lift_clinear: "clinear (tensor_lift F2)"
and tensor_lift_correct:  ‹(λa b. tensor_lift F2 (tensor_op a b)) = F2›
proof -
define F2' t4 φ where
‹F2' = tensor_lift F2› and
‹t4 = (λ(i,j,k,l). tensor_op (butterket i j) (butterket k l))› and
‹φ m = (let (i,j,k,l) = inv t4 m in F2 (butterket i j) (butterket k l))› for m
have t4inj: "x = y" if "t4 x = t4 y" for x y
proof (rule ccontr)
obtain i  j  k  l  where x: "x = (i,j,k,l)" by (meson prod_cases4)
obtain i' j' k' l' where y: "y = (i',j',k',l')" by (meson prod_cases4)
have 1: "bra (i,k) *⇩V t4 x *⇩V ket (j,l) = 1"
by (auto simp: t4_def x tensor_op_ell2 butterfly_def cinner_ket simp flip: tensor_ell2_ket)
assume ‹x ≠ y›
then have 2: "bra (i,k) *⇩V t4 y *⇩V ket (j,l) = 0"
by (auto simp: t4_def x y tensor_op_ell2 butterfly_def cblinfun_apply_cblinfun_compose cinner_ket
simp flip: tensor_ell2_ket)
from 1 2 that
show False
by auto
qed
have ‹φ (tensor_op (butterket i j) (butterket k l)) = F2 (butterket i j) (butterket k l)› for i j k l
apply (subst asm_rl[of ‹tensor_op (butterket i j) (butterket k l) = t4 (i,j,k,l)›])
apply (simp add: t4_def)
by (auto simp add: injI t4inj inv_f_f φ_def)

have *: ‹range t4 = {tensor_op (butterket i j) (butterket k l) |i j k l. True}›
apply (auto simp: case_prod_beta t4_def)
using image_iff by fastforce

have "cblinfun_extension_exists (range t4) φ"
thm cblinfun_extension_exists_finite_dim[where φ=φ]
apply (rule cblinfun_extension_exists_finite_dim)
apply auto unfolding *
using cindependent_tensor_op
using cspan_tensor_op
by auto

then obtain G where G: ‹G *⇩V (t4 (i,j,k,l)) = F2 (butterket i j) (butterket k l)› for i j k l
apply atomize_elim
unfolding cblinfun_extension_exists_def
apply auto
by (metis (no_types, lifting) t4inj φ_def f_inv_into_f rangeI split_conv)

have *: ‹G *⇩V tensor_op (butterket i j) (butterket k l) = F2 (butterket i j) (butterket k l)› for i j k l
using G by (auto simp: t4_def)
have *: ‹G *⇩V tensor_op a (butterket k l) = F2 a (butterket k l)› for a k l
apply (rule complex_vector.linear_eq_on_span[where g=‹λa. F2 a _› and B=‹{butterket k l|k l. True}›])
unfolding cspan_butterfly_ket
using * apply (auto intro!: clinear_compose[unfolded o_def, where f=‹λa. tensor_op a _› and g=‹(*⇩V) G›])
apply (metis cbilinear_def tensor_op_cbilinear)
using assms unfolding cbilinear_def by blast
have G_F2: ‹G *⇩V tensor_op a b = F2 a b› for a b
apply (rule complex_vector.linear_eq_on_span[where g=‹F2 a› and B=‹{butterket k l|k l. True}›])
unfolding cspan_butterfly_ket
using * apply (auto simp: cblinfun.add_right clinearI
intro!: clinear_compose[unfolded o_def, where f=‹tensor_op a› and g=‹(*⇩V) G›])
apply (meson cbilinear_def tensor_op_cbilinear)
using assms unfolding cbilinear_def by blast

have ‹clinear F2' ∧ (∀a b. F2' (tensor_op a b) = F2 a b)›
unfolding F2'_def tensor_lift_def
apply (rule someI[where x=‹(*⇩V) G› and P=‹λG. clinear G ∧ (∀a b. G (tensor_op a b) = F2 a b)›])
using G_F2 by (simp add: cblinfun.add_right clinearI)

then show ‹clinear F2'› and ‹(λa b. tensor_lift F2 (tensor_op a b)) = F2›
unfolding F2'_def by auto
qed

lift_definition assoc_ell20 :: ‹(('a::finite×'b::finite)×'c::finite) ell2 ⇒ ('a×('b×'c)) ell2› is
‹λf (a,(b,c)). f ((a,b),c)›
by auto

lift_definition assoc_ell20' :: ‹('a::finite×('b::finite×'c::finite)) ell2 ⇒ (('a×'b)×'c) ell2› is
‹λf ((a,b),c). f (a,(b,c))›
by auto

lift_definition assoc_ell2 :: ‹(('a::finite×'b::finite)×'c::finite) ell2 ⇒⇩C⇩L ('a×('b×'c)) ell2›
is assoc_ell20
apply (subst bounded_clinear_finite_dim)
apply (rule clinearI; transfer)
by auto

lift_definition assoc_ell2' :: ‹('a::finite×('b::finite×'c::finite)) ell2 ⇒⇩C⇩L (('a×'b)×'c) ell2› is
assoc_ell20'
apply (subst bounded_clinear_finite_dim)
apply (rule clinearI; transfer)
by auto

lemma assoc_ell2_tensor: ‹assoc_ell2 *⇩V tensor_ell2 (tensor_ell2 a b) c = tensor_ell2 a (tensor_ell2 b c)›
apply (rule clinear_equal_ket[THEN fun_cong, where x=a])
apply (simp add: clinear_tensor_ell22)
apply (rule clinear_equal_ket[THEN fun_cong, where x=b])
apply (rule clinear_equal_ket[THEN fun_cong, where x=c])
unfolding assoc_ell2.rep_eq
apply transfer
by auto

lemma assoc_ell2'_tensor: ‹assoc_ell2' *⇩V tensor_ell2 a (tensor_ell2 b c) = tensor_ell2 (tensor_ell2 a b) c›
apply (rule clinear_equal_ket[THEN fun_cong, where x=a])
apply (rule clinear_equal_ket[THEN fun_cong, where x=b])
apply (rule clinear_equal_ket[THEN fun_cong, where x=c])
unfolding assoc_ell2'.rep_eq
apply transfer
by auto

lemma adjoint_assoc_ell2[simp]: ‹assoc_ell2* = assoc_ell2'›
have [simp]: ‹clinear (cinner (assoc_ell2' *⇩V x))› for x :: ‹('a × 'b × 'c) ell2›
by (metis (no_types, lifting) cblinfun.add_right cinner_scaleC_right clinearI complex_scaleC_def mult.comm_neutral of_complex_def vector_to_cblinfun_adj_apply)
have [simp]: ‹clinear (λa. ⟨x, assoc_ell2 *⇩V a⟩)› for x :: ‹('a × 'b × 'c) ell2›
have [simp]: ‹antilinear (λa. ⟨a, y⟩)› for y :: ‹('a × 'b × 'c) ell2›
using bounded_antilinear_cinner_left bounded_antilinear_def by blast
have [simp]: ‹antilinear (λa. ⟨assoc_ell2' *⇩V a, y⟩)› for y :: ‹(('a × 'b) × 'c) ell2›
have ‹⟨assoc_ell2' *⇩V (ket x), ket y⟩ = ⟨ket x, assoc_ell2 *⇩V ket y⟩› for x :: ‹'a × 'b × 'c› and y
apply (cases x, cases y)
by (simp flip: tensor_ell2_ket add: assoc_ell2'_tensor assoc_ell2_tensor)
then have ‹⟨assoc_ell2' *⇩V (ket x), y⟩ = ⟨ket x, assoc_ell2 *⇩V y⟩› for x :: ‹'a × 'b × 'c› and y
by (rule clinear_equal_ket[THEN fun_cong, rotated 2], simp_all)
then show ‹⟨assoc_ell2' *⇩V x, y⟩ = ⟨x, assoc_ell2 *⇩V y⟩› for x :: ‹('a × 'b × 'c) ell2› and y
by (rule antilinear_equal_ket[THEN fun_cong, rotated 2], simp_all)
qed

lemma adjoint_assoc_ell2'[simp]: ‹assoc_ell2'* = assoc_ell2›
by (simp flip: adjoint_assoc_ell2)

lift_definition swap_ell20 :: ‹('a::finite×'b::finite) ell2 ⇒ ('b×'a) ell2› is
‹λf (a,b). f (b,a)›
by auto

lift_definition swap_ell2 :: ‹('a::finite×'b::finite) ell2 ⇒⇩C⇩L ('b×'a) ell2›
is swap_ell20
apply (subst bounded_clinear_finite_dim)
apply (rule clinearI; transfer)
by auto

lemma swap_ell2_tensor[simp]: ‹swap_ell2 *⇩V tensor_ell2 a b = tensor_ell2 b a›
apply (rule clinear_equal_ket[THEN fun_cong, where x=a])
apply (simp add: clinear_tensor_ell21)
apply (rule clinear_equal_ket[THEN fun_cong, where x=b])
unfolding swap_ell2.rep_eq
apply transfer
by auto

lemma adjoint_swap_ell2[simp]: ‹swap_ell2* = swap_ell2›
have [simp]: ‹clinear (cinner (swap_ell2 *⇩V x))› for x :: ‹('a × 'b) ell2›
by (metis (no_types, lifting) cblinfun.add_right cinner_scaleC_right clinearI complex_scaleC_def mult.comm_neutral of_complex_def vector_to_cblinfun_adj_apply)
have [simp]: ‹clinear (λa. ⟨x, swap_ell2 *⇩V a⟩)› for x :: ‹('a × 'b) ell2›
have [simp]: ‹antilinear (λa. ⟨a, y⟩)› for y :: ‹('a × 'b) ell2›
using bounded_antilinear_cinner_left bounded_antilinear_def by blast
have [simp]: ‹antilinear (λa. ⟨swap_ell2 *⇩V a, y⟩)› for y :: ‹('b × 'a) ell2›
have ‹⟨swap_ell2 *⇩V (ket x), ket y⟩ = ⟨ket x, swap_ell2 *⇩V ket y⟩› for x :: ‹'a × 'b› and y
apply (cases x, cases y)
by (simp flip: tensor_ell2_ket add: swap_ell2_tensor)
then have ‹⟨swap_ell2 *⇩V (ket x), y⟩ = ⟨ket x, swap_ell2 *⇩V y⟩› for x :: ‹'a × 'b› and y
by (rule clinear_equal_ket[THEN fun_cong, rotated 2], simp_all)
then show ‹⟨swap_ell2 *⇩V x, y⟩ = ⟨x, swap_ell2 *⇩V y⟩› for x :: ‹('a × 'b) ell2› and y
apply (rule antilinear_equal_ket[THEN fun_cong, rotated 2])
by simp_all
qed

lemma tensor_ell2_extensionality:
assumes "(⋀s t. a *⇩V (s ⊗⇩s t) = b *⇩V (s ⊗⇩s t))"
shows "a = b"
apply (rule equal_ket, case_tac x, hypsubst_thin)
by (simp add: assms flip: tensor_ell2_ket)

lemma assoc_ell2'_assoc_ell2[simp]: ‹assoc_ell2' o⇩C⇩L assoc_ell2 = id_cblinfun›
by (auto intro!: equal_ket simp: cblinfun_apply_cblinfun_compose assoc_ell2'_tensor assoc_ell2_tensor simp flip: tensor_ell2_ket)

lemma assoc_ell2_assoc_ell2'[simp]: ‹assoc_ell2 o⇩C⇩L assoc_ell2' = id_cblinfun›
by (auto intro!: equal_ket simp: cblinfun_apply_cblinfun_compose assoc_ell2'_tensor assoc_ell2_tensor simp flip: tensor_ell2_ket)

lemma unitary_assoc_ell2[simp]: "unitary assoc_ell2"
unfolding unitary_def by auto

lemma unitary_assoc_ell2'[simp]: "unitary assoc_ell2'"
unfolding unitary_def by auto

lemma tensor_op_left_add: ‹(x + y) ⊗⇩o b = x ⊗⇩o b + y ⊗⇩o b›
for x y :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
apply (auto intro!: equal_ket simp: tensor_op_ket)

lemma tensor_op_right_add: ‹b ⊗⇩o (x + y) = b ⊗⇩o x + b ⊗⇩o y›
for x y :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
apply (auto intro!: equal_ket simp: tensor_op_ket)

lemma tensor_op_scaleC_left: ‹(c *⇩C x) ⊗⇩o b = c *⇩C (x ⊗⇩o b)›
for x :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
apply (auto intro!: equal_ket simp: tensor_op_ket)
by (metis scaleC_cblinfun.rep_eq tensor_ell2_ket tensor_ell2_scaleC1 tensor_op_ell2)

lemma tensor_op_scaleC_right: ‹b ⊗⇩o (c *⇩C x) = c *⇩C (b ⊗⇩o x)›
for x :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
apply (auto intro!: equal_ket simp: tensor_op_ket)
by (metis scaleC_cblinfun.rep_eq tensor_ell2_ket tensor_ell2_scaleC2 tensor_op_ell2)

lemma clinear_tensor_left[simp]: ‹clinear (λa. a ⊗⇩o b :: _::finite ell2 ⇒⇩C⇩L _::finite ell2)›
apply (rule clinearI)
by (rule tensor_op_scaleC_left)

lemma clinear_tensor_right[simp]: ‹clinear (λb. a ⊗⇩o b :: _::finite ell2 ⇒⇩C⇩L _::finite ell2)›
apply (rule clinearI)
by (rule tensor_op_scaleC_right)

lemma tensor_ell2_nonzero: ‹a ⊗⇩s b ≠ 0› if ‹a ≠ 0› and ‹b ≠ 0›
apply (use that in transfer)
apply auto
by (metis mult_eq_0_iff old.prod.case)

lemma tensor_op_nonzero:
fixes a :: ‹'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2› and b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
assumes ‹a ≠ 0› and ‹b ≠ 0›
shows ‹a ⊗⇩o b ≠ 0›
proof -
from ‹a ≠ 0› obtain i where i: ‹a *⇩V ket i ≠ 0›
by (metis cblinfun.zero_left equal_ket)
from ‹b ≠ 0› obtain j where j: ‹b *⇩V ket j ≠ 0›
by (metis cblinfun.zero_left equal_ket)
from i j have ijneq0: ‹(a *⇩V ket i) ⊗⇩s (b *⇩V ket j) ≠ 0›
by (simp add: tensor_ell2_nonzero)
have ‹(a *⇩V ket i) ⊗⇩s (b *⇩V ket j) = (a ⊗⇩o b) *⇩V ket (i,j)›
by (simp add: tensor_op_ket)
with ijneq0 show ‹a ⊗⇩o b ≠ 0›
by force
qed

lemma inj_tensor_ell2_left: ‹inj (λa::'a::finite ell2. a ⊗⇩s b)› if ‹b ≠ 0› for b :: ‹'b::finite ell2›
proof (rule injI, rule ccontr)
fix x y :: ‹'a ell2›
assume eq: ‹x ⊗⇩s b = y ⊗⇩s b›
assume neq: ‹x ≠ y›
define a where ‹a = x - y›
from neq a_def have neq0: ‹a ≠ 0›
by auto
with ‹b ≠ 0› have ‹a ⊗⇩s b ≠ 0›
by (simp add: tensor_ell2_nonzero)
then have ‹x ⊗⇩s b ≠ y ⊗⇩s b›
unfolding a_def
with eq show False
by auto
qed

lemma inj_tensor_ell2_right: ‹inj (λb::'b::finite ell2. a ⊗⇩s b)› if ‹a ≠ 0› for a :: ‹'a::finite ell2›
proof (rule injI, rule ccontr)
fix x y :: ‹'b ell2›
assume eq: ‹a ⊗⇩s x = a ⊗⇩s y›
assume neq: ‹x ≠ y›
define b where ‹b = x - y›
from neq b_def have neq0: ‹b ≠ 0›
by auto
with ‹a ≠ 0› have ‹a ⊗⇩s b ≠ 0›
by (simp add: tensor_ell2_nonzero)
then have ‹a ⊗⇩s x ≠ a ⊗⇩s y›
unfolding b_def
with eq show False
by auto
qed

lemma inj_tensor_left: ‹inj (λa::'a::finite ell2 ⇒⇩C⇩L 'c::finite ell2. a ⊗⇩o b)› if ‹b ≠ 0› for b :: ‹'b::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
proof (rule injI, rule ccontr)
fix x y :: ‹'a ell2 ⇒⇩C⇩L 'c ell2›
assume eq: ‹x ⊗⇩o b = y ⊗⇩o b›
assume neq: ‹x ≠ y›
define a where ‹a = x - y›
from neq a_def have neq0: ‹a ≠ 0›
by auto
with ‹b ≠ 0› have ‹a ⊗⇩o b ≠ 0›
by (simp add: tensor_op_nonzero)
then have ‹x ⊗⇩o b ≠ y ⊗⇩o b›
unfolding a_def
with eq show False
by auto
qed

lemma inj_tensor_right: ‹inj (λb::'b::finite ell2 ⇒⇩C⇩L 'c::finite ell2. a ⊗⇩o b)› if ‹a ≠ 0› for a :: ‹'a::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
proof (rule injI, rule ccontr)
fix x y :: ‹'b ell2 ⇒⇩C⇩L 'c ell2›
assume eq: ‹a ⊗⇩o x = a ⊗⇩o y›
assume neq: ‹x ≠ y›
define b where ‹b = x - y›
from neq b_def have neq0: ‹b ≠ 0›
by auto
with ‹a ≠ 0› have ‹a ⊗⇩o b ≠ 0›
by (simp add: tensor_op_nonzero)
then have ‹a ⊗⇩o x ≠ a ⊗⇩o y›
unfolding b_def
with eq show False
by auto
qed

lemma tensor_ell2_almost_injective:
assumes ‹tensor_ell2 a b = tensor_ell2 c d›
assumes ‹a ≠ 0›
shows ‹∃γ. b = γ *⇩C d›
proof -
from ‹a ≠ 0› obtain i where i: ‹cinner (ket i) a ≠ 0›
by (metis cinner_eq_zero_iff cinner_ket_left ell2_pointwise_ortho)
have ‹cinner (ket i ⊗⇩s ket j) (a ⊗⇩s b) = cinner (ket i ⊗⇩s ket j) (c ⊗⇩s d)› for j
using assms by simp
then have eq2: ‹(cinner (ket i) a) * (cinner (ket j) b) = (cinner (ket i) c) * (cinner (ket j) d)› for j
by (metis tensor_ell2_inner_prod)
then obtain γ where ‹cinner (ket i) c = γ * cinner (ket i) a›
by (metis i eq_divide_eq)
with eq2 have ‹(cinner (ket i) a) * (cinner (ket j) b) = (cinner (ket i) a) * (γ * cinner (ket j) d)› for j
by simp
then have ‹cinner (ket j) b = cinner (ket j) (γ *⇩C d)› for j
using i by force
then have ‹b = γ *⇩C d›
by (simp add: cinner_ket_eqI)
then show ?thesis
by auto
qed

lemma tensor_op_almost_injective:
fixes a c :: ‹'a::finite ell2 ⇒⇩C⇩L 'b::finite ell2›
and b d :: ‹'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2›
assumes ‹tensor_op a b = tensor_op c d›
assumes ‹a ≠ 0›
shows ‹∃γ. b = γ *⇩C d›
proof (cases ‹d = 0›)
case False
from ‹a ≠ 0› obtain ψ where ψ: ‹a *⇩V ψ ≠ 0›
by (metis cblinfun.zero_left cblinfun_eqI)
have ‹(a ⊗⇩o b) (ψ ⊗⇩s φ) = (c ⊗⇩o d) (ψ ⊗⇩s φ)› for φ
using assms by simp
then have eq2: ‹(a ψ) ⊗⇩s (b φ) = (c ψ) ⊗⇩s (d φ)› for φ
by (simp add: tensor_op_ell2)
then have eq2': ‹(d φ) ⊗⇩s (c ψ) = (b φ) ⊗⇩s (a ψ)› for φ
by (metis swap_ell2_tensor)
from False obtain φ0 where φ0: ‹d φ0 ≠ 0›
by (metis cblinfun.zero_left cblinfun_eqI)
obtain γ where ‹c ψ = γ *⇩C a ψ›
apply atomize_elim
using eq2' φ0 by (rule tensor_ell2_almost_injective)
with eq2 have ‹(a ψ) ⊗⇩s (b φ) = (a ψ) ⊗⇩s (γ *⇩C d φ)› for φ
by (simp add: tensor_ell2_scaleC1 tensor_ell2_scaleC2)
then have ‹b φ = γ *⇩C d φ› for φ
by (smt (verit, best) ψ complex_vector.scale_cancel_right tensor_ell2_almost_injective tensor_ell2_nonzero tensor_ell2_scaleC2)
then have ‹b = γ *⇩C d›
by (simp add: cblinfun_eqI)
then show ?thesis
by auto
next
case True
then have ‹c ⊗⇩o d = 0›
then have ‹a ⊗⇩o b = 0›
using assms(1) by presburger
with ‹a ≠ 0› have ‹b = 0›
by (meson tensor_op_nonzero)
then show ?thesis
by auto
qed

lemma tensor_ell2_0_left[simp]: ‹tensor_ell2 0 x = 0›
apply transfer by auto

lemma tensor_ell2_0_right[simp]: ‹tensor_ell2 x 0 = 0›
apply transfer by auto

lemma tensor_op_0_left[simp]: ‹tensor_op 0 x = (0 :: ('a::finite*'b::finite) ell2 ⇒⇩C⇩L ('c::finite*'d::finite) ell2)›
apply (rule equal_ket)
by (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma tensor_op_0_right[simp]: ‹tensor_op x 0 = (0 :: ('a::finite*'b::finite) ell2 ⇒⇩C⇩L ('c::finite*'d::finite) ell2)›
apply (rule equal_ket)
by (auto simp flip: tensor_ell2_ket simp: tensor_op_ell2)

lemma bij_tensor_ell2_one_dim_left:
assumes ‹ψ ≠ 0›
shows ‹bij (λx::'b::finite ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
proof (rule bijI)
show ‹inj (λx::'b::finite ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
using assms by (rule inj_tensor_ell2_right)
have ‹∃x. ψ ⊗⇩s x = φ› for φ :: ‹('a*'b) ell2›
proof (use assms in transfer)
fix ψ :: ‹'a ⇒ complex› and φ :: ‹'a*'b ⇒ complex›
assume ‹has_ell2_norm φ› and ‹ψ ≠ (λ_. 0)›
define c where ‹c = ψ undefined›
then have ‹ψ a = c› for a
apply (subst everything_the_same[of _ undefined])
by simp
with ‹ψ ≠ (λ_. 0)› have ‹c ≠ 0›
by auto

define x where ‹x j = φ (undefined, j) / c› for j
have ‹(λ(i, j). ψ i * x j) = φ›
apply (auto intro!: ext simp: x_def ‹ψ _ = c› ‹c ≠ 0›)
apply (subst (2) everything_the_same[of _ undefined])
by simp
then show ‹∃x∈Collect has_ell2_norm. (λ(i, j). ψ i * x j) = φ›
apply (rule bexI[where x=x])
by simp
qed

then show ‹surj (λx::'b::finite ell2. (ψ :: 'a::CARD_1 ell2) ⊗⇩s x)›
by (metis surj_def)
qed

lemma bij_tensor_op_one_dim_left:
assumes ‹a ≠ 0›
shows ‹bij (λx::'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2. (a :: 'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2) ⊗⇩o x)›
proof (rule bijI)
define t where ‹t = (λx::'c ell2 ⇒⇩C⇩L 'd ell2. (a :: 'a ell2 ⇒⇩C⇩L 'b ell2) ⊗⇩o x)›
define i where
‹i = tensor_lift (λ(x::'a ell2 ⇒⇩C⇩L 'b ell2) (y::'c ell2 ⇒⇩C⇩L 'd ell2). (one_dim_iso x / one_dim_iso a) *⇩C y)›

have [simp]: ‹clinear i›
by (auto intro!: tensor_lift_clinear simp: i_def cbilinear_def clinearI scaleC_add_left add_divide_distrib)
have [simp]: ‹clinear t›
by (simp add: t_def)
have ‹i (x ⊗⇩o y) = (one_dim_iso x / one_dim_iso a) *⇩C y› for x y
by (auto intro!: clinearI tensor_lift_correct[THEN fun_cong, THEN fun_cong] simp: t_def i_def cbilinear_def  scaleC_add_left add_divide_distrib)
then have ‹t (i (x ⊗⇩o y)) = x ⊗⇩o y› for x y
apply (simp add: t_def)
by (smt (z3) assms complex_vector.scale_eq_0_iff nonzero_mult_div_cancel_right one_dim_scaleC_1 scaleC_scaleC tensor_op_scaleC_left tensor_op_scaleC_right times_divide_eq_left)
then have ‹t (i x) = x› for x
apply (rule_tac fun_cong[where x=x])
apply (rule tensor_extensionality)
by (auto intro: clinear_compose complex_vector.module_hom_ident simp flip: o_def[of t i])
then show ‹surj t›
by (rule surjI)

show ‹inj t›
unfolding t_def using assms by (rule inj_tensor_right)
qed

lemma swap_ell2_selfinv[simp]: ‹swap_ell2 o⇩C⇩L swap_ell2 = id_cblinfun›
apply (rule tensor_ell2_extensionality)
by auto

lemma bij_tensor_op_one_dim_right:
assumes ‹b ≠ 0›
shows ‹bij (λx::'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2. x ⊗⇩o (b :: 'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2))›
(is ‹bij ?f›)
proof -
let ?sf = ‹(λx. swap_ell2 o⇩C⇩L (?f x) o⇩C⇩L swap_ell2)›
let ?s = ‹(λx. swap_ell2 o⇩C⇩L x o⇩C⇩L swap_ell2)›
let ?g = ‹(λx::'c::finite ell2 ⇒⇩C⇩L 'd::finite ell2. (b :: 'a::{CARD_1,enum} ell2 ⇒⇩C⇩L 'b::{CARD_1,enum} ell2) ⊗⇩o x)›
have ‹?sf = ?g›
by (auto intro!: ext tensor_ell2_extensionality simp add: swap_ell2_tensor tensor_op_ell2)
have ‹bij ?g›
using assms by (rule bij_tensor_op_one_dim_left)
have ‹?s o ?sf = ?f›
apply (auto intro!: ext simp: cblinfun_assoc_left)
by (auto simp: cblinfun_assoc_right)
also have ‹bij ?s›
apply (rule o_bij[where g=‹(λx. swap_ell2 o⇩C⇩L x o⇩C⇩L swap_ell2)›])
apply (auto intro!: ext simp: cblinfun_assoc_left)
by (auto simp: cblinfun_assoc_right)
show ‹bij ?f›
apply (subst ‹?s o ?sf = ?f›[symmetric], subst ‹?sf = ?g›)
using ‹bij ?g› ‹bij ?s› by (rule bij_comp)
qed

lemma overlapping_tensor:
fixes a23 :: ‹('a2::finite*'a3::finite) ell2 ⇒⇩C⇩L ('b2::finite*'b3::finite) ell2›
and b12 :: ‹('a1::finite*'a2) ell2 ⇒⇩C⇩L ('b1::finite*'b2) ell2›
assumes eq: ‹butterfly ψ ψ' ⊗⇩o a23 = assoc_ell2 o⇩C⇩L (b12 ⊗⇩o butterfly φ φ') o⇩C⇩L assoc_ell2'›
assumes ‹ψ ≠ 0› ‹ψ' ≠ 0› ‹φ ≠ 0› ‹φ' ≠ 0›
shows ‹∃c. butterfly ψ ψ' ⊗⇩o a23 = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
proof -
note [[show_types]]
let ?id1 = ‹id_cblinfun :: unit ell2 ⇒⇩C⇩L unit ell2›
note id_cblinfun_eq_1[simp del]
define d where ‹d = butterfly ψ ψ' ⊗⇩o a23›

define ψ⇩n ψ⇩n' a23⇩n where ‹ψ⇩n = ψ /⇩C norm ψ› and ‹ψ⇩n' = ψ' /⇩C norm ψ'› and ‹a23⇩n = norm ψ *⇩C norm ψ' *⇩C a23›
have [simp]: ‹norm ψ⇩n = 1› ‹norm ψ⇩n' = 1›
using ‹ψ ≠ 0› ‹ψ' ≠ 0› by (auto simp: ψ⇩n_def ψ⇩n'_def norm_inverse)
have n1: ‹butterfly ψ⇩n ψ⇩n' ⊗⇩o a23⇩n = butterfly ψ ψ' ⊗⇩o a23›
apply (auto simp: ψ⇩n_def ψ⇩n'_def a23⇩n_def tensor_op_scaleC_left tensor_op_scaleC_right)
by (metis (no_types, lifting) assms(2) assms(3) inverse_mult_distrib mult.commute no_zero_divisors norm_eq_zero of_real_eq_0_iff right_inverse scaleC_one)

define φ⇩n φ⇩n' b12⇩n where ‹φ⇩n = φ /⇩C norm φ› and ‹φ⇩n' = φ' /⇩C norm φ'› and ‹b12⇩n = norm φ *⇩C norm φ' *⇩C b12›
have [simp]: ‹norm φ⇩n = 1› ‹norm φ⇩n' = 1›
using ‹φ ≠ 0› ‹φ' ≠ 0› by (auto simp: φ⇩n_def φ⇩n'_def norm_inverse)
have n2: ‹b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n' = b12 ⊗⇩o butterfly φ φ'›
apply (auto simp: φ⇩n_def φ⇩n'_def b12⇩n_def tensor_op_scaleC_left tensor_op_scaleC_right)
by (metis (no_types, lifting) assms(4) assms(5) field_class.field_inverse inverse_mult_distrib mult.commute no_zero_divisors norm_eq_zero of_real_hom.hom_0 scaleC_one)

define c' :: ‹(unit*'a2*unit) ell2 ⇒⇩C⇩L (unit*'b2*unit) ell2›
where ‹c' = (vector_to_cblinfun ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n)* o⇩C⇩L d
o⇩C⇩L (vector_to_cblinfun ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n')›

define c'' :: ‹'a2 ell2 ⇒⇩C⇩L 'b2 ell2›
where ‹c'' = inv (λc''. id_cblinfun ⊗⇩o c'' ⊗⇩o id_cblinfun) c'›

have *: ‹bij (λc''::'a2 ell2 ⇒⇩C⇩L 'b2 ell2. ?id1 ⊗⇩o c'' ⊗⇩o ?id1)›
apply (subst asm_rl[of ‹_ = (λx. id_cblinfun ⊗⇩o x) o (λc''. c'' ⊗⇩o id_cblinfun)›])
using [[show_consts]]
by (auto intro!: bij_comp bij_tensor_op_one_dim_left bij_tensor_op_one_dim_right)

have c'_c'': ‹c' = ?id1 ⊗⇩o c'' ⊗⇩o ?id1›
unfolding c''_def
apply (rule surj_f_inv_f[where y=c', symmetric])
using * by (rule bij_is_surj)

define c :: ‹'a2 ell2 ⇒⇩C⇩L 'b2 ell2›
where ‹c = c'' /⇩C norm ψ /⇩C norm ψ' /⇩C norm φ /⇩C norm φ'›

have aux: ‹assoc_ell2' o⇩C⇩L (assoc_ell2 o⇩C⇩L x o⇩C⇩L assoc_ell2') o⇩C⇩L assoc_ell2 = x› for x
apply (simp add: cblinfun_assoc_left)
by (simp add: cblinfun_assoc_right)
have aux2: ‹(assoc_ell2 o⇩C⇩L ((x ⊗⇩o y) ⊗⇩o z) o⇩C⇩L assoc_ell2') = x ⊗⇩o (y ⊗⇩o z)› for x y z
apply (rule equal_ket, rename_tac xyz)
apply (case_tac xyz, hypsubst_thin)
by (simp flip: tensor_ell2_ket add: assoc_ell2'_tensor assoc_ell2_tensor tensor_op_ell2)

have ‹d = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L d o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
by (auto simp: d_def n1[symmetric] comp_tensor_op cnorm_eq_1[THEN iffD1])
also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L (b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n')
o⇩C⇩L assoc_ell2' o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
by (auto simp: d_def eq n2 cblinfun_assoc_left)
also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L
((id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L (b12⇩n ⊗⇩o butterfly φ⇩n φ⇩n') o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n'))
o⇩C⇩L assoc_ell2' o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
by (auto simp: comp_tensor_op cnorm_eq_1[THEN iffD1])
also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L assoc_ell2 o⇩C⇩L
((id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L (assoc_ell2' o⇩C⇩L d o⇩C⇩L assoc_ell2) o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n'))
o⇩C⇩L assoc_ell2' o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun)›
by (auto simp: d_def n2 eq aux)
also have ‹… = ((butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun) o⇩C⇩L (assoc_ell2 o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n) o⇩C⇩L assoc_ell2'))
o⇩C⇩L d o⇩C⇩L ((assoc_ell2 o⇩C⇩L (id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n') o⇩C⇩L assoc_ell2') o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun))›
by (auto simp: sandwich_def cblinfun_assoc_left)
also have ‹… = (butterfly ψ⇩n ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o butterfly φ⇩n φ⇩n)
o⇩C⇩L d o⇩C⇩L (butterfly ψ⇩n' ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o butterfly φ⇩n' φ⇩n')›
apply (simp only: tensor_id[symmetric] comp_tensor_op aux2)
by (simp add: cnorm_eq_1[THEN iffD1])
also have ‹… = (vector_to_cblinfun ψ⇩n ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n)
o⇩C⇩L c' o⇩C⇩L (vector_to_cblinfun ψ⇩n' ⊗⇩o id_cblinfun ⊗⇩o vector_to_cblinfun φ⇩n')*›
apply (simp add: c'_def butterfly_def_one_dim[where 'c="unit ell2"] cblinfun_assoc_left comp_tensor_op
by (simp add: cblinfun_assoc_right comp_tensor_op)
also have ‹… = butterfly ψ⇩n ψ⇩n' ⊗⇩o c'' ⊗⇩o butterfly φ⇩n φ⇩n'›
by (simp add: c'_c'' comp_tensor_op tensor_op_adjoint butterfly_def_one_dim[symmetric])
also have ‹… = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
by (simp add: ψ⇩n_def ψ⇩n'_def φ⇩n_def φ⇩n'_def c_def tensor_op_scaleC_left tensor_op_scaleC_right)
finally have d_c: ‹d = butterfly ψ ψ' ⊗⇩o c ⊗⇩o butterfly φ φ'›
by -
then show ?thesis
by (auto simp: d_def)
qed

lemma norm_tensor_ell2: ‹norm (a ⊗⇩s b) = norm a * norm b›
apply transfer
by (simp add: ell2_norm_finite sum_product sum.cartesian_product case_prod_beta
norm_mult power_mult_distrib flip: real_sqrt_mult)

lemma bounded_cbilinear_tensor_ell2[bounded_cbilinear]: ‹bounded_cbilinear (⊗⇩s)›
proof standard
fix a a' :: "'a ell2" and b b' :: "'b ell2" and r :: complex
show ‹tensor_ell2 (a + a') b = tensor_ell2 a b + tensor_ell2 a' b›
show ‹tensor_ell2 a (b + b') = tensor_ell2 a b + tensor_ell2 a b'›