OAI/Combinatorics/KMedian/Compression/CompressionBinaryProgram.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.countProgram line 14
2. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.iterateProgram line 18
3. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.Input.compressed line 23
4. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.compressProgram line 27
5. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.RationalInput.compressed line 31
6. def OAI.MetricKMedian.IntegerLaw.BinaryCompression.rationalCompressProgram line 34
7. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.rationalCompress_binary_polytime line 37
8. theorem OAI.MetricKMedian.IntegerLaw.BinaryCompression.rationalCompress_finite_work line 41