Game-value bounds for actual question-indexed replacements #
Acceptance is compared before relabelling the outcomes. This permits a common answer alphabet without assuming that same-party squared distance contracts under coarse-graining.
Stated in a bipartite model (Phase 4 of planning/mipco-track.md).
theorem
MIPRE.Introspection.testAcceptance_map_left
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
(Ψ : BipartiteModel 𝒞 𝒜 ℬ)
{A : Type u_6}
{B : Type u_7}
{C : Type u_8}
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
[Fintype C]
[DecidableEq C]
(D : A → B → Bool)
(M : POVMIn C 𝒜)
(N : POVMIn B ℬ)
(f : C → A)
:
testAcceptance Ψ D (POVMIn.map f M).op N.op = testAcceptance Ψ (fun (c : C) (b : B) => D (f c) b) M.op N.op
Relabelling a measurement pulls the acceptance predicate back exactly.
theorem
MIPRE.Introspection.testAcceptance_stability_map_left
{𝒞 : Type u_1}
{𝒜 : Type u_2}
{ℬ : Type u_3}
[Ring 𝒞]
[StarRing 𝒞]
[Algebra ℂ 𝒞]
[Ring 𝒜]
[StarRing 𝒜]
[Algebra ℂ 𝒜]
[Ring ℬ]
[StarRing ℬ]
[Algebra ℂ ℬ]
[PartialOrder 𝒜]
[StarOrderedRing 𝒜]
[PartialOrder ℬ]
[StarOrderedRing ℬ]
(Ψ : BipartiteModel 𝒞 𝒜 ℬ)
{A : Type u_6}
{B : Type u_7}
{C : Type u_8}
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
[Fintype C]
[DecidableEq C]
(hΨ : ‖Ψ.ψ‖ = 1)
(D : A → B → Bool)
(M R : POVMIn C 𝒜)
(N : POVMIn B ℬ)
(f : C → A)
(hM : IsPVMIn M.op)
(hR : IsPVMIn R.op)
(hN : IsPVMIn N.op)
{δ : ℝ}
(hd : ∑ c : C, Ψ.stateSqNorm (M.op c - R.op c) ≤ δ)
:
|testAcceptance Ψ D (POVMIn.map f M).op N.op - testAcceptance Ψ D (POVMIn.map f R).op N.op| ≤ 2 * √δ
A projective replacement may be relabelled into a larger answer alphabet without an answer-cardinality cost in the acceptance estimate.
theorem
MIPRE.Introspection.povmValue_stability_of_condWin
{𝒞 : 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}
{A : Type u_6}
{B : Type u_7}
[Fintype X]
[Fintype Y]
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
(G : Game X Y A B)
(MA RA : X → POVMIn A 𝒜)
(MB : Y → POVMIn B ℬ)
(err : X → ℝ)
(herr : ∀ (x : X), 0 ≤ err x)
(hpoint : ∀ (x : X) (y : Y), |Ψ.condWin G MA MB x y - Ψ.condWin G RA MB x y| ≤ 2 * √(err x))
{δ : ℝ}
(hd : ∑ x : X, ∑ y : Y, G.μ x y * err x ≤ δ)
:
Averaging conditional acceptance changes costs no question-count factor.
theorem
MIPRE.Introspection.povmValue_stability_at
{𝒞 : 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}
{A : Type u_6}
{B : Type u_7}
{C : Type u_8}
[Fintype X]
[Fintype Y]
[Fintype A]
[DecidableEq A]
[Fintype B]
[DecidableEq B]
[Fintype C]
[DecidableEq C]
[DecidableEq X]
(G : Game X Y A B)
(hΨ : ‖Ψ.ψ‖ = 1)
(MA RA : X → POVMIn A 𝒜)
(MB : Y → POVMIn B ℬ)
(q : X)
(M R : POVMIn C 𝒜)
(f : C → A)
(hMA : MA q = POVMIn.map f M)
(hRA : RA q = POVMIn.map f R)
(hsame : ∀ (x : X), x ≠ q → MA x = RA x)
(hM : IsPVMIn M.op)
(hR : IsPVMIn R.op)
(hMB : ∀ (y : Y), IsPVMIn (MB y).op)
{δ : ℝ}
(hd : ∑ c : C, Ψ.stateSqNorm (M.op c - R.op c) ≤ δ)
:
A single changed question, with an arbitrary outcome relabelling. All other questions are literally unchanged, and the error pays at most its conditional bound since the question's marginal probability is at most one.