OAI/Combinatorics/KMedianRecovery/Recovery/ReferenceBridge.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.RationalSampling.fromArrays line 11
2. lemma OAI.MetricKMedianRecovery.RationalSampling.key_real line 13
3. lemma OAI.MetricKMedianRecovery.RationalSampling.key_dummy line 15
4. lemma OAI.MetricKMedianRecovery.RationalSampling.key_leaf line 17
5. lemma OAI.MetricKMedianRecovery.RationalSampling.tags_fromArrays line 21
6. lemma OAI.MetricKMedianRecovery.RationalSampling.values_finset line 25
7. lemma OAI.MetricKMedianRecovery.RationalSampling.run_chosen line 49
8. lemma OAI.MetricKMedianRecovery.RationalSampling.run_reference line 56
9. lemma OAI.MetricKMedianRecovery.RationalSampling.run_tagId line 63