OAI/Analysis/Laughlin/Pair/
168 declarations, 0 contain sorry, 0 declared as axioms; 35 files
Files
- AffineChart.lean 8 declarations
- AffineKernel.lean 3 declarations
- AffinePolynomial.lean 5 declarations
- Binomial.lean 9 declarations
- CoefficientSquare.lean 1 declarations
- Conjugation.lean 5 declarations
- CoupledBasis.lean 11 declarations
- CoupledIsometry.lean 4 declarations
- CoupledOne.lean 4 declarations
- CoupledParity.lean 9 declarations
- DiagonalCube.lean 6 declarations
- EnergyReturn.lean 4 declarations
- ExteriorRotation.lean 7 declarations
- FactorBounds.lean 3 declarations
- FactorLimit.lean 4 declarations
- FockCovariance.lean 3 declarations
- FockHaar.lean 5 declarations
- HomogeneousCube.lean 8 declarations
- Homogenize.lean 5 declarations
- LadderIntertwining.lean 5 declarations
- LoweringAlgebra.lean 3 declarations
- Moment.lean 5 declarations
- MomentKernel.lean 3 declarations
- NormalOrder.lean 3 declarations
- Normalization.lean 2 declarations
- NormalizedLadder.lean 7 declarations
- Orthonormality.lean 3 declarations
- PolynomialBridge.lean 2 declarations
- PolynomialLadder.lean 3 declarations
- PolynomialRaising.lean 5 declarations
- Spectators.lean 3 declarations
- SpinorCube.lean 4 declarations
- TensorBoundary.lean 6 declarations
- TensorLower.lean 4 declarations
- TensorRaise.lean 6 declarations