OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoveryGuesses.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.costWord line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.costWord_computes line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.costRange line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.costRange_computes line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.countRange line 18
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.countRange_computes line 19
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.choices line 21
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.choices_computes line 22
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.source line 23
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.source_computes line 24
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.price line 25
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.price_computes line 26
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.count line 28
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.count_computes line 29
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atParams line 30
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atParams_computes line 32
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atInput line 38
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atInput_computes line 40
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atChoice line 42
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atChoice_computes line 43
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.candidateWords line 45
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.candidateWords_computes line 48
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.sizeWord line 51
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.sizeWord_computes line 52
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.runInput line 54
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.runInput_computes line 57
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.run line 63
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.run_computes line 64
  29. abbrev OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.pack line 67
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.src_pack line 69
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.ranges_pack line 72
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.atInput_pack line 90
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.words line 95
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.candidateWords_pack line 99
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.run_pack line 106
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Guesses.word_mem line 119