OAI/Combinatorics/KMedian/Projection/Rounding.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.BiProjection.score line 18
2. def OAI.MetricKMedian.PCP.BiProjection.Sound line 21
3. def OAI.MetricKMedian.PCP.BiProjection.scalarPush line 23
4. lemma OAI.MetricKMedian.PCP.BiProjection.scalarPush_nonneg line 28
5. lemma OAI.MetricKMedian.PCP.BiProjection.scalarPush_total line 33
6. lemma OAI.MetricKMedian.PCP.BiProjection.fractional_score_reindex line 41
7. lemma OAI.MetricKMedian.PCP.BiProjection.fractional_score_le line 64
8. lemma OAI.MetricKMedian.PCP.BiProjection.scalar_collision_sound line 86
9. lemma OAI.MetricKMedian.PCP.BiProjection.collision_sound line 106