OAI/Probability/Localization/TerminalBudget.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.FiniteEntropy.terminalKL line 12
2. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_terminalKL line 16
3. lemma OAI.RepeatedLocalization.FiniteEntropy.measurable_depth_real line 21
4. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_historyKL line 26
5. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_cost_budget line 32
6. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_depth_integrable line 58
7. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_KL_integrable line 68
8. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_attempts_budget line 76
9. lemma OAI.RepeatedLocalization.FiniteEntropy.terminal_ennreal_budget line 105