OAI/Combinatorics/KMedian/Sparse/SparsePreparedLaw.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparsePrepared.requests line 16
  2. def OAI.MetricKMedian.SparsePrepared.total line 20
  3. theorem OAI.MetricKMedian.SparsePrepared.requests_le line 24
  4. theorem OAI.MetricKMedian.SparsePrepared.exact_total line 28
  5. theorem OAI.MetricKMedian.SparsePrepared.total_le line 35
  6. theorem OAI.MetricKMedian.SparsePrepared.total_half line 38
  7. def OAI.MetricKMedian.SparsePrepared.kernel line 43
  8. def OAI.MetricKMedian.SparsePrepared.law line 48
  9. theorem OAI.MetricKMedian.SparsePrepared.length line 55
  10. def OAI.MetricKMedian.SparsePrepared.Spec line 65
  11. theorem OAI.MetricKMedian.SparsePrepared.physical line 73