OAI/Analysis/Laughlin/Pair/Moment.lean
5 declarations, 0 contain sorry, 0 declared as axioms
- theorem
OAI.Laughlin.pairCoefficient_scaledline 8 - def
OAI.Laughlin.weightedPairCoordinateline 21 - def
OAI.Laughlin.pairMomentline 25 - theorem
OAI.Laughlin.pairMoment_eq_amplitudeline 29 - theorem
OAI.Laughlin.weightedPairCoordinate_swapline 57