Measurement lift infrastructure for the low individual degree test #
Measurement-level tensor-factor lifts built from the submeasurement placement API.
def
MIPStarRE.LDT.leftLiftedMeasurement
{α : Type u_1}
{ιA : Type u_2}
{ιB : Type u_3}
[Fintype α]
[Fintype ιA]
[DecidableEq ιA]
[Fintype ιB]
[DecidableEq ιB]
(A : Measurement α ιA)
:
Measurement α (ιA × ιB)
Lift a measurement to the left tensor factor of ιA × ιB.
Equations
- MIPStarRE.LDT.leftLiftedMeasurement A = { toSubMeas := MIPStarRE.LDT.leftPlacedSubMeas A.toSubMeas, total_eq_one := ⋯ }
Instances For
def
MIPStarRE.LDT.rightLiftedMeasurement
{α : Type u_1}
{ιA : Type u_2}
{ιB : Type u_3}
[Fintype α]
[Fintype ιA]
[DecidableEq ιA]
[Fintype ιB]
[DecidableEq ιB]
(A : Measurement α ιB)
:
Measurement α (ιA × ιB)
Lift a measurement to the right tensor factor of ιA × ιB.
Equations
- MIPStarRE.LDT.rightLiftedMeasurement A = { toSubMeas := MIPStarRE.LDT.rightPlacedSubMeas A.toSubMeas, total_eq_one := ⋯ }