Replacing a conditional hiding normalizer by its ideal prefix

The coarse outcome map may depend on the retained conditioning label. Positivity of the ideal commuting prefix/fine-projector products lets us retain the fine agreement without a factor depending on either outcome alphabet. The resulting replacement costs three times each of the conditional, prefix, and fine errors.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md): the fine and conditioning measurements of the second player are families in its algebra, and A ⊗ B is πA A * πB B.

theorem MIPRE.Introspection.isPVMIn_joint {R : Type u_1} [Ring R] [StarRing R] {A : Type u_5} {B : Type u_6} [Fintype A] [Fintype B] {P : A → R} {Q : B → R} (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (a : A) (b : B), Commute (P a) (Q b)) : IsPVMIn fun (ab : A × B) => P ab.1 * Q ab.2

Jointly reading two commuting projective measurements gives a projective measurement.

def MIPRE.Introspection.conditionalIdeal {R : Type u_1} [Ring R] {I : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype I] [DecidableEq Z] (P : I → R) (Q : Y → R) (f : Y → I → Z) (p : Y × Z) : R

The ideal joint outcome: its prefix times the fine family coarsened with the map selected by that prefix.

Equations

• MIPRE.Introspection.conditionalIdeal P Q f p = Q p.1 * MIPRE.fibSumIn P (f p.1) p.2

theorem MIPRE.Introspection.commute_fibSum_right {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → R) (Q : Y → R) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) (f : I → Z) (y : Y) (z : Z) : Commute (Q y) (fibSumIn P f z)

theorem MIPRE.Introspection.conditionalIdeal_isPVM {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → R) (Q : Y → R) (f : Y → I → Z) (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) : IsPVMIn (conditionalIdeal P Q f)

Conditional ideal outcomes form a complete PVM although their coarse maps vary.

theorem MIPRE.Introspection.conditionalIdeal_mul_normalizer {R : Type u_1} [Ring R] [StarRing R] {I : Type u_2} {Y : Type u_3} {Z : Type u_4} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (P : I → R) (Q : Y → R) (f : Y → I → Z) (hQ : IsPVMIn Q) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) (p : Y × Z) : conditionalIdeal P Q f p * Q p.1 = conditionalIdeal P Q f p

theorem MIPRE.Introspection.conditional_coarse_overlap {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (M : I → 𝒜) (P : I → ℬ) (Q : Y → ℬ) (f : Y → I → Z) (hM : IsPVMIn M) (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) : ∑ i : I, Ψ.bornProb (M i) (P i) ≤ ∑ p : Y × Z, Ψ.bornProb (fibSumIn M (f p.1) p.2) (conditionalIdeal P Q f p)

Keyed coarse agreement dominates fine agreement when the ideal normalizers commute with the fine ideal PVM. All extra cross terms are positive.

theorem MIPRE.Introspection.conditional_coarse_ideal_distance {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (hΨ : ‖Ψ.ψ‖ = 1) (M : I → 𝒜) (P : I → ℬ) (Q : Y → ℬ) (f : Y → I → Z) (hM : IsPVMIn M) (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) : ∑ p : Y × Z, Ψ.snorm (Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (Q p.1) - Ψ.πB (conditionalIdeal P Q f p)) ^ 2 ≤ ∑ i : I, Ψ.xSqNorm (M i) (P i)

With the ideal prefix attached, keyed coarse-graining costs no more than the fine cross-party squared error.

theorem MIPRE.Introspection.conditional_normalizer_change {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (M : I → 𝒜) (R Q : Y → ℬ) (f : Y → I → Z) (hM : IsPVMIn M) : ∑ p : Y × Z, Ψ.snorm (Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (R p.1) - Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (Q p.1)) ^ 2 ≤ ∑ y : Y, Ψ.snorm (Ψ.πB (R y - Q y)) ^ 2

Summing the complete keyed Alice PVM removes it from the normalizer error.

theorem MIPRE.Introspection.conditional_coarse_ideal_replacement {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {I : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype I] [DecidableEq I] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (hΨ : ‖Ψ.ψ‖ = 1) (M : I → 𝒜) (P : I → ℬ) (Q : Y → ℬ) (B : Y × Z → ℬ) (f : Y → I → Z) (hM : IsPVMIn M) (hP : IsPVMIn P) (hQ : IsPVMIn Q) (hc : ∀ (y : Y) (i : I), Commute (Q y) (P i)) {α η ε : ℝ} (hfine : ∑ i : I, Ψ.xSqNorm (M i) (P i) ≤ ε) (hnorm : ∑ y : Y, Ψ.snorm (Ψ.πB (∑ z : Z, B (y, z) - Q y)) ^ 2 ≤ η) (hconditional : ∑ p : Y × Z, Ψ.snorm (Ψ.πB (B p) - Ψ.πA (fibSumIn M (f p.1) p.2) * Ψ.πB (∑ z : Z, B (p.1, z))) ^ 2 ≤ α) : ∑ p : Y × Z, Ψ.snorm (Ψ.πB (B p) - Ψ.πB (conditionalIdeal P Q f p)) ^ 2 ≤ 3 * α + 3 * η + 3 * ε

Replace the actual conditioning marginal by the commuting ideal prefix. There is no factor depending on the fine, coarse, or conditioning alphabet.