OAI/Computability/VertexCover/PCP/TableIteration.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.TableIteration.run line 48
  2. def OAI.UniqueGames.Foundations.PCP.TableIteration.runTables line 50
  3. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.run_val line 53
  4. def OAI.UniqueGames.Foundations.PCP.TableIteration.iterationCount line 61
  5. def OAI.UniqueGames.Foundations.PCP.TableIteration.output line 63
  6. def OAI.UniqueGames.Foundations.PCP.TableIteration.outputTable line 65
  7. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_val line 68
  8. def OAI.UniqueGames.Foundations.PCP.TableIteration.gapMap line 71
  9. opaque OAI.UniqueGames.Foundations.PCP.TableIteration.degreeData line 73
  10. def OAI.UniqueGames.Foundations.PCP.TableIteration.polynomialDegree line 76
  11. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.sizeFactor_le_power line 78
  12. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.run_completeness line 81
  13. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_completeness line 85
  14. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.gapMap_completeness line 89
  15. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_darts_positive line 95
  16. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.gapMap_nonempty line 99
  17. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.run_size line 102
  18. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_size line 106
  19. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.initial_size_le line 111
  20. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_size_le_input line 114
  21. def OAI.UniqueGames.Foundations.PCP.TableIteration.tableSizePolynomial line 122
  22. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.tableSizePolynomial_eval line 125
  23. def OAI.UniqueGames.Foundations.PCP.TableIteration.tableBitsPolynomial line 130
  24. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.output_bits_le line 133
  25. def OAI.UniqueGames.Foundations.PCP.TableIteration.formulaBitsPolynomial line 138
  26. theorem OAI.UniqueGames.Foundations.PCP.TableIteration.gapMap_bits_le line 141