OAI/Analysis/Laughlin/Model.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.Laughlin.Configuration line 8

   Also declared: ComparatorChallenges/Laughlin.lean:8 (same declaration text), ComparatorChallenges/LaughlinGap.lean:8 (same declaration text).

2. abbrev OAI.Laughlin.State line 9

   Also declared: ComparatorChallenges/Laughlin.lean:9 (same declaration text), ComparatorChallenges/LaughlinGap.lean:9 (same declaration text).

3. def OAI.Laughlin.Antisymmetric line 11

   Also declared: ComparatorChallenges/Laughlin.lean:11 (same declaration text), ComparatorChallenges/LaughlinGap.lean:12 (same declaration text).

4. def OAI.Laughlin.pairCoefficient line 14

   Also declared: ComparatorChallenges/Laughlin.lean:14 (same declaration text), ComparatorChallenges/LaughlinFock.lean:11 (same declaration text), ComparatorChallenges/LaughlinGap.lean:16 (same declaration text).

5. def OAI.Laughlin.pairAmplitude line 23

   Also declared: ComparatorChallenges/Laughlin.lean:23 (same declaration text), ComparatorChallenges/LaughlinGap.lean:27 (same declaration text).

6. def OAI.Laughlin.energy line 28

   Also declared: ComparatorChallenges/Laughlin.lean:28 (same declaration text), ComparatorChallenges/LaughlinGap.lean:34 (same declaration text).

7. abbrev OAI.Laughlin.SpinorVariables line 34

   Also declared: ComparatorChallenges/Laughlin.lean:34 (same declaration text), ComparatorChallenges/LaughlinGap.lean:40 (same declaration text).

8. def OAI.Laughlin.bracket line 36

   Also declared: ComparatorChallenges/Laughlin.lean:36 (same declaration text), ComparatorChallenges/LaughlinGap.lean:43 (same declaration text).

9. def OAI.Laughlin.laughlinPolynomial line 40

   Also declared: ComparatorChallenges/Laughlin.lean:40 (same declaration text), ComparatorChallenges/LaughlinGap.lean:48 (same declaration text).

10. def OAI.Laughlin.monomialExponent line 43

    Also declared: ComparatorChallenges/Laughlin.lean:43 (same declaration text), ComparatorChallenges/LaughlinGap.lean:52 (same declaration text).

11. def OAI.Laughlin.laughlinVector line 48

    Also declared: ComparatorChallenges/Laughlin.lean:48 (same declaration text), ComparatorChallenges/LaughlinGap.lean:59 (same declaration text).

12. def OAI.Laughlin.distanceToLaughlinSq line 52

    Also declared: ComparatorChallenges/Laughlin.lean:52 (same declaration text), ComparatorChallenges/LaughlinGap.lean:65 (same declaration text).

13. def OAI.Laughlin.MainTarget line 56

    Also declared: ComparatorChallenges/Laughlin.lean:56 (same declaration text).