Switch-sandwich preparation: inner-product bounds

Cauchy–Schwarz-style inner-product bounds in the avgOver formulation used by the switch-sandwich argument: the counterpart of MIPRE/Background/LIDT/MIPStarRE/LDT/Preliminaries/SwitchSandwichPrep/InnerProduct.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 families of operators in K →L[ℂ] K, and they drop the vendored normalization hypothesis hψ : ψ.IsNormalized, a theorem of the vector state (V.ev_one_of_isNormalized). ev_adjoint_eq is the keystone's V.ev_conjTranspose under its vendored name; the vendored proof by the normalized trace of the density matrix is not needed.

Not ported

• avgOver_abs_le_sqrt_of_pointwise: classical, imported.

References

In LionSR/MIPStarRE at commit 507e8122, not in this repository:

• references/ldt-paper/preliminaries.tex, prop:switch-sandwich

theorem MIPRE.LIDT.Co.Preliminaries.ev_adjoint_eq {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] (V : VecState K) (X : K →L[ℂ] K) : V.ev (star X) = V.ev X

ev is invariant under taking adjoints.

theorem MIPRE.LIDT.Co.Preliminaries.closenessOfInnerProduct_left {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (γ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (A q) (B q)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b) * star (∑ b : OutcomeB, C q a b) ≤ 1) : |(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * A q a)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (C q a b * B q a)| ≤ √γ

prop:closeness-of-ip, left-action clause eq:closeness3.

theorem MIPRE.LIDT.Co.Preliminaries.closenessOfInnerProduct_right {K : Type u_1} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] {Question : Type u_2} {OutcomeA : Type u_3} {OutcomeB : Type u_4} [Fintype OutcomeA] [Fintype OutcomeB] (V : VecState K) (𝒟 : MIPStarRE.LDT.Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → K →L[ℂ] K) (C : Question → OutcomeA → OutcomeB → K →L[ℂ] K) (γ : ℝ) (hAB : (MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => V.qSDDCore (fun (a : OutcomeA) => star (A q a)) fun (a : OutcomeA) => star (B q a)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, star (∑ b : OutcomeB, C q a b) * ∑ b : OutcomeB, C q a b ≤ 1) : |(MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (A q a * C q a b)) - MIPStarRE.LDT.avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, V.ev (B q a * C q a b)| ≤ √γ

prop:closeness-of-ip, right-action clause eq:closeness4.