OAI/Computability/VertexCover/PCP/ExpanderTables.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.rowIndex line 12
  2. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.rowIndex_val line 14
  3. structure OAI.UniqueGames.Foundations.PCP.ExpanderTables.Table line 17
  4. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.reverseIndex line 21
  5. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.lookup line 24
  6. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.lookup_involutive line 27
  7. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.graph line 34
  8. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.graph_rot line 38
  9. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.ofGraph line 41
  10. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.lookup_ofGraph line 49
  11. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.graph_ext line 54
  12. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.graph_ofGraph line 62
  13. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.row_count line 65
  14. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.vertexIndex line 68
  15. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.stepGraph line 71
  16. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.step line 79
  17. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.stepLookup line 83
  18. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.lookup_step line 97
  19. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.step_certificate line 109
  20. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.initial line 120
  21. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.initial_certificate line 123
  22. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.vertexCount line 133
  23. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.vertexCount_eq line 137
  24. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.vertexCount_positive line 142
  25. def OAI.UniqueGames.Foundations.PCP.ExpanderTables.family line 147
  26. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.family_certificate line 152
  27. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.family_row_count line 163
  28. theorem OAI.UniqueGames.Foundations.PCP.ExpanderTables.exists_base_table line 167