QuantumParallelRepetition.entangledValue_exponential_decay

For arbitrary types $X,Y,A,B$, equipped with finite-type structures on all four types and with explicit nonemptiness assumptions only on $A$ and $B$, and for every game $G$ consisting of a real weight $q:X\to Y\to\mathbb R$ satisfying $q(x,y)\ge 0$ for every $x,y$ and $\sum_{x:X}\sum_{y:Y}q(x,y)=1$, together with a Boolean predicate $V:X\to Y\to A\to B\to\mathrm{Bool}$, assume that $\omega^*(G)<1$, where $\omega^*(G)$ is Lean’s real supremum of the winning probabilities of all structures $S$ having arbitrary finite types $D_A,D_B$ with decidable equality (with no separately stated $\mathrm{Nonempty}$ assumptions on them), a positive-semidefinite complex matrix $\rho$ on $D_A\times D_B$ with $\operatorname{tr}(\rho)=1$, and, for every $x:X$ and $y:Y$, respectively POVMs $\{M_x^a\}_{a:A}$ on $D_A$ and $\{N_y^b\}_{b:B}$ on $D_B$, meaning that every operator is positive semidefinite and $\sum_aM_x^a=I$ and $\sum_bN_y^b=I$; the winning probability whose supremum is taken is $\sum_{x:X}\sum_{y:Y}q(x,y)\sum_{a:A}\sum_{b:B}\bigl(\operatorname{Re}\operatorname{tr}(\rho(M_x^a\otimes N_y^b))\bigr)$ with each summand replaced by $0$ when $V(x,y,a,b)\ne\mathrm{true}$. Then there exist real numbers $C$ and $c$, in that order, such that $0<C$, $0<c$, and for every natural number $n$, $\omega^*(G^{\times n})\le C\,\exp(-c\,n)$, where $n$ is coerced to a real number and $G^{\times n}$ has question types $\mathrm{Fin}(n)\to X$ and $\mathrm{Fin}(n)\to Y$, answer types $\mathrm{Fin}(n)\to A$ and $\mathrm{Fin}(n)\to B$, question weight $\prod_{i:\mathrm{Fin}(n)}q(x_i,y_i)$, and Boolean predicate true exactly when $V(x_i,y_i,a_i,b_i)=\mathrm{true}$ for every $i:\mathrm{Fin}(n)$; $\omega^*(G^{\times n})$ is again the supremum over all finite-dimensional strategies of precisely the same form, now with measurements indexed by those question tuples and with outcomes indexed by those answer tuples. The universal quantifier includes $n=0$: all four tuple types then consist of the unique empty function, the question weight is the empty product $1$, the repeated predicate is true by the empty universal condition, and the asserted inequality is merely $\omega^*(G^{\times0})\le C$. There are no nonemptiness assumptions on $X$ or $Y$; however, if either is empty, the required normalization equation for $G$ would read $0=1$, so no such game $G$ exists in that case.