Conditional consistency

The paper's lem:conditional-consistency, with constant two in the summed squared state norm. The conditioning index may determine Alice's entire POVM.

Stated in a bipartite model (Phase 4 of planning/mipco-track.md); the submeasurement is self-adjoint in the joint algebra and positive on the Hilbert space, as the product of two commuting positive operators of the two players is.

theorem MIPRE.Introspection.submeasurement_agreement_dist {𝒞 : Type u_1} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] (Ψ : StateModel 𝒞) {I : Type u_2} [Fintype I] (hΨ : ‖Ψ.ψ‖ = 1) (P C : I → 𝒞) (hP : IsPVMIn P) (hCsa : ∀ (i : I), star (C i) = C i) (hC0 : ∀ (i : I), 0 ≤ Ψ.π (C i)) (hCsum : ∑ i : I, Ψ.π (C i) ≤ 1) : ∑ i : I, Ψ.snorm (P i - C i) ^ 2 ≤ 2 * (1 - ∑ i : I, Ψ.qform (P i * C i))

Agreement with a positive submeasurement controls distance to a PVM.

theorem MIPRE.Introspection.conditional_consistency {𝒞 : Type u_1} {𝒜 : Type u_2} {ℬ : Type u_3} [Ring 𝒞] [StarRing 𝒞] [Algebra ℂ 𝒞] [Ring 𝒜] [StarRing 𝒜] [Algebra ℂ 𝒜] [Ring ℬ] [StarRing ℬ] [Algebra ℂ ℬ] [PartialOrder 𝒜] [StarOrderedRing 𝒜] [PartialOrder ℬ] [StarOrderedRing ℬ] (Ψ : BipartiteModel 𝒞 𝒜 ℬ) {X : Type u_4} {Y : Type u_5} {Z : Type u_6} [Fintype X] [DecidableEq X] [Fintype Y] [DecidableEq Y] [Fintype Z] [DecidableEq Z] (hΨ : ‖Ψ.ψ‖ = 1) (A : Y → POVMIn (X × Z) 𝒜) (B : (X × Y) × Z → ℬ) (hB : IsPVMIn B) {δ : ℝ} (hagree : 1 - δ ≤ ∑ p : (X × Y) × Z, Ψ.bornProb ((A p.1.2).op (p.1.1, p.2)) (B p)) : ∑ p : (X × Y) × Z, Ψ.snorm (Ψ.πB (B p) - Ψ.πA ((A p.1.2).op (p.1.1, p.2)) * Ψ.πB (∑ z : Z, B (p.1, z))) ^ 2 ≤ 2 * δ

Conditioning Alice's measurement on Bob's first two reported indices preserves consistency.