OAI/Combinatorics/KMedianRecovery/Algorithms/IntegralRecoverySuccess.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.result_success line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.sampleCount line 60
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.sampleCount_computes line 62
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.raw line 68
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.raw_computes line 69
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.repack line 70
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.repack_computes line 73
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.run line 76
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.run_computes line 77
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.pack line 78
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.count line 80
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.layout line 82
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.layout_raw line 87
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.sampleCount_pack line 99
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.repack_pack line 106
  16. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.run_source line 117
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryIntegralRecovery.Fair.probability_layout line 128