OAI/Dynamics/StandardMap/BridgeAveraging.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.StandardMapEntropy.torusFastBridge line 11
2. lemma OAI.StandardMapEntropy.measurableSet_torusFastBridge line 13
3. def OAI.StandardMapEntropy.torusGoodMiddles line 15
4. lemma OAI.StandardMapEntropy.torus_good_middles_count line 18
5. lemma OAI.StandardMapEntropy.lintegral_count_cover line 46