OAI/Dynamics/StandardMap/CurveIterate.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.CurveTree line 11
2. instance OAI.StandardMapEntropy.curveTreeFintype line 14
3. lemma OAI.StandardMapEntropy.curveTree_card line 18
4. def OAI.StandardMapEntropy.fullCurveInterval line 24
5. lemma OAI.StandardMapEntropy.fullCurveInterval_parameter line 25
6. lemma OAI.StandardMapEntropy.curve_iterate_cover line 27
7. def OAI.StandardMapEntropy.curveIterVelocity line 63
8. lemma OAI.StandardMapEntropy.curveIter_hasDeriv line 66
9. lemma OAI.StandardMapEntropy.curveIter_velocity_continuous line 77