A common denominator for a rational payoff table

theorem CommutingRepetition.Game.exists_common_denominator {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (hQ : ∀ (x : X) (y : Y) (a : A) (b : B), ∃ (r : ℚ), G.payoff x y a b = ↑r) : ∃ (den : ℕ) (num : X → Y → A → B → ℕ), 0 < den ∧ (∀ (x : X) (y : Y) (a : A) (b : B), G.payoff x y a b = ↑(num x y a b) / ↑den) ∧ ∀ (x : X) (y : Y) (a : A) (b : B), num x y a b ≤ den

A rational [0,1]-payoff table has a common denominator: V = num/den with num ≤ den.

The private-coin probability space

@[reducible, inline]

abbrev CommutingRepetition.CoinSpace (n den : ℕ) (X Y A B : Type) : Type

Questions, answers, and one private coin per coordinate.

Equations

• CommutingRepetition.CoinSpace n den X Y A B = ((Fin n → X) × (Fin n → Y) × (Fin n → A) × (Fin n → B) × (Fin n → Fin den))

theorem CommutingRepetition.TracialStrategy.correlation_sum' {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (xw : Fin n → X) (yw : Fin n → Y) : ∑ as : Fin n → A, ∑ bs : Fin n → B, Trep.correlation xw yw as bs = 1

The tracial correlation sums to one over the answer words.

noncomputable def CommutingRepetition.coinWeight {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (ω : CoinSpace n den X Y A B) : ℝ

The private-coin weight: product prior, strategy correlation, uniform coins.

Equations

• CommutingRepetition.coinWeight G Trep den ω = (∏ j : Fin n, G.questionWeight (ω.1 j) (ω.2.1 j)) * Trep.correlation ω.1 ω.2.1 ω.2.2.1 ω.2.2.2.1 * (1 / ↑den) ^ n

theorem CommutingRepetition.coinWeight_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (ω : CoinSpace n den X Y A B) : 0 ≤ coinWeight G Trep den ω

theorem CommutingRepetition.sum_coinSpace {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] {n : ℕ} (den : ℕ) (f : CoinSpace n den X Y A B → ℝ) : ∑ ω : CoinSpace n den X Y A B, f ω = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, ∑ as : Fin n → A, ∑ bs : Fin n → B, ∑ c : Fin n → Fin den, f (xw, yw, as, bs, c)

Sums over the coin space, unfolded.

theorem CommutingRepetition.sum_coin_uniform {n : ℕ} (den : ℕ) (hden : 0 < den) : ∑ _c : Fin n → Fin den, (1 / ↑den) ^ n = 1

theorem CommutingRepetition.coinWeight_sum {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (hden : 0 < den) : ∑ ω : CoinSpace n den X Y A B, coinWeight G Trep den ω = 1

noncomputable def CommutingRepetition.coinLaw {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (hden : 0 < den) : FiniteEventLaw (CoinSpace n den X Y A B)

The private-coin law.

Equations

• CommutingRepetition.coinLaw G Trep den hden = { weight := CommutingRepetition.coinWeight G Trep den, weight_nonneg := ⋯, weight_sum := ⋯ }

def CommutingRepetition.coinWins {X Y A B : Type} {n : ℕ} (den : ℕ) (num : X → Y → A → B → ℕ) (i : Fin n) (ω : CoinSpace n den X Y A B) : Bool

Coordinate i accepts when its coin falls below the payoff numerator.

Equations

• CommutingRepetition.coinWins den num i ω = decide (↑(ω.2.2.2.2 i) < num (ω.1 i) (ω.2.1 i) (ω.2.2.1 i) (ω.2.2.2.1 i))

theorem CommutingRepetition.sum_coin_accept (den k : ℕ) (hk : k ≤ den) : (∑ v : Fin den, if ↑v < k then 1 else 0) = ↑k

The number of coin values accepting at threshold k ≤ den.

theorem CommutingRepetition.coinLaw_eventMass {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (hden : 0 < den) (num : X → Y → A → B → ℕ) (hnum : ∀ (x : X) (y : Y) (a : A) (b : B), num x y a b ≤ den) (S : Finset (Fin n)) : (coinLaw G Trep den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) S) = ∑ xw : Fin n → X, ∑ yw : Fin n → Y, ∑ as : Fin n → A, ∑ bs : Fin n → B, (∏ j : Fin n, G.questionWeight (xw j) (yw j)) * Trep.correlation xw yw as bs * ∏ j ∈ S, ↑(num (xw j) (yw j) (as j) (bs j)) / ↑den

Integrating out the coins: the mass of the acceptance event on a set of coordinates is the coin-free weighted sum.

theorem CommutingRepetition.coinLaw_eventMass_univ {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {n : ℕ} (Trep : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (den : ℕ) (hden : 0 < den) (num : X → Y → A → B → ℕ) (hnum : ∀ (x : X) (y : Y) (a : A) (b : B), num x y a b ≤ den) (hV : ∀ (x : X) (y : Y) (a : A) (b : B), G.payoff x y a b = ↑(num x y a b) / ↑den) : (coinLaw G Trep den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) Finset.univ) = (G.repeat n).win Trep.correlation

The all-coordinates acceptance mass is the repeated win probability.