OAI/Combinatorics/KMedian/Process/TaperGraphProgram.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedian.TaperGraphProgram.Row line 13
  2. abbrev OAI.MetricKMedian.TaperGraphProgram.BRow line 14
  3. abbrev OAI.MetricKMedian.TaperGraphProgram.Raw line 15
  4. structure OAI.MetricKMedian.TaperGraphProgram.Input line 17
  5. def OAI.MetricKMedian.TaperGraphProgram.Input.raw line 26
  6. abbrev OAI.MetricKMedian.TaperGraphProgram.Input.encode line 28
  7. theorem OAI.MetricKMedian.TaperGraphProgram.marginal_unit line 30
  8. theorem OAI.MetricKMedian.TaperGraphProgram.source_unit line 34
  9. def OAI.MetricKMedian.TaperGraphProgram.Input.qInput line 41
  10. def OAI.MetricKMedian.TaperGraphProgram.rawQ line 44
  11. theorem OAI.MetricKMedian.TaperGraphProgram.rawQ_poly line 46
  12. theorem OAI.MetricKMedian.TaperGraphProgram.rawQ_input line 52
  13. def OAI.MetricKMedian.TaperGraphProgram.qInputProgram line 56
  14. def OAI.MetricKMedian.TaperGraphProgram.program line 58