Direct parallel repetition of a game

The n-fold direct repetition G^{⊗n} of a game (blueprint def:direct-repetition): the referee samples n independent question pairs, sends the tuples to the players, and accepts if and only if every coordinate is accepted. The construction is that of the two vendored developments (MIPRE/Background/Repetition/), so that their theorems transfer without bookkeeping; the repetition of a synchronous game is synchronous.

def MIPRE.Game.repeat {X : Type u_1} {Y : Type u_2} {A : Type u_3} {B : Type u_4} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : Game (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)

The n-fold direct repetition of a game (blueprint def:direct-repetition): product question distribution on (Fin n → X) × (Fin n → Y) and the conjunction of the coordinate predicates.

Equations

• One or more equations did not get rendered due to their size.

def MIPRE.SynchronousGame.repeat {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (n : ℕ) : SynchronousGame (Fin n → X) (Fin n → A)

The n-fold direct repetition of a synchronous game is synchronous: unequal answer tuples to equal question tuples differ in some coordinate, which is then rejected.

Equations

• One or more equations did not get rendered due to their size.

theorem MIPRE.SynchronousGame.repeat_toGame {X : Type u_1} {A : Type u_3} [Fintype X] [Fintype A] [DecidableEq A] (G : SynchronousGame X A) (n : ℕ) : (G.repeat n).toGame = G.toGame.repeat n

The repetition of a synchronous game, viewed as a game, is the repetition of the underlying game.