OAI/Computability/VertexCover/Analysis/GridCentralCard.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.VertexCover.FiniteAntiConcentration.subsetSum line 43
  2. def OAI.VertexCover.FiniteAntiConcentration.intervalFamily line 45
  3. theorem OAI.VertexCover.FiniteAntiConcentration.subsetSum_increase line 49
  4. theorem OAI.VertexCover.FiniteAntiConcentration.interval_card_le line 59
  5. def OAI.VertexCover.FiniteAntiConcentration.choices line 98
  6. theorem OAI.VertexCover.FiniteAntiConcentration.choices_eq line 101
  7. theorem OAI.VertexCover.FiniteAntiConcentration.choice_card_le line 113
  8. def OAI.VertexCover.FiniteAntiConcentration.toggleEquiv line 127
  9. def OAI.VertexCover.FiniteAntiConcentration.orderedChoice line 141
  10. def OAI.VertexCover.FiniteAntiConcentration.rawChoice line 145
  11. theorem OAI.VertexCover.FiniteAntiConcentration.orderedChoice_eq line 149
  12. def OAI.VertexCover.FiniteAntiConcentration.coordinateShift line 162
  13. theorem OAI.VertexCover.FiniteAntiConcentration.rawChoice_eq line 166
  14. theorem OAI.VertexCover.FiniteAntiConcentration.sum_orderedChoices line 172
  15. def OAI.VertexCover.FiniteAntiConcentration.grid line 190
  16. def OAI.VertexCover.FiniteAntiConcentration.gridShift line 193
  17. theorem OAI.VertexCover.FiniteAntiConcentration.grid_gap line 196
  18. theorem OAI.VertexCover.FiniteAntiConcentration.grid_ordered_gap line 219
  19. theorem OAI.VertexCover.FiniteAntiConcentration.grid_neg line 226
  20. theorem OAI.VertexCover.FiniteAntiConcentration.grid_interval_card line 232
  21. theorem OAI.VertexCover.FiniteAntiConcentration.symmetric_tail_count line 266
  22. theorem OAI.VertexCover.FiniteAntiConcentration.grid_tail_count line 297
  23. theorem OAI.VertexCover.FiniteAntiConcentration.grid_central_card line 313