OAI/Combinatorics/KMedian/Geometry/BoundFreeCompression.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.IntegerLaw.exists_feature_bound line 10
2. def OAI.MetricKMedian.IntegerLaw.compressionStepAuto line 24
3. theorem OAI.MetricKMedian.IntegerLaw.compressionStepAuto_eq line 36
4. def OAI.MetricKMedian.IntegerLaw.compressStepsAuto line 41
5. theorem OAI.MetricKMedian.IntegerLaw.compressStepsAuto_eq line 47
6. def OAI.MetricKMedian.IntegerLaw.compressAuto line 58
7. theorem OAI.MetricKMedian.IntegerLaw.compressAuto_eq line 62
8. theorem OAI.MetricKMedian.IntegerLaw.compressAuto_spec line 69
9. theorem OAI.MetricKMedian.IntegerLaw.exists_rational_feature_bound line 80
10. theorem OAI.MetricKMedian.IntegerLaw.compressAuto_correct line 90