OAI/Combinatorics/KMedianRecovery/Recovery/GridFloor.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MetricKMedianRecovery.Ellipsoid.gridFloor line 12
  2. def OAI.MetricKMedianRecovery.Ellipsoid.realMatrix line 14
  3. def OAI.MetricKMedianRecovery.Ellipsoid.gridMatrix line 16
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridFloor_bounds line 18
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridFloor_error line 31
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.realMatrix_symm line 40
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridMatrix_symm line 45
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridMatrix_error line 50
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridFloor_numerator_bound line 55
  10. def OAI.MetricKMedianRecovery.Ellipsoid.sqrtUpperFraction line 68
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.sqrtUpperFraction_bounds line 71