structure CommutingRepetition.Game (X : Type u_1) (Y : Type u_2) (A : Type u_3) (B : Type u_4) [Fintype X] [Fintype Y] [Fintype A] [Fintype B] : Type (max (max (max u_1 u_2) u_3) u_4)

A finite two-player one-round game G = (X, Y, A, B, μ, V): finite nonempty question sets X, Y and answer sets A, B (nonemptiness is assumed at the theorems that need it), a probability distribution μ on X × Y given by questionWeight, and an acceptance function payoff = V(a, b | x, y) ∈ [0,1]. [02_preliminaries.tex, "Games and direct repetition"; audit def game]

• questionWeight : X → Y → ℝ
• weight_nonneg (x : X) (y : Y) : 0 ≤ self.questionWeight x y
• weight_normalized : ∑ x : X, ∑ y : Y, self.questionWeight x y = 1
• payoff : X → Y → A → B → ℝ
• payoff_nonneg (x : X) (y : Y) (a : A) (b : B) : 0 ≤ self.payoff x y a b
• payoff_le_one (x : X) (y : Y) (a : A) (b : B) : self.payoff x y a b ≤ 1

def CommutingRepetition.Game.IsPredicate {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) : Prop

The predicate case: every payoff value is 0 or 1. The manuscript proves the predicate case first (05_prerounding.tex lines 10–18 standing assumption; 07_main_theorem.tex sec 7.4 removes it).

Equations

• G.IsPredicate = ∀ (x : X) (y : Y) (a : A) (b : B), G.payoff x y a b = 0 ∨ G.payoff x y a b = 1

def CommutingRepetition.Game.marginalX {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) (x : X) : ℝ

Marginal law of Alice's question.

Equations

• G.marginalX x = ∑ y : Y, G.questionWeight x y

def CommutingRepetition.Game.marginalY {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) (y : Y) : ℝ

Marginal law of Bob's question.

Equations

• G.marginalY y = ∑ x : X, G.questionWeight x y

theorem CommutingRepetition.Game.marginalX_nonneg {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) (x : X) : 0 ≤ G.marginalX x

theorem CommutingRepetition.Game.marginalY_nonneg {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) (y : Y) : 0 ≤ G.marginalY y

theorem CommutingRepetition.Game.marginalX_normalized {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) : ∑ x : X, G.marginalX x = 1

theorem CommutingRepetition.Game.marginalY_normalized {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) : ∑ y : Y, G.marginalY y = 1

theorem CommutingRepetition.Game.questionWeight_le_one {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) (x : X) (y : Y) : G.questionWeight x y ≤ 1

Each question weight is at most one (a single term of a normalized nonnegative sum).

def CommutingRepetition.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)

Direct n-fold repetition G^{⊗n}: product question law on (Fin n → X) × (Fin n → Y) and product acceptance V^{⊗n}(a^n, b^n | x^n, y^n) = ∏ᵢ V(aᵢ, bᵢ | xᵢ, yᵢ). n = 0 is a total-function extension outside the paper's n ≥ 1 scope (empty products; the main theorem hypothesizes 1 ≤ n). [02_preliminaries.tex, eq for V^{⊗n}; audit def direct_repetition]

Equations

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

theorem CommutingRepetition.Game.repeat_isPredicate {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} (hG : G.IsPredicate) (n : ℕ) : (G.repeat n).IsPredicate