OAI/Combinatorics/KMedianRecovery/Sampling/ProbabilityProd.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_prod line 10
2. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_prod_lower line 16
3. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_prod_conj line 27
4. lemma OAI.MetricKMedianRecovery.FiniteSampling.average_pi_restrict line 40
5. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_pi_restrict line 48
6. lemma OAI.MetricKMedianRecovery.FiniteSampling.probability_uniform_fun line 54
7. lemma OAI.MetricKMedianRecovery.ColorLabel.color_event_probability line 71
8. lemma OAI.MetricKMedianRecovery.ColorLabel.label_event_probability line 77