OAI/Combinatorics/UniformKServer/PilotCompact.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Local optimality construction.

  1. def OAI.UniformKServer.PilotCompact.bumpB line 14
  2. def OAI.UniformKServer.PilotCompact.bumpA line 15
  3. def OAI.UniformKServer.PilotCompact.gate line 17
  4. def OAI.UniformKServer.PilotCompact.feasible line 18
  5. def OAI.UniformKServer.PilotCompact.integrand line 22
  6. def OAI.UniformKServer.PilotCompact.objective line 25
  7. def OAI.UniformKServer.PilotCompact.value line 27
  8. theorem OAI.UniformKServer.PilotCompact.gate_nonneg line 30
  9. theorem OAI.UniformKServer.PilotCompact.gate_zero line 31
  10. theorem OAI.UniformKServer.PilotCompact.zero_feasible line 33
  11. theorem OAI.UniformKServer.PilotCompact.feasible_upper line 44
  12. theorem OAI.UniformKServer.PilotCompact.feasible_closed_form line 55
  13. theorem OAI.UniformKServer.PilotCompact.feasible_isClosed line 76
  14. theorem OAI.UniformKServer.PilotCompact.feasible_isCompact line 95
  15. theorem OAI.UniformKServer.PilotCompact.objective_continuous line 102
  16. theorem OAI.UniformKServer.PilotCompact.minimum_exists line 107
  17. theorem OAI.UniformKServer.PilotCompact.value_le line 120
  18. theorem OAI.UniformKServer.PilotCompact.bumpB_bounds line 126
  19. theorem OAI.UniformKServer.PilotCompact.bumpA_bounds line 131
  20. theorem OAI.UniformKServer.PilotCompact.gate_eq_zero line 141
  21. theorem OAI.UniformKServer.PilotCompact.bumpB_zero line 147
  22. theorem OAI.UniformKServer.PilotCompact.bumpA_zero line 153
  23. theorem OAI.UniformKServer.PilotCompact.weighted_bumpB line 164
  24. theorem OAI.UniformKServer.PilotCompact.weighted_bumpA line 174
  25. theorem OAI.UniformKServer.PilotCompact.weighted_bumpB_sum line 183
  26. theorem OAI.UniformKServer.PilotCompact.surcharge_sum line 190
  27. theorem OAI.UniformKServer.PilotCompact.integrand_bounds line 209
  28. theorem OAI.UniformKServer.PilotCompact.value_bounds line 225
  29. theorem OAI.UniformKServer.PilotCompact.objective_linear line 248
  30. theorem OAI.UniformKServer.PilotCompact.value_concave line 256
  31. theorem OAI.UniformKServer.PilotCompact.candidate_drift line 269
  32. def OAI.UniformKServer.PilotCompact.ballMass line 296
  33. theorem OAI.UniformKServer.PilotCompact.feasible_mono line 299
  34. theorem OAI.UniformKServer.PilotCompact.erase_feasible line 307
  35. def OAI.UniformKServer.PilotCompact.coefficient line 315
  36. theorem OAI.UniformKServer.PilotCompact.sum_erase_weight line 319
  37. theorem OAI.UniformKServer.PilotCompact.integrand_erase line 328