OAI/Computability/BinPacking/Machines/GraphPackingBounds.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.BinPackingGap.nat_size_mono line 10
  2. theorem OAI.BinPackingGap.nat_size_mul_le line 13
  3. theorem OAI.BinPackingGap.nat_size_pow_succ_le line 19
  4. theorem OAI.BinPackingGap.nat_size_pow_le_of_pos line 30
  5. theorem OAI.BinPackingGap.nat_size_pow_le line 36
  6. theorem OAI.BinPackingGap.nat_size_add_le_max line 42
  7. theorem OAI.BinPackingGap.nat_size_add_le line 56
  8. theorem OAI.BinPackingGap.nat_size_le_self line 61
  9. theorem OAI.BinPackingGap.nat_size_sub_le line 64
  10. theorem OAI.BinPackingGap.nat_size_succ_le line 67
  11. def OAI.BinPackingGap.GraphPackingBounds.repetitionCoefficient line 79
  12. def OAI.BinPackingGap.GraphPackingBounds.binCoefficient line 81
  13. def OAI.BinPackingGap.GraphPackingBounds.widthCoefficient line 83
  14. theorem OAI.BinPackingGap.GraphPackingBounds.one_le_input_square line 87
  15. theorem OAI.BinPackingGap.GraphPackingBounds.input_le_input_square line 90
  16. theorem OAI.BinPackingGap.GraphPackingBounds.constant_le_quadratic line 92
  17. theorem OAI.BinPackingGap.GraphPackingBounds.linear_le_quadratic line 95
  18. theorem OAI.BinPackingGap.GraphPackingBounds.repetitions_le_linear line 99
  19. theorem OAI.BinPackingGap.GraphPackingBounds.bins_le_quadratic line 105
  20. theorem OAI.BinPackingGap.GraphPackingBounds.size_repetitions_le_linear line 123
  21. theorem OAI.BinPackingGap.GraphPackingBounds.size_bin_count_le_quadratic line 128
  22. theorem OAI.BinPackingGap.GraphPackingBounds.size_radix_le_linear line 134
  23. theorem OAI.BinPackingGap.GraphPackingBounds.size_edge_power_le_quadratic line 141
  24. theorem OAI.BinPackingGap.GraphPackingBounds.size_vertex_power_le_linear line 151
  25. theorem OAI.BinPackingGap.GraphPackingBounds.size_geometry_denominator_le_quadratic line 158
  26. theorem OAI.BinPackingGap.GraphPackingBounds.size_size_denominator_le_quadratic line 170
  27. theorem OAI.BinPackingGap.GraphPackingBounds.size_le_scaled_size_denominator line 186
  28. theorem OAI.BinPackingGap.GraphPackingBounds.construction_cost_le_degree_eight line 198