OAI/Combinatorics/KMedian/Projection/Bound.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedian.PCP.MixedNorm.selected_le line 15
  2. def OAI.MetricKMedian.PCP.BiProjection.CollisionBound line 29
  3. lemma OAI.MetricKMedian.PCP.BiProjection.collisionBound_of_expansion line 33
  4. lemma OAI.MetricKMedian.PCP.BiProjection.collisionBound_one line 42
  5. lemma OAI.MetricKMedian.PCP.BiProjection.score_nonneg line 50
  6. def OAI.MetricKMedian.PCP.BiProjection.pointLabel line 54
  7. lemma OAI.MetricKMedian.PCP.BiProjection.pointLabel_nonneg line 56
  8. lemma OAI.MetricKMedian.PCP.BiProjection.pointLabel_total line 61
  9. lemma OAI.MetricKMedian.PCP.BiProjection.score_eq_push line 65
  10. lemma OAI.MetricKMedian.PCP.BiProjection.score_sq_le_collision line 73
  11. lemma OAI.MetricKMedian.PCP.BiProjection.sound_of_collisionBound line 83