OAI/Combinatorics/KMedianRecovery/Encoding/Encode3.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.encode line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.product_le line 11
  3. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.product_length line 20
  4. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.mulOp line 25
  5. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.mulOp_computes line 27
  6. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.fold_mul line 29
  7. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.productWords line 38
  8. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.productWords_computes line 40
  9. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.productWords_encode line 43
  10. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.exponentiate line 60
  11. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.exponentiate_computes line 61
  12. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.exponentiate_pair line 62
  13. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.nextOp line 68
  14. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.nextOp_computes line 69
  15. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.factorialWords line 70
  16. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.factorialWords_computes line 72
  17. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.factorial_list line 80
  18. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.factorialWords_replicate line 84
  19. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.bits_length_log line 92
  20. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.unaryLog line 97
  21. def OAI.MetricKMedianRecovery.BitMachine.NaturalArray.unaryLog_computes line 99
  22. lemma OAI.MetricKMedianRecovery.BitMachine.NaturalArray.unaryLog_bits line 104