Conditional ideal replacement from an actual tested relation #
The conditional approximation is derived from the acceptance probability and concrete answer maps. It is not an additional rigidity premise.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md).
theorem
MIPRE.Introspection.conditional_coarse_ideal_of_test
{𝒞 : 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}
{O : Type u_5}
{Y : Type u_6}
{Z : Type u_7}
[Fintype I]
[DecidableEq I]
[Fintype O]
[DecidableEq O]
[Fintype Y]
[DecidableEq Y]
[Fintype Z]
[DecidableEq Z]
(hΨ : ‖Ψ.ψ‖ = 1)
(M : POVMIn I 𝒜)
(N : POVMIn O ℬ)
(P : I → ℬ)
(Q : Y → ℬ)
(f : Y → I → Z)
(g : O → Y × Z)
(test : I → O → Bool)
(hM : IsPVMIn M.op)
(hN : IsPVMIn N.op)
(hP : IsPVMIn P)
(hQ : IsPVMIn Q)
(hc : ∀ (y : Y) (i : I), Commute (Q y) (P i))
{δ η ε : ℝ}
(hfine : ∑ i : I, Ψ.xSqNorm (M.op i) (P i) ≤ ε)
(hnorm : ∑ y : Y, Ψ.snorm (Ψ.πB (∑ z : Z, (POVMIn.map g N).op (y, z) - Q y)) ^ 2 ≤ η)
(hwin : 1 - δ ≤ ∑ i : I, ∑ o : O, (if test i o = true then 1 else 0) * Ψ.bornProb (M.op i) (N.op o))
(hcheck : ∀ (i : I) (o : O), test i o = true → f (g o).1 i = (g o).2)
:
Replace the actual marginal in a tested conditional relation by its ideal commuting prefix, with constant six on the test's conditional failure.