Local isometries of bipartite models

The conclusion of a rigidity theorem moves a strategy along a pair of local isometries: in the tensor-product model, V_A : ℂ^{d_A} → ℂ^{register} ⊗ ℂ^{H_A} and its partner for the second player, each player's operator X going to V_A X V_Aᴴ, and the state ψ to (V_A ⊗ V_B) ψ (MIPRE.Introspection.isometricImage, isometricState). Phase 4 of planning/mipco-track.md needs the same move in any bipartite model, where there is no factorization of the space into the two players' parts. What survives is this (BipartiteModel.LocalIsometry): a linear isometry W of the Hilbert spaces, and for each player a non-unital ⋆-homomorphism Φ of the player's algebra into the other model's, with W intertwining the two representations, π' (πA' (Φ_A a)) ∘ W = W ∘ π (πA a), and likewise for the second player.

X ↦ V_A X V_Aᴴ is exactly such a Φ_A: it is multiplicative because V_Aᴴ V_A = 1, and not unital, Φ_A 1 = V_A V_Aᴴ being the projection onto the image. In the commuting-operator model the isometry built from a player's approximate Pauli operators has its entries in that player's algebra, and conjugation by it is again multiplicative, for the same reason.

• Born probabilities are carried over exactly on the transported state W ψ (LocalIsometry.bornProb_withState), and so are the players' state norms (LocalIsometry.stateSqNorm_withState). The transported state is a state of the target's Hilbert space but not its state, so the statements are about the target with its state replaced (BipartiteModel.withState).
• A projective measurement is carried over to a projective measurement (LocalIsometry.transportA): Φ_A of each element, with the complement 1 - Φ_A 1 of the image added at one fixed outcome. It is intertwined with the original by W (LocalIsometry.intertwine_transportA), so a strategy and its transport have the same value on the transported state (LocalIsometry.povmValue_transport). This is MIPRE.Introspection.isometricPOVM in any model.
• Local isometries compose (LocalIsometry.comp), and exchange with the players (LocalIsometry.swap).

Replacing the state

