OAI/Combinatorics/KMedian/Probability/FiniteLaws.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.FiniteLaw line 7
  2. def OAI.MetricKMedian.FiniteLaw.expect line 14
  3. def OAI.MetricKMedian.FiniteLaw.prob line 15
  4. theorem OAI.MetricKMedian.FiniteLaw.expect_mono line 18
  5. theorem OAI.MetricKMedian.FiniteLaw.expect_nonneg line 22
  6. theorem OAI.MetricKMedian.FiniteLaw.expect_const line 25
  7. theorem OAI.MetricKMedian.FiniteLaw.expect_add line 28
  8. theorem OAI.MetricKMedian.FiniteLaw.expect_sub line 32
  9. theorem OAI.MetricKMedian.FiniteLaw.expect_mul line 36
  10. theorem OAI.MetricKMedian.FiniteLaw.expect_mul_right line 40
  11. theorem OAI.MetricKMedian.FiniteLaw.expect_sum line 44
  12. theorem OAI.MetricKMedian.FiniteLaw.prob_nonneg line 49
  13. theorem OAI.MetricKMedian.FiniteLaw.prob_le_one line 54
  14. theorem OAI.MetricKMedian.FiniteLaw.prob_mono line 59
  15. theorem OAI.MetricKMedian.FiniteLaw.prob_congr line 66
  16. theorem OAI.MetricKMedian.FiniteLaw.prob_exists_le_sum line 70
  17. theorem OAI.MetricKMedian.BatchRemainder.pointwise line 91
  18. theorem OAI.MetricKMedian.BatchRemainder.expect_selected_sum line 119
  19. theorem OAI.MetricKMedian.BatchRemainder.expect_pair_count line 130
  20. theorem OAI.MetricKMedian.BatchRemainder.expectation_le line 149