OAI/Combinatorics/KMedianRecovery/Recovery/CenterUpdate.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.cutShape_pos line 11
2. def OAI.MetricKMedianRecovery.Ellipsoid.centerUpdate line 16
3. lemma OAI.MetricKMedianRecovery.Ellipsoid.shape_center_contains line 19
4. lemma OAI.MetricKMedianRecovery.Ellipsoid.inflatedShape_inverse line 44
5. def OAI.MetricKMedianRecovery.Ellipsoid.upperRound line 56
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.upperRound_above line 59
7. lemma OAI.MetricKMedianRecovery.Ellipsoid.upperRound_relative line 70
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.upperRound_pos line 90
9. lemma OAI.MetricKMedianRecovery.Ellipsoid.upperRound_inverse_bounds line 97
10. def OAI.MetricKMedianRecovery.Ellipsoid.gridShape line 122
11. lemma OAI.MetricKMedianRecovery.Ellipsoid.real_gridShape line 125