OAI/Computability/UniqueGames/Games/UniformRoundingTarget.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.UniqueGamesTheorem.Explicit.UniformRoundingTarget.rows line 15

   Source documentation

   Apply the concrete largest-remainder list of occurrence IDs to the original list. Equal records at different indices remain separate input occurrences.

   def rows {α : Type*} (C : Nat) (es : List α) : List α :=
   …

2. theorem OAI.UniqueGamesTheorem.Explicit.UniformRoundingTarget.rows_eq_occurrenceMajor line 19
3. theorem OAI.UniqueGamesTheorem.Explicit.UniformRoundingTarget.rows_perm_construct line 34

   Source documentation

   Exact multiplicities and full permutation records agree with the machine's copy-major target; only the enumeration order changes.

   theorem rows_perm_construct {q : Nat} (C : Nat) (hC : 0 < C) (g : Instance q) :
       (rows C g.constraints).Perm (UniformTarget.construct C hC g).constraints := by
   …

   Mentions: OAI.UniqueGamesTheorem.Explicit.UniformRoundingTarget.rows, OAI.UniqueGamesTheorem.Explicit.UniformTarget.construct

4. theorem OAI.UniqueGamesTheorem.Explicit.UniformRoundingTarget.selected_count_construct line 39