OAI/Combinatorics/KMedianRecovery/Recovery/StackLength.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.BitMachine.stackLength line 13
2. def OAI.MetricKMedianRecovery.BitMachine.pushBound line 15
3. lemma OAI.MetricKMedianRecovery.BitMachine.stackLength_pure line 24
4. lemma OAI.MetricKMedianRecovery.BitMachine.stackLength_update_le line 28
5. lemma OAI.MetricKMedianRecovery.BitMachine.stepAux_length line 42
6. def OAI.MetricKMedianRecovery.BitMachine.Program.maxPush line 67
7. lemma OAI.MetricKMedianRecovery.BitMachine.Program.step_length line 69
8. lemma OAI.MetricKMedianRecovery.BitMachine.iterate_length line 82
9. lemma OAI.MetricKMedianRecovery.BitMachine.Program.output_length line 104
10. structure OAI.MetricKMedianRecovery.BitMachine.PolyComputes line 112
11. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.toTM2 line 117
12. lemma OAI.MetricKMedianRecovery.BitMachine.polynomial_monotone line 125
13. def OAI.MetricKMedianRecovery.BitMachine.PolyComputes.comp line 130