QuantumParallelRepetition.entangledValue_tendsto_zero

Proved

by Henry Yuen · Aug 9, 2026 · Mathlib 0df444a (Lean v4.33.1)

nonlocal-gamesparallel-repetitionquantum-information

Let $G$ be a finite two-player one-round game with nonempty answer alphabets, and let $\omega^*(G)$ be the supremal winning probability of its finite-dimensional entangled strategies. Let $G^n$ denote the $n$ -fold parallel repetition, in which the referee samples all coordinates independently and the players win only if every coordinate accepts.

If the original game cannot be won with certainty,

\omega^*(G)<1,

then its repeated entangled value converges to zero:

\lim_{n\to\infty}\omega^*(G^n)=0.

Equivalently, for every $\varepsilon>0$ , all sufficiently large repetition counts $n$ satisfy $\omega^*(G^n)<\varepsilon$ . The theorem deliberately asserts no rate of convergence.

Formalization Note Lean expresses the conclusion as Tendsto (repeatedEntangledValue G) atTop (𝓝 0). The sequence includes the zero-fold repetition, but changing finitely many terms does not affect its limit.

Preamble

import Definitions.Def_quantum_parallel_repetition_game
import Mathlib.Topology.Order.Basic

open Filter
open scoped Topology

Formal statement

namespace QuantumParallelRepetition

/-- The entangled value of every nontrivial finite two-player game tends to zero under
parallel repetition. -/
theorem entangledValue_tendsto_zero
    {X Y A B : Type*}
    [Fintype X] [Fintype Y] [Fintype A] [Fintype B]
    [Nonempty A] [Nonempty B]
    (G : Game X Y A B)
    (hG : entangledValue G < 1) :
    Tendsto (repeatedEntangledValue G) atTop (𝓝 0) := by
  sorry

end QuantumParallelRepetition

Source

Henry Yuen, A parallel repetition theorem for all entangled games, arXiv:1604.04340v1, p. 2, qualitative consequence immediately before Theorem 1 and p. 1, abstract, https://arxiv.org/abs/1604.04340

View graph