Switch-sandwich preparation: approx_δ overlap gaps

Pointwise overlap-gap estimates used to bound the switch-sandwich approximation error under approx_δ families: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichPrep/ApproxDelta.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The statements use a single state and joint operators, so they take a vector state V : VecState K (a symmetric model is accepted through its coercion) and submeasurements in K →L[ℂ] K, and they drop the vendored normalization hypothesis hψ : ψ.IsNormalized, a theorem of the vector state. SDDRel ψ is V.SDDRel.

Both gaps are one estimate: for submeasurements A, B and a third one E (E = A on the left, E = B on the right), ∑_a ev ((A_a - B_a) E_a) is at most √(qSDD A B) in absolute value, by Cauchy–Schwarz and ∑_a ev (E_a²) ≤ 1 (subMeas_diagMass_le_one).

New here

• question_overlap_gap_aux: the common estimate above, from which both gaps follow.

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_overlap_gap_aux {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B E : SubMeas Outcome (K →L[ℂ] K)) : |∑ a : Outcome, V.ev ((A.outcome a - B.outcome a) * E.outcome a)| ≤ √(V.qSDD A B)

The common estimate behind question_overlap_gap_left and question_overlap_gap_right: |∑_a ev ((A_a - B_a) E_a)| ≤ √(qSDD A B) for submeasurements A, B, E.

theorem MIPRE.LIDT.Co.Preliminaries.question_overlap_gap_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B : SubMeas Outcome (K →L[ℂ] K)) : |∑ a : Outcome, V.ev (A.outcome a * A.outcome a) - ∑ a : Outcome, V.ev (A.outcome a * B.outcome a)| ≤ √(V.qSDD A B)

Left overlap gap: |∑_a ev (A_a A_a) - ∑_a ev (A_a B_a)| ≤ √(qSDD A B).

theorem MIPRE.LIDT.Co.Preliminaries.question_overlap_gap_right {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (A B : SubMeas Outcome (K →L[ℂ] K)) : |∑ a : Outcome, V.ev (A.outcome a * B.outcome a) - ∑ a : Outcome, V.ev (B.outcome a * B.outcome a)| ≤ √(V.qSDD A B)

Right overlap gap: |∑_a ev (A_a B_a) - ∑_a ev (B_a B_a)| ≤ √(qSDD A B).

theorem MIPRE.LIDT.Co.Preliminaries.easyApproxFromApproxDelta_twoFamily {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {Outcome : Type u_3} [Fintype Outcome] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxSubMeas Question Outcome (K →L[ℂ] K)) (δ : ℝ) : V.SDDRel 𝒟 A B δ → |(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.ev ((A q).outcome a * (A q).outcome a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.ev ((A q).outcome a * (B q).outcome a)| ≤ √δ ∧ |(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.ev ((A q).outcome a * (B q).outcome a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, V.ev ((B q).outcome a * (B q).outcome a)| ≤ √δ

prop:easy-approx-from-approx-delta.