OAI/Computability/VertexCover/PCP/FinalConstants.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.UniqueGames.Foundations.PCP.FinalConstants.alphabet line 10
  2. def OAI.UniqueGames.Foundations.PCP.FinalConstants.compositionLoss line 11
  3. def OAI.UniqueGames.Foundations.PCP.FinalConstants.denominator line 12
  4. def OAI.UniqueGames.Foundations.PCP.FinalConstants.windowHalf line 13
  5. def OAI.UniqueGames.Foundations.PCP.FinalConstants.windowSize line 14
  6. def OAI.UniqueGames.Foundations.PCP.FinalConstants.smoothingScale line 15
  7. def OAI.UniqueGames.Foundations.PCP.FinalConstants.endpointLength line 16
  8. def OAI.UniqueGames.Foundations.PCP.FinalConstants.walkLength line 17
  9. def OAI.UniqueGames.Foundations.PCP.FinalConstants.gain line 19
  10. def OAI.UniqueGames.Foundations.PCP.FinalConstants.cap line 20
  11. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.denominator_positive line 22
  12. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.windowHalf_positive line 25
  13. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.walkLength_positive line 28
  14. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.gain_large line 31
  15. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.cap_positive line 38
  16. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.cap_le_one line 41
  17. theorem OAI.UniqueGames.Foundations.PCP.FinalConstants.composed_gap line 45