OAI/Dynamics/StandardMap/TransferCore.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StandardMapEntropy.transferStep line 12

    Distinct definitions of this name: ComparatorChallenges/StandardMapComponents.lean:38 (same statement text; different proof or body), ComparatorChallenges/StandardMapLyapunov.lean:56 (same statement text; different proof or body). Qualify references as OAI.StandardMapEntropy.transferStep@path.

  2. lemma OAI.StandardMapEntropy.transferStep_re line 20
  3. lemma OAI.StandardMapEntropy.transferStep_im line 21
  4. def OAI.StandardMapEntropy.transferStepInv line 22
  5. lemma OAI.StandardMapEntropy.transferStepInv_re line 30
  6. lemma OAI.StandardMapEntropy.transferStepInv_im line 31
  7. lemma OAI.StandardMapEntropy.transferStep_area line 32
  8. lemma OAI.StandardMapEntropy.transferStepInv_area line 34
  9. lemma OAI.StandardMapEntropy.transferStep_inv line 36
  10. lemma OAI.StandardMapEntropy.transferStepInv_inv line 38
  11. lemma OAI.StandardMapEntropy.transferStep_norm line 40
  12. lemma OAI.StandardMapEntropy.transferStepInv_norm line 52
  13. def OAI.StandardMapEntropy.transferProduct line 56
  14. def OAI.StandardMapEntropy.transferProductInv line 59
  15. lemma OAI.StandardMapEntropy.transferProduct_pair line 62
  16. lemma OAI.StandardMapEntropy.transferProduct_area line 69
  17. lemma OAI.StandardMapEntropy.transferProductInv_area line 73
  18. lemma OAI.StandardMapEntropy.transferProduct_inverse line 77
  19. lemma OAI.StandardMapEntropy.transferProductInv_inverse line 82
  20. lemma OAI.StandardMapEntropy.transferProduct_norm_inverse line 87
  21. lemma OAI.StandardMapEntropy.transferProduct_norm_bounds line 91