OAI/Combinatorics/KMedian/Geometry/NearestFillingFormula.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.Preparation.before line 13
2. instance OAI.MetricKMedian.Preparation.(instance at line 14) line 14
3. def OAI.MetricKMedian.Preparation.priorMass line 15
4. theorem OAI.MetricKMedian.Preparation.first_before line 18
5. theorem OAI.MetricKMedian.Preparation.not_before_first line 25
6. theorem OAI.MetricKMedian.Preparation.priorMass_first line 31
7. theorem OAI.MetricKMedian.Preparation.priorMass_erase line 37
8. theorem OAI.MetricKMedian.Preparation.priorMass_nonneg line 46
9. theorem OAI.MetricKMedian.Preparation.fill_formula line 50
10. theorem OAI.MetricKMedian.Preparation.computedNearest_formula line 91