OAI/Combinatorics/KMedian/Process/TaperListProgram.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Taper.ListOperation.Row line 12
  2. abbrev OAI.MetricKMedian.Taper.ListOperation.Raw line 13
  3. def OAI.MetricKMedian.Taper.ListOperation.upper line 15
  4. def OAI.MetricKMedian.Taper.ListOperation.breaks line 16
  5. def OAI.MetricKMedian.Taper.ListOperation.aSum line 17
  6. def OAI.MetricKMedian.Taper.ListOperation.bSum line 18
  7. def OAI.MetricKMedian.Taper.ListOperation.candidateList line 19
  8. def OAI.MetricKMedian.Taper.ListOperation.mass line 22
  9. def OAI.MetricKMedian.Taper.ListOperation.roots line 23
  10. def OAI.MetricKMedian.Taper.ListOperation.radius line 24
  11. theorem OAI.MetricKMedian.Taper.ListOperation.upper_poly line 26
  12. theorem OAI.MetricKMedian.Taper.ListOperation.breaks_poly line 30
  13. theorem OAI.MetricKMedian.Taper.ListOperation.aSum_poly line 35
  14. theorem OAI.MetricKMedian.Taper.ListOperation.bSum_poly line 41
  15. theorem OAI.MetricKMedian.Taper.ListOperation.candidateList_poly line 47
  16. theorem OAI.MetricKMedian.Taper.ListOperation.mass_poly line 56
  17. theorem OAI.MetricKMedian.Taper.ListOperation.roots_poly line 62
  18. theorem OAI.MetricKMedian.Taper.ListOperation.radius_poly line 65
  19. theorem OAI.MetricKMedian.Taper.ListOperation.upper_list line 69
  20. theorem OAI.MetricKMedian.Taper.ListOperation.mem_breaks line 71
  21. theorem OAI.MetricKMedian.Taper.ListOperation.aSum_list line 76
  22. theorem OAI.MetricKMedian.Taper.ListOperation.bSum_list line 79
  23. theorem OAI.MetricKMedian.Taper.ListOperation.mem_candidates line 82
  24. theorem OAI.MetricKMedian.Taper.ListOperation.mass_list line 87
  25. theorem OAI.MetricKMedian.Taper.ListOperation.mem_roots line 90
  26. theorem OAI.MetricKMedian.Taper.ListOperation.radius_list line 94