Projective consistency evaluation

This module contains the data-processing lemmas which turn polynomial-level projective consistency into pointwise consistency after evaluation at a sampled point.

theorem MIPStarRE.LDT.Test.consRel_constPolynomialEvaluation {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] (ψ : QuantumState (ι × ι)) (A B : Measurement (Polynomial params) ι) {δ : Error} (h : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily B.toSubMeas) δ) : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params A.toSubMeas) (polynomialEvaluationFamily params B.toSubMeas) δ

A constant full-polynomial consistency statement postprocesses to pointwise polynomial evaluation with the same error.

This is the data-processing move used after paper line 156: once Q^A_g \otimes I \simeq I \otimes Q^B_g is available over the single polynomial question, evaluating both polynomial outcomes at a point u preserves consistency over the uniform point distribution.

theorem MIPStarRE.LDT.Test.consRel_constPolynomialEvaluation_heterogeneous {params : Parameters} [FieldModel params.q] {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (ψ : QuantumState (ιA × ιB)) (A : Measurement (Polynomial params) ιA) (B : Measurement (Polynomial params) ιB) {δ : Error} (h : ConsRel ψ (uniformDistribution Unit) (constSubMeasFamily A.toSubMeas) (constSubMeasFamily B.toSubMeas) δ) : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params A.toSubMeas) (polynomialEvaluationFamily params B.toSubMeas) δ

Heterogeneous form of consRel_constPolynomialEvaluation.

The same data-processing argument applies when Alice's polynomial measurement acts on H_A and Bob's on H_B.

theorem MIPStarRE.LDT.Test.projectiveEvaluationConsistency_ofFullPolynomialConsistency {params : Parameters} [FieldModel params.q] {ι : Type u_1} [Fintype ι] [DecidableEq ι] {ψ : QuantumState (ι × ι)} (Q_A Q_B : ProjMeas (Polynomial params) ι) {ζ₃ : Error} (hline : Preliminaries.BipartiteSDDRel ψ (uniformDistribution Unit) (constSubMeasFamily Q_A.toSubMeas) (constSubMeasFamily Q_B.toSubMeas) ζ₃) : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params Q_A.toSubMeas) (polynomialEvaluationFamily params Q_B.toSubMeas) (ζ₃ / 2)

Turn a line-156 projective approximation into the evaluated consistency used in the final point-consistency triangles.

The proof first applies the projective converse of prop:simeq-to-approx at the polynomial level, then uses question-dependent data processing to evaluate both projective polynomial measurements at each point.

theorem MIPStarRE.LDT.Test.projectiveEvaluationConsistency_ofFullPolynomialConsistency_heterogeneous {params : Parameters} [FieldModel params.q] {ιA : Type u_1} {ιB : Type u_2} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] {ψ : QuantumState (ιA × ιB)} (Q_A : ProjMeas (Polynomial params) ιA) (Q_B : ProjMeas (Polynomial params) ιB) {ζ₃ : Error} (hline : SDDRel ψ (uniformDistribution Unit) (constSubMeasFamily (leftPlacedSubMeas Q_A.toSubMeas)) (constSubMeasFamily (rightPlacedSubMeas Q_B.toSubMeas)) ζ₃) : ConsRel ψ (uniformDistribution (Point params)) (polynomialEvaluationFamily params Q_A.toSubMeas) (polynomialEvaluationFamily params Q_B.toSubMeas) (ζ₃ / 2)

Heterogeneous form of projectiveEvaluationConsistency_ofFullPolynomialConsistency.

It first applies the two-space projective converse to the placed state-dependent-distance relation, and then evaluates the polynomial outcomes at the sampled point.