OAI/Combinatorics/KMedianRecovery/Recovery/RecoveryEnumeration.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atBranch line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atBranch_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.promote line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.promote_computes line 17
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atZero line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.atZero_computes line 20
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.range line 22
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.range_computes line 23
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.blueRange line 24
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.blueRange_computes line 25
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.choices line 26
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.choices_computes line 27
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.candidateWords line 29
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.candidateWords_computes line 32
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.metricContext line 37
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.metricContext_computes line 38
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.run line 39
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.run_computes line 42
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.range_pack line 48
  20. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.blueRange_pack line 51
  21. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.choices_pack line 54
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.candidateWords_pack line 58
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.metricContext_pack line 64
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRecovery.run_of_candidates line 67