Preliminary comparison theorems: projective converse

Projective-case converse of prop:simeq-to-approx. This lemma lives in a sibling module to ComparisonCore because its proof uses projSubMeas_diagMass_eq_mass, which is introduced in SwitchSandwichPrep.Core, downstream of ComparisonCore.

The imports above are chosen to make the direct dependencies explicit rather than relying on transitive re-exports through SwitchSandwichPrep.Core: ComparisonCore is the sibling comparison module, ConsistencyBridges supplies the BipartiteSDDRel/ConsRel bridging machinery, and SwitchSandwichPrep.Core provides projSubMeas_diagMass_eq_mass.

theorem MIPStarRE.LDT.Preliminaries.approxToSimeq {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (𝒟 : Distribution Question) (A B : IdxProjMeas Question Outcome ι) (δ : Error) : BipartiteSDDRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas (2 * δ) → ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ

Projective converse of prop:simeq-to-approx (Proposition 4.9 of references/ldt-paper/preliminaries.tex, lines 426--455).

For projective measurements A, B, the ≈ relation at strength 2·δ implies the ≃ relation at strength δ, making the paper's implication an iff in the projective case (the forward direction is simeqToApprox).

theorem MIPStarRE.LDT.Preliminaries.approxToSimeq_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 : IdxProjMeas Question Outcome ιA) (B : IdxProjMeas Question Outcome ιB) (δ : Error) : SDDRel ψ 𝒟 A.toIdxSubMeas.placeLeft B.toIdxSubMeas.placeRight (2 * δ) → ConsRel ψ 𝒟 A.toIdxSubMeas B.toIdxSubMeas δ

Heterogeneous projective converse of prop:simeq-to-approx.

For projective measurements acting on different tensor factors, a state-dependent-distance estimate at strength 2·δ for the placed families implies the corresponding bipartite consistency statement at strength δ.