OAI/Combinatorics/BalancedRyser/Local/ReuseScheduleBounds.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Balanced.ReuseSchedule.Schedule line 11
  2. def OAI.Balanced.ReuseSchedule.cost line 13
  3. def OAI.Balanced.ReuseSchedule.listScore line 16
  4. def OAI.Balanced.ReuseSchedule.listCost line 19
  5. theorem OAI.Balanced.ReuseSchedule.listScore_ofFn line 22
  6. theorem OAI.Balanced.ReuseSchedule.listCost_ofFn line 26
  7. theorem OAI.Balanced.ReuseSchedule.cost_eq line 30
  8. theorem OAI.Balanced.ReuseSchedule.cost_le_inverse_cube line 34
  9. theorem OAI.Balanced.ReuseSchedule.count_short_schedules line 40
  10. theorem OAI.Balanced.ReuseSchedule.sum_mass_le_inverse_cube line 45
  11. theorem OAI.Balanced.ReuseSchedule.inverse_cube_constant_pos line 56
  12. theorem OAI.Balanced.ReuseSchedule.listCost_le_inverse_cube line 60
  13. theorem OAI.Balanced.ReuseSchedule.sum_list_mass_le_inverse_cube line 69
  14. theorem OAI.Balanced.ReuseSchedule.sum_high_score_le_reweighted line 83
  15. theorem OAI.Balanced.ReuseSchedule.sum_high_score_masses_le line 100