OAI/Combinatorics/KMedianRecovery/Machines/StartResources.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.RationalLeaves.BankBound.empty line 12
  2. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.StartOutput.Resources line 20
  3. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initial_resources line 25
  4. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.start_resources line 30
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.ctx line 62
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.bf line 63
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.bf_computes line 64
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.atPrice line 66
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.atPrice_computes line 68
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.atPrice_pack line 74
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.history line 80
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.history_computes line 82
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.history_pack line 85
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.opened line 93
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.opened_computes line 94
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.count line 96
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.count_computes line 97
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.count_pack line 98
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInitialQuery.search_pack line 112