OAI/Combinatorics/KMedian/Analysis/BernsteinFalse.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.MetricKMedian.Certificates.B0_0_0_nonneg_part0 line 9
  2. theorem OAI.MetricKMedian.Certificates.B0_0_0_nonneg line 21
  3. theorem OAI.MetricKMedian.Certificates.B1_0_0_positive_part0 line 25
  4. theorem OAI.MetricKMedian.Certificates.B1_0_0_positive line 47
  5. theorem OAI.MetricKMedian.Certificates.sum12_0_0_positive_part0 line 51
  6. theorem OAI.MetricKMedian.Certificates.sum12_0_0_positive line 73
  7. theorem OAI.MetricKMedian.Certificates.B0_0_1_nonneg_part0 line 77
  8. theorem OAI.MetricKMedian.Certificates.B0_0_1_nonneg line 89
  9. theorem OAI.MetricKMedian.Certificates.B1_0_1_positive_part0 line 93
  10. theorem OAI.MetricKMedian.Certificates.B1_0_1_positive line 116
  11. theorem OAI.MetricKMedian.Certificates.sum12_0_1_positive_part0 line 120
  12. theorem OAI.MetricKMedian.Certificates.sum12_0_1_positive line 142
  13. theorem OAI.MetricKMedian.Certificates.B0_0_2_nonneg_part0 line 146
  14. theorem OAI.MetricKMedian.Certificates.B0_0_2_nonneg line 167
  15. theorem OAI.MetricKMedian.Certificates.B1_0_2_positive_part0 line 171
  16. theorem OAI.MetricKMedian.Certificates.B1_0_2_positive line 194
  17. theorem OAI.MetricKMedian.Certificates.B2_0_2_positive_part0 line 198
  18. theorem OAI.MetricKMedian.Certificates.B2_0_2_positive line 221
  19. theorem OAI.MetricKMedian.Certificates.discr_0_2_positive_part0 line 225
  20. theorem OAI.MetricKMedian.Certificates.discr_0_2_positive line 258
  21. theorem OAI.MetricKMedian.Certificates.B0_0_3_nonneg_part0 line 262
  22. theorem OAI.MetricKMedian.Certificates.B0_0_3_nonneg line 284
  23. theorem OAI.MetricKMedian.Certificates.B1_0_3_positive_part0 line 288
  24. theorem OAI.MetricKMedian.Certificates.B1_0_3_positive line 312
  25. theorem OAI.MetricKMedian.Certificates.B2_0_3_positive_part0 line 316
  26. theorem OAI.MetricKMedian.Certificates.B2_0_3_positive line 338
  27. theorem OAI.MetricKMedian.Certificates.discr_0_3_positive_part0 line 342
  28. theorem OAI.MetricKMedian.Certificates.discr_0_3_positive_part1 line 377
  29. theorem OAI.MetricKMedian.Certificates.discr_0_3_positive line 412