Tensor normalization helpers for the evaluated-slice paper chain

This file contains the normalization estimates used as side conditions for closenessOfIP and its adjoint form in the scalar approximation chain.

theorem MIPStarRE.LDT.Commutativity.leftRightTensor_prefix_pointMeasurement_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (R : ProjMeas β ι) : ∑ a : α, (∑ b : β, leftTensor (A.outcome a * B.outcome b) * rightTensor (R.outcome b)) * (∑ b : β, leftTensor (A.outcome a * B.outcome b) * rightTensor (R.outcome b)).conjTranspose ≤ 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.

theorem MIPStarRE.LDT.Commutativity.leftRightTensor_prefix_pointMeasurement_adjoint_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (R : ProjMeas β ι) : ∑ a : α, (∑ b : β, leftTensor (A.outcome a * B.outcome b) * rightTensor (R.outcome b)).conjTranspose * ∑ b : β, leftTensor (A.outcome a * B.outcome b) * rightTensor (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.

theorem MIPStarRE.LDT.Commutativity.leftTensor_pair_prefix_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : ∑ b : β, (∑ a : α, leftTensor (A.outcome a * B.outcome b)) * (∑ a : α, leftTensor (A.outcome a * B.outcome b)).conjTranspose ≤ 1

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

theorem MIPStarRE.LDT.Commutativity.leftTensor_pair_prefix_adjoint_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) : ∑ b : β, (∑ a : α, leftTensor (A.outcome a * B.outcome b)).conjTranspose * ∑ a : α, leftTensor (A.outcome a * B.outcome b) ≤ 1

Adjoint-side version of leftTensor_pair_prefix_normalization.

theorem MIPStarRE.LDT.Commutativity.projSubMeas_total_mul_outcome_eq_outcome {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} [Fintype α] (A : ProjSubMeas α ι) (a : α) : A.total * A.outcome a = A.outcome a

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

theorem MIPStarRE.LDT.Commutativity.leftTensor_prefix_total_normalization {ι : Type u_1} [Fintype ι] [DecidableEq ι] {α : Type u_2} {β : Type u_3} [Fintype α] [Fintype β] (A : SubMeas α ι) (B : SubMeas β ι) (T : Quantum.Op ι) (hT_nonneg : 0 ≤ T) (hT_le_one : T ≤ 1) : ∑ ab : α × β, leftTensor (A.outcome ab.1 * B.outcome ab.2 * T) * Matrix.conjTranspose (leftTensor (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.