OAI/Computability/VertexCover/PCP/Regularization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.UniqueGames.Foundations.PCP.Regularization.Vertex line 19
  2. abbrev OAI.UniqueGames.Foundations.PCP.Regularization.Port line 20
  3. def OAI.UniqueGames.Foundations.PCP.Regularization.degree line 22
  4. theorem OAI.UniqueGames.Foundations.PCP.Regularization.degree_eq line 24
  5. theorem OAI.UniqueGames.Foundations.PCP.Regularization.degree_positive line 27
  6. def OAI.UniqueGames.Foundations.PCP.Regularization.cloudEquiv line 29
  7. def OAI.UniqueGames.Foundations.PCP.Regularization.cloudGraph line 35
  8. theorem OAI.UniqueGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 46
  9. theorem OAI.UniqueGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 54
  10. theorem OAI.UniqueGames.Foundations.PCP.Regularization.cloud_expansion line 63
  11. def OAI.UniqueGames.Foundations.PCP.Regularization.portGraph line 78
  12. def OAI.UniqueGames.Foundations.PCP.Regularization.graph line 81
  13. theorem OAI.UniqueGames.Foundations.PCP.Regularization.graph_tail line 86
  14. theorem OAI.UniqueGames.Foundations.PCP.Regularization.graph_reverse line 90
  15. def OAI.UniqueGames.Foundations.PCP.Regularization.degreeEquiv line 93
  16. theorem OAI.UniqueGames.Foundations.PCP.Regularization.fixed_degree line 105
  17. theorem OAI.UniqueGames.Foundations.PCP.Regularization.vertex_count_le line 110
  18. theorem OAI.UniqueGames.Foundations.PCP.Regularization.dart_count line 115
  19. theorem OAI.UniqueGames.Foundations.PCP.Regularization.dart_count_le line 120
  20. def OAI.UniqueGames.Foundations.PCP.Regularization.liftLabel line 130
  21. theorem OAI.UniqueGames.Foundations.PCP.Regularization.lift_rejectionCount line 135
  22. theorem OAI.UniqueGames.Foundations.PCP.Regularization.completeness line 140
  23. def OAI.UniqueGames.Foundations.PCP.Regularization.roundLabels line 145
  24. theorem OAI.UniqueGames.Foundations.PCP.Regularization.soundness line 148
  25. theorem OAI.UniqueGames.Foundations.PCP.Regularization.exists_rounding line 153
  26. theorem OAI.UniqueGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 157