OAI/Analysis/Laughlin/Planar/Model.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.Laughlin.Planar.Occupations line 11

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

  2. def OAI.Laughlin.Planar.pairMatrix line 13

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

  3. def OAI.Laughlin.Planar.planarCoefficient line 18

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

  4. def OAI.Laughlin.Planar.sphereCoefficient line 21
  5. theorem OAI.Laughlin.Planar.sphereCoefficient_eq line 25
  6. theorem OAI.Laughlin.Planar.sphereCoefficient_tendsto line 30
  7. def OAI.Laughlin.Planar.planarPairMatrix line 37

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

  8. def OAI.Laughlin.Planar.spherePairMatrix line 40
  9. theorem OAI.Laughlin.Planar.spherePairMatrix_tendsto line 43
  10. def OAI.Laughlin.Planar.planarHamiltonian line 53

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

  11. def OAI.Laughlin.Planar.sphereHamiltonian line 56
  12. theorem OAI.Laughlin.Planar.sphereHamiltonian_tendsto line 59
  13. def OAI.Laughlin.Planar.pairEnergy line 69

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

  14. def OAI.Laughlin.Planar.squareNorm line 73

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

  15. theorem OAI.Laughlin.Planar.sphere_pairEnergy_tendsto line 76
  16. theorem OAI.Laughlin.Planar.sphere_squareNorm_tendsto line 91
  17. theorem OAI.Laughlin.Planar.endpoint_of_sphere_blocks line 104