OAI/Combinatorics/KMedian/Projection/Operator.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.PCP.BiProjection line 13
  2. def OAI.MetricKMedian.PCP.ProjectionMass.push line 19
  3. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_total line 21
  4. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_nonneg line 27
  5. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_sub line 31
  6. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_abs line 40
  7. lemma OAI.MetricKMedian.PCP.ProjectionMass.push_sq_sum line 47
  8. def OAI.MetricKMedian.PCP.BiProjection.source line 67
  9. def OAI.MetricKMedian.PCP.BiProjection.average line 68
  10. def OAI.MetricKMedian.PCP.BiProjection.push line 69
  11. def OAI.MetricKMedian.PCP.BiProjection.collision line 71
  12. lemma OAI.MetricKMedian.PCP.BiProjection.source_expect line 75
  13. lemma OAI.MetricKMedian.PCP.BiProjection.average_mean line 81
  14. lemma OAI.MetricKMedian.PCP.BiProjection.push_nonneg line 88
  15. lemma OAI.MetricKMedian.PCP.BiProjection.push_sub line 95
  16. lemma OAI.MetricKMedian.PCP.BiProjection.push_total line 102
  17. lemma OAI.MetricKMedian.PCP.BiProjection.collision_le_abs_total line 109
  18. lemma OAI.MetricKMedian.PCP.BiProjection.collision_nonneg line 142