OAI/Combinatorics/KMedianRecovery/Sampling/SamplingReference.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leafBits line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.pack line 13
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.original line 16
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.original_computes line 18
  5. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.original_pack line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.originals line 23
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.originals_computes line 24
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.originals_pack line 26
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaf line 30
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaf_computes line 35
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaf_pack line 43
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaves line 48
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaves_computes line 50
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.leaves_pack line 53
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.values line 57
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.entries line 60
  17. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.entries_computes line 61
  18. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.entries_pack line 63
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.values_nonempty line 69
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.run line 74
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.run_computes line 75
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingReference.run_pack line 76