OAI/Combinatorics/KMedian/Sparse/SparseBindProgram.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.weights line 17
2. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.jointWeights line 18
3. def OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.bindData line 20
4. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.weights_law line 24
5. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.jointWeights_raw line 28
6. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.scaling_denominator_equiv line 37
7. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.scaling_numerator_equiv line 43
8. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.bindData_raw line 49
9. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.weights_poly line 70
10. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.jointWeights_poly line 74
11. theorem OAI.MetricKMedian.SparseIntegerLaw.BinarySparse.bindData_poly line 80