OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoveryMachine.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.src line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.src_computes line 12
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.params line 13
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.sampleRaw line 14
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.completeRaw line 15
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.extra line 16
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.sampleRaw_computes line 17
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.completeRaw_computes line 18
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.extra_computes line 19
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.mword line 20
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.mword_computes line 21
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.cfg line 22
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.cfg_computes line 23
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.precision line 24
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.precision_computes line 25
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.sampleContext line 26
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.sampleContext_computes line 28
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.recoveryContext line 31
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.recoveryContext_computes line 34
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.candidateWords line 41
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.candidateWords_computes line 44
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.metricContext line 51
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.metricContext_computes line 52
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.run line 53
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.run_computes line 55
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.pack line 57
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.params_pack line 70
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.data_pack line 72
  29. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.src_pack line 76
  30. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.mword_pack line 79
  31. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.cfg_pack line 83
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.precision_pack line 88
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.sampleContext_pack line 92
  34. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.recoveryContext_pack line 101
  35. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.metricContext_pack line 111
  36. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.start_pack line 114