QuantumParallelRepetition.entangledValue_polynomial_decay

For every four types $X,Y,A,B$, each equipped with a Fintype structure, with $A$ and $B$ additionally equipped with Nonempty structures, and for every $G$ consisting of a function $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 function $V:X\to Y\to A\to B\to\mathrm{Bool}$, assume that $\operatorname{sSup}\{W_G(S):S\text{ is a strategy for }G\}<1$, where a strategy $S$ chooses types $H_A,H_B$, Fintype and DecidableEq structures on each, a matrix $\rho\in\operatorname{Matrix}(H_A\times H_B,H_A\times H_B;\mathbb C)$ that is positive semidefinite and has trace $1$, for every $x:X$ matrices $M_x(a)\in\operatorname{Matrix}(H_A,H_A;\mathbb C)$, indexed by $a:A$, that are individually positive semidefinite and satisfy $\sum_{a:A}M_x(a)=I$, and for every $y:Y$ matrices $N_y(b)\in\operatorname{Matrix}(H_B,H_B;\mathbb C)$, indexed by $b:B$, that are individually positive semidefinite and satisfy $\sum_{b:B}N_y(b)=I$, and where $W_G(S)=\sum_{x:X}\sum_{y:Y}q(x,y)\sum_{a:A}\sum_{b:B}\bigl(\text{if }V(x,y,a,b)=\mathrm{true}\text{ then }\operatorname{Re}\operatorname{tr}(\rho(M_x(a)\otimes_kN_y(b)))\text{ else }0\bigr)$; then there exist real numbers $C$ and $\alpha$, in that order, such that $0<C$, $0<\alpha$, and for every natural number $n$, the real sSup of the winning probabilities of all strategies of the $(n+1)$-fold repeated game is at most $C\,\operatorname{rpow}(n+1,-\alpha)$, where that repeated game has questions $x_\bullet:\operatorname{Fin}(n+1)\to X$ and $y_\bullet:\operatorname{Fin}(n+1)\to Y$, answers $a_\bullet:\operatorname{Fin}(n+1)\to A$ and $b_\bullet:\operatorname{Fin}(n+1)\to B$, question weight $\prod_{i:\operatorname{Fin}(n+1)}q(x_i,y_i)$, and Boolean winning predicate equal to true exactly when $V(x_i,y_i,a_i,b_i)=\mathrm{true}$ for every $i:\operatorname{Fin}(n+1)$, with the supremum ranging afresh over strategies having arbitrary chosen finite, decidable-equality types $H_A,H_B$, a positive-semidefinite trace-one state, and complete positive-semidefinite POVMs for those function-valued questions and answers as above; the statement assumes no Nonempty structure on $X$ or $Y$ (although if either were empty, the required normalization $\sum_{x,y}q(x,y)=1$ could not hold), uses the total real sSup operation without separately hypothesizing that either strategy range is nonempty or bounded above, and includes $n=0$, for which it asserts the one-fold repeated-game value is at most $C\,\operatorname{rpow}(1,-\alpha)=C$, while making no assertion about a zero-fold repetition.