Two-prover one-round games

A two-prover one-round game Holenstein, Definition 1 draws a pair of questions (x, y) from a distribution on X × Y, sends x to Alice and y to Bob, and accepts their answers a and b according to a predicate Q x y a b. Its value is the largest winning probability of a pair of deterministic strategies X → A and Y → B (Cslib.PCP.TwoProverGame.value). Shared randomness does not help (winProb_shared_le_value) Holenstein, (3). The n-fold parallel repetition asks n independent pairs of questions at once and accepts when every coordinate is accepted (Cslib.PCP.TwoProverGame.pow) Holenstein, Definition 2. Answering each coordinate independently with an optimal strategy shows value G ^ n ≤ value (G.pow n) (pow_value_le_value_pow); the parallel repetition theorem bounds value (G.pow n) from above.

Main definitions

• Cslib.PCP.TwoProverGame: a two-prover one-round game.
• Cslib.PCP.TwoProverGame.winProb, Cslib.PCP.TwoProverGame.value: winning probability and value.
• Cslib.PCP.TwoProverGame.pow: parallel repetition.

Main results

• Cslib.PCP.TwoProverGame.winProb_le_value, Cslib.PCP.TwoProverGame.exists_winProb_eq_value: the value is attained by a deterministic strategy.
• Cslib.PCP.TwoProverGame.winProb_shared_le_value: shared randomness does not help.
• Cslib.PCP.TwoProverGame.pow_value_le_value_pow: value G ^ n ≤ value (G.pow n).

References

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

structure Cslib.PCP.TwoProverGame (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) : Type (max (max (max u_1 u_2) u_3) u_4)

A two-prover one-round game Holenstein, Definition 1: questions drawn from questions, answers accepted by accepts.

• questions : PMF (X × Y)

  The distribution of the pair of questions.

• accepts : X → Y → A → B → Prop

  The acceptance predicate on questions and answers.

noncomputable def Cslib.PCP.TwoProverGame.winProb {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) (ha : X → A) (hb : Y → B) : ℝ

The probability that the deterministic strategies ha and hb win.

noncomputable def Cslib.PCP.TwoProverGame.value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) : ℝ

The value of a game: the largest winning probability of deterministic strategies.

theorem Cslib.PCP.TwoProverGame.winProb_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) (ha : X → A) (hb : Y → B) : 0 ≤ G.winProb ha hb

theorem Cslib.PCP.TwoProverGame.winProb_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) (ha : X → A) (hb : Y → B) : G.winProb ha hb ≤ 1

theorem Cslib.PCP.TwoProverGame.winProb_le_value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] (ha : X → A) (hb : Y → B) : G.winProb ha hb ≤ G.value

theorem Cslib.PCP.TwoProverGame.exists_winProb_eq_value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] [Nonempty A] [Nonempty B] : ∃ (ha : X → A) (hb : Y → B), G.winProb ha hb = G.value

theorem Cslib.PCP.TwoProverGame.value_nonneg {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] [Nonempty A] [Nonempty B] : 0 ≤ G.value

theorem Cslib.PCP.TwoProverGame.value_le_one {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] [Nonempty A] [Nonempty B] : G.value ≤ 1

theorem Cslib.PCP.TwoProverGame.winProb_shared_le_value {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] [Nonempty A] [Nonempty B] {R : Type u_5} (ρ : PMF R) (ha : X → R → A) (hb : Y → R → B) : ((ρ.bind fun (r : R) => PMF.map (fun (q : X × Y) => (q, ha q.1 r, hb q.2 r)) G.questions).toOuterMeasure {z : (X × Y) × A × B | G.accepts z.1.1 z.1.2 z.2.1 z.2.2}).toReal ≤ G.value

Shared randomness does not help Holenstein, (3): strategies that read a common random string r drawn from ρ win with probability at most the value.

Parallel repetition

theorem Cslib.Probability.PMF.toOuterMeasure_pi_forall {ι : Type u_5} [Fintype ι] {α : ι → Type u_6} [∀ (i : ι), Finite (α i)] (p : (i : ι) → PMF (α i)) (E : (i : ι) → Set (α i)) : (pi p).toOuterMeasure {u : (i : ι) → α i | ∀ (i : ι), u i ∈ E i} = ∏ i : ι, (p i).toOuterMeasure (E i)

The probability that every coordinate of an independent tuple lies in its own event is the product of the probabilities.

noncomputable def Cslib.PCP.TwoProverGame.pow {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] (n : ℕ) : TwoProverGame (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

The n-fold parallel repetition Holenstein, Definition 2: n independent pairs of questions, accepted when every coordinate is accepted.

theorem Cslib.PCP.TwoProverGame.winProb_pow {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] (n : ℕ) (ha : X → A) (hb : Y → B) : ((G.pow n).winProb (fun (x : Fin n → X) (i : Fin n) => ha (x i)) fun (y : Fin n → Y) (i : Fin n) => hb (y i)) = G.winProb ha hb ^ n

Answering each coordinate independently wins with the product of the probabilities.

theorem Cslib.PCP.TwoProverGame.pow_value_le_value_pow {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} (G : TwoProverGame X Y A B) [Finite X] [Finite Y] [Finite A] [Finite B] [Nonempty A] [Nonempty B] (n : ℕ) : G.value ^ n ≤ (G.pow n).value

Answering each coordinate independently with an optimal strategy shows that parallel repetition cannot lower the value below value G ^ n.