Exact classical readout of an EPR register

The last step of introspection reads the two original questions from the same uniform EPR seed. This works for arbitrary question maps, in particular for conditionally linear maps; linearity of the complete map is not required.

def MIPRE.Introspection.readout {I : Type u_1} {X : Type u_2} [DecidableEq I] [DecidableEq X] (f : I → X) (x : X) : Matrix I I ℂ

The computational-basis projector onto a fibre of a question map.

Equations

• MIPRE.Introspection.readout f x = Matrix.diagonal fun (i : I) => if f i = x then 1 else 0

theorem MIPRE.Introspection.readout_isPVM {I : Type u_1} {X : Type u_2} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] (f : I → X) : IsPVM (readout f)

Reading a function of a classical basis label is a projective measurement.

theorem MIPRE.Introspection.bornProb_registerEPR_readout {I : Type u_1} {X : Type u_2} {Y : Type u_3} [Fintype I] [DecidableEq I] [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] (f : I → X) (g : I → Y) (x : X) (y : Y) : bornProb (registerEPR I) (readout f x) (readout g y) = SampledGame.dist f g x y

EPR readouts have exactly the pushforward of the common uniform seed law.

theorem MIPRE.Introspection.readout_eq_synOf {X : Type u_2} [Fintype X] [DecidableEq X] {F : Type u_4} {ι : Type u_5} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] [Fintype ι] [DecidableEq ι] (f : (ι → F) → X) (x : X) : readout f x = Weyl.synOf Weyl.wZ f x

The computational readout is the usual coarse-grained Pauli-Z measurement.

theorem MIPRE.Introspection.sampled_dist_eq_clDist {F : Type u_4} {ι : Type u_5} [Fintype F] [DecidableEq F] [Fintype ι] [DecidableEq ι] (L R : (ι → F) → ι → F) (x y : ι → F) : SampledGame.dist L R x y = CL.clDist L R x y

In a CL sampler the EPR readout law is the sampler's actual question law.