OAI/Combinatorics/KMedian/Analysis/PolynomialBounds.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Certificates.p_lower_part0 line 9
  2. theorem OAI.MetricKMedian.Certificates.p_lower line 25
  3. theorem OAI.MetricKMedian.Certificates.p_upper_part0 line 29
  4. theorem OAI.MetricKMedian.Certificates.p_upper line 45
  5. theorem OAI.MetricKMedian.Certificates.v_lower_part0 line 49
  6. theorem OAI.MetricKMedian.Certificates.v_lower line 65
  7. theorem OAI.MetricKMedian.Certificates.v_upper_part0 line 69
  8. theorem OAI.MetricKMedian.Certificates.v_upper line 86
  9. theorem OAI.MetricKMedian.Certificates.k_lower_part0 line 90
  10. theorem OAI.MetricKMedian.Certificates.k_lower line 105
  11. theorem OAI.MetricKMedian.Certificates.k_upper_part0 line 109
  12. theorem OAI.MetricKMedian.Certificates.k_upper line 124
  13. theorem OAI.MetricKMedian.Certificates.h_lower_part0 line 128
  14. theorem OAI.MetricKMedian.Certificates.h_lower line 143
  15. theorem OAI.MetricKMedian.Certificates.h_upper_part0 line 147
  16. theorem OAI.MetricKMedian.Certificates.h_upper line 161