OAI/Combinatorics/KMedianRecovery/Recovery/DataHeight.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.dataHeight line 10
  2. lemma OAI.MetricKMedianRecovery.Ellipsoid.dataHeight_bounds line 13
  3. def OAI.MetricKMedianRecovery.Ellipsoid.padMatrix line 32
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.padMatrix_sum line 35
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.pad_feasible line 40
  6. def OAI.MetricKMedianRecovery.Ellipsoid.boundedIntegerDecide line 58
  7. theorem OAI.MetricKMedianRecovery.Ellipsoid.boundedIntegerDecide_correct line 61
  8. def OAI.MetricKMedianRecovery.PolytopeCertificate.rowDenominator line 75
  9. def OAI.MetricKMedianRecovery.PolytopeCertificate.rowNumerator line 76
  10. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.rowDenominator_pos line 80
  11. lemma OAI.MetricKMedianRecovery.PolytopeCertificate.rowNumerator_cast line 85
  12. def OAI.MetricKMedianRecovery.Ellipsoid.rowEntries line 100
  13. def OAI.MetricKMedianRecovery.Ellipsoid.clearedMatrix line 102
  14. def OAI.MetricKMedianRecovery.Ellipsoid.clearedBounds line 105
  15. lemma OAI.MetricKMedianRecovery.Ellipsoid.clearRow_holds line 108
  16. lemma OAI.MetricKMedianRecovery.Ellipsoid.clearedRows_holds line 115
  17. def OAI.MetricKMedianRecovery.Ellipsoid.boundedRationalDecide line 127
  18. theorem OAI.MetricKMedianRecovery.Ellipsoid.boundedRationalDecide_correct line 130