Switch-sandwich preparation: approx_δ overlap gaps

Pointwise overlap-gap estimates used to bound the switch-sandwich approximation error under approx_δ families.

References

• references/ldt-paper/preliminaries.tex, prop:switch-sandwich
• blueprint/src/chapter/ch03_preliminaries.tex

theorem MIPStarRE.LDT.Preliminaries.question_overlap_gap_left {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (A B : SubMeas Outcome ι) : |∑ a : Outcome, ev ψ (A.outcome a * A.outcome a) - ∑ a : Outcome, ev ψ (A.outcome a * B.outcome a)| ≤ √(qSDD ψ A B)

theorem MIPStarRE.LDT.Preliminaries.question_overlap_gap_right {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (A B : SubMeas Outcome ι) : |∑ a : Outcome, ev ψ (A.outcome a * B.outcome a) - ∑ a : Outcome, ev ψ (B.outcome a * B.outcome a)| ≤ √(qSDD ψ A B)

theorem MIPStarRE.LDT.Preliminaries.easyApproxFromApproxDelta_twoFamily {Question : Type u_1} {Outcome : Type u_2} {ι : Type u_3} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (𝒟 : Distribution Question) (hψ : ψ.IsNormalized) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : IdxSubMeas Question Outcome ι) (δ : Error) : SDDRel ψ 𝒟 A B δ → |(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((A q).outcome a * (A q).outcome a)) - avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((A q).outcome a * (B q).outcome a)| ≤ √δ ∧ |(avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((A q).outcome a * (B q).outcome a)) - avgOver 𝒟 fun (q : Question) => ∑ a : Outcome, ev ψ ((B q).outcome a * (B q).outcome a)| ≤ √δ

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