OAI/Combinatorics/SharpRamsey/Selection/ScheduledBanks.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SharpLogRamsey.ScheduledBanks.Address line 13
  2. def OAI.SharpLogRamsey.ScheduledBanks.length line 16
  3. def OAI.SharpLogRamsey.ScheduledBanks.cutoff line 19
  4. abbrev OAI.SharpLogRamsey.ScheduledBanks.At line 21
  5. abbrev OAI.SharpLogRamsey.ScheduledBanks.Bank line 23
  6. def OAI.SharpLogRamsey.ScheduledBanks.atLaw line 25
  7. def OAI.SharpLogRamsey.ScheduledBanks.bankLaw line 30
  8. theorem OAI.SharpLogRamsey.ScheduledBanks.integral line 32
  9. def OAI.SharpLogRamsey.ReadyTests.Call.address line 53
  10. def OAI.SharpLogRamsey.ReadyTests.Call.accept line 58
  11. def OAI.SharpLogRamsey.ReadyTests.Call.bankRow line 64
  12. def OAI.SharpLogRamsey.ReadyTests.Call.bankIndex line 70
  13. theorem OAI.SharpLogRamsey.ReadyTests.Call.bank_loss_eq line 77
  14. theorem OAI.SharpLogRamsey.ReadyTests.Call.bank_production_eq line 91
  15. theorem OAI.SharpLogRamsey.ReadyTests.Call.bank_loss_bound line 101
  16. theorem OAI.SharpLogRamsey.ReadyTests.Call.bank_failure_bound line 110