OAI/Combinatorics/KMedianRecovery/Recovery/IfNat.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.RatOps.ifNatEq line 10
  2. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.variableWord line 21
  3. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.col line 24
  4. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.col_computes line 25
  5. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.row line 27
  6. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.row_computes line 28
  7. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.chooseEq line 30
  8. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.chooseColTag line 35
  9. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.chooseTag line 43
  10. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.chooseActive line 49
  11. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.chooseNear line 55
  12. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.bid line 62
  13. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.bid_computes line 64
  14. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.slack line 66
  15. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.slack_computes line 69
  16. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.dual line 73
  17. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.dual_computes line 76
  18. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.paymentQuery line 79
  19. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.paymentQuery_computes line 80
  20. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.paymentNear line 82
  21. instance OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.paymentNearDecidable line 85
  22. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.paymentNear_computes line 86
  23. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.payment line 107
  24. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.payment_computes line 110
  25. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.coefficient line 120
  26. def OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.coefficient_computes line 139
  27. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.coefficient_indexed line 149
  28. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryOpeningCoefficient.coefficient_source line 180