OAI/Analysis/IrrationalRotation/Model/Rotation.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.Invariant233.Rotation.circleMeasure_probability line 17

    Also declared: ComparatorChallenges/IrrationalRotation.lean:257 (same declaration text).

  2. abbrev OAI.Invariant233.Rotation.Fiber line 22

    Also declared: ComparatorChallenges/IrrationalRotation.lean:262 (same declaration text).

  3. abbrev OAI.Invariant233.Rotation.Hilbert line 23

    Also declared: ComparatorChallenges/IrrationalRotation.lean:263 (same declaration text).

  4. def OAI.Invariant233.Rotation.action line 25

    Also declared: ComparatorChallenges/IrrationalRotation.lean:265 (same declaration text).

  5. def OAI.Invariant233.Rotation.U line 28

    Also declared: ComparatorChallenges/IrrationalRotation.lean:268 (same declaration text).

  6. def OAI.Invariant233.Rotation.orbitWeight line 31

    Also declared: ComparatorChallenges/IrrationalRotation.lean:271 (same declaration text).

  7. def OAI.Invariant233.Rotation.character line 37

    Also declared: ComparatorChallenges/IrrationalRotation.lean:277 (same declaration text).

  8. def OAI.Invariant233.Rotation.representation line 39

    Also declared: ComparatorChallenges/IrrationalRotation.lean:279 (same declaration text).

  9. def OAI.Invariant233.Rotation.V line 48

    Also declared: ComparatorChallenges/IrrationalRotation.lean:288 (same declaration text).

  10. def OAI.Invariant233.Rotation.algebra line 50

    Also declared: ComparatorChallenges/IrrationalRotation.lean:290 (same declaration text).

  11. def OAI.Invariant233.Rotation.weighted line 53

    Also declared: ComparatorChallenges/IrrationalRotation.lean:293 (same declaration text).

  12. def OAI.Invariant233.Rotation.complexWeight line 56

    Also declared: ComparatorChallenges/IrrationalRotation.lean:296 (same declaration text).

  13. def OAI.Invariant233.Rotation.weightedReal line 59

    Also declared: ComparatorChallenges/IrrationalRotation.lean:299 (same declaration text).

  14. def OAI.Invariant233.Rotation.vacuum line 62

    Also declared: ComparatorChallenges/IrrationalRotation.lean:302 (same declaration text).

  15. def OAI.Invariant233.Rotation.vacuumFunctional line 64

    Also declared: ComparatorChallenges/IrrationalRotation.lean:304 (same declaration text).