OAI/Dynamics/StandardMap/Components/FineChartGraph.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.StandardMapEntropy.fine_plaque_second_bound line 13
2. theorem OAI.StandardMapEntropy.fine_compact_chart_graph line 41
3. lemma OAI.StandardMapEntropy.shrink_fine_holonomy_delta line 120
4. lemma OAI.StandardMapEntropy.small_chart_radius line 138
5. structure OAI.StandardMapEntropy.ReversibleRectangleBlock line 155
6. def OAI.StandardMapEntropy.ReversibleRectangleBlock.chart line 230
7. def OAI.StandardMapEntropy.ReversibleRectangleBlock.coordinates line 231
8. def OAI.StandardMapEntropy.ReversibleRectangleBlock.reverseCoordinates line 232
9. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.chart_coordinates line 235
10. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.coordinates_chart line 238
11. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.coordinates_swap line 240
12. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.continuous_chart line 245
13. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.continuous_coordinates line 246
14. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.chart_injective line 247
15. structure OAI.StandardMapEntropy.ReversibleGraphFamilies line 253
16. theorem OAI.StandardMapEntropy.reversible_graph_families line 273
17. theorem OAI.StandardMapEntropy.actual_stable_holonomy_local_bound line 368
18. theorem OAI.StandardMapEntropy.compact_actual_stable_holonomy_bounds line 406
19. theorem OAI.StandardMapEntropy.actual_graph_holonomy_bounds line 450