OAI/Dynamics/StandardMap/Bernoulli/ReverseFano.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.Entropy.shannon_ge_one_sub_max line 13
2. lemma OAI.StandardMapEntropy.Entropy.shannon_ge_total_sub_max line 26
3. theorem OAI.StandardMapEntropy.Entropy.exists_decoder_error_le_cond line 52
4. lemma OAI.HyperbolicCoding.exists_eventual_decoder line 107
5. theorem OAI.HyperbolicCoding.exists_factor_of_approx line 161
6. lemma OAI.StandardMapEntropy.Entropy.cond_factor_left line 192
7. lemma OAI.StandardMapEntropy.Entropy.cond_future_tendsto line 199
8. theorem OAI.StandardMapEntropy.Entropy.tailObservable_self_of_rate_zero line 227
9. def OAI.StandardMapEntropy.Entropy.wordPairEquiv line 272
10. lemma OAI.StandardMapEntropy.Entropy.wordPairEquiv_apply line 280
11. lemma OAI.StandardMapEntropy.Entropy.obs_word_pair line 286
12. lemma OAI.StandardMapEntropy.Entropy.rate_pair_ge_left line 290
13. lemma OAI.StandardMapEntropy.Entropy.rate_pair_subadd line 302
14. lemma OAI.StandardMapEntropy.Entropy.rate_pair_eq_of_zero line 314
15. lemma OAI.StandardMapEntropy.Entropy.rate_comp_iterate line 323
16. lemma OAI.StandardMapEntropy.Entropy.rate_mul_le_cond_future_zero line 346
17. lemma OAI.StandardMapEntropy.Entropy.cond_future_zero_bound line 385
18. lemma OAI.StandardMapEntropy.Entropy.inverse_iterate_forward_sub line 416
19. lemma OAI.StandardMapEntropy.Entropy.forward_iterate_inverse_sub line 423
20. def OAI.StandardMapEntropy.Entropy.wordReverseEquiv line 429
21. lemma OAI.StandardMapEntropy.Entropy.obs_word_inverse line 436
22. lemma OAI.StandardMapEntropy.Entropy.rate_inverse line 452