OAI/Computability/VertexCover/PCP/CloudRounding.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.dart_rejection_count_le line 12
  2. def OAI.UniqueGames.Foundations.PCP.CloudRounding.colorSet line 61
  3. def OAI.UniqueGames.Foundations.PCP.CloudRounding.minoritySet line 64
  4. def OAI.UniqueGames.Foundations.PCP.CloudRounding.directedCut line 67
  5. def OAI.UniqueGames.Foundations.PCP.CloudRounding.disagreementSet line 70
  6. abbrev OAI.UniqueGames.Foundations.PCP.CloudRounding.Nonmajor line 73
  7. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.exists_max_color line 76
  8. def OAI.UniqueGames.Foundations.PCP.CloudRounding.majority line 83
  9. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.majority_maximal line 87
  10. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.nonchosen_color_twice_le line 93
  11. def OAI.UniqueGames.Foundations.PCP.CloudRounding.minorityEquiv line 112
  12. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.minority_card_eq_sum line 129
  13. def OAI.UniqueGames.Foundations.PCP.CloudRounding.minorityCutEmbedding line 134
  14. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.minority_cut_sum_le line 160
  15. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.minority_expansion_bound line 167
  16. def OAI.UniqueGames.Foundations.PCP.CloudRounding.mismatchSet line 197
  17. def OAI.UniqueGames.Foundations.PCP.CloudRounding.copiedRejectionCount line 201
  18. def OAI.UniqueGames.Foundations.PCP.CloudRounding.innerDisagreementSet line 204
  19. def OAI.UniqueGames.Foundations.PCP.CloudRounding.roundLabels line 208
  20. def OAI.UniqueGames.Foundations.PCP.CloudRounding.mismatchFiberEquiv line 212
  21. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.mismatch_card_eq_sum line 230
  22. def OAI.UniqueGames.Foundations.PCP.CloudRounding.disagreementFiberEquiv line 237
  23. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.disagreement_card_eq_sum line 259
  24. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.rounded_mismatch_expansion line 267
  25. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.rounded_endpoint_bound line 284
  26. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.copied_satisfied_inl line 291
  27. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.copied_satisfied_inr line 297
  28. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.replacement_rejection_split line 304
  29. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.replacement_soundness line 316
  30. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.padded_replacement_soundness line 332
  31. theorem OAI.UniqueGames.Foundations.PCP.CloudRounding.combine_counts line 347