Section 11 commutativity: normalization definitions

The normalization-condition sandwich C_{a,b} = Q_b P_a Q_b and the associated indexed submeasurement family used in lem:normalization-condition.

References

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

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) (a : OutcomeA) (b : OutcomeB) : Quantum.Op ι

The operator C_{a,b} = Q_b P_a Q_b from lem:normalization-condition.

We propagate explicit matrix from the input operators so that the sum ∑_b C_{a,b} accumulates correctly.

Equations

• MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedOperator P Q a b = Q.outcome b * P.outcome a * Q.outcome b

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : IdxSubMeas OutcomeA OutcomeB ι

The sandwiched family b ↦ Q_b P_a Q_b.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedTotalFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : IdxSubMeas OutcomeA Unit ι

The total family a ↦ ∑_b C_{a,b} from lem:normalization-condition.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedTotalOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) (a : OutcomeA) : Quantum.Op ι

The formal operator ∑_b C_{a,b} from lem:normalization-condition.

Equations

• MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedTotalOperator P Q a = (MIPStarRE.LDT.Commutativity.normalizationConditionSandwichedTotalFamily P Q a).total

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSquareFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : SubMeas OutcomeA ι

The family a ↦ (∑_b C_{a,b})(∑_b C_{a,b})^†.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionAdjointSquareFamily {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : SubMeas OutcomeA ι

The family a ↦ (∑_b C_{a,b})^†(∑_b C_{a,b}).

Equations

• One or more equations did not get rendered due to their size.

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionSquareOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : Quantum.Op ι

The operator ∑_a (∑_b C_{a,b})(∑_b C_{a,b})^†.

Equations

• MIPStarRE.LDT.Commutativity.normalizationConditionSquareOperator P Q = (MIPStarRE.LDT.Commutativity.normalizationConditionSquareFamily P Q).total

noncomputable def MIPStarRE.LDT.Commutativity.normalizationConditionAdjointSquareOperator {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA ι) (Q : ProjSubMeas OutcomeB ι) : Quantum.Op ι

The operator ∑_a (∑_b C_{a,b})^†(∑_b C_{a,b}).

Equations

• MIPStarRE.LDT.Commutativity.normalizationConditionAdjointSquareOperator P Q = (MIPStarRE.LDT.Commutativity.normalizationConditionAdjointSquareFamily P Q).total

def MIPStarRE.LDT.Commutativity.normalizationConditionIdentityBound {ι : Type u_1} [Fintype ι] [DecidableEq ι] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (_P : SubMeas OutcomeA ι) (_Q : ProjSubMeas OutcomeB ι) : Quantum.Op ι

The identity bound appearing in lem:normalization-condition.

Equations

• MIPStarRE.LDT.Commutativity.normalizationConditionIdentityBound _P _Q = 1