OAI/Combinatorics/KMedian/Probability/BernoulliBatches.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.FiniteLaw.coinWeight line 10
  2. theorem OAI.MetricKMedian.FiniteLaw.coinWeight_true line 12
  3. theorem OAI.MetricKMedian.FiniteLaw.coinWeight_false line 13
  4. theorem OAI.MetricKMedian.FiniteLaw.coinWeight_nonneg line 15
  5. theorem OAI.MetricKMedian.FiniteLaw.coinWeight_total line 18
  6. def OAI.MetricKMedian.FiniteLaw.bernoulli line 21
  7. theorem OAI.MetricKMedian.FiniteLaw.bernoulli_expect_prod line 27
  8. theorem OAI.MetricKMedian.FiniteLaw.bernoulli_cylinder line 39
  9. theorem OAI.MetricKMedian.FiniteLaw.bernoulli_marginal line 74
  10. theorem OAI.MetricKMedian.FiniteLaw.bernoulli_pair line 79
  11. def OAI.MetricKMedian.FiniteLaw.selected line 85
  12. theorem OAI.MetricKMedian.FiniteLaw.filtered_marginal line 88
  13. theorem OAI.MetricKMedian.FiniteLaw.filtered_pair_le line 123
  14. theorem OAI.MetricKMedian.FiniteLaw.filtered_marginal_error line 135