OAI/Combinatorics/KMedianRecovery/Recovery/IterationBlocks.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.Ellipsoid.growth_up_to line 10
2. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_invalid_before line 22
3. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_determinant_growth line 31
4. lemma OAI.MetricKMedianRecovery.Ellipsoid.iterate_block_growth line 62
5. lemma OAI.MetricKMedianRecovery.Ellipsoid.factorial_bit_bound line 73
6. def OAI.MetricKMedianRecovery.Ellipsoid.iterationBlocks line 81
7. def OAI.MetricKMedianRecovery.Ellipsoid.iterationBudget line 83
8. lemma OAI.MetricKMedianRecovery.Ellipsoid.determinant_budget line 85