OAI/Computability/VertexCover/PCP/PreprocessingTableSpectral.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.portGraph_ext line 13
  2. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.materialize_portGraph line 21
  3. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.overlay_portGraph line 31
  4. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.overlay_rotation_eq line 41
  5. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.lazy_portGraph line 50
  6. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.lazy_rotation_eq line 58
  7. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.overlay_certificate_seven_eighths line 66
  8. theorem OAI.UniqueGames.Foundations.PCP.PreprocessingTableSpectral.lazy_certificate_31_32 line 82