Switch-sandwich main: middle-to-right transfer

The middle-to-right transfer estimate used in prop:switch-sandwich: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichMain/RightTransfer.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 ᴴ becomes star. The vendored normalization hypothesis hψ : ψ.IsNormalized is dropped: it is a theorem of the model (ev_one_of_isNormalized).

The proof is the vendored one, shortened. For each question, the gap is ev(LB (LT - RT)), where LB, LT, RT are the placements of B and of the total projector; Cauchy–Schwarz (ev_abs_mul_le_sqrt) and LB² ≤ 1 bound it by √ev((LT - RT)²), and ev((LT - RT)²) ≤ qSDD (A ⊗ 1) (1 ⊗ A) because both expand, for commuting projections, as ev L + ev R - 2 ev(L R) and the cross terms ev(Aₐ ⊗ A_b) are nonnegative. The Kronecker identities of the vendored proof become S.leftTensor_mul_leftTensor, S.rightTensor_mul_rightTensor and S.L_comm_R. The question average is avgOver_abs_le_sqrt_of_pointwise.

New here

• ev_star_L_sub_R_mul_self: for self-adjoint X, Y, the expansion ev((L X - R Y)^* (L X - R Y)) = ev L(X²) + ev R(Y²) - 2 ev(L X R Y), which the vendored proofs of switchSandwich_rightTransfer and wrongSideEstimate (SelfConsistency/DataProcessing) and of qBipartiteSSCDefect bounds (BipartiteSelfConsistency/Core) each repeat inline.

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.ev_star_L_sub_R_mul_self {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (S : SymModel 𝔓 K) {X Y : 𝔓} (hX : IsSelfAdjoint X) (hY : IsSelfAdjoint Y) : S.ev (star (S.L X - S.R Y) * (S.L X - S.R Y)) = S.ev (S.L (X * X)) + S.ev (S.R (Y * Y)) - 2 * S.ev (S.L X * S.R Y)

For self-adjoint local operators X, Y, ev((L X - R Y)^* (L X - R Y)) = ev L(X²) + ev R(Y²) - 2 ev(L X R Y): the difference is self-adjoint, and the two cross terms agree because the placements commute.

theorem MIPRE.LIDT.Co.Preliminaries.switchSandwich_rightTransfer {𝔓 : 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 δ → |middleSandwichExpectation S 𝒟 A B - rightSandwichExpectation S 𝒟 A B| ≤ √δ

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