Bridge, part 4: strategies

A tensor-product strategy for our game (TensorProductStrategy (lidtGame F m d)) is packaged as a MIPStarRE two-space projective strategy (ProjStrat): the state vector becomes a pure state (MIPStarRE's density matrices carry the normalization τ(ρ) = 1 for the normalized trace, so the density is dim · |ψ⟩⟨ψ|), and the measurement families are those of MIPRE.Background.LIDT.Bridge.Measurement.

theorem MIPRE.LIDT.Bridge.nonempty_of_unit {ι : Type u_2} [Fintype ι] (ψ : ι → ℂ) (h : star ψ ⬝ᵥ ψ = 1) : Nonempty ι

The index type of a unit vector is nonempty.

instance MIPRE.LIDT.Bridge.instNonemptyProdFinDAQuestionAnswerDB {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) : Nonempty (Fin S.dA × Fin S.dB)

def MIPRE.LIDT.Bridge.pureState {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) : MIPStarRE.LDT.PureState (Fin S.dA × Fin S.dB)

The shared state of a strategy, as a MIPStarRE pure state.

Equations

• MIPRE.LIDT.Bridge.pureState S = { vector := S.ψ, unit := ⋯ }

noncomputable def MIPRE.LIDT.Bridge.toProjStrat {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) : MIPStarRE.LDT.ProjStrat (lidtParams F m d) (Fin S.dA) (Fin S.dB)

The MIPStarRE two-space projective strategy induced by a strategy for our game.

Equations

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

theorem MIPRE.LIDT.Bridge.ev_toProjStrat {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] {m d : ℕ} [NeZero m] (S : TensorProductStrategy (lidtGame F m d)) (X : Matrix (Fin S.dA × Fin S.dB) (Fin S.dA × Fin S.dB) ℂ) : MIPStarRE.LDT.ev (toProjStrat S).state X = (star S.ψ ⬝ᵥ X.mulVec S.ψ).re

Expectation values in the induced strategy are the Born-rule expectations of S.ψ.