QuantumParallelRepetition.entangledValue_tendsto_zero

For every choice of types $X,Y,A,B$ equipped with $\mathrm{Fintype}$ instances, with $\mathrm{Nonempty}$ instances additionally assumed for $A$ and $B$ but not for $X$ or $Y$, and for every game $G$ consisting of a real weight $w:X\to Y\to\mathbb R$ satisfying $0\le w(x,y)$ for every $x,y$ and $\sum_{x\in X}\sum_{y\in Y}w(x,y)=1$, together with a Boolean predicate $p:X\to Y\to A\to B\to\mathrm{Bool}$, the following implication holds: if $\omega^*(G)<1$, then $\lim_{n\to\infty}\omega^*(G^{\otimes n})=0$, meaning that for every neighborhood $U$ of $0$ there is an $N\in\mathbb N$ such that $\omega^*(G^{\otimes n})\in U$ for every $n\ge N$. Here $\omega^*(H)$ is the real supremum of the winning probabilities over all strategy records for $H$; each such record chooses types $D_A,D_B:\mathrm{Type}$, each equipped with both a $\mathrm{Fintype}$ instance and a $\mathrm{DecidableEq}$ instance but with no explicit $\mathrm{Nonempty}$ assumption, a complex matrix $\rho$ indexed by $D_A\times D_B$ that is positive semidefinite and has $\operatorname{tr}(\rho)=1$, for every first-player question $q$ a family $(M_q^a)_a$ of positive-semidefinite complex matrices indexed by $D_A$ with $\sum_a M_q^a=I$, and for every second-player question $r$ a family $(N_r^b)_b$ of positive-semidefinite complex matrices indexed by $D_B$ with $\sum_b N_r^b=I$; its winning probability is $\sum_q\sum_r w_H(q,r)\sum_a\sum_b\bigl(\operatorname{Re}\operatorname{tr}(\rho(M_q^a\otimes N_r^b))\ \text{if }p_H(q,r,a,b)=\mathrm{true},\ \text{and }0\text{ otherwise}\bigr)$. For $G^{\otimes n}$, the questions are all functions $x:\operatorname{Fin}(n)\to X$ and $y:\operatorname{Fin}(n)\to Y$, the answers are all functions $a:\operatorname{Fin}(n)\to A$ and $b:\operatorname{Fin}(n)\to B$, the question weight is $\prod_{i\in\operatorname{Fin}(n)}w(x_i,y_i)$, and the Boolean predicate is true exactly when $p(x_i,y_i,a_i,b_i)=\mathrm{true}$ for every $i\in\operatorname{Fin}(n)$; the supremum defining $\omega^*(G^{\otimes n})$ ranges over all strategy records just described for these function-valued question and answer types. The sequence includes $n=0$: all four function types out of $\operatorname{Fin}(0)$ are singletons, the empty-product question weight is $1$, and the universal winning condition is vacuously true, so the zero-fold game’s strategy winning probabilities, and hence its entangled value, are $1$; convergence at infinity nevertheless imposes no separate restriction on this initial term. Finally, although no $\mathrm{Nonempty}$ assumptions are given for $X$ or $Y$, the normalization field required of $G$ cannot be satisfied if either is empty.