OAI/Combinatorics/KMedian/Preparation/SupplierPreparationProgram.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.Preparation.RationalSuppliers.Program.Input line 16
  2. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.Input.raw line 20
  3. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.Input.encode line 21
  4. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.qData line 23
  5. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.qData_poly line 24
  6. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.qData_view line 25
  7. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.Input.prepared line 30
  8. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.prepareData line 34
  9. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.prepareData_poly line 36
  10. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.prepareData_view line 37
  11. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.preparedInputProgram line 43
  12. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.ofFn_physical line 46
  13. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.index_inl line 54
  14. abbrev OAI.MetricKMedian.Preparation.RationalSuppliers.Program.PreparedRaw line 59
  15. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.countsData line 61
  16. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.countsData_poly line 64
  17. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.countsData_view line 70
  18. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.tablesData line 89
  19. theorem OAI.MetricKMedian.Preparation.RationalSuppliers.Program.tablesData_poly line 90
  20. def OAI.MetricKMedian.Preparation.RationalSuppliers.Program.tablesProgram line 91