OAI/Dynamics/StandardMap/EntropyLyapunov.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.PositiveLargestLyapunov line 10

   Also declared: ComparatorChallenges/StandardMapLyapunov.lean:94 (same declaration text).

2. lemma OAI.StandardMapEntropy.positiveLargestLyapunov_of_ae_spectrum line 17
3. theorem OAI.StandardMapEntropy.main_entropy_complete line 38

   Distinct definitions of this name: ComparatorChallenges/StandardMapLyapunov.lean:101 (same statement text; different proof or body). Qualify references as OAI.StandardMapEntropy.main_entropy_complete@path.