OAI/Dynamics/StandardMap/SmoothCap.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.capSlope line 11
  2. def OAI.StandardMapEntropy.capPrimitive line 12
  3. def OAI.StandardMapEntropy.capBase line 13
  4. def OAI.StandardMapEntropy.entropyCap line 14
  5. lemma OAI.StandardMapEntropy.capSlope_contDiff line 16
  6. lemma OAI.StandardMapEntropy.capSlope_continuous line 17
  7. lemma OAI.StandardMapEntropy.capSlope_bounds line 18
  8. lemma OAI.StandardMapEntropy.capSlope_one line 21
  9. lemma OAI.StandardMapEntropy.capSlope_zero line 24
  10. lemma OAI.StandardMapEntropy.capPrimitive_hasDerivAt line 27
  11. lemma OAI.StandardMapEntropy.capPrimitive_deriv line 30
  12. lemma OAI.StandardMapEntropy.capPrimitive_contDiff line 31
  13. lemma OAI.StandardMapEntropy.capPrimitive_monotone line 38
  14. lemma OAI.StandardMapEntropy.capPrimitive_linear line 45
  15. lemma OAI.StandardMapEntropy.capPrimitive_constant line 55
  16. lemma OAI.StandardMapEntropy.capBase_bounds line 67
  17. lemma OAI.StandardMapEntropy.entropyCap_contDiff line 78
  18. lemma OAI.StandardMapEntropy.entropyCap_linear line 82
  19. lemma OAI.StandardMapEntropy.entropyCap_one line 86
  20. lemma OAI.StandardMapEntropy.entropyCap_monotone line 90
  21. lemma OAI.StandardMapEntropy.entropyCap_bounds line 96
  22. lemma OAI.StandardMapEntropy.entropyCap_lower line 103