OAI/Dynamics/StandardMap/Coding/PositiveWeakBernoulliRate.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HyperbolicCoding.weakBernoulli_zero_rate_diagonal line 13
2. lemma OAI.HyperbolicCoding.weakBernoulli_zero_rate_constant line 40
3. theorem OAI.HyperbolicCoding.separating_weakBernoulli_positive_rate line 82
4. lemma OAI.HyperbolicCoding.weightEntropy_eq_shannon line 119
5. def OAI.HyperbolicCoding.entropyPath line 127
6. lemma OAI.HyperbolicCoding.entropyPath_nonneg line 130
7. lemma OAI.HyperbolicCoding.entropyPath_sum line 136
8. lemma OAI.HyperbolicCoding.entropyPath_continuous line 144
9. lemma OAI.HyperbolicCoding.entropyPath_zero line 152
10. lemma OAI.HyperbolicCoding.entropyPath_one line 159
11. theorem OAI.HyperbolicCoding.exists_finite_weight_entropy line 166
12. lemma OAI.StandardMapEntropy.normalizedArea_nullSingleton line 187
13. theorem OAI.StandardMapEntropy.actual_return_full_entropy_iid_factor line 193