OAI/Dynamics/StandardMap/Holonomy/FinePlaqueParameters.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StandardMapEntropy.fine_plaque_parameters line 13
  2. lemma OAI.StandardMapEntropy.fineStableGraph_slope line 40
  3. lemma OAI.StandardMapEntropy.fine_holonomy_parameters line 56
  4. lemma OAI.StandardMapEntropy.NonlinearStable.Recurrence.orbit_solution line 83
  5. lemma OAI.StandardMapEntropy.fine_central_orbit_decay line 89
  6. theorem OAI.StandardMapEntropy.fine_stable_matching_local_bound line 109
  7. theorem OAI.StandardMapEntropy.null_image_of_pointwise_local_bound line 179
  8. lemma OAI.StandardMapEntropy.fine_affine_coordinates line 230
  9. theorem OAI.StandardMapEntropy.actual_stable_holonomy_null_image line 239
  10. lemma OAI.StandardMapEntropy.strictMono_of_linear_error line 278
  11. theorem OAI.StandardMapEntropy.compact_graph_crossing line 285
  12. lemma OAI.StandardMapEntropy.fine_graph_pair_bound line 335
  13. def OAI.StandardMapEntropy.finePlaqueInChart line 343
  14. lemma OAI.StandardMapEntropy.fine_plaque_linear_error line 348
  15. lemma OAI.StandardMapEntropy.fine_plaque_crossing_unique line 370
  16. theorem OAI.StandardMapEntropy.fine_compact_graph_crossing line 377
  17. theorem OAI.StandardMapEntropy.fine_small_crossings_coincide line 409