Documentation

MIPRE.Background.LIDT.Co.Commutativity.ScalarApproximation.PaperChainBasic.Normalization

Section 11 commutativity: normalization helpers for the evaluated-slice paper chain #

The normalization estimates ∑ C C^* ≤ 1 and ∑ C^* C ≤ 1 used as side conditions of closenessOfIP and its adjoint form in the scalar approximation chain: the counterpart of Commutativity/ScalarApproximation/PaperChainBasic/Normalization.lean under MIPRE/Background/LIDT/MIPStarRE/LDT/ in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The vendored leftTensor (ι₂ := ι) and rightTensor (ι₁ := ι) are the placements S.L and S.R of a symmetric model, so each normalization lemma takes S : SymModel 𝔓 K as an explicit first argument, as M3's placement lemmas do (planning/c6b-plan.md, "Departures in M3 and M5"). projSubMeas_total_mul_outcome_eq_outcome does not mention the state and holds in any C*-algebra with its order.

The vendored proofs expand (∑_b L(X_b) R(P_b)) (∑_b L(X_b) R(P_b))^* twice, in a calc of Kronecker identities each time, and bound every summand separately. Here the expansion is one private lemma for each order of the product (the cross terms vanish because the outcomes of the projective measurement P are orthogonal), and a third private lemma reduces ∑_a ∑_b L(Y_{a,b}) R(P_b) ≤ 1 to the local bounds ∑_a Y_{a,b} ≤ 1, which are proved in 𝔓 from three private inequalities of a C*-algebra: c Y c ≤ c c for self-adjoint c and Y ≤ 1, X X ≤ 1 for 0 ≤ X ≤ 1, and ∑_a A_a A_a ≤ 1 for a submeasurement A.

Not ported #

Every declaration of the vendored file has a counterpart here.

References #

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

source
theorem MIPRE.LIDT.Co.Commutativity.projSubMeas_total_mul_outcome_eq_outcome {R : Type u_1} [CStarAlgebra R] [PartialOrder R] [StarOrderedRing R] {α : Type u_2} [Fintype α] (A : ProjSubMeas α R) (a : α) :
A.total * A.outcome a = A.outcome a

The total projector of a projective submeasurement absorbs each outcome on the left.

source
theorem MIPRE.LIDT.Co.Commutativity.leftRightTensor_prefix_pointMeasurement_normalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) (R : ProjMeas β 𝔓) :
∑ a : α, (∑ b : β, S.L (A.outcome a * B.outcome b) * S.R (R.outcome b)) * star (∑ b : β, S.L (A.outcome a * B.outcome b) * S.R (R.outcome b)) ≤ 1

Normalization side condition for the paper line-86 insertion.

For fixed evaluated-slice question q, this bounds the closenessOfIP family C_{a,b} = (A_a B_b) \otimes P_b, where P is a projective point measurement.

source
theorem MIPRE.LIDT.Co.Commutativity.leftRightTensor_prefix_pointMeasurement_adjoint_normalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) (R : ProjMeas β 𝔓) :
∑ a : α, star (∑ b : β, S.L (A.outcome a * B.outcome b) * S.R (R.outcome b)) * ∑ b : β, S.L (A.outcome a * B.outcome b) * S.R (R.outcome b) ≤ 1

Adjoint-side normalization for C_{a,b} = (A_a B_b) \otimes R_b.

This is the side condition needed by closenessOfIPAdjoint for the first reverse eq:add-an-a move after paper eq:gcom10.

source
theorem MIPRE.LIDT.Co.Commutativity.leftTensor_pair_prefix_normalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) :
∑ b : β, (∑ a : α, S.L (A.outcome a * B.outcome b)) * star (∑ a : α, S.L (A.outcome a * B.outcome b)) ≤ 1

Normalization for C_{b,a}=A_a B_b placed on the left tensor factor.

source
theorem MIPRE.LIDT.Co.Commutativity.leftTensor_pair_prefix_adjoint_normalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) :
∑ b : β, star (∑ a : α, S.L (A.outcome a * B.outcome b)) * ∑ a : α, S.L (A.outcome a * B.outcome b) ≤ 1

Adjoint-side version of leftTensor_pair_prefix_normalization.

source
theorem MIPRE.LIDT.Co.Commutativity.leftTensor_prefix_total_normalization {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) (T : 𝔓) (hT_nonneg : 0 ≤ T) (hT_le_one : T ≤ 1) :
∑ ab : α × β, S.L (A.outcome ab.1 * B.outcome ab.2 * T) * star (S.L (A.outcome ab.1 * B.outcome ab.2 * T)) ≤ 1

Normalization side condition for the paper line-87 right-register point swap.

For fixed evaluated-slice question q, the swap uses the family C_{a,b} = (G^{u,x}_a G^{v,y}_b G^x) \otimes I, represented here as a left tensor. The estimate only needs that the two evaluated-slice factors are submeasurements and that the inserted total T is a positive contraction.