OAI/Combinatorics/KMedianRecovery/Machines/MenuMachine.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.code line 9
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.kind line 10
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.exponent line 11
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.exponent_computes line 12
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.index line 13
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.index_computes line 14
  7. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.index_pair line 15
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.kind_pair line 17
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.relative line 19
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.relative_computes line 20
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.first line 22
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.first_computes line 23
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.weights line 25
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.denominator line 26
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.denominator_computes line 28
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.halfNumerator line 31
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.halfNumerator_computes line 33
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.halfNormalizer line 35
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.halfNormalizer_computes line 37
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.weight line 39
  21. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.weight_computes line 43
  22. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.weight_pair line 53
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.optBits line 68
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.radii line 69
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.denominatorPower line 70
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.denominatorPower_computes line 72
  27. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.divide line 74
  28. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.divide_computes line 76
  29. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.uniformRadius line 77
  30. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.uniformRadius_computes line 79
  31. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.radius line 83
  32. def OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.radius_computes line 87
  33. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryMenu.radius_pair line 92