OAI/Combinatorics/KMedian/Sparse/SparseGraphLaw.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SparseGraph.columns line 15
2. theorem OAI.MetricKMedian.SparseGraph.columns_moment line 18
3. theorem OAI.MetricKMedian.SparseGraph.columns_card line 33
4. def OAI.MetricKMedian.SparseGraph.law line 46
5. theorem OAI.MetricKMedian.SparseGraph.law_spec line 48
6. theorem OAI.MetricKMedian.SparseGraph.run_positive line 65
7. theorem OAI.MetricKMedian.SparseGraph.law_fixed line 80