OAI/Dynamics/StandardMap/Holonomy/CompactHolonomy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.compact_fibre_descent line 13
2. theorem OAI.StandardMapEntropy.compact_actual_stable_holonomy line 37
3. lemma OAI.StandardMapEntropy.fine_transverse_cone line 81
4. theorem OAI.StandardMapEntropy.actual_compact_slice_holonomy line 102
5. lemma OAI.StandardMapEntropy.complexRep_norm_le_two line 209
6. theorem OAI.StandardMapEntropy.compact_lift_fineRegular_block line 217
7. lemma OAI.StandardMapEntropy.positive_compact_neighborhood line 247
8. structure OAI.StandardMapEntropy.SmallPesinBlock line 277
9. theorem OAI.StandardMapEntropy.smallPesinBlock_within line 299
10. theorem OAI.StandardMapEntropy.exists_smallPesinBlock line 387