Reindexing the registers of a bipartite strategy

TensorProductStrategy (blueprint def:tensor-strategy) fixes the two players' registers to be Fin dA and Fin dB, and every soundness theorem proved through the vendored developments --- MIPRE.LIDT.Adapter.clSoundness_ldc_one_deltaCL in particular --- takes and returns its strategies in that form. The rigidity arguments of MIPRE.QLD, on the other hand, build their states and measurements on structured registers: a strategy's own space tensored with ancillas such as (dA × Anc F m) × (F × F), where the block structure is what the proofs compute with. A strategy in that form has a value (povmValue), but it is not a TensorProductStrategy, and nothing in the repository turned one into the other. This file is that bridge.

Everything transports along an equivalence e : d ≃ d' of a register:

• reindexStarAlgEquiv e is Matrix.reindex e e as a star-algebra equivalence, so that ProjectiveMeasurement.map moves projective measurement families across it;
• POVM.reindex e moves POVMs, and commutes with the relabelling POVM.map (POVM.map_reindex) and with ProjectiveMeasurement.toPOVM (ProjectiveMeasurement.toPOVM_map_reindex);
• reindexVec eA eB moves a bipartite state, and the Born rule is invariant (quadForm_reindex, bornProb_reindex), hence so are povmValue (povmValue_reindex) and inconsistency (inconsistency_reindex).

TensorProductStrategy.ofProjective then packages a projective strategy on arbitrary finite registers as a TensorProductStrategy on Fin (card dA) × Fin (card dB), with TensorProductStrategy.value_ofProjective identifying its value with the povmValue of the original; TensorProductStrategy.ofPVM is the same for measurements given as POVM families with IsPVM proofs, the form the rigidity arguments produce. A consumer applies a soundness theorem to the packaged strategy and reads the conclusion back through inconsistency_reindex and the reindex lemmas: MIPRE.Background.LIDT.Adapter.Registers does exactly that for the seeded low individual degree test.

The matrix algebra of a reindexed register

def MIPRE.reindexStarAlgEquiv {d : Type u_1} {d' : Type u_2} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] (e : d ≃ d') : Matrix d d ℂ ≃⋆ₐ[ℂ] Matrix d' d' ℂ

Matrix.reindex e e as a star-algebra equivalence of the two matrix algebras.

Equations

• MIPRE.reindexStarAlgEquiv e = StarAlgEquiv.ofAlgEquiv (Matrix.reindexAlgEquiv ℂ ℂ e) ⋯

@[simp]

theorem MIPRE.reindexStarAlgEquiv_apply {d : Type u_1} {d' : Type u_2} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] (e : d ≃ d') (M : Matrix d d ℂ) : (reindexStarAlgEquiv e) M = (Matrix.reindex e e) M

Reindexing POVMs and projective measurement families

def MIPRE.POVM.reindex {A : Type u_1} [Fintype A] {d : Type u_2} {d' : Type u_3} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] (e : d ≃ d') (M : POVM A d) : POVM A d'

Reindex a POVM along an equivalence of its register.

Equations

