OAI/Combinatorics/IndependentSets/PCP/GraphIterationBounds.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.inputBits line 11
  2. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.countedBits line 13
  3. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.words line 15
  4. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.count line 18
  5. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.lengthPolynomial line 20
  6. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.inputBits_le_countedBits line 23
  7. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.size_le_inputBits line 27
  8. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.count_le line 32
  9. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.intermediate_size line 36
  10. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.intermediate_bits line 44
  11. def OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial line 60
  12. theorem OAI.IndependentSetsGames.Foundations.Complexity.GraphIterationBounds.runtimePolynomial_eval line 64
  13. abbrev OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.Signs line 77
  14. abbrev OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.Names line 78
  15. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.clauseSigns line 80
  16. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.clauseNames line 83
  17. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.nameWord line 86
  18. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.decodedLabel line 91
  19. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.incidencePredicate line 94
  20. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.relationPredicate line 102
  21. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.relationWordsFor line 107
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.relationWordsFor_length line 110
  23. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.incidenceWords line 114
  24. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.clauseWords line 120
  25. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.dummyWords line 128
  26. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.orderedList line 131
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.orderedList_cast line 134
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.orderedList_prod line 139
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.orderedList_sum line 163
  30. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.clauseDarts line 177
  31. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.orderedList_dartOrder line 182
  32. def OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.rowFor line 195
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.rowList_table line 201
  34. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.rowWords_incidence line 207
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.rowWords_dummy line 227
  36. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.clauseDarts_rowWords line 240
  37. theorem OAI.IndependentSetsGames.Foundations.PCP.RawInitialRows.tableWords_eq line 246