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: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Defs/Normalization.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

Nothing here reads a state: every declaration is about local operators, and is stated over any C*-algebra 𝔓 with its order (the vendored Op ι). The vendored positive-semidefinite-matrix steps become the C*-algebra facts mul_star_self_nonneg, star_mul_self_nonneg and IsSelfAdjoint.of_nonneg, and sq_le_self is the keystone's (Co/Basic/QuantumState.lean). The private proj_conj_le (Q_b X Q_b ≤ Q_b for X ≤ 1) is the step the two vendored sum bounds repeat inline.

Not ported

Every declaration of the vendored file has a counterpart here.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

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

noncomputable def MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) (a : OutcomeA) (b : OutcomeB) : 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedOperator P Q a b = Q.outcome b * P.outcome a * Q.outcome b

theorem MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedOperator_sum_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) (a : OutcomeA) : ∑ b : OutcomeB, normalizationConditionSandwichedOperator P Q a b ≤ 1

The sandwiched operators sum to at most the identity.

noncomputable def MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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 MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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 MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) (a : OutcomeA) : 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalOperator P Q a = (MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalFamily P Q a).total

theorem MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalSum_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) {F : OutcomeA → 𝔓} (hF : ∀ (a : OutcomeA), F a ≤ normalizationConditionSandwichedTotalOperator P Q a) : ∑ a : OutcomeA, F a ≤ 1

Operators below the totals ∑_b C_{a,b} sum to at most the identity.

theorem MIPRE.LIDT.Co.Commutativity.normalizationConditionSandwichedTotalOperator_hermitian {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) (a : OutcomeA) : star (normalizationConditionSandwichedTotalOperator P Q a) = normalizationConditionSandwichedTotalOperator P Q a

The total ∑_b C_{a,b} is self-adjoint.

theorem MIPRE.LIDT.Co.Commutativity.normCondSandwichedTotal_sq_le {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) (a : OutcomeA) : normalizationConditionSandwichedTotalOperator P Q a * normalizationConditionSandwichedTotalOperator P Q a ≤ normalizationConditionSandwichedTotalOperator P Q a

The total ∑_b C_{a,b} dominates its square.

noncomputable def MIPRE.LIDT.Co.Commutativity.normalizationConditionSquareFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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 MIPRE.LIDT.Co.Commutativity.normalizationConditionAdjointSquareFamily {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {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 MIPRE.LIDT.Co.Commutativity.normalizationConditionSquareOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) : 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.normalizationConditionSquareOperator P Q = (MIPRE.LIDT.Co.Commutativity.normalizationConditionSquareFamily P Q).total

noncomputable def MIPRE.LIDT.Co.Commutativity.normalizationConditionAdjointSquareOperator {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (P : SubMeas OutcomeA 𝔓) (Q : ProjSubMeas OutcomeB 𝔓) : 𝔓

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

Equations

• MIPRE.LIDT.Co.Commutativity.normalizationConditionAdjointSquareOperator P Q = (MIPRE.LIDT.Co.Commutativity.normalizationConditionAdjointSquareFamily P Q).total

def MIPRE.LIDT.Co.Commutativity.normalizationConditionIdentityBound {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] {OutcomeA : Type u_2} {OutcomeB : Type u_3} [Fintype OutcomeA] [Fintype OutcomeB] (_P : SubMeas OutcomeA 𝔓) (_Q : ProjSubMeas OutcomeB 𝔓) : 𝔓

The identity bound appearing in lem:normalization-condition.

Equations

• MIPRE.LIDT.Co.Commutativity.normalizationConditionIdentityBound _P _Q = 1