OAI/Dynamics/StandardMap/LiftDynamics.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.liftStep line 11
  2. lemma OAI.StandardMapEntropy.liftStep_apply line 16
  3. lemma OAI.StandardMapEntropy.liftStep_symm_apply line 18
  4. def OAI.StandardMapEntropy.liftIter line 20
  5. lemma OAI.StandardMapEntropy.liftIter_add line 21
  6. lemma OAI.StandardMapEntropy.liftIter_zero line 24
  7. lemma OAI.StandardMapEntropy.liftIter_nat line 25
  8. lemma OAI.StandardMapEntropy.phi_lipschitz line 35
  9. lemma OAI.StandardMapEntropy.liftStep_lipschitz line 44
  10. lemma OAI.StandardMapEntropy.liftStep_symm_lipschitz line 60
  11. lemma OAI.StandardMapEntropy.liftIter_lipschitz line 69