OAI/Combinatorics/KMedianRecovery/Recovery/InitialState.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.MetricKMedianRecovery.Ellipsoid.realMatrix_one line 11
  2. def OAI.MetricKMedianRecovery.Ellipsoid.initialState line 16
  3. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_realShape line 18
  4. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_pos line 22
  5. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_shape_lower line 27
  6. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_inverse line 34
  7. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_inverse_det line 40
  8. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_contains_box line 44
  9. lemma OAI.MetricKMedianRecovery.Ellipsoid.single_diameter_bound line 63
  10. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_diameters line 74
  11. def OAI.MetricKMedianRecovery.Ellipsoid.weakSolve line 91
  12. lemma OAI.MetricKMedianRecovery.Ellipsoid.weakSolve_sound line 96
  13. lemma OAI.MetricKMedianRecovery.Ellipsoid.weakSolve_complete_diameters line 103
  14. def OAI.MetricKMedianRecovery.Ellipsoid.relaxedRow line 140
  15. def OAI.MetricKMedianRecovery.Ellipsoid.relaxedRows line 142
  16. lemma OAI.MetricKMedianRecovery.Ellipsoid.relaxedRows_feasible line 144
  17. lemma OAI.MetricKMedianRecovery.Ellipsoid.row_value_single line 154
  18. lemma OAI.MetricKMedianRecovery.Ellipsoid.relaxed_diameter line 160
  19. theorem OAI.MetricKMedianRecovery.Ellipsoid.weakSolve_complete line 176