OAI/Dynamics/StandardMap/Lyapunov/Definitions.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.tangentCoordinates line 11

    Also declared: ComparatorChallenges/StandardMapComponents.lean:49 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:65 (same declaration text).

  2. def OAI.StandardMapEntropy.standardDerivative line 22

    Also declared: ComparatorChallenges/StandardMapComponents.lean:60 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:76 (same declaration text).

  3. def OAI.StandardMapEntropy.standardDerivativeProduct line 25

    Distinct definitions of this name: ComparatorChallenges/StandardMapComponents.lean:63 (different declaration text), ComparatorChallenges/StandardMapLyapunov.lean:79 (same declaration text). Qualify references as OAI.StandardMapEntropy.standardDerivativeProduct@path.

  4. lemma OAI.StandardMapEntropy.standardDerivativeProduct_zero line 29
  5. lemma OAI.StandardMapEntropy.standardDerivativeProduct_succ line 32
  6. def OAI.StandardMapEntropy.standardInverseDerivative line 37
  7. def OAI.StandardMapEntropy.complexProjection line 41
  8. def OAI.StandardMapEntropy.standardLift line 42
  9. def OAI.StandardMapEntropy.standardInverseLift line 44
  10. def OAI.StandardMapEntropy.VectorGrowth line 47

    Also declared: ComparatorChallenges/StandardMapComponents.lean:67 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:85 (same declaration text).

  11. def OAI.StandardMapEntropy.LyapunovSpectrumAt line 51

    Also declared: ComparatorChallenges/StandardMapComponents.lean:71 (same declaration text), ComparatorChallenges/StandardMapLyapunov.lean:89 (same declaration text).