OAI/Analysis/Laughlin/Planar/Restriction.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Laughlin.Planar.pairMatrix_toMatrix line 11
2. theorem OAI.Laughlin.Planar.occupationInner_basis_left line 18
3. theorem OAI.Laughlin.Planar.occupationInner_basis_right line 22
4. theorem OAI.Laughlin.Planar.pairCreateMatrix_toMatrix line 26
5. theorem OAI.Laughlin.Planar.sphereHamiltonian_toMatrix line 36
6. theorem OAI.Laughlin.Planar.sphere_pairEnergy_eq line 48
7. theorem OAI.Laughlin.Planar.sphere_squareNorm_eq line 58
8. theorem OAI.Laughlin.Planar.finite_degree_endpoint_of_fock_square line 64
9. theorem OAI.Laughlin.Planar.finite_degree_endpoint line 78