OAI/Dynamics/EntropyCounterexample/EntropyBounds.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.Problem340.log_nat_div_tendsto_zero line 10
2. lemma OAI.Problem340.expGrowthSup_nat_pow line 15
3. lemma OAI.Problem340.expGrowthSup_le_zero_of_polynomial_bound line 34
4. lemma OAI.Problem340.coverEntropy_eq_zero_of_polynomial_cover_bound line 49
5. lemma OAI.Problem340.coverEntropy_eq_zero_of_polynomial_net_bound line 62
6. lemma OAI.Problem340.netMaxcard_le_card_of_orbit_code line 76
7. lemma OAI.Problem340.coverEntropy_eq_zero_of_eventually_polynomial_net_bound line 94
8. lemma OAI.Problem340.coverEntropy_eq_zero_of_polynomial_orbit_codes line 108