OAI/Combinatorics/IndependentSets/PCP/Gap.lean

GitHub source file

60 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.minimumRejections line 16
  2. def OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.gap line 18
  3. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.exists_minimizer line 20
  4. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.gap_nonnegative line 24
  5. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.gap_le_one line 26
  6. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.gap_eq_zero_iff line 28
  7. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.le_gap_iff line 31
  8. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.inverse_card_le_gap_of_unsatisfiable line 36
  9. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.one_le_dartCard_mul_gap line 40
  10. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.one_le_size_mul_gap line 46
  11. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_minimumRejections line 53
  12. theorem OAI.IndependentSetsGames.Foundations.PCP.FiniteGraph.Bundle.ofGraph_gap line 57
  13. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.alphabet line 68
  14. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.compositionLoss line 69
  15. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.denominator line 70
  16. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.windowHalf line 71
  17. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.windowSize line 72
  18. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.smoothingScale line 73
  19. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.endpointLength line 74
  20. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.walkLength line 75
  21. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.gain line 77
  22. def OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.cap line 78
  23. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.denominator_positive line 80
  24. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.windowHalf_positive line 83
  25. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.walkLength_positive line 86
  26. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.gain_large line 89
  27. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.cap_positive line 96
  28. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.cap_le_one line 99
  29. theorem OAI.IndependentSetsGames.Foundations.PCP.FinalConstants.composed_gap line 103
  30. abbrev OAI.IndependentSetsGames.Foundations.PCP.RoundTables.BaseTable line 126
  31. opaque OAI.IndependentSetsGames.Foundations.PCP.RoundTables.fixedWalkParameter line 128
  32. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.walkParameter line 131
  33. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.walkParameter_eq line 133
  34. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.alphabet line 136
  35. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.alphabet_positive line 138
  36. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.powered line 142
  37. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.build line 145
  38. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.sizeFactor line 148
  39. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.degree_positive line 151
  40. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.dartFactor_positive line 155
  41. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.sizeFactor_positive line 159
  42. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.powered_vertices line 166
  43. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.powered_darts line 169
  44. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.build_darts_positive line 173
  45. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.build_size_le line 181
  46. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.build_completeness line 208
  47. abbrev OAI.IndependentSetsGames.Foundations.PCP.RoundTables.Input line 217
  48. instance OAI.IndependentSetsGames.Foundations.PCP.RoundTables.(instance at line 219) line 219
  49. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.step line 221
  50. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.initial line 224
  51. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.size line 227
  52. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.Satisfiable line 229
  53. def OAI.IndependentSetsGames.Foundations.PCP.RoundTables.gap line 231
  54. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.size_positive line 233
  55. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.gap_nonnegative line 236
  56. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.gap_eq_zero_iff line 239
  57. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.one_le_size_mul_gap line 242
  58. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.initial_satisfiable_iff line 254
  59. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.step_completeness line 257
  60. theorem OAI.IndependentSetsGames.Foundations.PCP.RoundTables.step_size line 260