OAI/Analysis/Laughlin/Operators/
139 declarations, 0 contain sorry, 0 declared as axioms; 38 files
Files
- CAR.lean 10 declarations
- Certificate.lean 9 declarations
- CollectionAnnihilatorBound.lean 4 declarations
- ComplexCompression.lean 1 declarations
- CopyQuadraticMatrix.lean 2 declarations
- Energy.lean 1 declarations
- FourOccupationEquiv.lean 3 declarations
- GenericPhysicalResolution.lean 1 declarations
- GlobalPairCube.lean 4 declarations
- GramReadout.lean 3 declarations
- LocalFourCardinality.lean 3 declarations
- LocalFourIndexEquiv.lean 3 declarations
- MatrixCongruence.lean 2 declarations
- MatrixMetricError.lean 8 declarations
- MatrixPhysicalCompression.lean 1 declarations
- NormalCertificate.lean 4 declarations
- NormalOrder.lean 4 declarations
- NormalOrderFour.lean 2 declarations
- OrthonormalRows.lean 1 declarations
- PairNormalOrder.lean 2 declarations
- PhysicalCoupling.lean 3 declarations
- PhysicalFockGap.lean 3 declarations
- PhysicalPairCounting.lean 5 declarations
- PhysicalPairKernel.lean 5 declarations
- PhysicalPairRotation.lean 4 declarations
- PositiveFockLift.lean 9 declarations
- RationalPSD.lean 1 declarations
- RealComplexMatrixPositive.lean 2 declarations
- RowNormalSquare.lean 2 declarations
- SevenSquareAverage.lean 5 declarations
- SpectralKernelDistance.lean 1 declarations
- SymmetricPairSum.lean 3 declarations
- TruncatedConjugation.lean 2 declarations
- TruncatedFourCopy.lean 3 declarations
- TruncatedPairReturn.lean 3 declarations
- WedgePairRepresentation.lean 15 declarations
- WedgePairRotation.lean 4 declarations
- WeightedOccupationNorm.lean 1 declarations