OAI/Combinatorics/KMedian/Rounding/RationalTaperAffine.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Taper.marginal_piecewise line 12
2. def OAI.MetricKMedian.Taper.aCoef line 22
3. def OAI.MetricKMedian.Taper.bCoef line 24
4. theorem OAI.MetricKMedian.Taper.marginal_affine line 26
5. def OAI.MetricKMedian.Taper.upper line 44
6. def OAI.MetricKMedian.Taper.breakpoints line 46
7. def OAI.MetricKMedian.Taper.A line 49
8. def OAI.MetricKMedian.Taper.B line 51
9. theorem OAI.MetricKMedian.Taper.mass_affine line 53
10. theorem OAI.MetricKMedian.Taper.cuts_in_interval line 60