Projective sampling and joint hiding measurements

theorem MIPRE.Introspection.weyl_projectors_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (hw : Weyl.IsWeylFamily w) : IsPVM (Weyl.proj w)

theorem MIPRE.Introspection.linear_measurement_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (hw : Weyl.IsWeylFamily w) (L : (Fin n → F) →ₗ[F] Fin n → F) : IsPVM (Weyl.synOf w ⇑L)

Reading any linear map of a Weyl eigenbasis outcome is a projective measurement.

theorem MIPRE.Introspection.joint_measurement_isPVM {ι : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype A] [DecidableEq A] [Fintype B] [DecidableEq B] (P : A → Matrix ι ι ℂ) (Q : B → Matrix ι ι ℂ) (hP : IsPVM P) (hQ : IsPVM Q) (hc : ∀ (a : A) (b : B), Commute (P a) (Q b)) : IsPVM fun (ab : A × B) => P ab.1 * Q ab.2

Jointly reading two commuting projective measurements gives a projective measurement.

theorem MIPRE.Introspection.sampling_hiding_isPVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} (L R : (Fin n → F) →ₗ[F] Fin n → F) (hLR : CL.perp R.ker ≤ L.ker) : IsPVM fun (ab : (Fin n → F) × (Fin n → F)) => Weyl.synOf Weyl.wZ (⇑L) ab.1 * Weyl.synOf Weyl.wX (⇑R) ab.2

The sampling and hiding readouts used by the honest introspection strategy form a PVM.