OAI/Combinatorics/KMedianRecovery/Machines/CorrectionSize.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.Keys line 10
2. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Correction.Keys.mono line 14
3. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.Outcome.Keys line 18
4. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.resolve_keys line 21
5. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.step_keys line 36
6. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCorrection.length_bound line 51
7. def OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.bound line 68
8. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.length_bound line 69
9. lemma OAI.MetricKMedianRecovery.BitMachine.BinaryCoupled.output_length_bound line 90