OAI/Probability/Localization/TruncatedBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.RepeatedLocalization.FiniteEntropy.rewardLog_run_succ line 12
2. lemma OAI.RepeatedLocalization.FiniteEntropy.complementTotal_succ line 20
3. lemma OAI.RepeatedLocalization.FiniteEntropy.continuingTotal_succ line 24
4. lemma OAI.RepeatedLocalization.FiniteEntropy.truncatedAttempts_succ line 28
5. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_truncatedAttempts line 34
6. lemma OAI.RepeatedLocalization.FiniteEntropy.integrable_truncatedAttempts line 38
7. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_reward_bounds line 45
8. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_attempts_path line 73