Raw operator families for the low individual degree test

This file introduces the notion of an indexed family of operators used in the paper without positivity or boundedness requirements. These are used for ≈_δ chains whose intermediate objects are arbitrary matrix families rather than honest submeasurements.

References

• references/ldt-paper/self_improvement.tex
• references/ldt-paper/commutativity-points.tex
• references/ldt-paper/commutativity-G.tex
• references/ldt-paper/ld-pasting.tex
• blueprint/src/chapter/ch07_self_improvement.tex
• blueprint/src/chapter/ch08_commutativity.tex
• blueprint/src/chapter/ch09_pasting.tex

structure MIPStarRE.LDT.OpFamily (α : Type u_1) (ι : Type u_2) [Fintype ι] [DecidableEq ι] : Type (max u_1 u_2)

A raw operator family: outcome operators indexed by α, without PSD or bound requirements. This matches the paper's use of arbitrary matrix families in ≈_δ chains.

• outcome : α → Quantum.Op ι
• total : Quantum.Op ι

def MIPStarRE.LDT.IdxOpFamily (Question : Type u_1) (Outcome : Type u_2) (ι : Type u_3) [Fintype ι] [DecidableEq ι] : Type (max (max u_1 u_3) u_2)

Indexed raw operator family (question → outcome → operator).

Equations

• MIPStarRE.LDT.IdxOpFamily Question Outcome ι = (Question → MIPStarRE.LDT.OpFamily Outcome ι)

def MIPStarRE.LDT.SubMeas.toOpFamily {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] (A : SubMeas α ι) : OpFamily α ι

Forget the PSD and boundedness structure of a submeasurement.

Equations

• A.toOpFamily = { outcome := A.outcome, total := A.total }

@[instance_reducible]

instance MIPStarRE.LDT.instCoeSubMeasOpFamily {α : Type u_1} {ι : Type u_2} [Fintype α] [Fintype ι] [DecidableEq ι] : Coe (SubMeas α ι) (OpFamily α ι)

Equations

• MIPStarRE.LDT.instCoeSubMeasOpFamily = { coe := MIPStarRE.LDT.SubMeas.toOpFamily }

def MIPStarRE.LDT.IdxSubMeas.toIdxOpFamily {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype Outcome] [Fintype ι] [DecidableEq ι] (A : IdxSubMeas Question Outcome ι) : IdxOpFamily Question Outcome ι

Forget the PSD and boundedness structure of an indexed submeasurement family.

Equations

• A.toIdxOpFamily q = (A q).toOpFamily

def MIPStarRE.LDT.OpFamily.leftPlacedOpFamily {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : OpFamily α ιA) : OpFamily α (ιA × ιB)

Place a raw operator family on the left tensor factor of ιA × ιB.

Equations

• A.leftPlacedOpFamily = { outcome := fun (a : α) => MIPStarRE.LDT.leftTensor (A.outcome a), total := MIPStarRE.LDT.leftTensor A.total }

def MIPStarRE.LDT.OpFamily.rightPlacedOpFamily {α : Type u_1} {ιA : Type u_2} {ιB : Type u_3} [Fintype ιA] [DecidableEq ιA] [Fintype ιB] [DecidableEq ιB] (A : OpFamily α ιB) : OpFamily α (ιA × ιB)

Place a raw operator family on the right tensor factor of ιA × ιB.

Equations

• A.rightPlacedOpFamily = { outcome := fun (a : α) => MIPStarRE.LDT.rightTensor (A.outcome a), total := MIPStarRE.LDT.rightTensor A.total }

noncomputable def MIPStarRE.LDT.OpFamily.postprocess {α : Type u_1} {β : Type u_2} {ι : Type u_3} [Fintype α] [Fintype β] [Fintype ι] [DecidableEq ι] (A : OpFamily α ι) (f : α → β) : OpFamily β ι

Post-process the outcomes of a raw operator family.

Equations

• A.postprocess f = { outcome := fun (b : β) => ∑ a : α with f a = b, A.outcome a, total := A.total }

def MIPStarRE.LDT.IdxOpFamily.liftLeft {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] (A : IdxOpFamily Question Outcome ι) : IdxOpFamily Question Outcome (ι × ι)

Lift an indexed raw operator family to the left tensor factor.

Equations

• A.liftLeft q = (A q).leftPlacedOpFamily