OAI/Combinatorics/KMedianRecovery/Machines/LoopInput2.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.dimension_bound line 10
  2. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.entry_length_bound line 13
  3. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.input_height line 19
  4. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.encode_height line 22
  5. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterate_length_bound line 40
  6. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.loopInput line 63
  7. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.loopInput_computes line 64
  8. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.loopOp line 66
  9. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.loopOp_computes line 67
  10. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.loopOp_encode line 71
  11. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.fold_steps line 75
  12. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterationInput line 83
  13. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterationInput_computes line 84
  14. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterateWords line 86
  15. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterateWords_computes line 88
  16. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.iterateWords_encode line 90
  17. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rawDet line 122
  18. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rawDet_computes line 123
  19. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.rawDet_encode line 125
  20. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signOp line 130
  21. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signOp_computes line 132
  22. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.sign_fold line 134
  23. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signRun line 145
  24. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signRun_computes line 146
  25. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signRun_encode line 147
  26. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinantInput line 163
  27. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinantInput_computes line 164
  28. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signedDet line 166
  29. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.signedDet_computes line 167
  30. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinantWords line 168
  31. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinantWords_computes line 170
  32. lemma OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinantWords_encode line 174
  33. def OAI.MetricKMedianRecovery.BitMachine.RationalMatrix.determinant line 189