Dilating a POVM strategy to a projective one

A strategy built by a rigidity argument arrives as a family of POVMs on each party's register --- averages of sandwiches, coarse-grainings, mixtures --- while the soundness theorems take TensorProductStrategy, whose measurements are projective. Naimark's theorem closes the gap: each family of POVMs is the compression, by one question-independent isometry ancillaEmbed d a₀, of a projective family on d × A (exists_projective_dilation). This file packages that for a whole two-party strategy and records the two facts a consumer needs:

• povmValue_extVec2: on the twice-extended state extVec2 ψ a₀ b₀ a strategy has the value of its compression on ψ, so the dilated projective strategy has the value of the POVM strategy it came from;
• inconsistency_extVec2: likewise for the inconsistency of two measurement families, so a conclusion about the dilated strategy on the extended state reads back, through POVM.compress, as a conclusion about compressions on the original state.

ancCompress a₀ is the compression of a single matrix and POVM.compress a₀ of a POVM; the latter is a POVM because the isometry preserves positivity and sends the identity to the identity. exists_projective_dilation_povm is Naimark for a question-indexed family of bundled POVMs. MIPRE.Background.LIDT.Adapter.Registers combines these with the reindexing of that file to state the seeded low individual degree test's soundness for a POVM strategy.

Compression by an inert ancilla

def MIPRE.ancCompress {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] (a₀ : Anc) (X : Matrix (d × Anc) (d × Anc) ℂ) : Matrix d d ℂ

The compression of an operator on d × Anc by the ancilla state |a₀⟩.

Equations

• MIPRE.ancCompress a₀ X = (MIPRE.ancillaEmbed d a₀).conjTranspose * (X * MIPRE.ancillaEmbed d a₀)

theorem MIPRE.ancCompress_posSemidef {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] (a₀ : Anc) {X : Matrix (d × Anc) (d × Anc) ℂ} (hX : X.PosSemidef) : (ancCompress a₀ X).PosSemidef

theorem MIPRE.ancCompress_one {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] (a₀ : Anc) : ancCompress a₀ 1 = 1

theorem MIPRE.ancCompress_sum {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] {ι : Type u_3} (a₀ : Anc) (s : Finset ι) (X : ι → Matrix (d × Anc) (d × Anc) ℂ) : ancCompress a₀ (∑ i ∈ s, X i) = ∑ i ∈ s, ancCompress a₀ (X i)

theorem MIPRE.ancCompress_conjTranspose {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] (a₀ : Anc) (X : Matrix (d × Anc) (d × Anc) ℂ) : (ancCompress a₀ X).conjTranspose = ancCompress a₀ X.conjTranspose

def MIPRE.POVM.compress {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] {A : Type u_3} [Fintype A] (a₀ : Anc) (M : POVM A (d × Anc)) : POVM A d

The compression of a POVM is a POVM.

Equations

• MIPRE.POVM.compress a₀ M = { mats := fun (a : A) => ⟨MIPRE.ancCompress a₀ ↑(M.mats a), ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVM.compress_mats {d : Type u_1} {Anc : Type u_2} [Fintype d] [DecidableEq d] [Fintype Anc] [DecidableEq Anc] {A : Type u_3} [Fintype A] (a₀ : Anc) (M : POVM A (d × Anc)) (a : A) : ↑((compress a₀ M).mats a) = ancCompress a₀ ↑(M.mats a)

The Born rule on the twice-extended state

theorem MIPRE.bornProb_def {dA : Type u_1} {dB : Type u_2} [Fintype dA] [Fintype dB] (ψ : dA × dB → ℂ) (EA : Matrix dA dA ℂ) (EB : Matrix dB dB ℂ) : (star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) EA EB).mulVec ψ).re = bornProb ψ EA EB

The Born probability, in the form the definitions of the value and the inconsistency use.

theorem MIPRE.bornProb_extVec2_ancCompress {dA : Type u_1} {dB : Type u_2} {Anc : Type u_3} {Bnc : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype Anc] [DecidableEq Anc] [Fintype Bnc] [DecidableEq Bnc] (ψ : dA × dB → ℂ) (a₀ : Anc) (b₀ : Bnc) (EA : Matrix (dA × Anc) (dA × Anc) ℂ) (EB : Matrix (dB × Bnc) (dB × Bnc) ℂ) : bornProb (extVec2 ψ a₀ b₀) EA EB = bornProb ψ (ancCompress a₀ EA) (ancCompress b₀ EB)

bornProb_extVec2, with the compressions named.

theorem MIPRE.povmValue_extVec2 {dA : Type u_1} {dB : Type u_2} {Anc : Type u_3} {Bnc : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype Anc] [DecidableEq Anc] [Fintype Bnc] [DecidableEq Bnc] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (ψ : dA × dB → ℂ) (a₀ : Anc) (b₀ : Bnc) (MA : X → POVM A (dA × Anc)) (MB : Y → POVM B (dB × Bnc)) : povmValue G (extVec2 ψ a₀ b₀) MA MB = povmValue G ψ (fun (x : X) => POVM.compress a₀ (MA x)) fun (y : Y) => POVM.compress b₀ (MB y)

A strategy on the twice-extended state has the value of its compression.

theorem MIPRE.inconsistency_extVec2 {dA : Type u_1} {dB : Type u_2} {Anc : Type u_3} {Bnc : Type u_4} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] [Fintype Anc] [DecidableEq Anc] [Fintype Bnc] [DecidableEq Bnc] {X : Type u_5} {A : Type u_7} [Fintype X] [Fintype A] [DecidableEq A] (μ : X → ℝ) (ψ : dA × dB → ℂ) (a₀ : Anc) (b₀ : Bnc) (M : X → POVM A (dA × Anc)) (N : X → POVM A (dB × Bnc)) : inconsistency μ (extVec2 ψ a₀ b₀) M N = inconsistency μ ψ (fun (x : X) => POVM.compress a₀ (M x)) fun (x : X) => POVM.compress b₀ (N x)

Inconsistency on the twice-extended state is inconsistency of the compressions.

Naimark dilation of a POVM strategy

theorem MIPRE.exists_projective_dilation_povm {X : Type u_1} {A : Type u_2} {d : Type u_3} [Fintype A] [DecidableEq A] [Fintype d] [DecidableEq d] (M : X → POVM A d) (a₀ : A) : ∃ (P : ProjectiveMeasurement X A (Matrix (d × A) (d × A) ℂ)), ∀ (x : X), POVM.compress a₀ (P.toPOVM x) = M x

Naimark dilation of a question-indexed family of POVMs: a projective family on d × A whose compression by |a₀⟩ is the given family, question by question.