Documentation

MIPRE.Background.LIDT.Co.Commutativity.ScalarApproximation.Core

Section 11 commutativity: scalar approximation core #

Upstream scalar-approximation lemmas that do not depend on the later averaged commutation proof, so they can be shared by both ProcessedG and Pointwise without creating import cycles: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Commutativity/ScalarApproximation/Core.lean in the port of planning/c6b-plan.md (milestone M7, section "Port conventions").

qBipartiteSSCDefect_eq_half_qSDD_of_proj takes the symmetric model S as an explicit first argument in place of the vendored state ψ, and drops the vendored hypothesis hperm : PermInvState ψ: its one swap use is in Preliminaries.ev_adjoint_self_leftTensor_sub_rightTensor, which applies S.ev_L_eq_ev_R. For that lemma this file imports Co/Preliminaries/BipartiteSelfConsistency/Core.lean besides the counterpart of the vendored import, rather than repeat its expansion inline. The vendored proof shows the gap ev L(P) − ∑_a ev(P_a ⊗ P_a) nonnegative through the Kronecker inequality P_a ⊗ P_a ≤ P_a ⊗ I; here the gap is half of qSDD, a sum of expectations ev(X^* X), so it is nonnegative without that inequality.

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.qBipartiteSSCDefect_eq_half_qSDD_of_proj {𝔓 : Type u_1} [CStarAlgebra 𝔓] [PartialOrder 𝔓] [StarOrderedRing 𝔓] {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {α : Type u_3} [Fintype α] (S : SymModel 𝔓 K) (P : ProjSubMeas α 𝔓) :
S.qBipartiteSSCDefect P.toSubMeas = 1 / 2 * S.qSDD (SubMeas.liftLeft S P.toSubMeas) (SubMeas.liftRight S P.toSubMeas)

For a projective submeasurement on a symmetric model, the bipartite SSC defect is exactly half of the left/right SDD defect. The vendored lemma asks for a permutation-invariant state.