OAI/Combinatorics/KMedian/Geometry/RationalIntervals.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Preparation.RationalIntervals.height line 11
2. def OAI.MetricKMedian.Preparation.RationalIntervals.previous line 12
3. def OAI.MetricKMedian.Preparation.RationalIntervals.length line 13
4. theorem OAI.MetricKMedian.Preparation.RationalIntervals.height_nonneg line 15
5. theorem OAI.MetricKMedian.Preparation.RationalIntervals.height_eq line 18
6. theorem OAI.MetricKMedian.Preparation.RationalIntervals.previous_lt line 28
7. theorem OAI.MetricKMedian.Preparation.RationalIntervals.length_pos line 34
8. theorem OAI.MetricKMedian.Preparation.RationalIntervals.length_le line 37
9. theorem OAI.MetricKMedian.Preparation.RationalIntervals.previous_erase_max line 40
10. theorem OAI.MetricKMedian.Preparation.RationalIntervals.sum_lengths line 51
11. theorem OAI.MetricKMedian.Preparation.RationalIntervals.previous_filter_le line 79
12. theorem OAI.MetricKMedian.Preparation.RationalIntervals.prefix_sum line 87