OAI/Combinatorics/KMedianRecovery/Branching/PopulationMachine.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.near line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.near_computes line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.count line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.count_computes line 15
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.count_pack line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidate line 21
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidate_computes line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.pack line 30
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidateQ line 32
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidate_pack line 34
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidates line 38
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidates_computes line 40
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.radiusQ line 42
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.candidates_pack line 43
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.run line 49
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.run_computes line 50
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryPopulation.run_pack line 51