OAI/Computability/VertexCover/PCP/Preprocessing.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.Preprocessing.Vertex line 20
  2. abbrev OAI.UniqueGames.Foundations.PCP.Preprocessing.OverlayPort line 21
  3. abbrev OAI.UniqueGames.Foundations.PCP.Preprocessing.Port line 22
  4. def OAI.UniqueGames.Foundations.PCP.Preprocessing.degree line 24
  5. def OAI.UniqueGames.Foundations.PCP.Preprocessing.sizeFactor line 25
  6. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.card_lazy_sum line 27
  7. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.doubled_add line 32
  8. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.degree_eq_card line 34
  9. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.degree_positive line 43
  10. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.sizeFactor_positive line 47
  11. def OAI.UniqueGames.Foundations.PCP.Preprocessing.paddedGraph line 52
  12. def OAI.UniqueGames.Foundations.PCP.Preprocessing.overlayExpander line 56
  13. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.overlayExpander_certificate line 63
  14. def OAI.UniqueGames.Foundations.PCP.Preprocessing.overlayGraph line 67
  15. def OAI.UniqueGames.Foundations.PCP.Preprocessing.graph line 71
  16. def OAI.UniqueGames.Foundations.PCP.Preprocessing.portGraph line 75
  17. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.graph_tail line 79
  18. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.graph_reverse line 82
  19. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.accepts_reverse line 86
  20. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.portGraph_eq_lazyGraph line 91
  21. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.overlayGraph_certificate line 95
  22. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.spectral_certificate line 105
  23. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.vertex_count_le line 112
  24. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.dart_count line 122
  25. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.dart_count_le line 128
  26. def OAI.UniqueGames.Foundations.PCP.Preprocessing.liftLabel line 136
  27. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.lift_rejectionCount line 142
  28. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.completeness line 154
  29. def OAI.UniqueGames.Foundations.PCP.Preprocessing.roundLabels line 161
  30. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.soundness line 166
  31. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.satisfiable_iff line 179
  32. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.gap_transfer line 191
  33. theorem OAI.UniqueGames.Foundations.PCP.Preprocessing.gap_transfer_real line 207