OAI/Combinatorics/KMedian/Analysis/QuadraticEnvelopes.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.MetricKMedian.Certificates.quadratic_of_end_slopes line 12
2. theorem OAI.MetricKMedian.Certificates.quadratic_of_discriminant line 19
3. theorem OAI.MetricKMedian.Certificates.quadratic_of_total line 30
4. def OAI.MetricKMedian.Certificates.bernCoeff line 38
5. theorem OAI.MetricKMedian.Certificates.bernCoeff_0_0_nonneg line 41
6. theorem OAI.MetricKMedian.Certificates.bernCoeff_0_1_nonneg line 49
7. theorem OAI.MetricKMedian.Certificates.bernCoeff_0_2_nonneg line 57
8. theorem OAI.MetricKMedian.Certificates.bernCoeff_0_3_nonneg line 69
9. theorem OAI.MetricKMedian.Certificates.bernCoeff_1_0_nonneg line 81
10. theorem OAI.MetricKMedian.Certificates.bernCoeff_1_1_nonneg line 89
11. theorem OAI.MetricKMedian.Certificates.bernCoeff_1_2_nonneg line 97
12. theorem OAI.MetricKMedian.Certificates.bernCoeff_1_3_nonneg line 109
13. theorem OAI.MetricKMedian.Certificates.charge_expansion line 125
14. theorem OAI.MetricKMedian.Certificates.polynomial_charge_margin line 138