OAI/Analysis/IrrationalRotation/Rotation/MeasurableRotationDenseRange.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Invariant233.Rotation.measurableRepresentation_injective_of_ae_ne_zero line 12
  2. theorem OAI.Invariant233.Rotation.measurableRepresentation_denseRange_of_ae_ne_zero line 32
  3. theorem OAI.Invariant233.Rotation.U_mul_measurableRepresentation_injective_of_ae_ne_zero line 43
  4. theorem OAI.Invariant233.Rotation.U_mul_measurableRepresentation_denseRange_of_ae_ne_zero line 51
  5. theorem OAI.Invariant233.CircleParameterLaws.measurableOperator_injective line 65
  6. theorem OAI.Invariant233.CircleParameterLaws.measurableOperator_denseRange line 69