The recursion behind the parallel repetition theorem

Holenstein's proof of the parallel repetition theorem picks coordinates one at a time. With p_m the probability of winning the m coordinates picked so far, Lemma 15 bounds each step by p_{m+1} ≤ p_m (v + C √((m L + ln (1 / p_m)) / (n - m))), where v is the value of the game and L stands for ln (|A| |B|). Section 7 turns this recursion into an exponential bound Holenstein, Section 7: while 12 C² m L ≤ (1 - v)² (n - m), the probability p_m is at most ((1 + v) / 2)^m (le_pow_of_step), and therefore the probability of winning all n coordinates is at most ((1 + v) / 2)^⌊(1 - v)² n / (13 C² L)⌋ (le_pow_floor_of_step). Holenstein's proof takes C = 15, uses 12 · 15² = 2700 and 13 · 15² ≤ 3000, and ignores the rounding of the number of steps, which the floor here records. This file is the analytic part of the theorem only: it assumes the recursion, which the embedding lemmas establish.

Main results

• Cslib.PCP.ParallelRepetition.le_pow_of_step: the induction of Section 7.
• Cslib.PCP.ParallelRepetition.le_pow_floor_of_step: the resulting bound on p_n.
• Cslib.PCP.ParallelRepetition.le_two_mul_rpow_of_step: the bound in Holenstein's exponential form, p_n ≤ 2 (1 - (1 - v)³ / (26 C²))^{n / L}.

References

• T. Holenstein, Parallel repetition: simplifications and the no-signaling case

theorem Cslib.PCP.ParallelRepetition.le_one_of_antitone {p : ℕ → ℝ} (hp0 : p 0 = 1) (hmono : ∀ (m : ℕ), p (m + 1) ≤ p m) (m : ℕ) : p m ≤ 1

A nonincreasing sequence starting at 1 stays in [0, 1].

theorem Cslib.PCP.ParallelRepetition.le_pow_of_step {v C L : ℝ} {n : ℕ} {p : ℕ → ℝ} (hv : 0 ≤ v) (hv1 : v ≤ 1) (hL : 1 ≤ L) (hp0 : p 0 = 1) (hnn : ∀ (m : ℕ), 0 ≤ p m) (hmono : ∀ (m : ℕ), p (m + 1) ≤ p m) (hstep : ∀ m < n, p (m + 1) ≤ p m * (v + C * √((↑m * L + Real.log (1 / p m)) / (↑n - ↑m)))) (m : ℕ) : 12 * C ^ 2 * ↑m * L ≤ (1 - v) ^ 2 * (↑n - ↑m) → p m ≤ ((1 + v) / 2) ^ m

The induction of Holenstein's Section 7 Holenstein, Section 7: if p_0 = 1, p is nonnegative and nonincreasing, and every step satisfies p_{m+1} ≤ p_m (v + C √((m L + ln (1 / p_m)) / (n - m))), then p_m ≤ ((1 + v) / 2)^m as long as 12 C² m L ≤ (1 - v)² (n - m).

theorem Cslib.PCP.ParallelRepetition.le_pow_floor_of_step {v C L : ℝ} {n : ℕ} {p : ℕ → ℝ} (hv : 0 ≤ v) (hv1 : v ≤ 1) (hC : 1 ≤ C) (hL : 1 ≤ L) (hp0 : p 0 = 1) (hnn : ∀ (m : ℕ), 0 ≤ p m) (hmono : ∀ (m : ℕ), p (m + 1) ≤ p m) (hstep : ∀ m < n, p (m + 1) ≤ p m * (v + C * √((↑m * L + Real.log (1 / p m)) / (↑n - ↑m)))) : p n ≤ ((1 + v) / 2) ^ ⌊(1 - v) ^ 2 * ↑n / (13 * C ^ 2 * L)⌋₊

The bound of Holenstein's Section 7 Holenstein, Section 7: under the recursion of le_pow_of_step with C ≥ 1, p_n ≤ ((1 + v) / 2)^⌊(1 - v)² n / (13 C² L)⌋.

theorem Cslib.PCP.ParallelRepetition.le_two_mul_rpow_of_step {v C L : ℝ} {n : ℕ} {p : ℕ → ℝ} (hv : 0 ≤ v) (hv1 : v ≤ 1) (hC : 1 ≤ C) (hL : 1 ≤ L) (hp0 : p 0 = 1) (hnn : ∀ (m : ℕ), 0 ≤ p m) (hmono : ∀ (m : ℕ), p (m + 1) ≤ p m) (hstep : ∀ m < n, p (m + 1) ≤ p m * (v + C * √((↑m * L + Real.log (1 / p m)) / (↑n - ↑m)))) : p n ≤ 2 * (1 - (1 - v) ^ 3 / (26 * C ^ 2)) ^ (↑n / L)

The bound of Holenstein's Theorem 4, in exponential form [Holenstein, Section 7, (39)] [Hol09]: under the recursion of le_pow_of_step with C ≥ 1, p_n ≤ 2 (1 - (1 - v)³ / (26 C²))^{n / L}. The factor 2 accounts for rounding the number of steps down; Holenstein's 6000 corresponds to 26 C² with C = 15 (26 · 225 = 5850).