OAI/Combinatorics/KMedianRecovery/Sampling/SamplingPotential.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.RationalSampling.State.initial line 10
  2. def OAI.MetricKMedianRecovery.RationalSampling.State.Bounded line 11
  3. lemma OAI.MetricKMedianRecovery.RationalSampling.initial_height line 12
  4. lemma OAI.MetricKMedianRecovery.RationalSampling.initial_bounded line 13
  5. lemma OAI.MetricKMedianRecovery.RationalSampling.retain_bounded line 14
  6. lemma OAI.MetricKMedianRecovery.RationalSampling.update_bounded line 19
  7. lemma OAI.MetricKMedianRecovery.RationalSampling.fold_height line 39
  8. lemma OAI.MetricKMedianRecovery.RationalSampling.fold_bounded line 57
  9. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.finset_length line 68
  10. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.leaf_length line 76
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.leaves_length line 81
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.encode_length line 91
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySamplingState.option_length line 97
  14. def OAI.MetricKMedianRecovery.RationalSampling.next line 111
  15. lemma OAI.MetricKMedianRecovery.RationalSampling.next_height line 115
  16. lemma OAI.MetricKMedianRecovery.RationalSampling.fold_next_height line 124
  17. lemma OAI.MetricKMedianRecovery.RationalSampling.fold_next_bounded line 136
  18. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.context line 149
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.input line 150
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.input_computes line 151
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.drawInput line 153
  22. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.drawInput_computes line 155
  23. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.step line 159
  24. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.step_computes line 160
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Loop.step_pack line 161