OAI/Dynamics/StandardMap/MeanDeficit.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.torusIterMeasurableEquiv line 11
  2. lemma OAI.StandardMapEntropy.integral_torusIter line 17
  3. lemma OAI.StandardMapEntropy.integrable_productDistance line 20
  4. lemma OAI.StandardMapEntropy.continuous_wingDefect line 23
  5. lemma OAI.StandardMapEntropy.continuous_cancellationLoss line 25
  6. def OAI.StandardMapEntropy.meanDeficit line 28
  7. lemma OAI.StandardMapEntropy.integral_productDistance_bounds line 30
  8. lemma OAI.StandardMapEntropy.meanDeficit_bounds line 35
  9. lemma OAI.StandardMapEntropy.integral_distance_shift line 41
  10. lemma OAI.StandardMapEntropy.integral_wing_left line 46
  11. lemma OAI.StandardMapEntropy.integral_wingDefect_le line 50
  12. lemma OAI.StandardMapEntropy.integral_cancellationLoss line 77
  13. lemma OAI.StandardMapEntropy.meanDeficit_doubling_mono line 95