Preliminary comparison theorems: consistency-to-distance estimates #
Estimates converting consistency of a submeasurement and a measurement into
state-dependent distance controls for the diagonal and total sandwich families
of prop:cons-sub-meas.
Consistency controls for prop:cons-sub-meas #
theorem
MIPStarRE.LDT.Preliminaries.consSubMeas_heterogeneous
{Question : Type u_1}
{Outcome : Type u_2}
{ιA : Type u_3}
{ιB : Type u_4}
[Fintype ιA]
[DecidableEq ιA]
[Fintype ιB]
[DecidableEq ιB]
[Fintype Outcome]
(ψ : QuantumState (ιA × ιB))
(𝒟 : Distribution Question)
(A : IdxSubMeas Question Outcome ιA)
(B : IdxMeas Question Outcome ιB)
(γ : Error)
:
ConsRel ψ 𝒟 A B.toIdxSubMeas γ → ConsSubMeasHeterogeneousStmt ψ 𝒟 A B γ
prop:cons-sub-meas, in the two-space form stated in
references/ldt-paper/preliminaries.tex lines 708--744.
theorem
MIPStarRE.LDT.Preliminaries.consSubMeas
{Question : Type u_1}
{Outcome : Type u_2}
{ι : Type u_3}
[Fintype ι]
[DecidableEq ι]
[Fintype Outcome]
(ψ : QuantumState (ι × ι))
(𝒟 : Distribution Question)
(A : IdxSubMeas Question Outcome ι)
(B : IdxMeas Question Outcome ι)
(γ : Error)
:
ConsRel ψ 𝒟 A B.toIdxSubMeas γ → ConsSubMeasStmt ψ 𝒟 A B γ
Same-space specialization of prop:cons-sub-meas.
The paper-facing two-space theorem is consSubMeas_heterogeneous.