Pauli mixing with a retained classical fibre

The sampled register has a fixed coordinate presentation, with arbitrary auxiliary systems. The output consists of actual ancillary POVMs. Consistency and the two readout commutator errors control the squared state distance by an explicit square-root estimate.

In the register model (Phase 4 of planning/mipco-track.md): the EPR state on the sampled register adjoined to an ancillary model Ξ, Ξ.reg (Fin n → F); the output POVMs are in the ancilla's algebra.

noncomputable def MIPRE.Introspection.readoutCommutatorError {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] {B : Type u_6} [Fintype B] (Ψ : BipartiteModel 𝒞 (Matrix (Fin n → F) (Fin n → F) 𝒜) ℬ) (M : B → Matrix (Fin n → F) (Fin n → F) 𝒜) (w : (Fin n → F) → Matrix (Fin n → F) (Fin n → F) ℂ) (L : (Fin n → F) →ₗ[F] Fin n → F) : ℝ

Sum of the commutator errors against a linear-map readout, over all outcomes and fibres.

Equations

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

noncomputable def MIPRE.Introspection.readoutMarginalError {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {A : Type u_2} [Fintype A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (L : (Fin n → F) →ₗ[F] Fin n → F) (Ψ : BipartiteModel 𝒞 (Matrix (Fin n → F) (Fin n → F) 𝒜) ℬ) (M : (Fin n → F) × A → Matrix (Fin n → F) (Fin n → F) 𝒜) : ℝ

The first marginal's consistency error with the retained Z readout.

Equations

• MIPRE.Introspection.readoutMarginalError L Ψ M = ∑ y : Fin n → F, Ψ.stateSqNorm (∑ a : A, M (y, a) - MIPRE.smulKron 1 (MIPRE.Weyl.synOf MIPRE.Weyl.wZ (⇑L) y))

noncomputable def MIPRE.Introspection.mixingError {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {A : Type u_2} [Fintype A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (L : (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : POVMIn ((Fin n → F) × A) (Matrix (Fin n → F) (Fin n → F) 𝒜)) : ℝ

The error before completing the retained submeasurement: coefficients 2, 8, 8.

Equations

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

theorem MIPRE.Introspection.mixingError_nonneg {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (L : (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (M : POVMIn ((Fin n → F) × A) (Matrix (Fin n → F) (Fin n → F) 𝒜)) : 0 ≤ mixingError L Ξ M

Every term entering the mixing error is a squared norm.

theorem MIPRE.Introspection.exists_pauli_mixing {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] (L : (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : POVMIn ((Fin n → F) × A) (Matrix (Fin n → F) (Fin n → F) 𝒜)) (hM : IsPVMIn M.op) : ∃ (Q : (Fin n → F) → POVMIn A 𝒜), ∑ p : (Fin n → F) × A, (Ξ.reg (Fin n → F)).stateSqNorm (M.op p - smulKron ((Q p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑L) p.1)) ≤ 2 * mixingError L Ξ M + 4 * √(mixingError L Ξ M)

Pauli mixing produces normalized POVMs on the ancilla at every retained fibre.

theorem MIPRE.Introspection.exists_pauli_mixing_avg {F : Type u_1} [Field F] [Fintype F] [DecidableEq F] [Algebra (ZMod 2) F] {n : ℕ} {A : Type u_2} [Fintype A] [DecidableEq A] {𝒞 : Type u_3} {𝒜 : Type u_4} {ℬ : Type u_5} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [StarModule ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [StarModule ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [StarProper 𝒜] {X : Type u_6} [Fintype X] (D : X → ℝ) (hD0 : ∀ (x : X), 0 ≤ D x) (hD1 : ∑ x : X, D x = 1) (L : X → (Fin n → F) →ₗ[F] Fin n → F) (Ξ : BipartiteModel 𝒞 𝒜 ℬ) (hΞ : ‖Ξ.ψ‖ = 1) (M : X → POVMIn ((Fin n → F) × A) (Matrix (Fin n → F) (Fin n → F) 𝒜)) (hM : ∀ (x : X), IsPVMIn (M x).op) {δ : ℝ} (hδ : ∑ x : X, D x * mixingError (L x) Ξ (M x) ≤ δ) : ∃ (Q : X → (Fin n → F) → POVMIn A 𝒜), ∑ x : X, D x * ∑ p : (Fin n → F) × A, (Ξ.reg (Fin n → F)).stateSqNorm ((M x).op p - smulKron ((Q x p.1).op p.2) (Weyl.synOf Weyl.wZ (⇑(L x)) p.1)) ≤ 2 * δ + 4 * √δ

Question averaging costs no dimension factor and moves the error inside one square root.