OAI/Combinatorics/KMedian/Sparse/SparseTargetSubset.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparseTargetSubset.initial line 15
  2. theorem OAI.MetricKMedian.SparseTargetSubset.point_initial line 18
  3. theorem OAI.MetricKMedian.SparseTargetSubset.initial_unit line 22
  4. def OAI.MetricKMedian.SparseTargetSubset.vectors line 30
  5. def OAI.MetricKMedian.SparseTargetSubset.law line 33
  6. theorem OAI.MetricKMedian.SparseTargetSubset.integral line 36
  7. theorem OAI.MetricKMedian.SparseTargetSubset.mean line 42
  8. theorem OAI.MetricKMedian.SparseTargetSubset.positive line 52
  9. theorem OAI.MetricKMedian.SparseTargetSubset.subset line 58
  10. theorem OAI.MetricKMedian.SparseTargetSubset.fixed line 65
  11. theorem OAI.MetricKMedian.SparseTargetSubset.count_error line 80
  12. theorem OAI.MetricKMedian.SparseTargetSubset.length line 100