OAI/Dynamics/StandardMap/RealArrays.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.UnitArray line 11
  2. def OAI.StandardMapEntropy.TreeArray line 12
  3. lemma OAI.StandardMapEntropy.isClosed_unitArray line 15
  4. lemma OAI.StandardMapEntropy.isClosed_treeArray line 19
  5. lemma OAI.StandardMapEntropy.unitArray_diff line 26
  6. lemma OAI.StandardMapEntropy.unitArray_lipschitz line 41
  7. lemma OAI.StandardMapEntropy.denseRange_dyadicTime line 50
  8. lemma OAI.StandardMapEntropy.dyadicPairDense line 51
  9. def OAI.StandardMapEntropy.realArray line 54
  10. lemma OAI.StandardMapEntropy.continuous_realArray line 56
  11. lemma OAI.StandardMapEntropy.realArray_coe line 61
  12. lemma OAI.StandardMapEntropy.realArray_nonneg line 66
  13. lemma OAI.StandardMapEntropy.realArray_le line 69
  14. lemma OAI.StandardMapEntropy.realArray_self line 72
  15. lemma OAI.StandardMapEntropy.realArray_symm line 77
  16. lemma OAI.StandardMapEntropy.realArray_triangle line 81
  17. lemma OAI.StandardMapEntropy.realArray_tree line 88