OAI/Dynamics/StandardMap/Components/BoundedBirkhoff.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedSubadditive.observation_integral_rate line 14
  2. theorem OAI.BoundedSubadditive.exists_bounded_birkhoff_limit line 38
  3. theorem OAI.BoundedSubadditive.forward_backward_birkhoff line 51
  4. lemma OAI.birkhoff_difference_tendsto_zero line 108
  5. lemma OAI.birkhoff_limit_eq_of_asymptotic line 124
  6. lemma OAI.StandardMapEntropy.complexProjection_dist_le line 133
  7. lemma OAI.StandardMapEntropy.fineStableCurve_asymptotic line 147
  8. theorem OAI.StandardMapEntropy.fineStableCurve_birkhoff_eq line 158
  9. def OAI.StandardMapEntropy.fineUnstableCurve line 177
  10. lemma OAI.StandardMapEntropy.fineUnstableCurve_zero line 180
  11. lemma OAI.StandardMapEntropy.fineUnstableCurve_contraction line 184
  12. lemma OAI.StandardMapEntropy.fineUnstableCurve_contDiffOn line 193
  13. lemma OAI.StandardMapEntropy.fineUnstableCurve_asymptotic line 197
  14. lemma OAI.StandardMapEntropy.fineUnstableCurve_birkhoff_eq line 208
  15. lemma OAI.StandardMapEntropy.ae_unstableVector_reversal_stable line 226
  16. lemma OAI.StandardMapEntropy.fineSize_eq_delta_mul line 233
  17. lemma OAI.StandardMapEntropy.fineFrame_eq_delta_smul line 238
  18. lemma OAI.StandardMapEntropy.fineInverse_eq_inv_delta_smul line 243
  19. lemma OAI.StandardMapEntropy.fine_relative_frame_independent_delta line 250
  20. lemma OAI.StandardMapEntropy.tangentReversal_wedge line 256
  21. lemma OAI.StandardMapEntropy.fineFrame_first line 260
  22. lemma OAI.StandardMapEntropy.fineFrame_second line 268
  23. lemma OAI.StandardMapEntropy.fineInverse_first_zero line 276
  24. lemma OAI.StandardMapEntropy.fineInverse_second_zero line 280
  25. theorem OAI.StandardMapEntropy.fine_reversal_frame_swap line 284
  26. theorem OAI.StandardMapEntropy.compact_reversible_fineRegular_block line 341
  27. theorem OAI.StandardMapEntropy.compact_lift_reversible_block line 395