OAI/Combinatorics/KMedian/Process/PhysicalBatchLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.FiniteLaw.prob_false line 9
2. theorem OAI.MetricKMedian.FiniteLaw.prob_true line 13
3. def OAI.MetricKMedian.PhysicalBatchLaw.balanced line 23
4. def OAI.MetricKMedian.PhysicalBatchLaw.unbalanced line 25
5. def OAI.MetricKMedian.PhysicalBatchLaw.law line 28
6. theorem OAI.MetricKMedian.PhysicalBatchLaw.prob_eq line 35
7. theorem OAI.MetricKMedian.PhysicalBatchLaw.marginal line 46
8. theorem OAI.MetricKMedian.PhysicalBatchLaw.pair_le line 62
9. theorem OAI.MetricKMedian.PhysicalBatchLaw.marginal_error line 84