Transporting a strategy through local isometries

Conjugating a PVM by a rectangular isometry normalizes it only on the isometry's image. Assigning the image complement to a fixed outcome gives an actual projective measurement on the whole target space. On the embedded state this completion preserves all probabilities and every intertwining identity exactly, including after an outcome map.

def MIPRE.Introspection.isometricImage {H : Type u_1} {R : Type u_2} [Fintype H] (V : Matrix R H ℂ) (M : Matrix H H ℂ) : Matrix R R ℂ

Conjugation into the image of a rectangular linear map.

Equations

• MIPRE.Introspection.isometricImage V M = V * M * V.conjTranspose

theorem MIPRE.Introspection.isometricImage_mul {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (M N : Matrix H H ℂ) : isometricImage V M * isometricImage V N = isometricImage V (M * N)

theorem MIPRE.Introspection.isometricImage_conjTranspose {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (M : Matrix H H ℂ) : (isometricImage V M).conjTranspose = isometricImage V M.conjTranspose

def MIPRE.Introspection.isometricComplement {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [DecidableEq R] (V : Matrix R H ℂ) : Matrix R R ℂ

The orthogonal complement of the image of an isometry.

Equations

• MIPRE.Introspection.isometricComplement V = 1 - MIPRE.Introspection.isometricImage V 1

theorem MIPRE.Introspection.isometricComplement_conjTranspose {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) : (isometricComplement V).conjTranspose = isometricComplement V

theorem MIPRE.Introspection.isometricComplement_mul_image {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (M : Matrix H H ℂ) : isometricComplement V * isometricImage V M = 0

theorem MIPRE.Introspection.isometricImage_mul_complement {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (M : Matrix H H ℂ) : isometricImage V M * isometricComplement V = 0

theorem MIPRE.Introspection.isometricComplement_idem {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) : isometricComplement V * isometricComplement V = isometricComplement V

theorem MIPRE.Introspection.isometricComplement_mul {H : Type u_1} {R : Type u_2} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) : isometricComplement V * V = 0

noncomputable def MIPRE.Introspection.isometricEffect {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [DecidableEq R] (V : Matrix R H ℂ) (a₀ : A) (M : A → Matrix H H ℂ) (a : A) : Matrix R R ℂ

Put the image complement at one fixed outcome.

Equations

• MIPRE.Introspection.isometricEffect V a₀ M a = MIPRE.Introspection.isometricImage V (M a) + if a = a₀ then MIPRE.Introspection.isometricComplement V else 0

theorem MIPRE.Introspection.isometricEffect_isPVM {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) {M : A → Matrix H H ℂ} (hM : IsPVM M) : IsPVM (isometricEffect V a₀ M)

Completion of the conjugated effects is a PVM on the whole target.

theorem MIPRE.Introspection.isometricEffect_intertwine {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : A → Matrix H H ℂ) (a : A) : isometricEffect V a₀ M a * V = V * M a

The completed measurement intertwines with the original one.

theorem MIPRE.Introspection.isometricEffect_compress {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : A → Matrix H H ℂ) (a : A) : V.conjTranspose * (isometricEffect V a₀ M a * V) = M a

Compression of the completed effect is precisely the source effect.

noncomputable def MIPRE.Introspection.isometricPOVM {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : POVM A H) (hM : IsPVM fun (a : A) => ↑(M.mats a)) : POVM A R

The concrete projective POVM on the isometry's target.

Equations

• MIPRE.Introspection.isometricPOVM V hV a₀ M hM = ⋯.toPOVM

theorem MIPRE.Introspection.isometricPOVM_mats {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : POVM A H) (hM : IsPVM fun (a : A) => ↑(M.mats a)) (a : A) : ↑((isometricPOVM V hV a₀ M hM).mats a) = isometricEffect V a₀ (fun (a : A) => ↑(M.mats a)) a

theorem MIPRE.Introspection.isometricPOVM_isPVM {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : POVM A H) (hM : IsPVM fun (a : A) => ↑(M.mats a)) : IsPVM fun (a : A) => ↑((isometricPOVM V hV a₀ M hM).mats a)

theorem MIPRE.Introspection.isometricPOVM_map_intertwine {H : Type u_1} {R : Type u_2} {A : Type u_3} [Fintype H] [DecidableEq H] [Fintype R] [DecidableEq R] [Fintype A] {B : Type u_4} [Fintype B] (V : Matrix R H ℂ) (hV : V.conjTranspose * V = 1) (a₀ : A) (M : POVM A H) (hM : IsPVM fun (a : A) => ↑(M.mats a)) (f : A → B) (b : B) : ↑((POVM.map f (isometricPOVM V hV a₀ M hM)).mats b) * V = V * ↑((POVM.map f M).mats b)

Relabelled effects retain exact intertwining, including labels that collect malformed source answers.

def MIPRE.Introspection.isometricState {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype H] [Fintype K] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (ψ : H × K → ℂ) : R × S → ℂ

Tensor both local isometries into the actual state vector.

Equations

• MIPRE.Introspection.isometricState V W ψ = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V W).mulVec ψ

theorem MIPRE.Introspection.isometricTensor_isometry {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hV : V.conjTranspose * V = 1) (hW : W.conjTranspose * W = 1) : (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V W).conjTranspose * Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V W = 1

theorem MIPRE.Introspection.isometricState_unit {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hV : V.conjTranspose * V = 1) (hW : W.conjTranspose * W = 1) (ψ : H × K → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) : star (isometricState V W ψ) ⬝ᵥ isometricState V W ψ = 1

theorem MIPRE.Introspection.bornProb_isometricState {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] [Fintype A] [Fintype B] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hV : V.conjTranspose * V = 1) (hW : W.conjTranspose * W = 1) (ψ : H × K → ℂ) (a₀ : A) (b₀ : B) (M : A → Matrix H H ℂ) (N : B → Matrix K K ℂ) (a : A) (b : B) : bornProb (isometricState V W ψ) (isometricEffect V a₀ M a) (isometricEffect W b₀ N b) = bornProb ψ (M a) (N b)

Local completion leaves every individual Born probability unchanged.

theorem MIPRE.Introspection.povmValue_isometricState {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} {B : Type u_6} {X : Type u_7} {Y : Type u_8} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] [Fintype A] [Fintype B] [Fintype X] [Fintype Y] (G : Game X Y A B) (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hV : V.conjTranspose * V = 1) (hW : W.conjTranspose * W = 1) (ψ : H × K → ℂ) (a₀ : A) (b₀ : B) (MA : X → POVM A H) (MB : Y → POVM B K) (hMA : ∀ (x : X), IsPVM fun (a : A) => ↑((MA x).mats a)) (hMB : ∀ (y : Y), IsPVM fun (b : B) => ↑((MB y).mats b)) : (povmValue G (isometricState V W ψ) (fun (x : X) => isometricPOVM V hV a₀ (MA x) ⋯) fun (y : Y) => isometricPOVM W hW b₀ (MB y) ⋯) = povmValue G ψ MA MB

Every game value is exactly preserved by the concrete transported PVMs.

theorem MIPRE.Introspection.isometricState_map_alice_deviation {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} {A : Type u_5} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] [Fintype A] {C : Type u_9} [Fintype C] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hV : V.conjTranspose * V = 1) (ψ : H × K → ℂ) (a₀ : A) (M : POVM A H) (hM : IsPVM fun (a : A) => ↑(M.mats a)) (f : A → C) (c : C) (T : Matrix R R ℂ) : (aOp (↑((POVM.map f (isometricPOVM V hV a₀ M hM)).mats c) - T)).mulVec (isometricState V W ψ) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) (V * ↑((POVM.map f M).mats c) - T * V) W).mulVec ψ

Alice's same intertwining identity after any answer projection.

theorem MIPRE.Introspection.isometricState_map_bob_deviation {H : Type u_1} {K : Type u_2} {R : Type u_3} {S : Type u_4} {B : Type u_6} [Fintype H] [DecidableEq H] [Fintype K] [DecidableEq K] [Fintype R] [DecidableEq R] [Fintype S] [DecidableEq S] [Fintype B] {C : Type u_9} [Fintype C] (V : Matrix R H ℂ) (W : Matrix S K ℂ) (hW : W.conjTranspose * W = 1) (ψ : H × K → ℂ) (b₀ : B) (N : POVM B K) (hN : IsPVM fun (b : B) => ↑(N.mats b)) (f : B → C) (c : C) (T : Matrix S S ℂ) : (bOp (↑((POVM.map f (isometricPOVM W hW b₀ N hN)).mats c) - T)).mulVec (isometricState V W ψ) = (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) V (W * ↑((POVM.map f N).mats c) - T * W)).mulVec ψ

Bob's same intertwining identity after any answer projection.