OAI/Dynamics/StandardMap/NonaffineLimits.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. instance OAI.StandardMapEntropy.(instance at line 11) line 11
2. def OAI.StandardMapEntropy.nonaffinePart line 12
3. instance OAI.StandardMapEntropy.(instance at line 13) line 13
4. lemma OAI.StandardMapEntropy.integral_nonaffinePart_le line 14
5. lemma OAI.StandardMapEntropy.integrable_nonaffinePart line 22
6. lemma OAI.StandardMapEntropy.compact_test_domination line 28
7. lemma OAI.StandardMapEntropy.cc_integral_nonaffine_bound line 49
8. lemma OAI.StandardMapEntropy.exists_nonaffine_vague_limit line 72