OAI/Combinatorics/KMedian/Optimization/LPBinaryInput.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedian.LPBinary.Input line 16
  2. instance OAI.MetricKMedian.LPBinary.Input.(instance at line 27) line 27
  3. instance OAI.MetricKMedian.LPBinary.Input.(instance at line 28) line 28
  4. def OAI.MetricKMedian.LPBinary.Input.rows line 29
  5. def OAI.MetricKMedian.LPBinary.Input.raw line 30
  6. abbrev OAI.MetricKMedian.LPBinary.Input.encode line 31
  7. theorem OAI.MetricKMedian.LPBinary.Input.bounds line 33
  8. def OAI.MetricKMedian.LPBinary.Input.vector line 55
  9. def OAI.MetricKMedian.LPBinary.Input.iterate line 60
  10. def OAI.MetricKMedian.LPBinary.gradientBound line 63
  11. def OAI.MetricKMedian.LPBinary.baseBound line 64
  12. def OAI.MetricKMedian.LPBinary.stepsBound line 65
  13. def OAI.MetricKMedian.LPBinary.exponentBound line 66
  14. def OAI.MetricKMedian.LPBinary.heightBound line 67
  15. theorem OAI.MetricKMedian.LPBinary.penalty_bound line 69
  16. theorem OAI.MetricKMedian.LPBinary.grad_bound line 73
  17. theorem OAI.MetricKMedian.LPBinary.steps_bound line 80
  18. theorem OAI.MetricKMedian.LPBinary.iterate_height line 87
  19. theorem OAI.MetricKMedian.LPBinary.iterate_size line 130
  20. def OAI.MetricKMedian.LPBinary.stepsPolynomial line 140
  21. def OAI.MetricKMedian.LPBinary.heightPolynomial line 141
  22. theorem OAI.MetricKMedian.LPBinary.stepsPolynomial_eval line 143
  23. theorem OAI.MetricKMedian.LPBinary.heightPolynomial_eval line 145