OAI/Analysis/Laughlin/Planar/Forms.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.Laughlin.Planar.HomogeneousState line 11

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

2. def OAI.Laughlin.Planar.fullNormSq line 15
3. def OAI.Laughlin.Planar.IsHilbertState line 18
4. def OAI.Laughlin.Planar.fullEnergy line 20

   Also declared: ComparatorChallenges/LaughlinPlanar.lean:65 (same declaration text).

5. def OAI.Laughlin.Planar.fullSquareNorm line 24

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

6. theorem OAI.Laughlin.Planar.full_planar_endpoint line 28