OAI/Probability/Localization/Termination.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.FiniteEntropy.exists_fiber_good line 15
2. lemma OAI.RepeatedLocalization.FiniteEntropy.ae_fiber_positive line 23
3. lemma OAI.RepeatedLocalization.FiniteEntropy.frozen_nonnegative_bound line 34
4. lemma OAI.RepeatedLocalization.FiniteEntropy.truncatedDepth_mono line 62
5. lemma OAI.RepeatedLocalization.FiniteEntropy.run_eventually_terminal line 84
6. lemma OAI.RepeatedLocalization.FiniteEntropy.budget_nonneg line 90
7. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_uniform_attempts line 93
8. lemma OAI.RepeatedLocalization.FiniteEntropy.almost_sure_termination line 108
9. lemma OAI.RepeatedLocalization.FiniteEntropy.history_regular_of_stopped line 136
10. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_regular line 160