OAI/Dynamics/StandardMap/ScaleAction.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.nonaffineDouble line 11
  2. lemma OAI.StandardMapEntropy.measurable_nonaffineDouble line 13
  3. lemma OAI.StandardMapEntropy.nonaffineDouble_unit line 15
  4. lemma OAI.StandardMapEntropy.nonaffineHalf_unit_iff line 19
  5. def OAI.StandardMapEntropy.scaleEquiv line 23
  6. def OAI.StandardMapEntropy.scaleZ line 36
  7. lemma OAI.StandardMapEntropy.scaleZ_add line 37
  8. lemma OAI.StandardMapEntropy.scaleZ_zero line 40
  9. lemma OAI.StandardMapEntropy.scaleZ_one line 41
  10. lemma OAI.StandardMapEntropy.scaleZ_neg_one line 42
  11. lemma OAI.StandardMapEntropy.scaleZ_unit line 43
  12. lemma OAI.StandardMapEntropy.measurable_scaleZ line 50
  13. lemma OAI.StandardMapEntropy.map_scaleZ line 61