OAI/Combinatorics/KMedian/Projection/Repeat.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.PCP.Nested line 13
2. instance OAI.MetricKMedian.PCP.Nested.fintype line 17
3. instance OAI.MetricKMedian.PCP.Nested.nonempty line 20
4. lemma OAI.MetricKMedian.PCP.Nested.card line 23
5. def OAI.MetricKMedian.PCP.BiProjection.trivial line 31
6. def OAI.MetricKMedian.PCP.BiProjection.power line 34
7. lemma OAI.MetricKMedian.PCP.BiProjection.collisionBound_power line 44
8. theorem OAI.MetricKMedian.PCP.BiProjection.arbitrarily_small line 54
9. def OAI.MetricKMedian.PCP.BiProjection.Perfect line 59
10. def OAI.MetricKMedian.PCP.BiProjection.Consistent line 61