OAI/Combinatorics/KMedian/Programs/RationalFeatureProgram.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.QRow line 12
2. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.QRows line 13
3. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.eqr line 14
4. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.eqm line 15
5. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.QData line 16
6. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.eqd line 17
7. structure OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput line 19
8. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.lawData line 25
9. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.features line 26
10. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.raw line 27
11. abbrev OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.encode line 28
12. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.scaledRows line 30
13. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.scaledRows_raw line 35
14. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.scaledRowsProgram line 47
15. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.integer line 57
16. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.integerInputProgram line 59