• MIPRE.POVM.reindex e M = { mats := fun (a : A) => ⟨(Matrix.reindex e e) ↑(M.mats a), ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.POVM.reindex_mats {A : Type u_1} [Fintype A] {d : Type u_2} {d' : Type u_3} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] (e : d ≃ d') (M : POVM A d) (a : A) : ↑((reindex e M).mats a) = (Matrix.reindex e e) ↑(M.mats a)

theorem MIPRE.POVM.reindex_symm_reindex {A : Type u_1} [Fintype A] {d : Type u_2} {d' : Type u_3} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] (e : d ≃ d') (M : POVM A d') : reindex e (reindex e.symm M) = M

Reindexing back and forth is the identity, in the other order.

theorem MIPRE.POVM.map_reindex {A : Type u_1} [Fintype A] {d : Type u_2} {d' : Type u_3} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] {B : Type u_4} [Fintype B] [DecidableEq B] (e : d ≃ d') (f : A → B) (M : POVM A d) : reindex e (map f M) = map f (reindex e M)

Reindexing the register commutes with relabelling the outcomes.

theorem MIPRE.ProjectiveMeasurement.toPOVM_map_reindex {A : Type u_1} [Fintype A] {d : Type u_2} {d' : Type u_3} [Fintype d] [Fintype d'] [DecidableEq d] [DecidableEq d'] {X : Type u_4} [Fintype X] (e : d ≃ d') (P : ProjectiveMeasurement X A (Matrix d d ℂ)) (x : X) : (map (reindexStarAlgEquiv e) P).toPOVM x = POVM.reindex e (P.toPOVM x)

The POVM of a projective measurement family transported along reindexStarAlgEquiv e is the reindexed POVM.

def MIPRE.ProjectiveMeasurement.ofIsPVM {A : Type u_1} [Fintype A] {d : Type u_2} [Fintype d] [DecidableEq d] {X : Type u_4} (M : X → POVM A d) (h : ∀ (x : X), IsPVM fun (a : A) => ↑((M x).mats a)) : ProjectiveMeasurement X A (Matrix d d ℂ)

A family of POVMs whose elements are projective, as a ProjectiveMeasurement. This is the form the rigidity arguments produce their measurements in (IsPVM on the bare matrices), and TensorProductStrategy consumes the bundled form.

Equations

• MIPRE.ProjectiveMeasurement.ofIsPVM M h = { M := fun (x : X) (a : A) => ↑((M x).mats a), selfAdjoint := ⋯, projective := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.ProjectiveMeasurement.toPOVM_ofIsPVM {A : Type u_1} [Fintype A] {d : Type u_2} [Fintype d] [DecidableEq d] {X : Type u_4} [Fintype X] (M : X → POVM A d) (h : ∀ (x : X), IsPVM fun (a : A) => ↑((M x).mats a)) (x : X) : (ofIsPVM M h).toPOVM x = M x

Reindexing a bipartite state, and the invariance of the Born rule

def MIPRE.reindexVec {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} (eA : dA ≃ dA') (eB : dB ≃ dB') (ψ : dA × dB → ℂ) : dA' × dB' → ℂ

Reindex a bipartite state along equivalences of the two registers.

Equations

• MIPRE.reindexVec eA eB ψ = ψ ∘ ⇑(eA.prodCongr eB).symm

theorem MIPRE.reindex_kronecker_reindex {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} (eA : dA ≃ dA') (eB : dB ≃ dB') (M : Matrix dA dA ℂ) (N : Matrix dB dB ℂ) : Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((Matrix.reindex eA eA) M) ((Matrix.reindex eB eB) N) = (Matrix.reindex (eA.prodCongr eB) (eA.prodCongr eB)) (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N)

The Kronecker product of two reindexed matrices is the reindexing of the Kronecker product along the product equivalence.

theorem MIPRE.quadForm_reindex {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} [Fintype dA] [Fintype dB] [Fintype dA'] [Fintype dB'] (eA : dA ≃ dA') (eB : dB ≃ dB') (ψ : dA × dB → ℂ) (M : Matrix dA dA ℂ) (N : Matrix dB dB ℂ) : star (reindexVec eA eB ψ) ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) ((Matrix.reindex eA eA) M) ((Matrix.reindex eB eB) N)).mulVec (reindexVec eA eB ψ) = star ψ ⬝ᵥ (Matrix.kroneckerMap (fun (x1 x2 : ℂ) => x1 * x2) M N).mulVec ψ

The Born rule is invariant under reindexing.

theorem MIPRE.reindexVec_unit {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} [Fintype dA] [Fintype dB] [Fintype dA'] [Fintype dB'] (eA : dA ≃ dA') (eB : dB ≃ dB') {ψ : dA × dB → ℂ} (hψ : star ψ ⬝ᵥ ψ = 1) : star (reindexVec eA eB ψ) ⬝ᵥ reindexVec eA eB ψ = 1

A reindexed unit vector is a unit vector.

theorem MIPRE.bornProb_reindex {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} [Fintype dA] [Fintype dB] [Fintype dA'] [Fintype dB'] (eA : dA ≃ dA') (eB : dB ≃ dB') (ψ : dA × dB → ℂ) (EA : Matrix dA dA ℂ) (EB : Matrix dB dB ℂ) : bornProb (reindexVec eA eB ψ) ((Matrix.reindex eA eA) EA) ((Matrix.reindex eB eB) EB) = bornProb ψ EA EB

theorem MIPRE.povmValue_reindex {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} [Fintype dA] [Fintype dB] [Fintype dA'] [Fintype dB'] [DecidableEq dA] [DecidableEq dB] [DecidableEq dA'] [DecidableEq dB'] {X : Type u_5} {Y : Type u_6} {A : Type u_7} {B : Type u_8} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (eA : dA ≃ dA') (eB : dB ≃ dB') (G : Game X Y A B) (ψ : dA × dB → ℂ) (MA : X → POVM A dA) (MB : Y → POVM B dB) : (povmValue G (reindexVec eA eB ψ) (fun (x : X) => POVM.reindex eA (MA x)) fun (y : Y) => POVM.reindex eB (MB y)) = povmValue G ψ MA MB

The value of a strategy is invariant under reindexing its registers.

theorem MIPRE.inconsistency_reindex {dA : Type u_1} {dB : Type u_2} {dA' : Type u_3} {dB' : Type u_4} [Fintype dA] [Fintype dB] [Fintype dA'] [Fintype dB'] [DecidableEq dA] [DecidableEq dB] [DecidableEq dA'] [DecidableEq dB'] {X : Type u_5} {A : Type u_7} [Fintype X] [Fintype A] [DecidableEq A] (eA : dA ≃ dA') (eB : dB ≃ dB') (μ : X → ℝ) (ψ : dA × dB → ℂ) (M : X → POVM A dA) (N : X → POVM A dB) : (inconsistency μ (reindexVec eA eB ψ) (fun (x : X) => POVM.reindex eA (M x)) fun (x : X) => POVM.reindex eB (N x)) = inconsistency μ ψ M N

Inconsistency is invariant under reindexing the registers.

A projective strategy on arbitrary registers, as a TensorProductStrategy

theorem MIPRE.TensorProductStrategy.value_eq_povmValue {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {G : Game X Y A B} (S : TensorProductStrategy G) : S.value = povmValue G S.ψ (fun (x : X) => S.PA.toPOVM x) fun (y : Y) => S.PB.toPOVM y

TensorProductStrategy.value is the povmValue of the strategy's own measurements, read as POVMs.

noncomputable def MIPRE.TensorProductStrategy.ofProjective {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (G : Game X Y A B) (ψ : dA × dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (PA : ProjectiveMeasurement X A (Matrix dA dA ℂ)) (PB : ProjectiveMeasurement Y B (Matrix dB dB ℂ)) : TensorProductStrategy G

A projective strategy on arbitrary finite registers dA, dB, packaged as a TensorProductStrategy on Fin (card dA) × Fin (card dB) along Fintype.equivFin.

Equations

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

theorem MIPRE.TensorProductStrategy.value_ofProjective {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (G : Game X Y A B) (ψ : dA × dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (PA : ProjectiveMeasurement X A (Matrix dA dA ℂ)) (PB : ProjectiveMeasurement Y B (Matrix dB dB ℂ)) : (ofProjective G ψ hψ PA PB).value = povmValue G ψ (fun (x : X) => PA.toPOVM x) fun (y : Y) => PB.toPOVM y

The packaged strategy has the value of the original. The two sides agree definitionally once TensorProductStrategy.value is read as a povmValue: the packaged state is the reindexed state and the packaged measurements are the reindexed POVMs.

noncomputable def MIPRE.TensorProductStrategy.ofPVM {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {dA : Type u_5} {dB : Type u_6} [Fintype dA] [DecidableEq dA] [Fintype dB] [DecidableEq dB] (G : Game X Y A B) (ψ : dA × dB → ℂ) (hψ : star ψ ⬝ᵥ ψ = 1) (MA : X → POVM A dA) (MB : Y → POVM B dB) (hA : ∀ (x : X), IsPVM fun (a : A) => ↑((MA x).mats a)) (hB : ∀ (y : Y), IsPVM fun (b : B) => ↑((MB y).mats b)) : TensorProductStrategy G

A strategy given by POVM families with projective elements, packaged as a TensorProductStrategy.

Equations

• MIPRE.TensorProductStrategy.ofPVM G ψ hψ MA MB hA hB = MIPRE.TensorProductStrategy.ofProjective G ψ hψ (MIPRE.ProjectiveMeasurement.ofIsPVM MA hA) (MIPRE.ProjectiveMeasurement.ofIsPVM MB hB)