OAI/Dynamics/StandardMap/Components/SliceRectangleNonsingular.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.rectangle_quasiMeasurePreserving line 11
  2. theorem OAI.StandardMapEntropy.compact_graph_product_nonsingular line 51
  3. theorem OAI.StandardMapEntropy.compact_graph_rectangle line 106
  4. structure OAI.StandardMapEntropy.ReversibleGraphRectangle line 161
  5. theorem OAI.StandardMapEntropy.reversible_graph_rectangle line 170
  6. theorem OAI.StandardMapEntropy.complexProjection_quasiMeasurePreserving line 242
  7. theorem OAI.StandardMapEntropy.fineStableCurve_contracting_tangent line 272
  8. lemma OAI.StandardMapEntropy.vectorGrowth_le_log_of_bound line 306
  9. theorem OAI.StandardMapEntropy.fineStableCurve_spectrum_positive line 322
  10. theorem OAI.BoundedSubadditive.continuous_birkhoff_limit line 345
  11. structure OAI.BoundedSubadditive.ContinuousBirkhoffCode line 419
  12. theorem OAI.BoundedSubadditive.exists_continuousBirkhoffCode line 431
  13. lemma OAI.BoundedSubadditive.continuousMap_integrable line 444
  14. lemma OAI.BoundedSubadditive.continuous_integral_continuousMap line 447
  15. lemma OAI.BoundedSubadditive.measure_eq_of_dense_continuous_integrals line 454