OAI/Probability/Localization/RewardBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.FiniteEntropy.rewardStep line 14
2. lemma OAI.RepeatedLocalization.FiniteEntropy.reward_only_none line 19
3. lemma OAI.RepeatedLocalization.FiniteEntropy.integrable_fixed_reward line 24
4. lemma OAI.RepeatedLocalization.FiniteEntropy.integral_fixed_reward_event line 37
5. lemma OAI.RepeatedLocalization.FiniteEntropy.exists_run_fiber_root line 58
6. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardStep_fiber_integrable line 71
7. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardStep_fiber_integral line 82
8. lemma OAI.RepeatedLocalization.FiniteEntropy.integrable_activeIndicator line 101
9. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardStep_integral_bound line 114
10. lemma OAI.RepeatedLocalization.FiniteEntropy.complementReward_some line 136
11. lemma OAI.RepeatedLocalization.FiniteEntropy.continuingReward_some line 139
12. lemma OAI.RepeatedLocalization.FiniteEntropy.complementStep_bound line 142
13. lemma OAI.RepeatedLocalization.FiniteEntropy.continuingStep_bound line 153