OAI/Combinatorics/KMedian/Geometry/RationalParameterizedHistory.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.FixedBatch.RationalParameters.probabilityQ line 14
2. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.probabilityQ_pos line 16
3. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.probabilityQ_le line 21
4. def OAI.MetricKMedian.FixedBatch.RationalParameters.taperAt line 24
5. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.taperAt_pos line 26
6. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.taperAt_le line 32
7. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.taperAt_error line 38
8. def OAI.MetricKMedian.FixedBatch.RationalParameters.allowance line 42
9. def OAI.MetricKMedian.FixedBatch.RationalParameters.tree line 47
10. theorem OAI.MetricKMedian.FixedBatch.RationalParameters.completed_expectation line 51