OAI/Combinatorics/KMedianRecovery/Sampling/SamplerDraw.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.pack line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.input line 14
  3. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.input_computes line 15
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.actions line 16
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.actions_computes line 17
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.weights line 21
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.weights_computes line 23
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.index line 27
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.index_computes line 28
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.run line 31
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.run_computes line 32
  12. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.input_pack line 33
  13. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.actions_pack line 36
  14. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.weights_pack line 42
  15. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Draw.run_pack line 47
  16. lemma OAI.MetricKMedianRecovery.RationalSampling.height_max line 60
  17. lemma OAI.MetricKMedianRecovery.RationalSampling.height_minimum line 64
  18. def OAI.MetricKMedianRecovery.RationalSampling.State.Height line 74
  19. lemma OAI.MetricKMedianRecovery.RationalSampling.State.Height.mono line 75
  20. lemma OAI.MetricKMedianRecovery.RationalSampling.height_nat line 77
  21. lemma OAI.MetricKMedianRecovery.RationalSampling.population_height line 79
  22. lemma OAI.MetricKMedianRecovery.RationalSampling.nearest_height line 92
  23. def OAI.MetricKMedianRecovery.RationalSampling.heightIncrement line 102
  24. lemma OAI.MetricKMedianRecovery.RationalSampling.menu_height line 103
  25. lemma OAI.MetricKMedianRecovery.RationalSampling.retain_height line 126
  26. lemma OAI.MetricKMedianRecovery.RationalSampling.update_height line 131