OAI/Probability/Ballisticity/Estimates/RestartLyapunov.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.DirectionalTransience.observerRewardSum line 15
2. lemma OAI.DirectionalTransience.measurable_observerRewardSum line 19
3. lemma OAI.DirectionalTransience.observerRewardSum_mono line 26
4. lemma OAI.DirectionalTransience.restart_lyapunov_finite line 34
5. lemma OAI.DirectionalTransience.restart_lyapunov_total line 63
6. lemma OAI.DirectionalTransience.restart_bounded_potential_total line 79
7. lemma OAI.DirectionalTransience.restart_reward_comparison_total line 131
8. lemma OAI.DirectionalTransience.observerRewardSum_mul line 164