OAI/Analysis/RotationWeights/Model.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContinuousCircleWeight.CircleX line 10

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:10 (same declaration text).

2. abbrev OAI.ContinuousCircleWeight.TracialHilbert line 12

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

3. abbrev OAI.ContinuousCircleWeight.Operator line 13

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:13 (same declaration text).

4. def OAI.ContinuousCircleWeight.circleIdentification line 15

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:15 (same declaration text).

5. def OAI.ContinuousCircleWeight.circleFunction line 17

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:17 (same declaration text).

6. def OAI.ContinuousCircleWeight.negativeLog line 20

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:20 (same declaration text).

7. structure OAI.ContinuousCircleWeight.IsTracialRotation line 23

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

8. def OAI.ContinuousCircleWeight.rotationAlgebra line 34

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:34 (same declaration text).

9. def OAI.ContinuousCircleWeight.weightedRotation line 37

   Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:37 (same declaration text).

10. def OAI.ContinuousCircleWeight.MainStatement line 40

    Also declared: ComparatorChallenges/ContinuousCircleWeight.lean:40 (same declaration text).