Documentation

MIPRE.Background.LIDT.Co.Commutativity.Transport.FullSlice.ZeroBounds

Zero-family bounds on the full-slice product #

Pointwise qSDDOp bounds and averaged SDDOpRel bounds for the ordered fullSliceProductLeft and reversed fullSliceProductRight factors against the zero family, each at most 1: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/Transport/FullSlice/ZeroBounds.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

The vendored proofs repeat, once per factor order, a Kronecker computation of ∑ (B_b A_a ⊗ I)^* (B_b A_a ⊗ I) as the placed total of the sandwich A_a B_b A_a. Here it is proved once in the local algebra and placed by S.L, as sum_ev_adjoint_self_leftTensor_mul_le_one below, which the evaluated-slice bounds of Co/Commutativity/Main/Auxiliary/HEvalTransport.lean use as well. The vendored hypothesis hnorm : strategy.state.IsNormalized is dropped: it is a theorem of the model (VecState.ev_one_of_isNormalized).

New here #

sum_ev_adjoint_self_leftTensor_mul_le_one: for submeasurements A, B of 𝔓 with B projective, ∑_{a,b} ev((B_b A_a ⊗ I)^* (B_b A_a ⊗ I)) ≤ 1.

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.sum_ev_adjoint_self_leftTensor_mul_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} {β : Type u_4} [Fintype α] [Fintype β] (S : SymModel 𝔓 K) (A : SubMeas α 𝔓) (B : SubMeas β 𝔓) (hB : ∀ (b : β), B.outcome b * B.outcome b = B.outcome b) :
∑ a : α, ∑ b : β, S.ev (star (S.L (B.outcome b * A.outcome a)) * S.L (B.outcome b * A.outcome a)) ≤ 1

For submeasurements A, B of the local algebra with B projective, the placed products B_b A_a ⊗ I have total squared norm on the state at most 1: the sum ∑_{a,b} (B_b A_a)^* (B_b A_a) is the total ∑_a A_a (∑_b B_b) A_a of the sandwich sandwichByOuterSubMeas A B, which is at most 1.

source
theorem MIPRE.LIDT.Co.Commutativity.fullSliceProductLeft_qSDDOp_zero_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) :
strategy.state.qSDDOp (fullSliceProductLeft params strategy family q) (zeroFullSliceOpFamily params) ≤ 1

Questionwise, the ordered full-slice product has squared distance at most 1 from the zero family.

source
theorem MIPRE.LIDT.Co.Commutativity.zero_qSDDOp_fullSliceProductRight_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) (q : MIPStarRE.LDT.Commutativity.FullSliceQuestion params) :
strategy.state.qSDDOp (zeroFullSliceOpFamily params) (fullSliceProductRight params strategy family q) ≤ 1

Questionwise, the reversed full-slice product has squared distance at most 1 from the zero family.

source
theorem MIPRE.LIDT.Co.Commutativity.fullSliceProductLeft_to_zero_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) :
strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductLeft params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) (fun (x : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => zeroFullSliceOpFamily params) 1

Averaging the ordered full-slice product against zero costs at most 1.

source
theorem MIPRE.LIDT.Co.Commutativity.zero_to_fullSliceProductRight_le_one {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (params : MIPStarRE.LDT.Parameters) [MIPStarRE.LDT.FieldModel params.q] (strategy : SymStrat params.next 𝔓 K) (family : IdxPolyFamily params 𝔓) :
strategy.state.SDDOpRel (MIPStarRE.LDT.uniformDistribution (MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params)) (fun (x : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => zeroFullSliceOpFamily params) (fun (q : MIPStarRE.LDT.Commutativity.EvaluatedSliceQuestion params) => fullSliceProductRight params strategy family (MIPStarRE.LDT.Commutativity.fullSliceQuestionOfEvaluatedSlice params q)) 1

Averaging zero against the reversed full-slice product costs at most 1.