OAI/Combinatorics/KMedian/Preparation/SupplierListOperations.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.QRow line 14
  2. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.BTable line 15
  3. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.SupplierRaw line 16
  4. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.supplierView line 17
  5. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.ofFn_sum line 21
  6. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.finSum_symm_castLE line 29
  7. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.append_poly line 33
  8. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.ofFn_star line 37
  9. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.targetsData line 50
  10. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.targetsData_poly line 55
  11. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.flagsData line 69
  12. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.flagsData_poly line 71
  13. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.outsideData line 81
  14. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.pairWeight line 82
  15. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.weightsData line 85
  16. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.outsideData_poly line 89
  17. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.pairWeight_poly line 91
  18. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.weightsData_poly line 93
  19. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.targetsData_view line 102
  20. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.flagsData_view line 111
  21. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.outsideData_view line 116
  22. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.pairWeight_view line 125
  23. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.weightsData_view line 135