OAI/Dynamics/StandardMap/Components/CurvedHolonomy.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.StandardMapEntropy.curved_holonomy_local_bound line 12
  2. theorem OAI.StandardMapEntropy.curved_inverse_holonomy_local_bound line 35
  3. theorem OAI.StandardMapEntropy.curved_holonomy_null_image line 57
  4. def OAI.StandardMapEntropy.AffineGraphControl line 75
  5. lemma OAI.StandardMapEntropy.AffineGraphControl.fibres line 80
  6. theorem OAI.StandardMapEntropy.compact_curved_inverse_control line 89
  7. lemma OAI.StandardMapEntropy.AffineGraphControl.comp line 150
  8. lemma OAI.StandardMapEntropy.AffineGraphControl.scale line 164
  9. def OAI.StandardMapEntropy.ReversibleRectangleBlock.holonomyConstant line 200
  10. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.holonomyConstant_pos line 201
  11. def OAI.StandardMapEntropy.ReversibleRectangleBlock.stableInterval line 202
  12. def OAI.StandardMapEntropy.ReversibleRectangleBlock.unstableInterval line 203
  13. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.mem_stableInterval line 204
  14. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.mem_unstableInterval line 208
  15. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.reverseCoordinates_chart line 212
  16. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.reverse_chart_coordinates line 224
  17. lemma OAI.StandardMapEntropy.ReversibleGraphFamilies.stable_control line 233
  18. lemma OAI.StandardMapEntropy.ReversibleGraphFamilies.reverse_representation line 246
  19. lemma OAI.StandardMapEntropy.ReversibleGraphFamilies.unstable_control line 262
  20. def OAI.StandardMapEntropy.ReversibleRectangleBlock.coordinateCarrier line 307
  21. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.compact_coordinateCarrier line 308
  22. def OAI.StandardMapEntropy.ReversibleRectangleBlock.label line 309
  23. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.continuous_label line 314
  24. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.coordinates_label line 316
  25. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.chart_image_carrier line 318
  26. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.volume_chart_image line 327
  27. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.positive_coordinateCarrier line 335
  28. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.volume_coordinate_univ line 341
  29. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.finite_coordinate_volume line 345
  30. lemma OAI.StandardMapEntropy.ReversibleRectangleBlock.chart_quasiMeasurePreserving line 350
  31. theorem OAI.StandardMapEntropy.label_nonsingular_of_vertical_inverse line 379
  32. theorem OAI.StandardMapEntropy.label_nonsingular_of_horizontal_inverse line 408
  33. theorem OAI.ae_constant_of_product_rows_columns line 444
  34. theorem OAI.positive_atom_of_hopf_product line 465