OAI/Combinatorics/KMedian/Sparse/SparsePreparedMoments.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.SparsePrepared.outer_expectation line 14
2. theorem OAI.MetricKMedian.SparsePrepared.kernel_mean line 23
3. theorem OAI.MetricKMedian.SparsePrepared.kernel_pair line 32
4. theorem OAI.MetricKMedian.SparsePrepared.mean line 42
5. theorem OAI.MetricKMedian.SparsePrepared.pair line 54
6. theorem OAI.MetricKMedian.SparsePrepared.joint_opening_probability line 69