OAI/Combinatorics/KMedianRecovery/Branching/BlueTableSize.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueSize.states_bounds line 9
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueSize.table_length line 20
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueSize.tableRun_best_bound line 54
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.pack line 78
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.statePack line 82
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.oldTable line 86
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.oldTable_computes line 87
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.oldBest line 88
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.oldBest_computes line 89
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.nextCtx line 90
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.nextCtx_computes line 92
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.newTable line 95
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.newTable_computes line 96
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.newBest line 100
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.newBest_computes line 102
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.step line 105
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.step_computes line 106
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.step_pack line 107
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.iterate_pack line 123
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.initial line 132
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.initial_computes line 133
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.initial_pack line 137
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.capPoly line 141
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.cap line 142
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.iterate_length line 143
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.loop line 155
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.loop_computes line 157
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.loop_pack line 159
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.run line 169
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.run_computes line 170
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryBlueLoop.run_pack line 174