OAI/Dynamics/StandardMap/CriticalSequence.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.doublingConstant_ge_one line 11
  2. def OAI.StandardMapEntropy.BadGrowth line 15
  3. lemma OAI.StandardMapEntropy.badGrowth_arbitrarily_large line 16
  4. lemma OAI.StandardMapEntropy.choose_critical_parameter line 22
  5. def OAI.StandardMapEntropy.criticalTheta line 49
  6. def OAI.StandardMapEntropy.criticalLowerExponent line 50
  7. lemma OAI.StandardMapEntropy.criticalTheta_pos line 51
  8. lemma OAI.StandardMapEntropy.criticalTheta_lt_one line 52
  9. lemma OAI.StandardMapEntropy.criticalTheta_square line 54
  10. lemma OAI.StandardMapEntropy.criticalTheta_tendsto line 60
  11. structure OAI.StandardMapEntropy.CriticalScaleSequence line 69
  12. lemma OAI.StandardMapEntropy.exists_critical_scale_sequence line 82
  13. def OAI.StandardMapEntropy.CriticalScaleSequence.epsilon line 114
  14. lemma OAI.StandardMapEntropy.CriticalScaleSequence.epsilon_pos line 115
  15. lemma OAI.StandardMapEntropy.CriticalScaleSequence.epsilon_tendsto line 116
  16. lemma OAI.StandardMapEntropy.CriticalScaleSequence.parameter_tendsto line 119
  17. lemma OAI.StandardMapEntropy.CriticalScaleSequence.initial_ratio_bound line 121
  18. lemma OAI.StandardMapEntropy.CriticalScaleSequence.initial_ratio_tendsto line 132