def MIPRE.StateModel.withState {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (φ : M.H) : StateModel 𝒞

The state model with its state replaced by the vector φ of its Hilbert space.

Equations

• M.withState φ = { H := M.H, normedAddCommGroup := M.normedAddCommGroup, innerProductSpace := M.innerProductSpace, completeSpace := ⋯, ψ := φ, π := M.π }

@[simp]

theorem MIPRE.StateModel.withState_ψ {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (φ : M.H) : (M.withState φ).ψ = φ

@[simp]

theorem MIPRE.StateModel.withState_π {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (φ : M.H) (T : 𝒞) : (M.withState φ).π T = M.π T

theorem MIPRE.StateModel.withState_snorm {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (φ : M.H) (T : 𝒞) : (M.withState φ).snorm T = ‖(M.π T) φ‖

theorem MIPRE.StateModel.withState_qform {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) (φ : M.H) (T : 𝒞) : (M.withState φ).qform T = (inner ℂ φ ((M.π T) φ)).re

@[simp]

theorem MIPRE.StateModel.withState_self {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (M : StateModel 𝒞) : M.withState M.ψ = M

def MIPRE.BipartiteModel.withState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (φ : M.H) : BipartiteModel 𝒞 𝒜 ℬ

The bipartite model with its state replaced by the vector φ of its Hilbert space.

Equations

• M.withState φ = { toStateModel := M.withState φ, πA := M.πA, πB := M.πB, commute := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.withState_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (φ : M.H) : (M.withState φ).ψ = φ

@[simp]

theorem MIPRE.BipartiteModel.withState_πA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (φ : M.H) (a : 𝒜) : (M.withState φ).πA a = M.πA a

@[simp]

theorem MIPRE.BipartiteModel.withState_πB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) (φ : M.H) (b : ℬ) : (M.withState φ).πB b = M.πB b

@[simp]

theorem MIPRE.BipartiteModel.withState_self {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (M : BipartiteModel 𝒞 𝒜 ℬ) : M.withState M.ψ = M

Pushing a measurement forward along a unital ⋆-homomorphism

theorem MIPRE.IsPVMIn.pushforward {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {X : Type u_3} [Fintype X] {f : R →⋆ₙₐ[ℂ] S} (hf : f 1 = 1) {P : X → R} (hP : IsPVMIn P) : IsPVMIn fun (x : X) => f (P x)

The image of a projective measurement under a ⋆-homomorphism preserving the unit.

def MIPRE.POVMIn.pushforward {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {X : Type u_3} [Fintype X] [PartialOrder R] [StarOrderedRing R] [PartialOrder S] [StarOrderedRing S] (f : R →⋆ₙₐ[ℂ] S) (hf : f 1 = 1) (P : POVMIn X R) : POVMIn X S

A POVM pushed forward along a ⋆-homomorphism preserving the unit.

Equations

• MIPRE.POVMIn.pushforward f hf P = { mats := fun (x : X) => ⟨f (P.op x), ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVMIn.pushforward_op {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {X : Type u_3} [Fintype X] [PartialOrder R] [StarOrderedRing R] [PartialOrder S] [StarOrderedRing S] (f : R →⋆ₙₐ[ℂ] S) (hf : f 1 = 1) (P : POVMIn X R) (x : X) : (pushforward f hf P).op x = f (P.op x)

theorem MIPRE.POVMIn.isPVMIn_pushforward {R : Type u_1} {S : Type u_2} [Ring R] [StarRing R] [Algebra ℂ R] [Ring S] [StarRing S] [Algebra ℂ S] {X : Type u_3} [Fintype X] [PartialOrder R] [StarOrderedRing R] [PartialOrder S] [StarOrderedRing S] (f : R →⋆ₙₐ[ℂ] S) (hf : f 1 = 1) {P : POVMIn X R} (hP : IsPVMIn P.op) : IsPVMIn (pushforward f hf P).op

def MIPRE.IsPVMIn.toPOVMIn {R : Type u_1} [Ring R] [StarRing R] {X : Type u_3} [Fintype X] [PartialOrder R] [StarOrderedRing R] {P : X → R} (hP : IsPVMIn P) : POVMIn X R

A projective measurement, as a POVM: its elements are nonnegative, being star projections.

Equations

• hP.toPOVMIn = { mats := fun (x : X) => ⟨P x, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.IsPVMIn.toPOVMIn_op {R : Type u_1} [Ring R] [StarRing R] {X : Type u_3} [Fintype X] [PartialOrder R] [StarOrderedRing R] {P : X → R} (hP : IsPVMIn P) (x : X) : hP.toPOVMIn.op x = P x

Local isometries

structure MIPRE.BipartiteModel.LocalIsometry {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] (M : BipartiteModel 𝒞 𝒜 ℬ) (M' : BipartiteModel 𝒞' 𝒜' ℬ') : Type (max (max (max (max (max u u') u_2) u_3) u_5) u_6)

A local isometry from the bipartite model M into the bipartite model M': a linear isometry W of the Hilbert spaces, and for each player a non-unital ⋆-homomorphism of the player's algebra into the other model's, the two representations intertwined by W. The states play no part: how far W ψ is from the state of M' is the error of whatever produced the isometry.

• W : M.H →ₗᵢ[ℂ] M'.H

  The isometry of the Hilbert spaces.

• ΦA : 𝒜 →⋆ₙₐ[ℂ] 𝒜'

  The first player's operators, moved along the isometry.

• ΦB : ℬ →⋆ₙₐ[ℂ] ℬ'

  The second player's operators, moved along the isometry.

• intertwineA (a : 𝒜) (v : M.H) : (M'.π (M'.πA (self.ΦA a))) (self.W v) = self.W ((M.π (M.πA a)) v)

  The isometry intertwines the first player's operators with their images.

• intertwineB (b : ℬ) (v : M.H) : (M'.π (M'.πB (self.ΦB b))) (self.W v) = self.W ((M.π (M.πB b)) v)

  The isometry intertwines the second player's operators with their images.

def MIPRE.BipartiteModel.LocalIsometry.swap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : M.swap.LocalIsometry M'.swap

The local isometry with the players exchanged.

Equations

• Φ.swap = { W := Φ.W, ΦA := Φ.ΦB, ΦB := Φ.ΦA, intertwineA := ⋯, intertwineB := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.swap_W {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : Φ.swap.W = Φ.W

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.swap_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : Φ.swap.ΦA = Φ.ΦB

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.swap_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : Φ.swap.ΦB = Φ.ΦA

def MIPRE.BipartiteModel.LocalIsometry.comp {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ' : M'.LocalIsometry M'') (Φ : M.LocalIsometry M') : M.LocalIsometry M''

Local isometries compose.

Equations

• Φ'.comp Φ = { W := Φ'.W.comp Φ.W, ΦA := Φ'.ΦA.comp Φ.ΦA, ΦB := Φ'.ΦB.comp Φ.ΦB, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.LocalIsometry.comp_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} {Φ' : M'.LocalIsometry M''} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (h' : Φ'.W M'.ψ = M''.ψ) : (Φ'.comp Φ).W M.ψ = M''.ψ

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.comp_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ' : M'.LocalIsometry M'') (Φ : M.LocalIsometry M') (a : 𝒜) : (Φ'.comp Φ).ΦA a = Φ'.ΦA (Φ.ΦA a)

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.comp_ΦB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} {𝒞'' : Type u_7} {𝒜'' : Type u_8} {ℬ'' : Type u_9} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] [Ring 𝒞''] [StarRing 𝒞''] [Algebra ℂ 𝒞''] [Ring 𝒜''] [StarRing 𝒜''] [Algebra ℂ 𝒜''] [Ring ℬ''] [StarRing ℬ''] [Algebra ℂ ℬ''] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {M'' : BipartiteModel 𝒞'' 𝒜'' ℬ''} (Φ' : M'.LocalIsometry M'') (Φ : M.LocalIsometry M') (b : ℬ) : (Φ'.comp Φ).ΦB b = Φ'.ΦB (Φ.ΦB b)

def MIPRE.BipartiteModel.LocalIsometry.symm {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (W' : M'.H →ₗᵢ[ℂ] M.H) (hW : ∀ (v : M'.H), Φ.W (W' v) = v) (ΨA : 𝒜' →⋆ₙₐ[ℂ] 𝒜) (hA : ∀ (a : 𝒜'), Φ.ΦA (ΨA a) = a) (ΨB : ℬ' →⋆ₙₐ[ℂ] ℬ) (hB : ∀ (b : ℬ'), Φ.ΦB (ΨB b) = b) : M'.LocalIsometry M

The inverse of a local isometry with an inverse isometry and inverse homomorphisms.

Equations

• Φ.symm W' hW ΨA hA ΨB hB = { W := W', ΦA := ΨA, ΦB := ΨB, intertwineA := ⋯, intertwineB := ⋯ }

theorem MIPRE.BipartiteModel.LocalIsometry.symm_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (W' : M'.H →ₗᵢ[ℂ] M.H) (hW : ∀ (v : M'.H), Φ.W (W' v) = v) (ΨA : 𝒜' →⋆ₙₐ[ℂ] 𝒜) (hA : ∀ (a : 𝒜'), Φ.ΦA (ΨA a) = a) (ΨB : ℬ' →⋆ₙₐ[ℂ] ℬ) (hB : ∀ (b : ℬ'), Φ.ΦB (ΨB b) = b) (h : Φ.W M.ψ = M'.ψ) : (Φ.symm W' hW ΨA hA ΨB hB).W M'.ψ = M.ψ

theorem MIPRE.BipartiteModel.LocalIsometry.intertwine {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) (b : ℬ) (v : M.H) : (M'.π (M'.πA (Φ.ΦA a) * M'.πB (Φ.ΦB b))) (Φ.W v) = Φ.W ((M.π (M.πA a * M.πB b)) v)

The isometry intertwines a product of the two players' operators with the product of their images.

theorem MIPRE.BipartiteModel.LocalIsometry.π_πA_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (v : M.H) : (M'.π (M'.πA (Φ.ΦA 1))) (Φ.W v) = Φ.W v

The image of the unit of the first player's algebra fixes the image of the isometry.

theorem MIPRE.BipartiteModel.LocalIsometry.bornProb_withState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) (b : ℬ) : (M'.withState (Φ.W M.ψ)).bornProb (Φ.ΦA a) (Φ.ΦB b) = M.bornProb a b

Born probabilities are carried over exactly, on the transported state.

theorem MIPRE.BipartiteModel.LocalIsometry.stateNorm_withState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : (M'.withState (Φ.W M.ψ)).stateNorm (Φ.ΦA a) = M.stateNorm a

The first player's state norms are carried over exactly, on the transported state.

theorem MIPRE.BipartiteModel.LocalIsometry.stateSqNorm_withState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : (M'.withState (Φ.W M.ψ)).stateSqNorm (Φ.ΦA a) = M.stateSqNorm a

theorem MIPRE.BipartiteModel.LocalIsometry.norm_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : ‖Φ.W M.ψ‖ = ‖M.ψ‖

The transported state has the norm of the state.

An isometry carrying the state to the state

The local isometries between extensions of one model by registers carry the state exactly, and then every quantity computed from the state is carried over.

theorem MIPRE.BipartiteModel.LocalIsometry.bornProb_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (a : 𝒜) (b : ℬ) : M'.bornProb (Φ.ΦA a) (Φ.ΦB b) = M.bornProb a b

theorem MIPRE.BipartiteModel.LocalIsometry.stateNorm_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (a : 𝒜) : M'.stateNorm (Φ.ΦA a) = M.stateNorm a

theorem MIPRE.BipartiteModel.LocalIsometry.stateSqNorm_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (a : 𝒜) : M'.stateSqNorm (Φ.ΦA a) = M.stateSqNorm a

theorem MIPRE.BipartiteModel.LocalIsometry.swap_stateSqNorm_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (b : ℬ) : M'.swap.stateSqNorm (Φ.ΦB b) = M.swap.stateSqNorm b

theorem MIPRE.BipartiteModel.LocalIsometry.xNorm_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (a : 𝒜) (b : ℬ) : M'.xNorm (Φ.ΦA a) (Φ.ΦB b) = M.xNorm a b

The cross norm ‖(πA a - πB b) ψ‖ is carried over.

theorem MIPRE.BipartiteModel.LocalIsometry.xSqNorm_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (a : 𝒜) (b : ℬ) : M'.xSqNorm (Φ.ΦA a) (Φ.ΦB b) = M.xSqNorm a b

theorem MIPRE.BipartiteModel.LocalIsometry.norm_ψ_of_W_ψ {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) : ‖M'.ψ‖ = ‖M.ψ‖

The image of the unit

theorem MIPRE.BipartiteModel.LocalIsometry.ΦA_one_mul_self {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : Φ.ΦA 1 * Φ.ΦA 1 = Φ.ΦA 1

theorem MIPRE.BipartiteModel.LocalIsometry.star_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : star (Φ.ΦA 1) = Φ.ΦA 1

theorem MIPRE.BipartiteModel.LocalIsometry.ΦA_mul_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : Φ.ΦA a * Φ.ΦA 1 = Φ.ΦA a

theorem MIPRE.BipartiteModel.LocalIsometry.ΦA_one_mul_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : Φ.ΦA 1 * Φ.ΦA a = Φ.ΦA a

theorem MIPRE.BipartiteModel.LocalIsometry.compl_ΦA_one_mul_self {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : (1 - Φ.ΦA 1) * (1 - Φ.ΦA 1) = 1 - Φ.ΦA 1

The complement of the image of the first player's unit.

theorem MIPRE.BipartiteModel.LocalIsometry.star_compl_ΦA_one {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') : star (1 - Φ.ΦA 1) = 1 - Φ.ΦA 1

theorem MIPRE.BipartiteModel.LocalIsometry.ΦA_mul_compl {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : Φ.ΦA a * (1 - Φ.ΦA 1) = 0

theorem MIPRE.BipartiteModel.LocalIsometry.compl_mul_ΦA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (a : 𝒜) : (1 - Φ.ΦA 1) * Φ.ΦA a = 0

theorem MIPRE.BipartiteModel.LocalIsometry.π_πA_compl {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') (v : M.H) : (M'.π (M'.πA (1 - Φ.ΦA 1))) (Φ.W v) = 0

The complement of the image of the unit kills the image of the isometry.

Transporting a projective measurement

def MIPRE.BipartiteModel.LocalIsometry.transportOpA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [DecidableEq X] (x₀ : X) (P : X → 𝒜) (x : X) : 𝒜'

The transport of a family of the first player's operators: the image of each, with the complement of the image of the unit added at the outcome x₀.

Equations

• Φ.transportOpA x₀ P x = Φ.ΦA (P x) + if x = x₀ then 1 - Φ.ΦA 1 else 0

theorem MIPRE.BipartiteModel.LocalIsometry.isPVMIn_transportOpA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [Fintype X] [DecidableEq X] (x₀ : X) {P : X → 𝒜} (hP : IsPVMIn P) : IsPVMIn (Φ.transportOpA x₀ P)

The transport of a projective measurement is a projective measurement.

theorem MIPRE.BipartiteModel.LocalIsometry.intertwine_transportOpA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [DecidableEq X] (x₀ : X) (P : X → 𝒜) (x : X) (v : M.H) : (M'.π (M'.πA (Φ.transportOpA x₀ P x))) (Φ.W v) = Φ.W ((M.π (M.πA (P x))) v)

The transport is intertwined with the original by the isometry.

def MIPRE.BipartiteModel.LocalIsometry.transportA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [Fintype X] [DecidableEq X] [PartialOrder 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (x₀ : X) (P : POVMIn X 𝒜) (hP : IsPVMIn P.op) : POVMIn X 𝒜'

The transport of a projective measurement, as a POVM of the target's first player.

Equations

• Φ.transportA x₀ P hP = { mats := fun (x : X) => ⟨Φ.transportOpA x₀ P.op x, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.transportA_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [Fintype X] [DecidableEq X] [PartialOrder 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (x₀ : X) (P : POVMIn X 𝒜) (hP : IsPVMIn P.op) (x : X) : (Φ.transportA x₀ P hP).op x = Φ.transportOpA x₀ P.op x

theorem MIPRE.BipartiteModel.LocalIsometry.isPVMIn_transportA {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} [Fintype X] [DecidableEq X] [PartialOrder 𝒜] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] (x₀ : X) (P : POVMIn X 𝒜) (hP : IsPVMIn P.op) : IsPVMIn (Φ.transportA x₀ P hP).op

def MIPRE.BipartiteModel.LocalIsometry.transportB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {Y : Type u_10} [Fintype Y] [DecidableEq Y] [PartialOrder ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (y₀ : Y) (Q : POVMIn Y ℬ) (hQ : IsPVMIn Q.op) : POVMIn Y ℬ'

The transport of a projective measurement of the second player.

Equations

• Φ.transportB y₀ Q hQ = Φ.swap.transportA y₀ Q hQ

@[simp]

theorem MIPRE.BipartiteModel.LocalIsometry.transportB_op {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {Y : Type u_10} [Fintype Y] [DecidableEq Y] [PartialOrder ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (y₀ : Y) (Q : POVMIn Y ℬ) (hQ : IsPVMIn Q.op) (y : Y) : (Φ.transportB y₀ Q hQ).op y = Φ.swap.transportOpA y₀ Q.op y

theorem MIPRE.BipartiteModel.LocalIsometry.isPVMIn_transportB {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {Y : Type u_10} [Fintype Y] [DecidableEq Y] [PartialOrder ℬ] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (y₀ : Y) (Q : POVMIn Y ℬ) (hQ : IsPVMIn Q.op) : IsPVMIn (Φ.transportB y₀ Q hQ).op

The value of a transported strategy

theorem MIPRE.BipartiteModel.LocalIsometry.bornProb_transport {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {A : Type u_12} {B : Type u_13} [DecidableEq A] [DecidableEq B] (a₀ : A) (b₀ : B) (P : A → 𝒜) (Q : B → ℬ) (a : A) (b : B) : (M'.withState (Φ.W M.ψ)).bornProb (Φ.transportOpA a₀ P a) (Φ.swap.transportOpA b₀ Q b) = M.bornProb (P a) (Q b)

The Born probabilities of a transported pair of measurements are the original ones, on the transported state.

theorem MIPRE.BipartiteModel.LocalIsometry.povmValue_transport {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] [PartialOrder 𝒜] [PartialOrder ℬ] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (G : Game X Y A B) (a₀ : A) (b₀ : B) (PA : X → POVMIn A 𝒜) (PB : Y → POVMIn B ℬ) (hPA : ∀ (x : X), IsPVMIn (PA x).op) (hPB : ∀ (y : Y), IsPVMIn (PB y).op) : ((M'.withState (Φ.W M.ψ)).povmValue G (fun (x : X) => Φ.transportA a₀ (PA x) ⋯) fun (y : Y) => Φ.transportB b₀ (PB y) ⋯) = M.povmValue G PA PB

A strategy and its transport have the same value, on the transported state.

The value of a strategy moved along a unital local isometry

theorem MIPRE.BipartiteModel.LocalIsometry.povmValue_pushforward_withState {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} (Φ : M.LocalIsometry M') {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] (hA : Φ.ΦA 1 = 1) (hB : Φ.ΦB 1 = 1) (G : Game X Y A B) (PA : X → POVMIn A 𝒜) (PB : Y → POVMIn B ℬ) : ((M'.withState (Φ.W M.ψ)).povmValue G (fun (x : X) => POVMIn.pushforward Φ.ΦA hA (PA x)) fun (y : Y) => POVMIn.pushforward Φ.ΦB hB (PB y)) = M.povmValue G PA PB

A strategy moved along a local isometry preserving the units has its value, on the transported state.

theorem MIPRE.BipartiteModel.LocalIsometry.povmValue_pushforward {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} {𝒞' : Type u_4} {𝒜' : Type u_5} {ℬ' : Type u_6} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [Ring 𝒞'] [StarRing 𝒞'] [Algebra ℂ 𝒞'] [Ring 𝒜'] [StarRing 𝒜'] [Algebra ℂ 𝒜'] [Ring ℬ'] [StarRing ℬ'] [Algebra ℂ ℬ'] {M : BipartiteModel 𝒞 𝒜 ℬ} {M' : BipartiteModel 𝒞' 𝒜' ℬ'} {X : Type u_10} {Y : Type u_11} {A : Type u_12} {B : Type u_13} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] [PartialOrder 𝒜'] [StarOrderedRing 𝒜'] [PartialOrder ℬ'] [StarOrderedRing ℬ'] {Φ : M.LocalIsometry M'} (h : Φ.W M.ψ = M'.ψ) (hA : Φ.ΦA 1 = 1) (hB : Φ.ΦB 1 = 1) (G : Game X Y A B) (PA : X → POVMIn A 𝒜) (PB : Y → POVMIn B ℬ) : (M'.povmValue G (fun (x : X) => POVMIn.pushforward Φ.ΦA hA (PA x)) fun (y : Y) => POVMIn.pushforward Φ.ΦB hB (PB y)) = M.povmValue G PA PB

The same, for a local isometry carrying the state to the state.