OAI/Dynamics/StandardMap/ClippedTests.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.clippedTest line 11
  2. lemma OAI.StandardMapEntropy.clippedTest_eq line 13
  3. lemma OAI.StandardMapEntropy.clippedTest_nonneg line 17
  4. lemma OAI.StandardMapEntropy.clippedTest_le line 20
  5. lemma OAI.StandardMapEntropy.continuous_clippedTest line 31
  6. lemma OAI.StandardMapEntropy.integrable_clippedTest line 33
  7. lemma OAI.StandardMapEntropy.unitArray_shortfall_mem line 36
  8. lemma OAI.StandardMapEntropy.clippedTest_unit line 48
  9. def OAI.StandardMapEntropy.clippedShortfall line 52
  10. lemma OAI.StandardMapEntropy.clippedShortfall_nonneg line 53
  11. lemma OAI.StandardMapEntropy.continuous_clippedShortfall line 54
  12. lemma OAI.StandardMapEntropy.clippedShortfall_unit line 56
  13. lemma OAI.StandardMapEntropy.clippedShortfall_sample line 58
  14. lemma OAI.StandardMapEntropy.integral_clippedShortfall_sample line 65