OAI/Combinatorics/IndependentSets/Expansion/Regularization.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.IndependentSetsGames.Foundations.PCP.Regularization.Vertex line 17
  2. abbrev OAI.IndependentSetsGames.Foundations.PCP.Regularization.Port line 18
  3. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.degree line 20
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.degree_eq line 22
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.degree_positive line 25
  6. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.cloudEquiv line 27
  7. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.cloudGraph line 33
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.cloudGraph_of_pos line 44
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.cloudGraph_certificate_of_pos line 52
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.cloud_expansion line 60
  11. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.portGraph line 75
  12. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.graph line 78
  13. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.graph_tail line 83
  14. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.graph_reverse line 87
  15. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.degreeEquiv line 90
  16. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.fixed_degree line 102
  17. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.vertex_count_le line 107
  18. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.dart_count line 112
  19. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.dart_count_le line 117
  20. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.liftLabel line 127
  21. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.lift_rejectionCount line 131
  22. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.completeness line 136
  23. def OAI.IndependentSetsGames.Foundations.PCP.Regularization.roundLabels line 141
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.soundness line 144
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.exists_rounding line 149
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.Regularization.soundness_of_uniform_lower_bound line 153