The ancillary blocks of a twirled POVM are POVMs

For block matrices over an ordered ⋆-algebra 𝒜 (Phase 4 of planning/mipco-track.md), ordered as sums of elements Z⋆ Z (MIPRE.MatrixStar.instPartialOrderStar): a POVM of the register and the ancilla, twirled, is a linear-map readout on the register followed by a POVM in 𝒜.

theorem MIPRE.Introspection.averagedBlock_sum {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {A : Type u_3} [Fintype A] (K : Submodule F (Fin n → F)) (M : A → Matrix (Fin n → F) (Fin n → F) 𝒜) (x : Fin n → F) : averagedBlock K (∑ a : A, M a) x = ∑ a : A, averagedBlock K (M a) x

theorem MIPRE.Introspection.averagedBlock_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (K : Submodule F (Fin n → F)) (x : Fin n → F) : averagedBlock K 1 x = 1

theorem MIPRE.Introspection.sum_averagedBlock_eq_one {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] {A : Type u_3} [Fintype A] (K : Submodule F (Fin n → F)) (M : A → Matrix (Fin n → F) (Fin n → F) 𝒜) (hM : ∑ a : A, M a = 1) (x : Fin n → F) : ∑ a : A, averagedBlock K (M a) x = 1

Each averaged diagonal block of a normalized family is itself normalized.

theorem MIPRE.Introspection.star_averagedBlock {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) (hM : star M = M) (x : Fin n → F) : star (averagedBlock K M x) = averagedBlock K M x

An averaged block of a self-adjoint matrix is self-adjoint.

theorem MIPRE.Introspection.averagedBlock_nonneg {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (K : Submodule F (Fin n → F)) (M : Matrix (Fin n → F) (Fin n → F) 𝒜) (hM : 0 ≤ M) (x : Fin n → F) : 0 ≤ averagedBlock K M x

Averaging diagonal compressions preserves positivity.

noncomputable def MIPRE.Introspection.blockPOVM {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_3} [Fintype A] (K : Submodule F (Fin n → F)) (P : POVMIn A (Matrix (Fin n → F) (Fin n → F) 𝒜)) (x : Fin n → F) : POVMIn A 𝒜

The actual ancillary POVM at a selected fiber, obtained by compressing and averaging.

Equations

• MIPRE.Introspection.blockPOVM K P x = { mats := fun (a : A) => ⟨MIPRE.Introspection.averagedBlock K (P.op a) x, ⋯⟩, nonneg := ⋯, normalized := ⋯ }

@[simp]

theorem MIPRE.Introspection.blockPOVM_mats {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_3} [Fintype A] (K : Submodule F (Fin n → F)) (P : POVMIn A (Matrix (Fin n → F) (Fin n → F) 𝒜)) (x : Fin n → F) (a : A) : (blockPOVM K P x).op a = averagedBlock K (P.op a) x

theorem MIPRE.Introspection.linear_twirl_povm {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒜 : Type u_2} [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {A : Type u_3} [Fintype A] (L : (Fin n → F) →ₗ[F] Fin n → F) (P : POVMIn A (Matrix (Fin n → F) (Fin n → F) 𝒜)) : ∃ (Q : (Fin n → F) → POVMIn A 𝒜), ∀ (a : A), averageX L.ker (dephaseZ (P.op a)) = ∑ y : Fin n → F, smulKron ((Q y).op a) (Weyl.synOf Weyl.wZ (⇑L) y)

A Pauli-twirled POVM is a linear-map readout followed by an actual ancillary POVM.