Self-consistency: strategy-level extensions

Good-strategy characterization lemmas (lem:good-strategy-characterization) bundling the axis-parallel, self-consistency, and diagonal branches.

References

• references/ldt-paper/preliminaries.tex
• blueprint/src/chapter/ch03_preliminaries.tex

theorem MIPStarRE.LDT.Preliminaries.goodStrategyCharacterization {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (strategy : SymStrat params ι) (eps delta gamma : Error) : strategy.IsGood eps delta gamma ↔ ConsRel strategy.state (uniformDistribution (AxisParallelTestSample params)) (axisParallelPointAnswerFamily strategy) (axisParallelLineAnswerFamily strategy) eps ∧ ConsRel strategy.state (uniformDistribution (Point params)) strategy.pointMeasurement.toIdxSubMeas strategy.pointMeasurement.toIdxSubMeas delta ∧ strategy.diagonalFailureProbability ≤ gamma

lem:good-strategy-characterization.

The axis-parallel branch is already definitionally a consistency bound. The self-consistency branch is the same consistency bound specialized to the point measurement, since that family is complete. The diagonal branch remains bundled as strategy.diagonalFailureProbability because its sampled question type depends on the restriction index j.

theorem MIPStarRE.LDT.Preliminaries.twoNotionsOfSelfConsistencyAfterEvaluation {Question : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype α] [Fintype β] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (𝒟 : Distribution Question) (A : IdxSubMeas Question α ι) (δ : Error) (f : Question → α → β) : BipartiteSSCRel ψ 𝒟 A δ → SDDRel ψ 𝒟 (IdxSubMeas.liftLeft fun (q : Question) => postprocess (A q) (f q)) (IdxSubMeas.liftRight fun (q : Question) => postprocess (A q) (f q)) (2 * δ)

prop:two-notions-of-self-consistency-after-evaluation.

Proof:

1. Question-dependent postprocessing preserves the total mass and can only increase the diagonal overlap term ∑_b ⟨ψ|A_[f_q(a)=b] ⊗ A_[f_q(a)=b]|ψ⟩.
2. Hence bipartite SSC transfers from A to the postprocessed family.
3. Apply twoNotionsOfSelfConsistency to the postprocessed family.

theorem MIPStarRE.LDT.Preliminaries.completenessTransferSelfConsistentA {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState (ι × ι)) (hperm : PermInvState ψ) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxSubMeas Question Outcome ι) (δ ε : Error) : BipartiteSSCRel ψ 𝒟 A δ → SDDRel ψ 𝒟 A.liftLeft B.liftLeft ε → idxSubMeasMass ψ 𝒟 B.liftLeft ≥ idxSubMeasMass ψ 𝒟 A.liftLeft - δ - 2 * √ε

prop:completeness-transfer-self-consistent-A.

Proof:

1. Lower-bound ⟨ψ|B ⊗ I|ψ⟩ by the mixed overlap ∑ₐ ⟨ψ|B_a ⊗ A_a|ψ⟩ using A_a ≤ I.
2. Compare ∑ₐ ⟨ψ|B_a ⊗ A_a|ψ⟩ with ∑ₐ ⟨ψ|A_a ⊗ A_a|ψ⟩ by a Cauchy-Schwarz overlap estimate from the hypothesis A ⊗ I ≈_ε B ⊗ I.
3. Use bipartite SSC to replace the latter by ⟨ψ|A ⊗ I|ψ⟩ - δ.
4. Relax the resulting bound to the requested δ + 2√ε form.