OAI/Combinatorics/KMedianRecovery/Recovery/VectorHeight.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.Ellipsoid.vectorHeight line 11
2. def OAI.MetricKMedianRecovery.Ellipsoid.quadHeight line 12
3. def OAI.MetricKMedianRecovery.Ellipsoid.rootHeight line 13
4. def OAI.MetricKMedianRecovery.Ellipsoid.incrementHeight line 14
5. def OAI.MetricKMedianRecovery.Ellipsoid.storedShapeHeight line 16
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.mulVec_height line 18
7. lemma OAI.MetricKMedianRecovery.Ellipsoid.rationalQuad_height line 24
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.rationalRootUpper_height line 31
9. lemma OAI.MetricKMedianRecovery.Ellipsoid.center_increment_height line 39
10. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_shape_Height line 50
11. theorem OAI.MetricKMedianRecovery.Ellipsoid.iterate_center_height line 57