OAI/Analysis/IrrationalRotation/Model/Analytic.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Invariant233.Circle line 14

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

2. def OAI.Invariant233.circleMeasure line 16

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

3. def OAI.Invariant233.negLogCost line 18

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

4. def OAI.Invariant233.HasNegInfiniteLogIntegral line 21

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

5. def OAI.Invariant233.scalarWeightDeterminant line 25

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

6. def OAI.Invariant233.NormQuasinilpotent line 29

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

7. def OAI.Invariant233.IsContinuousCircleWeight line 32

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