OAI/Combinatorics/KMedianRecovery/Recovery/Grid.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.advance_upper line 10
2. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_shape_upper line 24
3. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_shape_entry_bound line 39
4. def OAI.MetricKMedianRecovery.Ellipsoid.OnGrid line 57
5. lemma OAI.MetricKMedianRecovery.Ellipsoid.onGrid_den line 59
6. lemma OAI.MetricKMedianRecovery.Ellipsoid.gridShape_onGrid line 66
7. lemma OAI.MetricKMedianRecovery.Ellipsoid.initial_onGrid line 77
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_onGrid line 89
9. lemma OAI.MetricKMedianRecovery.Ellipsoid.numerator_bound line 103
10. theorem OAI.MetricKMedianRecovery.Ellipsoid.iterate_shape_height line 114