`OAI/Analysis/LaughlinFock/`

5346 declarations, 0 contain sorry, 0 declared as axioms; 293 files

Files

AllowanceOrbit.lean 6 declarations
Assembly.lean 2 declarations
AveragedOperators.lean 10 declarations
Averaging.lean 18 declarations
BesselComparison.lean 15 declarations
Certificate01.lean 8 declarations
Certificate02.lean 8 declarations
Certificate03.lean 8 declarations
Certificate04.lean 8 declarations
Certificate05.lean 9 declarations
Certificate05Data.lean 11 declarations
Certificate06.lean 8 declarations
Certificate07.lean 9 declarations
Certificate07Data.lean 15 declarations
Certificate08.lean 13 declarations
Certificate08Data.lean 15 declarations
Certificate09.lean 15 declarations
Certificate09Data.lean 20 declarations
Certificate10.lean 15 declarations
Certificate10Data.lean 20 declarations
Certificate11.lean 17 declarations
Certificate11Data.lean 26 declarations
Certificate12.lean 11 declarations
Certificate12Data.lean 26 declarations
Certificate13.lean 19 declarations
Certificate13Data.lean 33 declarations
Certificate14.lean 20 declarations
Certificate14Data.lean 33 declarations
Certificate15.lean 22 declarations
Certificate15Data.lean 41 declarations
Certificate16.lean 23 declarations
Certificate16Data.lean 41 declarations
Certificate17.lean 26 declarations
Certificate17Data.lean 50 declarations
Certificate18.lean 27 declarations
Certificate18Data.lean 50 declarations
Certificate19.lean 30 declarations
Certificate19Data.lean 60 declarations
Certificate20.lean 32 declarations
Certificate20Data.lean 60 declarations
Certificate21.lean 35 declarations
Certificate21Data.lean 71 declarations
Certificate22.lean 37 declarations
Certificate22Data.lean 71 declarations
Certificate23.lean 41 declarations
Certificate23Data.lean 83 declarations
CertificateRows.lean 6 declarations
CopyAverage.lean 6 declarations
CopyNormalization.lean 9 declarations
CopyVectors.lean 15 declarations
CoupledLie.lean 15 declarations
CouplingTables.lean 51 declarations
Covariance.lean 23 declarations
CreationRows.lean 15 declarations
CrossOrbit.lean 10 declarations
EntryEnumeration.lean 24 declarations
ExchangeSpectrum.lean 14 declarations
FastCoupling.lean 4 declarations
FastTrace.lean 7 declarations
FastWedge.lean 13 declarations
FasterTrace.lean 8 declarations
FermionOperators.lean 25 declarations
FiniteComparison.lean 12 declarations
FiniteCoupling.lean 26 declarations
Flow.lean 6 declarations
FockRotations.lean 17 declarations
FourBasis.lean 9 declarations
FourBound.lean 3 declarations
FourCoefficients.lean 12 declarations
FourCopies.lean 9 declarations
FourHighest.lean 9 declarations
FourLie.lean 8 declarations
FourRetained.lean 5 declarations
FourTrace.lean 5 declarations
FourTraces.lean 17 declarations
GramCache.lean 8 declarations
GramCompression.lean 3 declarations
HighestTails.lean 10 declarations
IntegerCompression.lean 1 declarations
IntegerCoupling.lean 2 declarations
IntegerFour.lean 12 declarations
LDL.lean 4 declarations
LadderCalculus.lean 44 declarations
LocalEnergy.lean 33 declarations
Main.lean 2 declarations
Model.lean 35 declarations
NormalOrdering.lean 94 declarations
NullComponents.lean 7 declarations
NumericTrace.lean 27 declarations
OscillatorLimit.lean 18 declarations
PairDecomposition.lean 15 declarations
PairIdentification.lean 13 declarations
PairLie.lean 7 declarations
PairNormalization.lean 16 declarations
PairOrbit.lean 6 declarations
PartsTrace.lean 4 declarations
PolynomialPositivity.lean 6 declarations
PositiveIntegrals.lean 8 declarations
RationalCoupling.lean 6 declarations
RationalFour.lean 12 declarations
RationalThree.lean 9 declarations
RationalWedge.lean 15 declarations
RectangularOrbit.lean 5 declarations
RelativePerturbation.lean 46 declarations
RelativeTransfer.lean 26 declarations
Rotations.lean 16 declarations
RowTraces.lean 25 declarations
ScalarAction.lean 9 declarations
Sparse0801.lean 17 declarations
Sparse0802.lean 16 declarations
Sparse0803.lean 16 declarations
Sparse0804.lean 14 declarations
Sparse0805.lean 14 declarations
Sparse0806.lean 13 declarations
Sparse0807.lean 14 declarations
Sparse0808.lean 14 declarations
Sparse0809.lean 12 declarations
Sparse0810.lean 12 declarations
Sparse0811.lean 12 declarations
Sparse0812.lean 13 declarations
Sparse0813.lean 13 declarations
Sparse0814.lean 12 declarations
Sparse0815.lean 11 declarations
Sparse0816.lean 13 declarations
Sparse0817.lean 13 declarations
Sparse0818.lean 13 declarations
Sparse0819.lean 11 declarations
Sparse0820.lean 11 declarations
Sparse0821.lean 13 declarations
Sparse0822.lean 12 declarations
Sparse0823.lean 12 declarations
Sparse0824.lean 12 declarations
Sparse0825.lean 11 declarations
Sparse0826.lean 14 declarations
Sparse0827.lean 13 declarations
Sparse0828.lean 13 declarations
Sparse0829.lean 12 declarations
Sparse0830.lean 15 declarations
Sparse0831.lean 14 declarations
Sparse0832.lean 14 declarations
Sparse0833.lean 7 declarations
Sparse0901.lean 21 declarations
Sparse0902.lean 16 declarations
Sparse0903.lean 17 declarations
Sparse0904.lean 17 declarations
Sparse0905.lean 14 declarations
Sparse0906.lean 13 declarations
Sparse0907.lean 17 declarations
Sparse0908.lean 14 declarations
Sparse0909.lean 13 declarations
Sparse0910.lean 13 declarations
Sparse0911.lean 16 declarations
Sparse0912.lean 13 declarations
Sparse0913.lean 13 declarations
Sparse0914.lean 11 declarations
Sparse0915.lean 15 declarations
Sparse0916.lean 14 declarations
Sparse0917.lean 13 declarations
Sparse0918.lean 11 declarations
Sparse0919.lean 13 declarations
Sparse0920.lean 15 declarations
Sparse0921.lean 13 declarations
Sparse0922.lean 12 declarations
Sparse0923.lean 12 declarations
Sparse0924.lean 15 declarations
Sparse0925.lean 14 declarations
Sparse0926.lean 13 declarations
Sparse0927.lean 15 declarations
Sparse0928.lean 15 declarations
Sparse0929.lean 14 declarations
Sparse0930.lean 14 declarations
Sparse1001.lean 23 declarations
Sparse1002.lean 17 declarations
Sparse1003.lean 21 declarations
Sparse1004.lean 17 declarations
Sparse1005.lean 15 declarations
Sparse1006.lean 19 declarations
Sparse1007.lean 17 declarations
Sparse1008.lean 14 declarations
Sparse1009.lean 15 declarations
Sparse1010.lean 17 declarations
Sparse1011.lean 15 declarations
Sparse1012.lean 13 declarations
Sparse1013.lean 14 declarations
Sparse1014.lean 17 declarations
Sparse1015.lean 13 declarations
Sparse1016.lean 13 declarations
Sparse1017.lean 14 declarations
Sparse1018.lean 17 declarations
Sparse1019.lean 15 declarations
Sparse1020.lean 13 declarations
Sparse1021.lean 16 declarations
Sparse1022.lean 15 declarations
Sparse1023.lean 15 declarations
Sparse1024.lean 14 declarations
Sparse1025.lean 18 declarations
Sparse1026.lean 15 declarations
Sparse1027.lean 14 declarations
Sparse1101.lean 28 declarations
Sparse1102.lean 18 declarations
Sparse1103.lean 25 declarations
Sparse1104.lean 18 declarations
Sparse1105.lean 21 declarations
Sparse1106.lean 19 declarations
Sparse1107.lean 16 declarations
Sparse1108.lean 19 declarations
Sparse1109.lean 19 declarations
Sparse1110.lean 15 declarations
Sparse1111.lean 14 declarations
Sparse1112.lean 22 declarations
Sparse1113.lean 16 declarations
Sparse1114.lean 13 declarations
Sparse1115.lean 18 declarations
Sparse1116.lean 17 declarations
Sparse1117.lean 15 declarations
Sparse1118.lean 13 declarations
Sparse1119.lean 21 declarations
Sparse1120.lean 16 declarations
Sparse1121.lean 13 declarations
Sparse1122.lean 21 declarations
Sparse1123.lean 16 declarations
Sparse1124.lean 13 declarations
Sparse1301.lean 40 declarations
Sparse1302.lean 36 declarations
Sparse1303.lean 23 declarations
Sparse1304.lean 34 declarations
Sparse1305.lean 19 declarations
Sparse1306.lean 32 declarations
Sparse1307.lean 21 declarations
Sparse1308.lean 30 declarations
Sparse1309.lean 20 declarations
Sparse1310.lean 23 declarations
Sparse1311.lean 28 declarations
Sparse1312.lean 17 declarations
Sparse1313.lean 28 declarations
Sparse1314.lean 22 declarations
Sparse1315.lean 28 declarations
Sparse1316.lean 21 declarations
Sparse1317.lean 4 declarations
Sparse1401.lean 52 declarations
Sparse1402.lean 41 declarations
Sparse1403.lean 42 declarations
Sparse1404.lean 32 declarations
Sparse1405.lean 32 declarations
Sparse1406.lean 35 declarations
Sparse1407.lean 27 declarations
Sparse1408.lean 34 declarations
Sparse1409.lean 25 declarations
Sparse1410.lean 34 declarations
Sparse1411.lean 22 declarations
Sparse1412.lean 37 declarations
Sparse1413.lean 13 declarations
Sparse1501.lean 23 declarations
Sparse1502.lean 23 declarations
Sparse1503.lean 23 declarations
Sparse1504.lean 23 declarations
Sparse1505.lean 23 declarations
Sparse1506.lean 23 declarations
Sparse1507.lean 23 declarations
Sparse1508.lean 7 declarations
Sparse1601.lean 23 declarations
Sparse1602.lean 23 declarations
Sparse1603.lean 23 declarations
Sparse1604.lean 23 declarations
Sparse1605.lean 12 declarations
Sparse1701.lean 23 declarations
Sparse1702.lean 23 declarations
Sparse1703.lean 12 declarations
Sparse1801.lean 23 declarations
Sparse1802.lean 8 declarations
Sparse19.lean 16 declarations
Sparse20.lean 8 declarations
Sparse21.lean 4 declarations
Sparse22.lean 3 declarations
Sparse23.lean 3 declarations
SparseTrace.lean 11 declarations
SphereScaling.lean 34 declarations
SpinSchur.lean 16 declarations
SpinTails.lean 25 declarations
SquareSplitting.lean 9 declarations
SwapCompression.lean 25 declarations
TableTrace.lean 6 declarations
TailOrbit.lean 5 declarations
TensorBasis.lean 16 declarations
TensorIntegrals.lean 8 declarations
ThreeCertificate.lean 18 declarations
ThreeGram.lean 12 declarations
ThreeOrbit.lean 7 declarations
ThreeRows.lean 10 declarations
ThreeSpectrum.lean 14 declarations
ThreeTraces.lean 19 declarations
TraceSymmetry.lean 3 declarations
WedgeLie.lean 12 declarations