Section 10 commutativity points: shared-line helpers

Compatibility lemmas between sampled point pairs and shared-diagonal line questions, used by both the lift and drop comparisons.

References

• references/ldt-paper/commutativity-points.tex
• blueprint/src/chapter/ch08_commutativity.tex

theorem MIPStarRE.LDT.CommutativityPoints.avgOver_pointPairSharedDiagonalLine_ignore_first (params : Parameters) [FieldModel params.q] (f : PointDiagonalLineQuestion params → Error) : (avgOver (pointPairSharedDiagonalLineDistribution params) fun (q : PointPairDiagonalLineQuestion params) => f (q.1, q.2.2)) = avgOver (pointWithDiagonalLineDistribution params) f

theorem MIPStarRE.LDT.CommutativityPoints.avgOver_pointPairSharedDiagonalLine_ignore_second (params : Parameters) [FieldModel params.q] (f : PointDiagonalLineQuestion params → Error) : (avgOver (pointPairSharedDiagonalLineDistribution params) fun (q : PointPairDiagonalLineQuestion params) => f (q.1, q.2.1)) = avgOver (pointWithDiagonalLineDistribution params) f

theorem MIPStarRE.LDT.CommutativityPoints.avgOver_pointPairSharedDiagonalLine_sampled_pair (params : Parameters) [FieldModel params.q] (f : GlobalVariance.PointPairQuestion params → Error) : (avgOver (pointPairSharedDiagonalLineDistribution params) fun (q : PointPairDiagonalLineQuestion params) => f (sampledPointPairFromSharedDiagonalQuestion params q)) = avgOver (uniformDistribution (GlobalVariance.PointPairQuestion params)) f

theorem MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductAlongSharedLine_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : (pointMeasurementProductAlongSharedLine params strategy q).outcome (a, b) = leftTensor ((strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a * (strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b)

theorem MIPStarRE.LDT.CommutativityPoints.pointMeasurementProductAlongSharedLineReversed_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : (pointMeasurementProductAlongSharedLineReversed params strategy q).outcome (a, b) = leftTensor ((strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b * (strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a)

theorem MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineMixedProductLeft_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : ((pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily q).outcome (a, b) = opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.1)).outcome a) ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b)

theorem MIPStarRE.LDT.CommutativityPoints.pointDiagonalLineMixedProductRight_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : ((pointDiagonalLineMixedProductRight params strategy).toIdxOpFamily q).outcome (a, b) = opTensor ((strategy.pointMeasurement (q.1.pointAt q.2.2)).outcome b) ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a)

theorem MIPStarRE.LDT.CommutativityPoints.diagonalLineProductOrdered_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : (diagonalLineProductOrdered params strategy q).outcome (a, b) = rightTensor ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b * (sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a)

theorem MIPStarRE.LDT.CommutativityPoints.diagonalLineProductReversed_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (q : PointPairDiagonalLineQuestion params) (a b : Fq params) : (diagonalLineProductReversed params strategy q).outcome (a, b) = rightTensor ((sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).outcome a * (sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).outcome b)

theorem MIPStarRE.LDT.CommutativityPoints.sampledDiagonalLineApproximation_ignore_first {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : SDDOpRel strategy.state (pointPairSharedDiagonalLineDistribution params) (fun (q : PointPairDiagonalLineQuestion params) => (strategy.pointMeasurement (q.1.pointAt q.2.2)).toOpFamily.leftPlacedOpFamily) (fun (q : PointPairDiagonalLineQuestion params) => (sampledDiagonalLineEvaluation params strategy (q.1, q.2.2)).toOpFamily.rightPlacedOpFamily) (pointDiagonalLineApproxError params gamma)

theorem MIPStarRE.LDT.CommutativityPoints.sampledDiagonalLineApproximation_ignore_second {ι : Type u_1} [Fintype ι] [DecidableEq ι] (params : Parameters) [FieldModel params.q] (strategy : SymStrat params ι) (eps delta gamma : Error) (hgood : strategy.IsGood eps delta gamma) : SDDOpRel strategy.state (pointPairSharedDiagonalLineDistribution params) (fun (q : PointPairDiagonalLineQuestion params) => (strategy.pointMeasurement (q.1.pointAt q.2.1)).toOpFamily.leftPlacedOpFamily) (fun (q : PointPairDiagonalLineQuestion params) => (sampledDiagonalLineEvaluation params strategy (q.1, q.2.1)).toOpFamily.rightPlacedOpFamily) (pointDiagonalLineApproxError params gamma)