OAI/Combinatorics/KMedianRecovery/Recovery/CoupledInitial.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initial line 12
2. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initial_certified line 18
3. inductive OAI.MetricKMedianRecovery.CanonicalCoupledMerge.StartOutput line 65
4. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initialHistory line 69
5. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initialCount line 74
6. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.start line 78
7. def OAI.MetricKMedianRecovery.CanonicalCoupledMerge.StartOutput.Correct line 94
8. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.initialHistory_spec line 101
9. lemma OAI.MetricKMedianRecovery.CanonicalCoupledMerge.start_correct line 109