OAI/Combinatorics/KMedianRecovery/Geometry/RoundingPrecision.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Guided.pathWeight_constant line 11
2. lemma OAI.MetricKMedianRecovery.Guided.eventMass_domination line 17
3. lemma OAI.MetricKMedianRecovery.Guided.hitMass_domination line 32
4. def OAI.MetricKMedianRecovery.Guided.roundingPrecision line 39
5. lemma OAI.MetricKMedianRecovery.Guided.roundingPrecision_spec line 43
6. def OAI.MetricKMedianRecovery.Guided.rounded line 47
7. lemma OAI.MetricKMedianRecovery.Guided.rounded_domination line 52
8. lemma OAI.MetricKMedianRecovery.Guided.rounded_draw line 58
9. lemma OAI.MetricKMedianRecovery.Guided.rounded_hitMass line 64