OAI/Combinatorics/KMedian/Compression/GaussianTabulated.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Gaussian.RatMatrix line 9
2. def OAI.MetricKMedian.Gaussian.values line 11
3. def OAI.MetricKMedian.Gaussian.tabulate line 14
4. theorem OAI.MetricKMedian.Gaussian.values_tabulate line 17
5. def OAI.MetricKMedian.Gaussian.kernelVector line 22
6. theorem OAI.MetricKMedian.Gaussian.kernelVector_eq line 34