Switch-sandwich main: left-to-middle transfer

The left-to-middle transfer estimate used in prop:switch-sandwich, bounding the gap between the left and middle expressions via the Cauchy–Schwarz-based gap bounds: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichMain/LeftTransfer.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The state ψ : QuantumState (ι × ι) becomes a symmetric model S : SymModel 𝔓 K and the placements leftTensor, rightTensor become S.L, S.R. The vendored normalization hypothesis hψ : ψ.IsNormalized is dropped: it is a theorem of the model (ev_one_of_isNormalized), and the gap bounds question_switchSandwich_left_gap and question_switchSandwich_middle_gap no longer take it. The proof is the vendored one: both gaps through the intermediate term E_x ∑ₐ ev(Aₐ B ⊗ Aₐ), each averaged by avgOver_abs_le_sqrt_of_pointwise, and the triangle inequality.

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.switchSandwich_leftTransfer {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (S : SymModel 𝔓 K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxProjSubMeas Question Outcome 𝔓) (B : 𝔓) (hB : OpBounded01 B) (δ : ℝ) : BipartiteSDDRel S 𝒟 A.toIdxSubMeas A.toIdxSubMeas δ → |leftSandwichExpectation S 𝒟 A B - middleSandwichExpectation S 𝒟 A B| ≤ 2 * √δ

Left-to-middle transfer estimate used in the switch-sandwich theorem: |E_x ∑ₐ ev(Aₐ B Aₐ ⊗ I) - E_x ∑ₐ ev(B ⊗ Aₐ)| ≤ 2√δ when A ⊗ I ≈_δ I ⊗ A.