OAI/Combinatorics/KMedianRecovery/Geometry/RoundingArithmetic.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.NatOps.min line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.NatOps.max line 19
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.pack line 32
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.ceil line 33
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.ceil_computes line 35
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.positive line 37
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.positive_computes line 38
  8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRound.positive_pack line 42
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.rational line 46
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryRound.rational_computes line 47
  11. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryRound.rational_pack line 48