Splitting the maximally entangled state along computational registers

noncomputable def MIPRE.Introspection.registerState {H : Type u_4} {K : Type u_5} (I : Type u_6) [Fintype I] [DecidableEq I] (ξ : H × K → ℂ) : (I × H) × I × K → ℂ

EPR together with the original ancillary state, in the original basis.

Equations

• MIPRE.Introspection.registerState I ξ = MIPRE.expVec (MIPRE.Introspection.registerEPR I) ξ

def MIPRE.Introspection.registerParty {I : Type u_1} {J : Type u_2} {R : Type u_3} (e : I ≃ J × R) (H : Type u_6) : I × H ≃ J × R × H

Split a local basis and keep the original ancilla last.

Equations

• MIPRE.Introspection.registerParty e H = (e.prodCongr (Equiv.refl H)).trans (Equiv.prodAssoc J R H)

theorem MIPRE.Introspection.registerState_split {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} {K : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] (e : I ≃ J × R) (ξ : H × K → ℂ) : registerState I ξ = registerState J (registerState R ξ) ∘ ⇑((registerParty e H).prodCongr (registerParty e K))

The EPR factorization under the actual party-wise register permutation.

def MIPRE.Introspection.registerOutside {I : Type u_1} {J : Type u_2} {R : Type u_3} (e : I ≃ J × R) (H : Type u_6) : I × H ≃ (J × H) × R

The complementary register is moved behind the original auxiliary register.

Equations

• MIPRE.Introspection.registerOutside e H = ((MIPRE.Introspection.registerParty e H).trans ((Equiv.refl J).prodCongr (Equiv.prodComm R H))).trans (Equiv.prodAssoc J H R).symm

def MIPRE.Introspection.registerExtend {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} [DecidableEq R] (e : I ≃ J × R) (M : Matrix (J × H) (J × H) ℂ) : Matrix (I × H) (I × H) ℂ

Put a local operator on the first register, leaving the complement untouched.

Equations

• MIPRE.Introspection.registerExtend e M = MIPRE.Introspection.registerOp (MIPRE.Introspection.registerOutside e H) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M 1)

@[simp]

theorem MIPRE.Introspection.registerExtend_sub {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype H] [DecidableEq H] (e : I ≃ J × R) (M N : Matrix (J × H) (J × H) ℂ) : registerExtend e (M - N) = registerExtend e M - registerExtend e N

@[simp]

theorem MIPRE.Introspection.registerExtend_mul {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype H] [DecidableEq H] (e : I ≃ J × R) (M N : Matrix (J × H) (J × H) ℂ) : registerExtend e (M * N) = registerExtend e M * registerExtend e N

@[simp]

theorem MIPRE.Introspection.registerExtend_sum {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype H] [DecidableEq H] {A : Type u_6} [Fintype A] (e : I ≃ J × R) (M : A → Matrix (J × H) (J × H) ℂ) : registerExtend e (∑ a : A, M a) = ∑ a : A, registerExtend e (M a)

theorem MIPRE.Introspection.stateSqNorm_registerExtend {I : Type u_1} {J : Type u_2} {R : Type u_3} {H : Type u_4} {K : Type u_5} [Fintype I] [DecidableEq I] [Fintype J] [DecidableEq J] [Fintype R] [DecidableEq R] [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Nonempty R] (e : I ≃ J × R) (ξ : H × K → ℂ) (M : Matrix (J × H) (J × H) ℂ) : stateSqNorm (registerState I ξ) (registerExtend e M) = stateSqNorm (registerState J ξ) M

Extending a local operator by identity on complementary EPR coordinates costs no error.