OAI/Combinatorics/KMedianRecovery/Sampling/InverseCDF.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.prefixCounts line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.prefix_computes line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.total line 17
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.total_computes line 19
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.predicate line 20
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.predicate_computes line 23
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.predicate_pack line 25
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.find line 32
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.find_computes line 34
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.encodeOption line 36
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.find_pack line 39
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.pack line 52
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.searched line 53
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.searched_computes line 54
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.run line 57
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.run_computes line 58
  17. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryInverseCDF.run_pack line 62
  18. def OAI.MetricKMedianRecovery.BitMachine.RatOps.natFloor line 69
  19. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.bits_two_pow line 78
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.power line 82
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.power_computes line 83
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.power_replicate line 88
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.scale line 90
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.scale_computes line 91
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.scale_replicate line 92
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.count line 94
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.count_computes line 96
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.count_pack line 98
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.pack line 102
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.counts line 104
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.counts_computes line 106
  32. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.counts_pack line 110
  33. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.prepared line 114
  34. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.prepared_computes line 115
  35. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.run line 117
  36. def OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.run_computes line 118
  37. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.run_pack line 119
  38. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.floor_cast line 125
  39. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryDyadic.rawCount_cast line 127