OAI/Dynamics/StandardMap/DyadicArrays.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.dyadicTimes line 12
  2. abbrev OAI.StandardMapEntropy.DyadicTime line 24
  3. lemma OAI.StandardMapEntropy.dyadicTime_mem line 25
  4. instance OAI.StandardMapEntropy.(instance at line 26) line 26
  5. def OAI.StandardMapEntropy.dyadicInt line 32
  6. lemma OAI.StandardMapEntropy.dyadicInt_val line 33
  7. def OAI.StandardMapEntropy.dyadicHalf line 34
  8. lemma OAI.StandardMapEntropy.dyadicHalf_val line 39
  9. lemma OAI.StandardMapEntropy.dyadicHalf_add_self line 40
  10. lemma OAI.StandardMapEntropy.dyadicHalf_double line 43
  11. def OAI.StandardMapEntropy.dyadicMid line 46
  12. lemma OAI.StandardMapEntropy.dyadicMid_val line 47
  13. lemma OAI.StandardMapEntropy.dyadicTime_dense line 48
  14. def OAI.StandardMapEntropy.AmbientArray line 79
  15. abbrev OAI.StandardMapEntropy.DistanceArray line 82
  16. lemma OAI.StandardMapEntropy.isClosed_ambientArray line 83
  17. lemma OAI.StandardMapEntropy.isCompact_ambientArray line 100
  18. instance OAI.StandardMapEntropy.(instance at line 106) line 106
  19. def OAI.StandardMapEntropy.arrayEval line 107
  20. lemma OAI.StandardMapEntropy.continuous_arrayEval line 108
  21. def OAI.StandardMapEntropy.affineArray line 110
  22. lemma OAI.StandardMapEntropy.continuous_affineArray line 122
  23. def OAI.StandardMapEntropy.affineLocus line 127
  24. lemma OAI.StandardMapEntropy.isCompact_affineLocus line 128
  25. lemma OAI.StandardMapEntropy.isClosed_affineLocus line 129
  26. abbrev OAI.StandardMapEntropy.NonAffineArray line 130