OAI/Analysis/Laughlin/Asymptotics/TruncatedMetricPerturbation.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- def
OAI.Laughlin.Fock.occupationQuadraticline 8 - theorem
OAI.Laughlin.Fock.occupationQuadratic_coordinatesline 12 - theorem
OAI.Laughlin.Fock.truncatedQuadratic_errorline 26