OAI/Combinatorics/KMedianRecovery/Sampling/Kernel.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.MetricKMedianRecovery.Guided.Kernel line 10
2. def OAI.MetricKMedianRecovery.Guided.pathWeight line 15
3. lemma OAI.MetricKMedianRecovery.Guided.pathWeight_nonneg line 21
4. lemma OAI.MetricKMedianRecovery.Guided.sum_fin_succ line 28
5. lemma OAI.MetricKMedianRecovery.Guided.pathWeight_total line 37
6. def OAI.MetricKMedianRecovery.Guided.Hits line 46
7. def OAI.MetricKMedianRecovery.Guided.eventMass line 51
8. lemma OAI.MetricKMedianRecovery.Guided.eventMass_nonneg line 56
9. lemma OAI.MetricKMedianRecovery.Guided.pathWeight_domination line 64
10. lemma OAI.MetricKMedianRecovery.Guided.supported_path_hits line 79
11. theorem OAI.MetricKMedianRecovery.Guided.history_likelihood_bound line 99
12. def OAI.MetricKMedianRecovery.Guided.eligibleMass line 125
13. def OAI.MetricKMedianRecovery.Guided.conditioned line 129
14. lemma OAI.MetricKMedianRecovery.Guided.conditioned_ratio line 148