Switch-sandwich gap bounds: Cauchy–Schwarz core

Shared Cauchy–Schwarz contraction used in both the left and middle gap estimates of the switch-sandwich argument.

References

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

theorem MIPStarRE.LDT.Preliminaries.sum_ev_mul_leftBounded_le_of_leftHermitian {Outcome : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq ι] [Fintype Outcome] (ψ : QuantumState ι) (LB : Quantum.Op ι) (X Y : Outcome → Quantum.Op ι) (hLB_herm : Matrix.conjTranspose LB = LB) (hLB_sq_le_one : LB * LB ≤ 1) (hXherm : ∀ (a : Outcome), Matrix.conjTranspose (X a) = X a) (hYherm : ∀ (a : Outcome), Matrix.conjTranspose (Y a) = Y a) : |∑ a : Outcome, ev ψ (X a * (LB * Y a))| ≤ √(∑ a : Outcome, ev ψ (X a * X a)) * √(∑ a : Outcome, ev ψ (Matrix.conjTranspose (Y a) * Y a))

Cauchy-Schwarz contraction used in both switch-sandwich gap estimates.