OAI/Combinatorics/KMedianRecovery/Recovery/CoordinateRow.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.coordinateRow line 10
  2. lemma OAI.MetricKMedianRecovery.Ellipsoid.coordinateRow_value line 13
  3. def OAI.MetricKMedianRecovery.Ellipsoid.boxRows line 17
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.boxRows_holds line 20
  5. def OAI.MetricKMedianRecovery.Ellipsoid.withBox line 39
  6. def OAI.MetricKMedianRecovery.Ellipsoid.finalFace line 41
  7. def OAI.MetricKMedianRecovery.Ellipsoid.rowMatrix line 44
  8. def OAI.MetricKMedianRecovery.Ellipsoid.rowBounds line 47
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.rowMatrix_region line 50
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.finalFace_feasible line 61
  11. theorem OAI.MetricKMedianRecovery.Ellipsoid.finalFace_kernel line 69
  12. def OAI.MetricKMedianRecovery.PositiveSolve.freezeVec line 108
  13. def OAI.MetricKMedianRecovery.PositiveSolve.freezeMat line 112
  14. lemma OAI.MetricKMedianRecovery.PositiveSolve.freezeVec_eq line 116
  15. lemma OAI.MetricKMedianRecovery.PositiveSolve.freezeMat_eq line 119
  16. def OAI.MetricKMedianRecovery.PositiveSolve.schur line 123
  17. def OAI.MetricKMedianRecovery.PositiveSolve.rhs line 126
  18. def OAI.MetricKMedianRecovery.PositiveSolve.solve line 129
  19. lemma OAI.MetricKMedianRecovery.PositiveSolve.schur_mulVec line 137
  20. lemma OAI.MetricKMedianRecovery.PositiveSolve.schur_isHermitian line 148
  21. lemma OAI.MetricKMedianRecovery.PositiveSolve.schur_posDef line 156
  22. theorem OAI.MetricKMedianRecovery.PositiveSolve.solve_correct line 179