OAI/Combinatorics/KMedianRecovery/Sampling/PrefixFreeMono.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.CommonPrefixTransfer.prefix_free_mono line 10
2. lemma OAI.MetricKMedianRecovery.CommonPrefixTransfer.history_free_mono line 23
3. lemma OAI.MetricKMedianRecovery.CommonPrefixTransfer.history_rows line 31
4. lemma OAI.MetricKMedianRecovery.CommonPrefixTransfer.history_append line 42
5. theorem OAI.MetricKMedianRecovery.CommonPrefixTransfer.current_phase line 53