OAI/Combinatorics/KMedianRecovery/Recovery/State.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.MetricKMedianRecovery.Ellipsoid.State line 10
  2. def OAI.MetricKMedianRecovery.Ellipsoid.badRow line 14
  3. def OAI.MetricKMedianRecovery.Ellipsoid.advance line 17
  4. def OAI.MetricKMedianRecovery.Ellipsoid.iterate line 23
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.badRow_none line 27
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.badRow_some line 31
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.advance_eq_self line 36
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_stable line 40
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.badRow_nonzero line 48
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.advance_pos_lower line 60
  11. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_pos line 72
  12. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_shape_lower line 79
  13. lemma OAI.MetricKMedianRecovery.Ellipsoid.advance_contains line 86
  14. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_contains line 107