Section 10 commutativity points: lift comparisons

Comparison lemmas lifting the ordered shared-line point product to the mixed line family, used in the lift direction of the Section 10 point-commutativity argument.

References

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

theorem MIPStarRE.LDT.CommutativityPoints.orderedLiftToMixedLine {ι : 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) (pointMeasurementProductAlongSharedLine params strategy) (pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily (pointDiagonalLineApproxError params gamma)

Lift the ordered shared-line point product to the mixed line family.

theorem MIPStarRE.LDT.CommutativityPoints.orderedLiftToLineProduct {ι : 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) (pointDiagonalLineMixedProductLeft params strategy).toIdxOpFamily (diagonalLineProductOrdered params strategy) (pointDiagonalLineApproxError params gamma)

Lift the mixed line family to the ordered shared-line line product.