OAI/Combinatorics/KMedian/Preparation/RationalSupplierPreparation.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.size line 16
2. def OAI.MetricKMedian.Preparation.RationalSuppliers.index line 18
3. def OAI.MetricKMedian.Preparation.RationalSuppliers.flagQ line 22
4. def OAI.MetricKMedian.Preparation.RationalSuppliers.weightQ line 26
5. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.flag_cast line 32
6. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.weight_cast line 35
7. def OAI.MetricKMedian.Preparation.RationalSuppliers.D line 44
8. def OAI.MetricKMedian.Preparation.RationalSuppliers.a line 46
9. def OAI.MetricKMedian.Preparation.RationalSuppliers.q line 48
10. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.a_bounds line 51
11. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.q_nonneg line 56
12. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.scaled_q line 66
13. def OAI.MetricKMedian.Preparation.RationalSuppliers.coupled line 73