@[reducible, inline]

abbrev CommutingRepetition.Correlation (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 correlation table on alphabets X, Y, A, B.

Equations

• CommutingRepetition.Correlation X Y A B = (X → Y → A → B → ℝ)

def CommutingRepetition.IsCommutingCorrelation {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (p : Correlation X Y A B) : Prop

Realizability by a commuting-operator strategy at universe 0, per the universe policy in this file's header (fidelity review #1: the pinning propagates into TracialDensityHypothesis, where it only weakens what is assumed).

Equations

• CommutingRepetition.IsCommutingCorrelation p = ∃ (S : CommutingRepetition.CommutingStrategy X Y A B), S.correlation = p

def CommutingRepetition.Game.win {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (p : Correlation X Y A B) : ℝ

Expected payoff of a correlation in the game G: win_G(p) = ∑ μ(x,y) V(a,b|x,y) p(a,b|x,y) — a linear functional of the correlation table, as the tracial reduction (03_tracial_reduction.tex) requires.

Equations

• G.win p = ∑ x : X, ∑ y : Y, ∑ a : A, ∑ b : B, G.questionWeight x y * G.payoff x y a b * p x y a b

theorem CommutingRepetition.Game.win_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : Correlation X Y A B} (hp : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ p x y a b) : 0 ≤ G.win p

theorem CommutingRepetition.Game.win_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) {p : Correlation X Y A B} (hp : ∀ (x : X) (y : Y) (a : A) (b : B), 0 ≤ p x y a b) (hsum : ∀ (x : X) (y : Y), ∑ a : A, ∑ b : B, p x y a b ≤ 1) : G.win p ≤ 1

If a correlation is pointwise nonnegative with answer sums ≤ 1, the winning probability is at most one.

noncomputable def CommutingRepetition.Game.omegaCO {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : ℝ

The commuting-operator value ω^co(G): the supremum of winning probabilities over commuting-operator strategies. [02_preliminaries.tex, "The supremum of this expression is the commuting value"; non-attainment is never assumed anywhere downstream.]

Equations

• G.omegaCO = sSup (Set.range fun (S : CommutingRepetition.CommutingStrategy X Y A B) => G.win S.correlation)

theorem CommutingRepetition.Game.winProbabilities_bddAbove {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : BddAbove (Set.range fun (S : CommutingStrategy X Y A B) => G.win S.correlation)

theorem CommutingRepetition.Game.omegaCO_le_one {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : G.omegaCO ≤ 1

theorem CommutingRepetition.Game.omegaCO_nonneg {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] [Nonempty A] [Nonempty B] (G : Game X Y A B) : 0 ≤ G.omegaCO

0 ≤ ω^co(G). The Nonempty guards mirror the paper's nonempty answer sets (the statement would also hold vacuously via sSup ∅ = 0, but the guards keep the hypothesis surface paper-faithful).

theorem CommutingRepetition.Game.le_omegaCO {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (S : CommutingStrategy X Y A B) : G.win S.correlation ≤ G.omegaCO

Any single realizable strategy's value lower-bounds ω^co. Producing one legal strategy above a threshold contradicts ω^co ≤ threshold — the shape used by the final contradiction (07_main_theorem.tex, node 1.5.4).

noncomputable def CommutingRepetition.Game.repeatedOmegaCO {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) (n : ℕ) : ℝ

The n-fold repeated value ω^co(G^{⊗n}).

Equations

• G.repeatedOmegaCO n = (G.repeat n).omegaCO