OAI/Combinatorics/KMedian/Probability/SupportedLaw.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.FiniteLaw.supported line 13
2. theorem OAI.MetricKMedian.FiniteLaw.expect_supported line 30
3. def OAI.MetricKMedian.FiniteLaw.independent line 42
4. theorem OAI.MetricKMedian.FiniteLaw.expect_independent line 45
5. theorem OAI.MetricKMedian.FiniteLaw.independent_left line 49
6. theorem OAI.MetricKMedian.FiniteLaw.independent_right line 54
7. theorem OAI.MetricKMedian.FiniteLaw.independent_pair line 59
8. theorem OAI.MetricKMedian.FiniteLaw.support_independent line 64