OAI/Probability/Localization/EntropyBudget.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.RepeatedLocalization.FiniteEntropy.entropySlope line 13
2. def OAI.RepeatedLocalization.FiniteEntropy.historyKL line 15
3. def OAI.RepeatedLocalization.FiniteEntropy.historyCost line 18
4. lemma OAI.RepeatedLocalization.FiniteEntropy.entropySlope_pos line 21
5. lemma OAI.RepeatedLocalization.FiniteEntropy.historyCost_nonneg line 25
6. lemma OAI.RepeatedLocalization.FiniteEntropy.historyKL_ne_top_budget line 30
7. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_cost_bound line 51
8. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_depth_integrable line 81
9. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_KL_integrable line 93
10. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_attempts_integral line 105
11. lemma OAI.RepeatedLocalization.FiniteEntropy.slope_absorption line 125
12. lemma OAI.RepeatedLocalization.FiniteEntropy.truncated_final_budget line 132