OAI/Combinatorics/KMedian/Rounding/RationalTaper.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Taper.rationalMarginal line 12
2. def OAI.MetricKMedian.Taper.rationalMass line 14
3. theorem OAI.MetricKMedian.Taper.cast_rationalMarginal line 17
4. theorem OAI.MetricKMedian.Taper.cast_rationalMass line 22
5. def OAI.MetricKMedian.Taper.rootCandidates line 26
6. def OAI.MetricKMedian.Taper.inverseRadius line 29
7. theorem OAI.MetricKMedian.Taper.rootCandidates_card line 32
8. theorem OAI.MetricKMedian.Taper.inverseRadius_spec line 36
9. theorem OAI.MetricKMedian.Taper.positive_data line 65