OAI/Computability/VertexCover/PCP/PCPIteration.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.PCPIteration.Label line 50
  2. abbrev OAI.UniqueGames.Foundations.PCP.PCPIteration.Graph line 51
  3. abbrev OAI.UniqueGames.Foundations.PCP.PCPIteration.Addresses line 52
  4. def OAI.UniqueGames.Foundations.PCP.PCPIteration.step line 54
  5. def OAI.UniqueGames.Foundations.PCP.PCPIteration.run line 58
  6. def OAI.UniqueGames.Foundations.PCP.PCPIteration.initial line 61
  7. def OAI.UniqueGames.Foundations.PCP.PCPIteration.iterationCount line 63
  8. def OAI.UniqueGames.Foundations.PCP.PCPIteration.output line 65
  9. def OAI.UniqueGames.Foundations.PCP.PCPIteration.polynomialDegree line 68
  10. def OAI.UniqueGames.Foundations.PCP.PCPIteration.finalClauseGap line 70
  11. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 72
  12. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 76
  13. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 79
  14. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.initial_size_positive line 83
  15. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.initial_size_bound line 86
  16. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.step_completeness line 94
  17. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.step_gap line 98
  18. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.step_size line 102
  19. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.run_completeness line 106
  20. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.run_gap line 112
  21. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.run_size line 118
  22. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_completeness line 124
  23. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_gap line 130
  24. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 140
  25. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_size_polynomial line 150
  26. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 157
  27. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.output_count_gap line 165
  28. def OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF line 191
  29. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_satisfiable_iff line 194
  30. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_clause_count line 199
  31. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_variable_count line 203
  32. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_nonempty line 207
  33. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_gap line 214
  34. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_clauseGap line 226
  35. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_total_size line 232
  36. theorem OAI.UniqueGames.Foundations.PCP.PCPIteration.finalCNF_polynomial_size line 249