OAI/Dynamics/EntropyCounterexample/SparseLogBound.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem340.SparseLogBound.rate line 11
2. def OAI.Problem340.SparseLogBound.principalRate line 15
3. lemma OAI.Problem340.SparseLogBound.log_code_count line 18
4. theorem OAI.Problem340.SparseLogBound.rate_le line 26
5. theorem OAI.Problem340.SparseLogBound.principalRate_le_rate line 46
6. theorem OAI.Problem340.SparseLogBound.tendsto_rate line 65
7. theorem OAI.Problem340.SparseLogBound.eventually_rate_lt line 83
8. theorem OAI.Problem340.SparseLogBound.eventually_nat_log_rate_lt line 90