OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoveryRepeat.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.counter line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.rword line 11
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.rword_computes line 12
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.bword line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.bword_computes line 15
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.rows line 16
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.rows_computes line 18
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.context line 21
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.context_computes line 22
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.atSeedInput line 23
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.atSeedInput_computes line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.atSeed line 27
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.atSeed_computes line 28
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.candidates line 29
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.candidates_computes line 32
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.run line 35
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.run_computes line 37
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.run_of_candidates line 39
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.output line 48
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.rows_pack line 51
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.candidates_of_rows line 66
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.atSeed_pack line 74
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Repeat.run_source line 79