OAI/Computability/BinPacking/Hardness/PCPPackingGap.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.BinPackingGap.PCPFoundation.gap line 23
  2. def OAI.BinPackingGap.PCPFoundation.rho line 25
  3. theorem OAI.BinPackingGap.PCPFoundation.gap_pos line 27
  4. theorem OAI.BinPackingGap.PCPFoundation.gap_cast_pos line 29
  5. theorem OAI.BinPackingGap.PCPFoundation.rho_pos line 31
  6. theorem OAI.BinPackingGap.PCPFoundation.rho_lt_gap_third line 33
  7. def OAI.BinPackingGap.PCPFoundation.formula line 37
  8. def OAI.BinPackingGap.PCPFoundation.graph line 39
  9. def OAI.BinPackingGap.PCPFoundation.target line 41
  10. theorem OAI.BinPackingGap.PCPFoundation.formula_nonempty line 43
  11. theorem OAI.BinPackingGap.PCPFoundation.clause_count_pos line 46
  12. theorem OAI.BinPackingGap.PCPFoundation.edges_nonempty line 49
  13. theorem OAI.BinPackingGap.PCPFoundation.target_le_vertices line 52
  14. theorem OAI.BinPackingGap.PCPFoundation.cover_complete line 56
  15. theorem OAI.BinPackingGap.PCPFoundation.failedCount_eq_card line 61
  16. theorem OAI.BinPackingGap.PCPFoundation.realGapOfRatGap line 66
  17. theorem OAI.BinPackingGap.PCPFoundation.realCountBound line 70
  18. theorem OAI.BinPackingGap.PCPFoundation.normalized_failed_gap line 74
  19. theorem OAI.BinPackingGap.PCPFoundation.cover_bound_from_failed_gap line 82
  20. theorem OAI.BinPackingGap.PCPFoundation.cover_sound line 95
  21. theorem OAI.BinPackingGap.PCPFoundation.no_small_cover line 100
  22. theorem OAI.BinPackingGap.PCPFoundation.normalizedSource line 113
  23. def OAI.BinPackingGap.PCPFoundation.graphInput line 134
  24. def OAI.BinPackingGap.PCPFoundation.packingOutput line 140
  25. theorem OAI.BinPackingGap.PCPFoundation.packingOutput_valid line 143
  26. theorem OAI.BinPackingGap.PCPFoundation.packingOutput_count line 147
  27. theorem OAI.BinPackingGap.PCPFoundation.packingOutput_size_lower line 151
  28. theorem OAI.BinPackingGap.PCPFoundation.packingOutput_complete line 156
  29. theorem OAI.BinPackingGap.PCPFoundation.packingOutput_sound line 163