OAI/Combinatorics/KMedianRecovery/Strictness/SurplusPostprocess.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.pack line 14
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.target line 16
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.target_computes line 18
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.padded line 20
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.padded_computes line 22
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.localInput line 25
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.localInput_computes line 27
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.run line 33
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.run_computes line 34
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.target_pack line 38
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.padded_pack line 43
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.localInput_pack line 48
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySurplusPostprocess.integral_spec line 60
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.pack line 90
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.postInput line 93
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.postInput_computes line 96
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.run line 104
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.run_computes line 105
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCanonicalSurplus.produce line 107