Switch-sandwich main: completeness estimate

prop:switch-sandwich assembled from the left and right transfer steps, and prop:completeness-transfer-projective-P: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichMain/Completeness.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

switchSandwich takes a symmetric model S : SymModel 𝔓 K in place of the state ψ : QuantumState (ι × ι). The completeness transfer is about a state on a single space (ψ : QuantumState ι), so completenessTransfer_core and completenessTransferProjectiveP take a vector state V : VecState K (a symmetric model is accepted through its coercion) and families of joint operators in K →L[ℂ] K, as CompTransferStmt does in Co/Preliminaries/Defs.lean. All three drop the vendored normalization hypothesis hψ : ψ.IsNormalized, a theorem of the vector state (ev_one_of_isNormalized); the subprobability hypothesis h𝒟 stays.

The proofs are the vendored ones. Per question, the mass gap of A against the projective P is at most the diagonal gap ∑ₐ ev(Pₐ²) - ∑ₐ ev(Aₐ²) (projSubMeas_diagMass_eq_mass, subMeas_diagMass_le_mass), which the two overlap gaps (question_overlap_gap_left, question_overlap_gap_right) bound by 2 √(qSDD A P); the average of the square roots is at most the square root of the average (avgOver_abs_le_sqrt_of_pointwise).

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, prop:completeness-transfer-projective-P

theorem MIPRE.LIDT.Co.Preliminaries.switchSandwich {𝔓 : 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 δ → SwitchSandwichStmt S 𝒟 A B δ

prop:switch-sandwich.

The paper proof assumes a normalized state and a probability distribution (weights summing to ≤ 1). Normalization is a theorem of the model; the distribution hypothesis is h𝒟.

theorem MIPRE.LIDT.Co.Preliminaries.completenessTransfer_core {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) (P : IdxProjSubMeas Question Outcome (K →L[ℂ] K)) (ε : ℝ) : V.sddError 𝒟 A P.toIdxSubMeas ≤ ε → V.idxSubMeasMass 𝒟 A ≥ V.idxSubMeasMass 𝒟 P.toIdxSubMeas - 2 * √ε

Core of prop:completeness-transfer-projective-P: if A ≈_ε P with P projective, the mass of A is at least that of P minus 2 √ε.

theorem MIPRE.LIDT.Co.Preliminaries.completenessTransferProjectiveP {K : Type u_2} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_3} {Outcome : Type u_4} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A : IdxSubMeas Question Outcome (K →L[ℂ] K)) (P : IdxProjSubMeas Question Outcome (K →L[ℂ] K)) (ε : ℝ) : V.SDDRel 𝒟 A P.toIdxSubMeas ε → CompTransferStmt V 𝒟 A P ε

prop:completeness-transfer-projective-P.

The paper proof uses a normalized state and a probability distribution. Normalization is a theorem of the vector state; the distribution hypothesis is h𝒟.