OAI/Combinatorics/KMedianRecovery/Recovery/BoundRow.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.MetricKMedianRecovery.Ellipsoid.BoundRow line 11
  2. def OAI.MetricKMedianRecovery.Ellipsoid.boundedMatrix line 13
  3. def OAI.MetricKMedianRecovery.Ellipsoid.boundedBounds line 17
  4. def OAI.MetricKMedianRecovery.Ellipsoid.integerRow line 21
  5. def OAI.MetricKMedianRecovery.Ellipsoid.boundedRows line 23
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.boundedRows_all line 28
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.bounded_region line 49
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.rows_real_region line 76
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.bounded_data_bound line 82
  10. def OAI.MetricKMedianRecovery.Ellipsoid.gapDenominator line 102
  11. def OAI.MetricKMedianRecovery.Ellipsoid.gapEpsilon line 105
  12. def OAI.MetricKMedianRecovery.Ellipsoid.precisionLog line 107
  13. def OAI.MetricKMedianRecovery.Ellipsoid.radiusLog line 109
  14. def OAI.MetricKMedianRecovery.Ellipsoid.integerDecide line 111
  15. lemma OAI.MetricKMedianRecovery.Ellipsoid.gapDenominator_pos line 115
  16. lemma OAI.MetricKMedianRecovery.Ellipsoid.gapEpsilon_bounds line 121
  17. lemma OAI.MetricKMedianRecovery.Ellipsoid.gapDenominator_cast line 131
  18. lemma OAI.MetricKMedianRecovery.Ellipsoid.precisionLog_bound line 139
  19. lemma OAI.MetricKMedianRecovery.Ellipsoid.radiusLog_bound line 148
  20. theorem OAI.MetricKMedianRecovery.Ellipsoid.integerDecide_correct line 151