OAI/Combinatorics/UniformKServer/PilotDeletion.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.UniformKServer.PilotCompact.objective_erase line 9
  2. theorem OAI.UniformKServer.PilotCompact.normalized_triangle line 25
  3. theorem OAI.UniformKServer.PilotCompact.bumpA_inner_lower line 31
  4. theorem OAI.UniformKServer.PilotCompact.bumpB_outer_bound line 50
  5. theorem OAI.UniformKServer.PilotCompact.coefficient_lower line 62
  6. theorem OAI.UniformKServer.PilotCompact.middle_site_zero line 82
  7. def OAI.UniformKServer.PilotCompact.innerMoment line 117
  8. def OAI.UniformKServer.PilotCompact.insertUnit line 120
  9. theorem OAI.UniformKServer.PilotCompact.gate_one line 124
  10. theorem OAI.UniformKServer.PilotCompact.insertUnit_at line 130
  11. theorem OAI.UniformKServer.PilotCompact.insertUnit_nonneg line 134
  12. theorem OAI.UniformKServer.PilotCompact.insertUnit_le line 140
  13. theorem OAI.UniformKServer.PilotCompact.insertUnit_positive line 147
  14. theorem OAI.UniformKServer.PilotCompact.insertUnit_feasible line 156
  15. theorem OAI.UniformKServer.PilotCompact.bumpB_one line 206
  16. def OAI.UniformKServer.PilotCompact.nearWeight line 211
  17. theorem OAI.UniformKServer.PilotCompact.inner_bump_sum line 214
  18. theorem OAI.UniformKServer.PilotCompact.nearWeight_bounds line 232
  19. theorem OAI.UniformKServer.PilotCompact.old_inner_lower line 242
  20. theorem OAI.UniformKServer.PilotCompact.new_inner_upper line 254
  21. theorem OAI.UniformKServer.PilotCompact.unchanged_outside line 296
  22. theorem OAI.UniformKServer.PilotCompact.innerMoment_bounds line 324