OAI/Analysis/IrrationalRotation/Rotation/RotationTransfer.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.mem_exponentialTransfer_domain_iff line 12
  2. theorem OAI.Invariant233.Rotation.exponentialTransfer_apply_ae line 18
  3. theorem OAI.Invariant233.Rotation.exponentialTransfer_injective line 24
  4. theorem OAI.Invariant233.Rotation.exponentialTransfer_coefficient_measurable line 29
  5. theorem OAI.Invariant233.Rotation.dense_exponentialTransfer_domain line 34
  6. theorem OAI.Invariant233.Rotation.exponentialTransfer_selfAdjoint line 41
  7. theorem OAI.Invariant233.Rotation.exponentialTransfer_isClosed line 47
  8. theorem OAI.Invariant233.Rotation.exponentialTransfer_nonnegative line 51