OAI/Dynamics/StandardMap/Components/PowerAtomCycles.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.BoundedSubadditive.PowerAtomFamily line 14
  2. lemma OAI.BoundedSubadditive.PowerAtomFamily.refinement line 25
  3. def OAI.BoundedSubadditive.PowerAtomFamily.cycle line 32
  4. lemma OAI.BoundedSubadditive.PowerAtomFamily.periods_bounded line 37
  5. lemma OAI.BoundedSubadditive.PowerAtomFamily.exists_max_period line 53
  6. theorem OAI.BoundedSubadditive.PowerAtomFamily.exists_totally_ergodic_cycle line 64
  7. theorem OAI.StandardMapEntropy.exists_reversibleRectangleBlock line 114
  8. theorem OAI.StandardMapEntropy.actual_hyperbolic_ergodic_component line 264
  9. lemma OAI.StandardMapEntropy.exists_positive_spectral_gap line 299
  10. theorem OAI.StandardMapEntropy.eventually_actual_hyperbolic_ergodic_component line 317
  11. theorem OAI.StandardMapEntropy.actual_powerAtomFamily line 338
  12. lemma OAI.StandardMapEntropy.positive_spectrum_on_ergodic_component line 361
  13. theorem OAI.StandardMapEntropy.actual_cyclic_totally_ergodic_component line 384
  14. theorem OAI.StandardMapEntropy.eventually_actual_cyclic_totally_ergodic_component line 420