OAI/Combinatorics/KMedianRecovery/Sampling/SamplerContext.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.config line 11
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.c line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.c_computes line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.deleted line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.leaves line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.deleted_computes line 18
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.leaves_computes line 19
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.undeleted line 20
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.undeleted_computes line 21
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.reference line 22
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.reference_computes line 23
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.oracle line 25
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.oracle_computes line 26
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.reference_pair line 28
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.oracle_pair line 32
  16. def OAI.MetricKMedianRecovery.Dyadic.Canonical.select line 41
  17. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.select_sum line 44
  18. def OAI.MetricKMedianRecovery.Dyadic.Canonical.list line 70
  19. def OAI.MetricKMedianRecovery.Dyadic.Canonical.draw line 71
  20. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.list_sum line 74
  21. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.draw_average line 79
  22. def OAI.MetricKMedianRecovery.Dyadic.Canonical.rank line 109
  23. def OAI.MetricKMedianRecovery.Dyadic.Canonical.findRank line 112
  24. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.findRank_eq line 114
  25. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.select_relabel line 134
  26. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.rank_select line 141
  27. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.rank_select_zero line 155
  28. lemma OAI.MetricKMedianRecovery.Dyadic.Canonical.select_index line 158