OAI/Combinatorics/KMedianRecovery/Recovery/EnumeratedBest.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.MetricKMedianRecovery.FiniteSampling.enumeratedBest line 9
2. lemma OAI.MetricKMedianRecovery.FiniteSampling.enumeratedBest_mem line 13
3. lemma OAI.MetricKMedianRecovery.FiniteSampling.enumeratedBest_le line 23
4. def OAI.MetricKMedianRecovery.Sampling.completeState line 37
5. lemma OAI.MetricKMedianRecovery.Sampling.completeState_feasible line 47
6. lemma OAI.MetricKMedianRecovery.Sampling.completeState_le line 67
7. lemma OAI.MetricKMedianRecovery.Sampling.Comparison.completeState_success line 84
8. def OAI.MetricKMedianRecovery.Guided.pure line 105
9. def OAI.MetricKMedianRecovery.Guided.stoppedKernel line 109
10. def OAI.MetricKMedianRecovery.Guided.stoppedUpdate line 119
11. def OAI.MetricKMedianRecovery.Guided.hitMass line 122
12. lemma OAI.MetricKMedianRecovery.Guided.hitMass_zero line 125
13. lemma OAI.MetricKMedianRecovery.Guided.hitMass_succ line 130
14. lemma OAI.MetricKMedianRecovery.Guided.hitMass_eq_of_agree line 148
15. lemma OAI.MetricKMedianRecovery.Guided.hitMass_stopped line 163
16. def OAI.MetricKMedianRecovery.Guided.routed line 175
17. lemma OAI.MetricKMedianRecovery.Guided.routed_at line 185
18. lemma OAI.MetricKMedianRecovery.Guided.routed_pos line 191
19. lemma OAI.MetricKMedianRecovery.Guided.routed_domination line 201
20. def OAI.MetricKMedianRecovery.Guided.states line 213
21. lemma OAI.MetricKMedianRecovery.Guided.states_zero line 218
22. lemma OAI.MetricKMedianRecovery.Guided.states_step line 223
23. lemma OAI.MetricKMedianRecovery.Guided.pathWeight_eq_prod line 235
24. lemma OAI.MetricKMedianRecovery.Guided.supported_step line 245
25. lemma OAI.MetricKMedianRecovery.Guided.states_invariant line 253