OAI/Probability/SKBarriers/Dynamics/GreedyRecursion.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.SK.Analytic.GreedyRecord line 13
2. def OAI.SK.Analytic.greedyRun line 18
3. def OAI.SK.Analytic.greedyReference line 30
4. theorem OAI.SK.Analytic.greedyRun_predictable line 35
5. theorem OAI.SK.Analytic.greedyReference_predictable line 45
6. theorem OAI.SK.Analytic.greedyRun_refs line 52
7. theorem OAI.SK.Analytic.greedyRun_range line 65
8. def OAI.SK.Analytic.bankPick line 79
9. theorem OAI.SK.Analytic.bankPick_mem line 86
10. theorem OAI.SK.Analytic.bankPick_spec line 94