OAI/Analysis/Laughlin/Fock/
130 declarations, 0 contain sorry, 0 declared as axioms; 26 files
Files
- Adjoint.lean 3 declarations
- Annihilation.lean 8 declarations
- Bidegree.lean 5 declarations
- ContractionBound.lean 6 declarations
- Coordinates.lean 2 declarations
- Creation.lean 4 declarations
- EigenvalueGap.lean 5 declarations
- EnergyRotation.lean 4 declarations
- FourLabels.lean 4 declarations
- HaarQuadratic.lean 3 declarations
- Hamiltonian.lean 8 declarations
- Inner.lean 6 declarations
- LaughlinGap.lean 3 declarations
- MatrixQuadratic.lean 2 declarations
- ModeEmbedding.lean 12 declarations
- NormalSquare.lean 4 declarations
- OrbitIntegration.lean 5 declarations
- PairNormalization.lean 6 declarations
- Perturbation.lean 2 declarations
- Quadruple.lean 4 declarations
- RankOneHaar.lean 5 declarations
- SharpGap.lean 9 declarations
- SpectralDistance.lean 7 declarations
- SpinContinuity.lean 3 declarations
- SpinRepresentation.lean 8 declarations
- UnitaryFamilies.lean 2 declarations