OAI/Dynamics/StandardMap/GraphFamilySmooth.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.hasStrictFDerivAt_liftedOrbit_shift line 11
2. lemma OAI.StandardMapEntropy.hasDerivAt_liftedOrbit_curve line 25
3. lemma OAI.StandardMapEntropy.continuousAt_of_local_lipschitz line 36
4. lemma OAI.StandardMapEntropy.contracting_family_derivatives line 48