OAI/Combinatorics/KMedian/Sparse/SparseSignedPreparation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseSignedPreparation.State line 14
  2. def OAI.MetricKMedian.SparseSignedPreparation.kernel line 16
  3. def OAI.MetricKMedian.SparseSignedPreparation.signed line 21
  4. def OAI.MetricKMedian.SparseSignedPreparation.law line 24
  5. theorem OAI.MetricKMedian.SparseSignedPreparation.kernel_nominal line 32
  6. theorem OAI.MetricKMedian.SparseSignedPreparation.kernel_nominal_pair line 38
  7. theorem OAI.MetricKMedian.SparseSignedPreparation.kernel_target line 45
  8. theorem OAI.MetricKMedian.SparseSignedPreparation.kernel_target_pair line 57
  9. theorem OAI.MetricKMedian.SparseSignedPreparation.nominal line 70
  10. theorem OAI.MetricKMedian.SparseSignedPreparation.nominal_pair line 77
  11. theorem OAI.MetricKMedian.SparseSignedPreparation.target line 86
  12. theorem OAI.MetricKMedian.SparseSignedPreparation.target_pair line 98
  13. theorem OAI.MetricKMedian.SparseSignedPreparation.length line 110