OAI/Combinatorics/KMedian/Compression/GaussianListCompiler.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Gaussian.ListOperation.er line 17
2. abbrev OAI.MetricKMedian.Gaussian.ListOperation.ers line 18
3. abbrev OAI.MetricKMedian.Gaussian.ListOperation.ef line 19
4. abbrev OAI.MetricKMedian.Gaussian.ListOperation.eu line 20
5. abbrev OAI.MetricKMedian.Gaussian.ListOperation.eslots line 21
6. def OAI.MetricKMedian.Gaussian.ListOperation.pivotProgram line 23
7. def OAI.MetricKMedian.Gaussian.ListOperation.coefficientsProgram line 26
8. def OAI.MetricKMedian.Gaussian.ListOperation.reduceProgram line 36
9. def OAI.MetricKMedian.Gaussian.ListOperation.residualProgram line 56
10. def OAI.MetricKMedian.Gaussian.ListOperation.liftProgram line 65
11. def OAI.MetricKMedian.Gaussian.ListOperation.basisProgram line 75