OAI/Combinatorics/KMedianRecovery/Sampling/SamplerParameters.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.M line 12
  2. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.E line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.thirdSize_eq line 14
  4. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.pack line 18
  5. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.bound line 21
  6. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.unary line 22
  7. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.unary_computes line 24
  8. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.Jword line 26
  9. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.Jword_computes line 27
  10. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.nword line 29
  11. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.nword_computes line 30
  12. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.precision line 31
  13. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.precision_computes line 33
  14. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.menus line 36
  15. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.menus_computes line 37
  16. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.dimension line 39
  17. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.dimension_computes line 40
  18. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.diameter line 41
  19. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.diameter_computes line 42
  20. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.run line 43
  21. def OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.run_computes line 45
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.pack_resources line 61
  23. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.unary_pack line 73
  24. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.Jword_pack line 83
  25. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.precision_pack line 93
  26. lemma OAI.MetricKMedianRecovery.BitMachine.BinarySampler.Parameters.run_pack line 100