OAI/Combinatorics/KMedian/Projection/Product.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_sum line 15
2. lemma OAI.MetricKMedian.PCP.BiProjection.push_sum line 35
3. def OAI.MetricKMedian.PCP.BiProjection.prod line 39
4. lemma OAI.MetricKMedian.PCP.BiProjection.prod_source line 53
5. lemma OAI.MetricKMedian.PCP.BiProjection.prod_push line 61
6. def OAI.MetricKMedian.PCP.BiProjection.partialPush line 78
7. lemma OAI.MetricKMedian.PCP.BiProjection.partialPush_nonneg line 84
8. lemma OAI.MetricKMedian.PCP.BiProjection.partialPush_total line 91
9. lemma OAI.MetricKMedian.PCP.BiProjection.prod_collision line 99