OAI/Combinatorics/BalancedRyser/Local/ReuseScheduleAggregation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Balanced.ReuseSchedule.score line 10
  2. theorem OAI.Balanced.ReuseSchedule.product_extension_eq line 13
  3. theorem OAI.Balanced.ReuseSchedule.schedule_bound_le line 18
  4. theorem OAI.Balanced.ReuseSchedule.sum_schedule_bounds_le line 33
  5. theorem OAI.Balanced.ReuseSchedule.schedule_count line 48
  6. theorem OAI.Balanced.ReuseSchedule.sum_all_schedule_bounds_le line 51
  7. theorem OAI.Balanced.ReuseSchedule.sum_masses_le line 63
  8. theorem OAI.Balanced.ReuseSchedule.sum_reweighted_costs_le line 80
  9. theorem OAI.Balanced.ReuseSchedule.sum_length_masses_le line 97
  10. theorem OAI.Balanced.ReuseSchedule.aggregate_constant_pos line 104