OAI/Combinatorics/KMedianRecovery/Strictness/Clipped.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalPhase.clipped line 9
2. lemma OAI.MetricKMedianRecovery.RationalPhase.clipped_real line 13
3. def OAI.MetricKMedianRecovery.RationalPhase.advance line 25
4. lemma OAI.MetricKMedianRecovery.RationalPhase.advance_get line 31
5. lemma OAI.MetricKMedianRecovery.RationalPhase.advance_real line 37
6. inductive OAI.MetricKMedianRecovery.RationalPhase.Instruction line 59
7. def OAI.MetricKMedianRecovery.RationalPhase.run line 63
8. theorem OAI.MetricKMedianRecovery.RationalPhase.run_spec line 72
9. def OAI.MetricKMedianRecovery.RationalPhase.initial line 117
10. lemma OAI.MetricKMedianRecovery.RationalPhase.initial_real line 119