OAI/Dynamics/StandardMap/GridPartition.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.circleRep line 11
  2. lemma OAI.StandardMapEntropy.circleRep_mem line 12
  3. lemma OAI.StandardMapEntropy.measurable_circleRep line 15
  4. lemma OAI.StandardMapEntropy.coe_circleRep line 17
  5. lemma OAI.StandardMapEntropy.circleRep_coe line 18
  6. lemma OAI.StandardMapEntropy.circleRep_coe_of_mem line 20
  7. def OAI.StandardMapEntropy.torusRep line 22
  8. lemma OAI.StandardMapEntropy.torusRep_mem line 23
  9. lemma OAI.StandardMapEntropy.liftProjection_torusRep line 24
  10. lemma OAI.StandardMapEntropy.torusRep_projection line 26
  11. def OAI.StandardMapEntropy.gridIndex line 28
  12. lemma OAI.StandardMapEntropy.measurable_gridIndex line 31
  13. def OAI.StandardMapEntropy.gridLabel line 39
  14. lemma OAI.StandardMapEntropy.measurable_gridLabel line 41
  15. def OAI.StandardMapEntropy.gridPartition line 44
  16. lemma OAI.StandardMapEntropy.gridLabel_eq_iff line 46
  17. lemma OAI.StandardMapEntropy.gridIndex_bounds line 56
  18. lemma OAI.StandardMapEntropy.gridIndex_close line 64
  19. lemma OAI.StandardMapEntropy.gridLabel_close line 71
  20. lemma OAI.StandardMapEntropy.projection_wrappedBox line 75
  21. lemma OAI.StandardMapEntropy.unit_ico_cell_integral line 82
  22. def OAI.StandardMapEntropy.gridInterval line 89
  23. lemma OAI.StandardMapEntropy.gridInterval_length line 95
  24. lemma OAI.StandardMapEntropy.gridInterval_mem line 97