The ancilla extension of a tensor-product model

The extension of the tensor-product model of ξ on ℂ^{dA × dB} by registers α and β in the vector e (BipartiteModel.expand) is the tensor-product model of the expanded vector expVec e ξ on ℂ^{(α × dA) × (β × dB)}, the register first: its block matrices of matrices are the matrices on the products of the indices (Matrix.comp), and its ℓ² sum of copies of ℂ^{dA × dB} is ℂ^{(α × dA) × (β × dB)} (BipartiteModel.tensorExpand, carrying the state exactly). This is the bridge between the register model of MIPRE/Foundations/Introspection/ RegisterModel.lean, in which the introspection analysis is stated, and the matrix states MIPRE.Introspection.registerState I ξ = expVec (registerEPR I) ξ of the tensor-product proof and of the Pauli basis test.

noncomputable def MIPRE.BipartiteModel.flattenIsometry {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : ((tensor ξ).expand e).H →ₗᵢ[ℂ] (tensor (expVec e ξ)).H

The flattening of ℂ^{dA × dB} ⊗ ℂ^{α × β} onto ℂ^{(α × dA) × (β × dB)}.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.BipartiteModel.flattenIsometry_apply {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (v : ((tensor ξ).expand e).H) (q : (α × dA) × β × dB) : ((flattenIsometry ξ e) v).ofLp q = ((((tensor ξ).ampl e) v).ofLp (q.1.1, q.2.1)).ofLp (q.1.2, q.2.2)

theorem MIPRE.BipartiteModel.tensor_π_apply {N : Type u_5} {N' : Type u_6} [Fintype N] [DecidableEq N] [Fintype N'] [DecidableEq N'] (v : N × N' → ℂ) (T : Matrix (N × N') (N × N') ℂ) (w : (tensor v).H) (i : N × N') : (((tensor v).π T) w).ofLp i = ∑ j : N × N', T i j * w.ofLp j

The action of the tensor-product model's matrices, entrywise.

noncomputable def MIPRE.BipartiteModel.euclid {N : Type u_5} {N' : Type u_6} [Fintype N] [DecidableEq N] [Fintype N'] [DecidableEq N'] (v : N × N' → ℂ) : (tensor v).H ≃ₗᵢ[ℂ] EuclideanSpace ℂ (N × N')

The Hilbert space of the tensor-product model is ℂ^{dA × dB}.

Equations

• MIPRE.BipartiteModel.euclid v = LinearIsometryEquiv.refl ℂ (MIPRE.BipartiteModel.tensor v).H

theorem MIPRE.BipartiteModel.tensor_ofLp_sum {N : Type u_5} {N' : Type u_6} [Fintype N] [DecidableEq N] [Fintype N'] [DecidableEq N'] (v : N × N' → ℂ) {ι : Type u_7} (s : Finset ι) (f : ι → (tensor v).H) (i : N × N') : (∑ a ∈ s, f a).ofLp i = ∑ a ∈ s, (f a).ofLp i

The components of a sum of vectors of the tensor-product model.

noncomputable def MIPRE.BipartiteModel.tensorExpand {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : ((tensor ξ).expand e).LocalIsometry (tensor (expVec e ξ))

The extension of a tensor-product model is the tensor-product model of the expanded vector: a local isometry carrying the state to the state, the players' block matrices of matrices read as matrices on the products of the indices.

Equations

• MIPRE.BipartiteModel.tensorExpand ξ e = { W := MIPRE.BipartiteModel.flattenIsometry ξ e, ΦA := MIPRE.compHom, ΦB := MIPRE.compHom, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.tensorExpand_W_ψ {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : (tensorExpand ξ e).W ((tensor ξ).expand e).ψ = (tensor (expVec e ξ)).ψ

@[simp]

theorem MIPRE.BipartiteModel.tensorExpand_ΦA {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (X : Matrix α α (Matrix dA dA ℂ)) : (tensorExpand ξ e).ΦA X = compHom X

@[simp]

theorem MIPRE.BipartiteModel.tensorExpand_ΦB {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (Y : Matrix β β (Matrix dB dB ℂ)) : (tensorExpand ξ e).ΦB Y = compHom Y

The inverse of the flattening

def MIPRE.BipartiteModel.compSymmHom {dA : Type u_1} {α : Type u_3} [Fintype dA] [Fintype α] {R : Type u_5} [Ring R] [StarRing R] [Algebra ℂ R] : Matrix (α × dA) (α × dA) R →⋆ₙₐ[ℂ] Matrix α α (Matrix dA dA R)

Matrices on the products of the indices as block matrices of matrices (Matrix.comp inverted), as a ⋆-homomorphism.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem MIPRE.BipartiteModel.compSymmHom_apply {dA : Type u_1} {α : Type u_3} [Fintype dA] [Fintype α] {R : Type u_5} [Ring R] [StarRing R] [Algebra ℂ R] (X : Matrix (α × dA) (α × dA) R) (a a' : α) (h h' : dA) : compSymmHom X a a' h h' = X (a, h) (a', h')

theorem MIPRE.BipartiteModel.compHom_compSymmHom {dA : Type u_1} {α : Type u_3} [Fintype dA] [Fintype α] {R : Type u_5} [Ring R] [StarRing R] [Algebra ℂ R] (X : Matrix (α × dA) (α × dA) R) : compHom (compSymmHom X) = X

noncomputable def MIPRE.BipartiteModel.unflattenIsometry {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : (tensor (expVec e ξ)).H →ₗᵢ[ℂ] ((tensor ξ).expand e).H

The inverse of the flattening.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.BipartiteModel.flattenIsometry_unflattenIsometry {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (v : (tensor (expVec e ξ)).H) : (flattenIsometry ξ e) ((unflattenIsometry ξ e) v) = v

noncomputable def MIPRE.BipartiteModel.tensorUnexpand {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : (tensor (expVec e ξ)).LocalIsometry ((tensor ξ).expand e)

The tensor-product model of an expanded vector is the extension of the tensor-product model: the inverse of tensorExpand.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.BipartiteModel.tensorUnexpand_W_ψ {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) : (tensorUnexpand ξ e).W (tensor (expVec e ξ)).ψ = ((tensor ξ).expand e).ψ

@[simp]

theorem MIPRE.BipartiteModel.tensorUnexpand_ΦA {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (X : Matrix (α × dA) (α × dA) ℂ) : (tensorUnexpand ξ e).ΦA X = compSymmHom X

@[simp]

theorem MIPRE.BipartiteModel.tensorUnexpand_ΦB {dA : Type u_1} {dB : Type u_2} {α : Type u_3} {β : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype α] [DecidableEq α] [Fintype β] [DecidableEq β] (ξ : dA × dB → ℂ) (e : α × β → ℂ) (Y : Matrix (β × dB) (β × dB) ℂ) : (tensorUnexpand ξ e).ΦB Y = compSymmHom Y

theorem MIPRE.BipartiteModel.compSymmHom_kronecker_one {dA : Type u_1} {α : Type u_3} [Fintype dA] [DecidableEq dA] [Fintype α] (P : Matrix α α ℂ) : compSymmHom (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) P 1) = smulKron 1 P

A register operator acting as P ⊗ 1 on the flat space is smulKron 1 P in blocks.

Local isometries of tensor-product models given by matrices

noncomputable def MIPRE.matrixIsometry {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] (V : Matrix m n ℂ) (hV : V.conjTranspose * V = 1) : EuclideanSpace ℂ n →ₗᵢ[ℂ] EuclideanSpace ℂ m

A matrix with orthonormal columns as an isometry of the Euclidean spaces.

Equations

• MIPRE.matrixIsometry V hV = { toLinearMap := Matrix.toEuclideanLin V, norm_map' := ⋯ }

def MIPRE.conjHom {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] (V : Matrix m n ℂ) (hV : V.conjTranspose * V = 1) : Matrix n n ℂ →⋆ₙₐ[ℂ] Matrix m m ℂ

Conjugation by a matrix with orthonormal columns, X ↦ V X Vᴴ, a ⋆-homomorphism.

Equations

• MIPRE.conjHom V hV = { toFun := fun (X : Matrix n n ℂ) => V * X * V.conjTranspose, map_smul' := ⋯, map_zero' := ⋯, map_add' := ⋯, map_mul' := ⋯, map_star' := ⋯ }

@[simp]

theorem MIPRE.conjHom_apply {n : Type u_1} {m : Type u_2} [Fintype n] [DecidableEq n] [Fintype m] (V : Matrix m n ℂ) (hV : V.conjTranspose * V = 1) (X : Matrix n n ℂ) : (conjHom V hV) X = V * X * V.conjTranspose

noncomputable def MIPRE.BipartiteModel.tensorIsometry {dA : Type u_1} {dB : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (ψ : dA × dB → ℂ) (ψ' : R × S → ℂ) (VA : Matrix R dA ℂ) (VB : Matrix S dB ℂ) (hA : VA.conjTranspose * VA = 1) (hB : VB.conjTranspose * VB = 1) : (tensor ψ).LocalIsometry (tensor ψ')

The local isometry of two tensor-product models given by matrix isometries V_A and V_B: the space moved by V_A ⊗ V_B, the players' operators by X ↦ V_A X V_Aᴴ and Y ↦ V_B Y V_Bᴴ. The states of the two models play no part.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.BipartiteModel.tensorIsometry_W {dA : Type u_1} {dB : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (ψ : dA × dB → ℂ) (ψ' : R × S → ℂ) (VA : Matrix R dA ℂ) (VB : Matrix S dB ℂ) (hA : VA.conjTranspose * VA = 1) (hB : VB.conjTranspose * VB = 1) (v : (tensor ψ).H) : ((tensorIsometry ψ ψ' VA VB hA hB).W v).ofLp = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) VA VB).mulVec v.ofLp

@[simp]

theorem MIPRE.BipartiteModel.tensorIsometry_ΦA {dA : Type u_1} {dB : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (ψ : dA × dB → ℂ) (ψ' : R × S → ℂ) (VA : Matrix R dA ℂ) (VB : Matrix S dB ℂ) (hA : VA.conjTranspose * VA = 1) (hB : VB.conjTranspose * VB = 1) (X : Matrix dA dA ℂ) : (tensorIsometry ψ ψ' VA VB hA hB).ΦA X = VA * X * VA.conjTranspose

@[simp]

theorem MIPRE.BipartiteModel.tensorIsometry_ΦB {dA : Type u_1} {dB : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (ψ : dA × dB → ℂ) (ψ' : R × S → ℂ) (VA : Matrix R dA ℂ) (VB : Matrix S dB ℂ) (hA : VA.conjTranspose * VA = 1) (hB : VB.conjTranspose * VB = 1) (Y : Matrix dB dB ℂ) : (tensorIsometry ψ ψ' VA VB hA hB).ΦB Y = VB * Y * VB.conjTranspose