OAI/Combinatorics/IndependentSets/PCP/PCPIteration.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.Label line 13
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.Graph line 14
  3. abbrev OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.Addresses line 15
  4. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.step line 17
  5. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.run line 21
  6. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.initial line 24
  7. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.iterationCount line 26
  8. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output line 28
  9. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.polynomialDegree line 31
  10. def OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalClauseGap line 33
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.finalClauseGap_positive line 35
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.sizeFactor_le_power line 39
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.initial_satisfiable_iff line 42
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.initial_size_positive line 46
  15. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.initial_size_bound line 49
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.step_completeness line 57
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.step_gap line 61
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.step_size line 65
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.run_completeness line 69
  20. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.run_gap line 75
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.run_size line 81
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_completeness line 87
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_gap line 93
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_satisfiable_iff line 103
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_size_polynomial line 113
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_size_clause_bound line 120
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.PCPIteration.output_count_gap line 128