theorem CommutingRepetition.sum_comm3 {α β γ : Type} [Fintype α] [Fintype β] [Fintype γ] (F : α → β → γ → ℝ) : ∑ a : α, ∑ b : β, ∑ c : γ, F a b c = ∑ b : β, ∑ c : γ, ∑ a : α, F a b c

Moving the first of three finite sums to the back.

Core words and their canonical extensions

theorem CommutingRepetition.agreesOn_extendCoreA_restrict {n : ℕ} {A : Type} [Fintype A] [DecidableEq A] [Nonempty A] (D : Finset (Fin n)) (as : Fin n → A) : agreesOn D as (extendCoreA D fun (j : ↥D) => as ↑j)

theorem CommutingRepetition.agreesOn_extendCoreB_restrict {n : ℕ} {B : Type} [Fintype B] [DecidableEq B] [Nonempty B] (D : Finset (Fin n)) (bs : Fin n → B) : agreesOn D bs (extendCoreB D fun (j : ↥D) => bs ↑j)

theorem CommutingRepetition.eq_restrict_of_agreesOn_extendCoreA {n : ℕ} {A : Type} [Fintype A] [DecidableEq A] [Nonempty A] (D : Finset (Fin n)) {as : Fin n → A} {zA : ↥D → A} (h : agreesOn D as (extendCoreA D zA)) : zA = fun (j : ↥D) => as ↑j

theorem CommutingRepetition.eq_restrict_of_agreesOn_extendCoreB {n : ℕ} {B : Type} [Fintype B] [DecidableEq B] [Nonempty B] (D : Finset (Fin n)) {bs : Fin n → B} {zB : ↥D → B} (h : agreesOn D bs (extendCoreB D zB)) : zB = fun (j : ↥D) => bs ↑j

theorem CommutingRepetition.sum_core_collapse {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty A] [Nonempty B] (D : Finset (Fin n)) (w : (Fin n → X) → (Fin n → Y) → (↥D → A) → (↥D → B) → ℝ) (xw : Fin n → X) (yw : Fin n → Y) (T : (Fin n → A) → (Fin n → B) → ℝ) : (∑ zD : (↥D → A) × (↥D → B), w xw yw zD.1 zD.2 * ∑ as : Fin n → A, ∑ bs : Fin n → B, if agreesOn D as (extendCoreA D zD.1) ∧ agreesOn D bs (extendCoreB D zD.2) then T as bs else 0) = ∑ as : Fin n → A, ∑ bs : Fin n → B, (w xw yw (fun (j : ↥D) => as ↑j) fun (j : ↥D) => bs ↑j) * T as bs

Summing out the core word: a core-indexed sum of w(z) · (agreement indicator) collapses to the restriction of the answer words.

The core weight of a payoff table

noncomputable def CommutingRepetition.coreW {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (D : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) : ℝ

The private-coin core weight w_D(x, y, z) = ∏_{j ∈ D} V(z_j | x_j, y_j) (eq private-coin-core-weight).

Equations

• CommutingRepetition.coreW G D xw yw zA zB = ∏ j : ↥D, G.payoff (xw ↑j) (yw ↑j) (zA j) (zB j)

theorem CommutingRepetition.coreW_nonneg {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (D : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) : 0 ≤ coreW G D xw yw zA zB

theorem CommutingRepetition.coreW_le_one {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (D : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) : coreW G D xw yw zA zB ≤ 1

theorem CommutingRepetition.coreW_agree {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (D : Finset (Fin n)) (xw xw' : Fin n → X) (yw yw' : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) : agreesOn D xw xw' → agreesOn D yw yw' → coreW G D xw yw zA zB = coreW G D xw' yw' zA zB

The core weight reads the question words only on D.

theorem CommutingRepetition.coreW_restrict {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] (G : Game X Y A B) (D : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (as : Fin n → A) (bs : Fin n → B) : (coreW G D xw yw (fun (j : ↥D) => as ↑j) fun (j : ↥D) => bs ↑j) = ∏ j ∈ D, G.payoff (xw j) (yw j) (as j) (bs j)

The core weight at the restriction of full answer words.

theorem CommutingRepetition.TracialStrategy.re_corePair_expand {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (D : Finset (Fin n)) (xw : Fin n → X) (yw : Fin n → Y) (zA : ↥D → A) (zB : ↥D → B) : (S.M.τ (star S.σ * (S.coreEffectA D xw (extendCoreA D zA) * S.σ * S.coreEffectB D yw (extendCoreB D zB)))).re = ∑ as : Fin n → A, ∑ bs : Fin n → B, if agreesOn D as (extendCoreA D zA) ∧ agreesOn D bs (extendCoreB D zB) then S.correlation xw yw as bs else 0

The core pairing expanded over the answer words.

theorem CommutingRepetition.TracialStrategy.coreMass_eq_eventMass {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (G : Game X Y A B) {den : ℕ} {num : X → Y → A → B → ℕ} (hden : 0 < den) (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) (D : Finset (Fin n)) : S.coreMass D G.questionWeight (coreW G D) = (coinLaw G S den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) D)

The weighted core mass is the private-coin acceptance mass P(W_D).

theorem CommutingRepetition.TracialStrategy.liveSucc_eq_eventMass {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (G : Game X Y A B) {den : ℕ} {num : X → Y → A → B → ℕ} (hden : 0 < den) (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) (D : Finset (Fin n)) (i : Fin n) (hi : i ∉ D) : S.liveSucc G.questionWeight G.payoff (coreW G D) i = (coinLaw G S den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) (insert i D))

The live success is the private-coin acceptance mass P(W_{D∪{i}}).

theorem CommutingRepetition.TracialStrategy.flatQ_idealPayoff_ge {n : ℕ} {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [DecidableEq X] [DecidableEq Y] [DecidableEq A] [DecidableEq B] [Nonempty X] [Nonempty Y] [Nonempty A] [Nonempty B] (S : TracialStrategy (Fin n → X) (Fin n → Y) (Fin n → A) (Fin n → B)) (G : Game X Y A B) {den : ℕ} {num : X → Y → A → B → ℕ} (hden : 0 < den) (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) (D : Finset (Fin n)) (hDn : D.card ≤ n) {δ : ℝ} (hgreedy : 1 - δ ≤ 1 / (↑n - ↑D.card) * ∑ i ∈ Finset.univ \ D, (coinLaw G S den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) (insert i D)) / (coinLaw G S den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) D)) (R : ResolverArena S.M (S.refinedA D G.questionWeight) (S.refinedB D G.questionWeight)) : 1 - δ ≤ ∑ u : PostTuple n X Y A B D × X × Y, S.flatQ R D G.questionWeight (coreW G D) ((coinLaw G S den hden).eventMass (FiniteEventLaw.winEvent (coinWins den num) D)) u * S.idealPayoffFlat G.questionWeight G.payoff R u

The ideal success of the package is the greedy core's average conditional success (05_prerounding.tex, end of the proof of prop tracial-prerounding: "has payoff q by the tower property").