OAI/Combinatorics/KMedian/Sparse/SparseBernoulliFeatures.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.SparseBernoulli.used line 9
  2. def OAI.MetricKMedian.SparseBernoulli.without line 12
  3. theorem OAI.MetricKMedian.SparseBernoulli.used_without line 15
  4. def OAI.MetricKMedian.SparseBernoulli.flag line 33
  5. def OAI.MetricKMedian.SparseBernoulli.monomial line 35
  6. def OAI.MetricKMedian.SparseBernoulli.features line 38
  7. theorem OAI.MetricKMedian.SparseBernoulli.features_code line 41
  8. def OAI.MetricKMedian.SparseBernoulli.endpoint line 45
  9. theorem OAI.MetricKMedian.SparseBernoulli.flag_endpoint line 48
  10. theorem OAI.MetricKMedian.SparseBernoulli.monomial_endpoint line 52
  11. def OAI.MetricKMedian.SparseBernoulli.target line 72
  12. theorem OAI.MetricKMedian.SparseBernoulli.target_succ line 75