OAI/Combinatorics/KMedianRecovery/Encoding/Matrix.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.matrix line 11
  2. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.vector line 14
  3. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.matrix_eq line 17
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.vector_eq line 20
  5. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.state line 24
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.state_eq line 25
  7. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.iterate line 29
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.iterate_eq line 33
  9. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.weakSolve line 39
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.weakSolve_eq line 43
  11. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.integerDecide line 47
  12. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.integerDecide_eq line 50
  13. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.boundedIntegerDecide line 54
  14. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.boundedIntegerDecide_eq line 56
  15. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.boundedRationalDecide line 60
  16. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.boundedRationalDecide_eq line 62
  17. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.selectFace line 66
  18. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.selectFace_eq line 73
  19. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.finalFace line 79
  20. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.finalFace_eq line 81
  21. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.point line 84
  22. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.linearSolve_eq line 90
  23. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.point_eq line 95
  24. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.facePoint line 105
  25. lemma OAI.MetricKMedianRecovery.Ellipsoid.Stored.facePoint_eq line 108
  26. def OAI.MetricKMedianRecovery.Ellipsoid.Stored.exactSolve line 115
  27. theorem OAI.MetricKMedianRecovery.Ellipsoid.Stored.exactSolve_eq line 117
  28. theorem OAI.MetricKMedianRecovery.Ellipsoid.Stored.exactSolve_some line 125
  29. theorem OAI.MetricKMedianRecovery.Ellipsoid.Stored.exactSolve_complete line 130