OAI/Dynamics/StandardMap/FixedDeficit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.cosineBad line 11
  2. lemma OAI.StandardMapEntropy.measurable_cosineBad line 13
  3. lemma OAI.StandardMapEntropy.integrable_cosineBad line 15
  4. lemma OAI.StandardMapEntropy.integral_cosineBad line 17
  5. lemma OAI.StandardMapEntropy.circleFst_preserving line 21
  6. lemma OAI.StandardMapEntropy.bad_time_integrable line 23
  7. lemma OAI.StandardMapEntropy.bad_time_integral line 26
  8. lemma OAI.StandardMapEntropy.potential_large_of_cosine line 32
  9. lemma OAI.StandardMapEntropy.shortfall_small_of_cosine line 46
  10. lemma OAI.StandardMapEntropy.fixed_shortfall_pointwise line 72
  11. lemma OAI.StandardMapEntropy.meanDeficit_eq_integral_shortfall line 90
  12. lemma OAI.StandardMapEntropy.meanDeficit_fixed_bound line 101
  13. lemma OAI.StandardMapEntropy.meanDeficit_fixed_small line 118