OAI/Combinatorics/KMedian/Compression/IntegerKernelProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.Row line 13
2. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.Rows line 14
3. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.er line 15
4. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.em line 16
5. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.ed line 17
6. structure OAI.MetricKMedian.Gaussian.IntegerProgram.Input line 19
7. def OAI.MetricKMedian.Gaussian.IntegerProgram.Input.raw line 25
8. abbrev OAI.MetricKMedian.Gaussian.IntegerProgram.Input.encode line 27
9. def OAI.MetricKMedian.Gaussian.IntegerProgram.Input.rational line 29
10. def OAI.MetricKMedian.Gaussian.IntegerProgram.castRows line 31
11. theorem OAI.MetricKMedian.Gaussian.IntegerProgram.castRows_ofFn line 33
12. def OAI.MetricKMedian.Gaussian.IntegerProgram.rationalProgram line 37
13. def OAI.MetricKMedian.Gaussian.IntegerProgram.Input.result line 45
14. def OAI.MetricKMedian.Gaussian.IntegerProgram.kernelProgram line 47