Switch-sandwich preparation: inner-product bounds

Cauchy–Schwarz-style inner-product bounds in the avgOver formulation used by the switch-sandwich argument.

References

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

theorem MIPStarRE.LDT.Preliminaries.avgOver_abs_le_sqrt_of_pointwise {Question : Type u_1} (𝒟 : Distribution Question) (f g : Question → Error) (hf : ∀ (q : Question), |f q| ≤ √(g q)) (hg : ∀ (q : Question), 0 ≤ g q) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) : |avgOver 𝒟 f| ≤ √(avgOver 𝒟 g)

theorem MIPStarRE.LDT.Preliminaries.closenessOfInnerProduct_left {Question : Type u_1} {OutcomeA : Type u_2} {OutcomeB : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype OutcomeA] [Fintype OutcomeB] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → Quantum.Op ι) (C : Question → OutcomeA → OutcomeB → Quantum.Op ι) (γ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (A q) (B q)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b) * (∑ b : OutcomeB, C q a b).conjTranspose ≤ 1) : |(avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * A q a)) - avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (C q a b * B q a)| ≤ √γ

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

theorem MIPStarRE.LDT.Preliminaries.closenessOfInnerProduct_right {Question : Type u_1} {OutcomeA : Type u_2} {OutcomeB : Type u_3} {ι : Type u_4} [Fintype ι] [DecidableEq ι] [Fintype OutcomeA] [Fintype OutcomeB] (ψ : QuantumState ι) (hψ : ψ.IsNormalized) (𝒟 : Distribution Question) (h𝒟 : ∑ q ∈ 𝒟.support, 𝒟.weight q ≤ 1) (A B : Question → OutcomeA → Quantum.Op ι) (C : Question → OutcomeA → OutcomeB → Quantum.Op ι) (γ : Error) (hAB : (avgOver 𝒟 fun (q : Question) => qSDDCore ψ (fun (a : OutcomeA) => Matrix.conjTranspose (A q a)) fun (a : OutcomeA) => Matrix.conjTranspose (B q a)) ≤ γ) (hC : ∀ (q : Question), ∑ a : OutcomeA, (∑ b : OutcomeB, C q a b).conjTranspose * ∑ b : OutcomeB, C q a b ≤ 1) : |(avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (A q a * C q a b)) - avgOver 𝒟 fun (q : Question) => ∑ a : OutcomeA, ∑ b : OutcomeB, ev ψ (B q a * C q a b)| ≤ √γ

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