def MainStatement.toGame {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : CommutingRepetition.Game X Y A B

Equations

• MainStatement.toGame G = { questionWeight := G.questionWeight, weight_nonneg := ⋯, weight_normalized := ⋯, payoff := G.payoff, payoff_nonneg := ⋯, payoff_le_one := ⋯ }

def MainStatement.toStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingStrategy X Y A B) : CommutingRepetition.CommutingStrategy X Y A B

Equations

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

def MainStatement.ofStrategy {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (S : CommutingRepetition.CommutingStrategy X Y A B) : CommutingStrategy X Y A B

Equations

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

theorem MainStatement.omegaCO_eq {X Y A B : Type} [Fintype X] [Fintype Y] [Fintype A] [Fintype B] (G : Game X Y A B) : G.omegaCO = (toGame G).omegaCO

The two suprema defining ω^co range over the same set.

def MainStatement.ofAlgebra (M : CommutingRepetition.StdTracialAlgebra) : StdTracialAlgebra

Equations

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

def MainStatement.ofEmbeddable {Xc Ac : Type} [Fintype Xc] [Fintype Ac] (q : CommutingRepetition.TraciallyEmbeddableCorrelation Xc Ac) : TraciallyEmbeddableCorrelation Xc Ac

Equations

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

theorem MainStatement.tracialDensity : TracialDensityHypothesis

Lin's density theorem in the vocabulary of Statement.lean (audit node 1.1.1): the standalone file's own TracialDensityHypothesis is a theorem, transferred from CommutingRepetition.Density.tracialDensity (stage E7 of the density programme) through the field-by-field identification of the two copies of StdTracialAlgebra and TraciallyEmbeddableCorrelation. This is why UniformParallelRepetition below carries no hypothesis.

theorem MainStatement.uniform_parallel_repetition : UniformParallelRepetition

The development proves the standalone statement of Statement.lean.