OAI/Combinatorics/KMedianRecovery/Geometry/LocalFuel.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.run_input_length line 11
  2. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalSearch.run_word line 15
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.seed line 27
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.seed_computes line 30
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.state line 32
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.state_computes line 34
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.fuelPoly line 43
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.fuel line 45
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.run line 46
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.run_computes line 48
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.pack line 50
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.seed_pack line 52
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.state_pack line 60
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.run_pack line 65
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.fuel_bound line 76
  16. lemma OAI.MetricKMedianRecovery.LocalSearch.executableAnchorFuel_spec line 93
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryLocalAnchor.integral_spec line 118