OAI/Combinatorics/KMedian/Hardness/Lists.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Coverage.ProjectionSystem.DuplicateConsistent line 17
  2. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.consistent_of_injective line 22
  3. def OAI.MetricKMedian.Coverage.ProjectionSystem.agreement line 27
  4. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.mem_agreement line 33
  5. def OAI.MetricKMedian.Coverage.ProjectionSystem.heavyHit line 38
  6. def OAI.MetricKMedian.Coverage.ProjectionSystem.lowBad line 41
  7. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.heavy_bound line 44
  8. def OAI.MetricKMedian.Coverage.ProjectionSystem.cappedLabels line 62
  9. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.capped_nonempty line 66
  10. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.capped_card line 74
  11. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.mem_capped line 82
  12. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.lowBad_bound line 89
  13. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.bad_bound line 129
  14. theorem OAI.MetricKMedian.Coverage.ProjectionSystem.coverage_agreement_bound line 157