OAI/Combinatorics/KMedian/Projection/Expansion.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_coordinates line 15
2. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_center line 19
3. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_mean_le line 25
4. lemma OAI.MetricKMedian.PCP.MixedNorm.sq_le_uniform line 29
5. def OAI.MetricKMedian.PCP.BiProjection.Expands line 40
6. lemma OAI.MetricKMedian.PCP.BiProjection.collision_le_average line 44
7. lemma OAI.MetricKMedian.PCP.BiProjection.collision_variance line 58
8. lemma OAI.MetricKMedian.PCP.BiProjection.variance_bound line 70