OAI/Combinatorics/KMedian/Analysis/BernsteinTrue.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Certificates.B0_1_0_nonneg_part0 line 9
  2. theorem OAI.MetricKMedian.Certificates.B0_1_0_nonneg line 21
  3. theorem OAI.MetricKMedian.Certificates.B1_1_0_positive_part0 line 25
  4. theorem OAI.MetricKMedian.Certificates.B1_1_0_positive line 47
  5. theorem OAI.MetricKMedian.Certificates.sum12_1_0_positive_part0 line 51
  6. theorem OAI.MetricKMedian.Certificates.sum12_1_0_positive line 77
  7. theorem OAI.MetricKMedian.Certificates.B0_1_1_nonneg_part0 line 81
  8. theorem OAI.MetricKMedian.Certificates.B0_1_1_nonneg line 93
  9. theorem OAI.MetricKMedian.Certificates.B1_1_1_positive_part0 line 97
  10. theorem OAI.MetricKMedian.Certificates.B1_1_1_positive line 120
  11. theorem OAI.MetricKMedian.Certificates.sum12_1_1_positive_part0 line 124
  12. theorem OAI.MetricKMedian.Certificates.sum12_1_1_positive line 150
  13. theorem OAI.MetricKMedian.Certificates.B0_1_2_nonneg_part0 line 154
  14. theorem OAI.MetricKMedian.Certificates.B0_1_2_nonneg line 175
  15. theorem OAI.MetricKMedian.Certificates.B1_1_2_positive_part0 line 179
  16. theorem OAI.MetricKMedian.Certificates.B1_1_2_positive line 206
  17. theorem OAI.MetricKMedian.Certificates.B2_1_2_positive_part0 line 210
  18. theorem OAI.MetricKMedian.Certificates.B2_1_2_positive line 236
  19. theorem OAI.MetricKMedian.Certificates.discr_1_2_positive_part0 line 240
  20. theorem OAI.MetricKMedian.Certificates.discr_1_2_positive line 281
  21. theorem OAI.MetricKMedian.Certificates.B0_1_3_nonneg_part0 line 285
  22. theorem OAI.MetricKMedian.Certificates.B0_1_3_nonneg line 307
  23. theorem OAI.MetricKMedian.Certificates.B1_1_3_positive_part0 line 311
  24. theorem OAI.MetricKMedian.Certificates.B1_1_3_positive line 338
  25. theorem OAI.MetricKMedian.Certificates.B2_1_3_positive_part0 line 342
  26. theorem OAI.MetricKMedian.Certificates.B2_1_3_positive line 367
  27. theorem OAI.MetricKMedian.Certificates.discr_1_3_positive_part0 line 371
  28. theorem OAI.MetricKMedian.Certificates.discr_1_3_positive line 412
  29. theorem OAI.MetricKMedian.Certificates.total_1_3_positive_part0 line 416
  30. theorem OAI.MetricKMedian.Certificates.total_1_3_positive line 443
  31. theorem OAI.MetricKMedian.Certificates.diff02_1_3_positive_part0 line 447
  32. theorem OAI.MetricKMedian.Certificates.diff02_1_3_positive line 472