OAI/Analysis/Laughlin/Spin/
298 declarations, 0 contain sorry, 0 declared as axioms; 54 files
Files
- Array.lean 3 declarations
- ArrayLimit.lean 2 declarations
- Basic.lean 12 declarations
- Basis.lean 8 declarations
- Basis2.lean 7 declarations
- BinomialWeights.lean 3 declarations
- Compact.lean 7 declarations
- CompactAverage.lean 4 declarations
- CopySchur.lean 7 declarations
- DescendantNorm.lean 8 declarations
- Disjoint.lean 3 declarations
- EmbeddedSpinHaar.lean 1 declarations
- Endpoint.lean 3 declarations
- GeneralSpinAction.lean 8 declarations
- GenericNormalizedLadder.lean 1 declarations
- GenericOrthogonality.lean 3 declarations
- Haar.lean 8 declarations
- HaarOrthogonality.lean 2 declarations
- Highest.lean 6 declarations
- Highest2.lean 7 declarations
- HighestSpace.lean 12 declarations
- Intertwining.lean 6 declarations
- LadderGroupIntertwining.lean 2 declarations
- LadderMatrix.lean 6 declarations
- LoweringLimit.lean 2 declarations
- MatrixAverage.lean 10 declarations
- Mixing.lean 6 declarations
- Multidegree.lean 6 declarations
- OrbitalExpansion.lean 5 declarations
- Orthogonal.lean 3 declarations
- OscillatorHighest.lean 7 declarations
- OscillatorHighestNormalization.lean 4 declarations
- PairDecomposition.lean 5 declarations
- ParticleSpinAction.lean 8 declarations
- Polynomial.lean 2 declarations
- Polynomial2.lean 7 declarations
- PolynomialDegree.lean 4 declarations
- RectangularAverage.lean 7 declarations
- RelativeHighest.lean 8 declarations
- Representation.lean 8 declarations
- Sandwich.lean 2 declarations
- ScaleLimit.lean 3 declarations
- Schur.lean 7 declarations
- Sl2DescendantNorm.lean 6 declarations
- Sl2Matrix.lean 5 declarations
- Sl2Orthogonal.lean 1 declarations
- Specializations.lean 6 declarations
- Support.lean 2 declarations
- TensorAction.lean 8 declarations
- Torus.lean 3 declarations
- TotalSl2Matrix.lean 5 declarations
- TripleLadderIntertwining.lean 16 declarations
- TwoBodyCertificateHaar.lean 4 declarations
- WeightSlice.lean 9 declarations