OAI/Analysis/IrrationalRotation/Model/WeightedShift.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.WeightedShift.Hilbert line 13

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

2. abbrev OAI.Invariant233.WeightedShift.Weight line 14

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

3. def OAI.Invariant233.WeightedShift.reindex line 16

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

4. def OAI.Invariant233.WeightedShift.shift line 30

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

5. def OAI.Invariant233.WeightedShift.diagonal line 32

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

6. def OAI.Invariant233.WeightedShift.diagonalAlgHom line 38

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

7. def OAI.Invariant233.WeightedShift.translate line 61

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

8. def OAI.Invariant233.WeightedShift.operator line 67

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

9. def OAI.Invariant233.WeightedShift.orbitProduct line 70

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

10. def OAI.Invariant233.WeightedShift.tailWeight line 83

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

11. def OAI.Invariant233.WeightedShift.tailProjection line 89

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