OAI/Computability/VertexCover/PCP/Expanders.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.Expanders.Generators line 18
  2. def OAI.UniqueGames.Foundations.PCP.Expanders.badFrequency line 20
  3. def OAI.UniqueGames.Foundations.PCP.Expanders.badMass line 24
  4. theorem OAI.UniqueGames.Foundations.PCP.Expanders.badFrequency_nonnegative line 27
  5. theorem OAI.UniqueGames.Foundations.PCP.Expanders.mean_badFrequency_le line 32
  6. theorem OAI.UniqueGames.Foundations.PCP.Expanders.mean_badMass_le line 44
  7. theorem OAI.UniqueGames.Foundations.PCP.Expanders.exists_generators line 56
  8. def OAI.UniqueGames.Foundations.PCP.Expanders.baseDimension line 77
  9. def OAI.UniqueGames.Foundations.PCP.Expanders.initialDegree line 78
  10. def OAI.UniqueGames.Foundations.PCP.Expanders.initialQuarterDegree line 79
  11. def OAI.UniqueGames.Foundations.PCP.Expanders.basePower line 80
  12. theorem OAI.UniqueGames.Foundations.PCP.Expanders.base_arithmetic line 82
  13. theorem OAI.UniqueGames.Foundations.PCP.Expanders.exists_initial_generators line 94
  14. abbrev OAI.UniqueGames.Foundations.PCP.Expanders.BaseVertex line 100
  15. abbrev OAI.UniqueGames.Foundations.PCP.Expanders.BasePort line 101
  16. def OAI.UniqueGames.Foundations.PCP.Expanders.baseDegree line 102
  17. theorem OAI.UniqueGames.Foundations.PCP.Expanders.card_basePort line 104
  18. theorem OAI.UniqueGames.Foundations.PCP.Expanders.card_baseVertex line 109
  19. theorem OAI.UniqueGames.Foundations.PCP.Expanders.exists_baseGraph line 113