OAI/Dynamics/StandardMap/ClosedEligibility.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.fast_prefix_row line 11
2. lemma OAI.StandardMapEntropy.eligible_prefix_dirichlet line 25
3. def OAI.StandardMapEntropy.prefixEligible line 53
4. lemma OAI.StandardMapEntropy.continuous_transferStep line 59
5. lemma OAI.StandardMapEntropy.continuous_transferProduct_params line 67
6. lemma OAI.StandardMapEntropy.continuous_orbitCoefficient_pair line 74
7. lemma OAI.StandardMapEntropy.isClosed_prefixEligible line 80