OAI/Combinatorics/KMedian/Probability/BernoulliListOperations.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.SparseBernoulli.ListOperation.Row line 12
  2. abbrev OAI.MetricKMedian.SparseBernoulli.ListOperation.er line 13
  3. def OAI.MetricKMedian.SparseBernoulli.ListOperation.units line 15
  4. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.units_poly line 19
  5. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.units_length line 28
  6. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.units_eq line 33
  7. def OAI.MetricKMedian.SparseBernoulli.ListOperation.tests line 37
  8. def OAI.MetricKMedian.SparseBernoulli.ListOperation.value line 39
  9. def OAI.MetricKMedian.SparseBernoulli.ListOperation.featureList line 40
  10. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.tests_poly line 43
  11. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.value_poly line 48
  12. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.featureList_poly line 51
  13. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.flag_product line 56
  14. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.get_true_iff line 65
  15. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.tests_true_iff line 80
  16. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.featureList_ofFn line 94
  17. def OAI.MetricKMedian.SparseBernoulli.ListOperation.endpoint line 106
  18. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.endpoint_poly line 108
  19. theorem OAI.MetricKMedian.SparseBernoulli.ListOperation.endpoint_ofFn line 112