OAI/Dynamics/StandardMap/ScaleEndpoints.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.coreLength line 11
2. lemma OAI.StandardMapEntropy.measurable_coreLength line 12
3. lemma OAI.StandardMapEntropy.coreLength_translate line 13
4. lemma OAI.StandardMapEntropy.coreLength_dilate line 17
5. lemma OAI.StandardMapEntropy.twoRayClass_half line 21
6. lemma OAI.StandardMapEntropy.coreLength_half line 26
7. lemma OAI.StandardMapEntropy.scaleZ_twoRay line 31
8. lemma OAI.StandardMapEntropy.scaleZ_length line 40
9. def OAI.StandardMapEntropy.lengthBand line 52
10. lemma OAI.StandardMapEntropy.measurableSet_lengthBand line 53
11. lemma OAI.StandardMapEntropy.lengthBand_scaleZ line 57
12. lemma OAI.StandardMapEntropy.lengthBand_translate line 80