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: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichGapBounds/Core.lean in the port of planning/c6b-plan.md (milestone M3, section "Port conventions").

The lemma uses a single state and joint operators, so it takes a vector state V : VecState K (a symmetric model is accepted through its coercion) and operators in K →L[ℂ] K; ᴴ becomes star. The proof is the vendored one: Cauchy–Schwarz termwise (V.ev_abs_mul_le_sqrt), then over the outcomes (Real.sum_sqrt_mul_sqrt_le), and the contraction LB * LB ≤ 1 conjugated by Y a (IsSelfAdjoint.conjugate_le_conjugate, then V.ev_mono).

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.sum_ev_mul_leftBounded_le_of_leftHermitian {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Outcome : Type u_2} [Fintype Outcome] (V : VecState K) (LB : K →L[ℂ] K) (X Y : Outcome → K →L[ℂ] K) (hLB_herm : star LB = LB) (hLB_sq_le_one : LB * LB ≤ 1) (hXherm : ∀ (a : Outcome), star (X a) = X a) (hYherm : ∀ (a : Outcome), star (Y a) = Y a) : |∑ a : Outcome, V.ev (X a * (LB * Y a))| ≤ √(∑ a : Outcome, V.ev (X a * X a)) * √(∑ a : Outcome, V.ev (star (Y a) * Y a))

Cauchy-Schwarz contraction used in both switch-sandwich gap estimates: |∑ₐ ev (Xₐ LB Yₐ)| ≤ √(∑ₐ ev (Xₐ Xₐ)) √(∑ₐ ev (Yₐ* Yₐ)) for self-adjoint Xₐ, Yₐ and a self-adjoint contraction LB.