OAI/Combinatorics/KMedian/Analysis/CertificatePolynomials.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedian.Certificates.p line 8
  2. def OAI.MetricKMedian.Certificates.v line 10
  3. def OAI.MetricKMedian.Certificates.k line 12
  4. def OAI.MetricKMedian.Certificates.h line 14
  5. def OAI.MetricKMedian.Certificates.pSeries line 16
  6. def OAI.MetricKMedian.Certificates.aSeries line 18
  7. def OAI.MetricKMedian.Certificates.bit line 20
  8. def OAI.MetricKMedian.Certificates.d line 21
  9. def OAI.MetricKMedian.Certificates.H line 22
  10. def OAI.MetricKMedian.Certificates.c line 23
  11. def OAI.MetricKMedian.Certificates.N line 24
  12. def OAI.MetricKMedian.Certificates.l line 25
  13. def OAI.MetricKMedian.Certificates.hh line 26
  14. def OAI.MetricKMedian.Certificates.uZero line 27
  15. def OAI.MetricKMedian.Certificates.uOne line 28
  16. def OAI.MetricKMedian.Certificates.Tk line 29
  17. def OAI.MetricKMedian.Certificates.T1 line 30
  18. def OAI.MetricKMedian.Certificates.T2 line 31
  19. def OAI.MetricKMedian.Certificates.Q0 line 32
  20. def OAI.MetricKMedian.Certificates.Q1 line 33
  21. def OAI.MetricKMedian.Certificates.Y line 34
  22. def OAI.MetricKMedian.Certificates.Yprime line 35
  23. def OAI.MetricKMedian.Certificates.B0 line 37
  24. def OAI.MetricKMedian.Certificates.B1 line 40
  25. def OAI.MetricKMedian.Certificates.B2 line 47
  26. def OAI.MetricKMedian.Certificates.discr line 52
  27. def OAI.MetricKMedian.Certificates.total line 53