Switch-sandwich gap bounds: left gap

The left gap estimate question_switchSandwich_left_gap, bounding the question-level left gap of the switch-sandwich argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichGapBounds/Left.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The state ψ : QuantumState (ι × ι) becomes a symmetric model S : SymModel 𝔓 K, the placements leftTensor, rightTensor become S.L, S.R, and the lifts A.toSubMeas.liftLeft, A.toSubMeas.liftRight take the model, A.toSubMeas.liftLeft S. The vendored normalization hypothesis hψ : ψ.IsNormalized is dropped: it is a theorem of the model (ev_one_of_isNormalized), used through subMeas_diagMass_le_one. The proof is the vendored one, the self-adjointness of the placed outcomes coming from IsSelfAdjoint.of_nonneg in place of positive semidefiniteness of matrices.

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/preliminaries.tex, prop:switch-sandwich

theorem MIPRE.LIDT.Co.Preliminaries.question_switchSandwich_left_gap {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_3} [Fintype Outcome] (S : SymModel 𝔓 K) (A : ProjSubMeas Outcome 𝔓) (B : 𝔓) (hB : OpBounded01 B) : |∑ a : Outcome, S.ev (S.L (A.outcome a) * S.L B * S.L (A.outcome a)) - ∑ a : Outcome, S.ev (S.L (A.outcome a) * S.L B * S.R (A.outcome a))| ≤ √(S.qSDD (SubMeas.liftLeft S A.toSubMeas) (SubMeas.liftRight S A.toSubMeas))

The question-level left gap of the switch sandwich: |∑ₐ ev(Aₐ B Aₐ ⊗ 1) - ∑ₐ ev(Aₐ B ⊗ Aₐ)| ≤ √(qSDD (A ⊗ 1) (1 ⊗ A)) for a projective sub-measurement A and 0 ≤ B ≤ 1.